top_quark_pred_order
plain-language theorem explainer
The theorem shows that the top-quark structural mass prediction phi^51 divided by two million lies between 10000 and 1000000. Mass-scale verifiers in the Recognition framework cite it to confirm the top quark sits in the multi-GeV to TeV window before gap corrections are applied. The proof unfolds the definition, substitutes the golden-ratio identification, imports the precomputed phi^51 bounds, and closes both sides with linear arithmetic after rewriting the division inequalities.
Claim. Let $phi$ denote the golden ratio. The structural top-quark mass prediction satisfies $10000 < phi^{51}/2000000 < 1000000$.
background
In the Masses.Verification module experimental PDG values remain imported constants while structural predictions are generated from the phi-ladder. The top_quark_pred definition is phi^51 divided by 2000000, where phi is identified with the golden ratio by the phi_eq_goldenRatio lemma imported from ElectroweakMasses and from the local module. This expression implements the bare rung-21 term of the Recognition mass formula (yardstick times phi to a suitable power) without the gap(Z) adjustment. The module also imports the interval bounds phi_pow51_gt and phi_pow51_lt from Numerics.Interval.PhiBounds to control the size of high powers.
proof idea
Unfold top_quark_pred to expose the explicit quotient. Apply phi_eq_goldenRatio to replace Constants.phi by goldenRatio, then invoke phi_pow51_gt and phi_pow51_lt to obtain the concrete numerical brackets on phi^51. Split the conjunction with constructor. Rewrite each inequality using lt_div_iff0 and div_lt_iff0 (with the positive denominator 2000000), then close both goals by linarith.
why it matters
The result is consumed directly by row_top_quark_in_band in QuarkScoreCard and by row_top_order_MeV in TopQuarkMassScoreCard, supplying the order-of-magnitude anchor for the top quark on the phi-ladder. It fills the structural prediction slot for the UpQuark sector at rung 21, confirming that the bare phi^51 term already lands inside the observed band even before the full gap correction. Within the Recognition framework this supports the mass formula derived from the forcing chain (T5 J-uniqueness through T8 D=3) and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.