Golf the cubic root-count endpoint

[PerAlexandersson]

Summary

• inline the right-degree equality as hdeg.trans hfdeg3 in the
  degree-at-most-three root-count endpoint
• retain the native Nat.le_or_eq_of_le_succ case split from PR Split root-count tactic into theorem and frontend layers #515
• update the exact architecture line/closure metric

This is the isolated post-merge adoption of the useful equality-transitivity
idea from owner-labeled Aristotle project
a081360c-f706-4531-b949-b6b47fb79f66, task
84b3da16-38b1-4220-b56c-3b897e957855. The generated proof itself used a
different outer case split; only the independently replayed improvement was
distilled here.

Verification

• isolated combined-snippet elaboration
• focused LowDegree, LowDegreeRules, and Examples.RootCount build
• full lake-workspace build RealRooted: 9,401 jobs passed
• import-architecture self-test and live check
• proof-status self-test and live check
• representative axiom audit: only propext, Classical.choice, and
  Quot.sound
• changed-file width and git diff --check