bottom_mass_pred_bounds
plain-language theorem explainer
Bounds are established for the bottom quark mass prediction under the quarter-ladder hypothesis, specifically that the value computed from the structural mass scaled by the golden ratio to the power minus two lies strictly between 4140 and 4155 in MeV units. Researchers verifying quark mass derivations in the Recognition Science framework would reference this result to confirm the geometric match before comparing to experimental values. The proof substitutes the rung definition for the bottom quark and chains interval inequalities from the pre-
Claim. $4140 < m_0 · φ^{-2} < 4155$, where $m_0$ is the structural mass shared by leptons and quarks on the φ-ladder and φ denotes the golden ratio.
background
The module develops T12 on quark masses via the Quarter-Ladder Hypothesis: quarks occupy quarter-integer rungs on the φ-ladder while sharing the lepton structural base mass. The structural mass is the yardstick scaled by φ to the power (rung minus eight). The predicted mass for residue res is then this structural mass multiplied by φ to the power res. For the bottom quark the residue equals -2 exactly. Upstream lemmas supply the interval (10856, 10858) for the structural mass together with the explicit bounds 0.3818 < φ^{-2} < 0.382.
proof idea
The tactic proof first simplifies the predicted-mass expression and records that the bottom residue equals -2. It pulls in the structural-mass interval theorem and the two φ^{-2} bound theorems, rewrites the real power to an integer exponent, and establishes positivity of both factors. A constructor splits the conjunction; each half is discharged by a calc chain that feeds the interval hypotheses into nlinarith.
why it matters
The lemma supplies the concrete interval required by the downstream theorem that the bottom quark matches the observed mass to within one percent. It fills a step in the T12 quarter-ladder derivation inside the Recognition framework, where the φ-ladder and structural mass furnish the geometric origin of the mass spectrum. The result supports verification of the eight-tick octave scaling before non-perturbative QCD corrections are considered for lighter flavors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.