gap_minus_shift_bounds_proven
plain-language theorem explainer
The lemma places the difference between the gap function at charge index 1332 and the refined shift strictly between -20.7063 and -20.705. Researchers deriving forced muon and tau masses from the Recognition Science lepton ladder cite it to anchor the predicted residue step. The proof is a direct one-line wrapper that imports the separate numeric bounds on gap 1332 and refined_shift then applies linear arithmetic to their difference.
Claim. Let $g(Z) := (1 + Z/φ) / ln(φ)$ denote the gap function and let $s$ denote the refined shift. Then $-20.7063 < g(1332) - s < -20.705$.
background
The gap function is the closed-form residue $g(Z) = ln(1 + Z/φ) / ln(φ)$ at the anchor scale for a fermion species with charge index Z. The refined shift is the sum of a base shift and a radiative correction drawn from mass topology. This lemma appears inside the T10 module whose goal is to replace two axioms in the lepton-generations file with proven inequalities for the muon and tau masses.
proof idea
The proof imports gap_1332_bounds (13.953 < g(1332) < 13.954) and refined_shift_bounds (34.6590 < s < 34.6593). It then applies the constructor tactic and feeds the four endpoint inequalities to linarith, which immediately yields the two-sided bound on the difference.
why it matters
The result is the immediate parent of predicted_residue_mu_bounds and predicted_residue_mu_bounds_v2, which in turn supply the numeric anchor for the forced muon mass in the T10 necessity chain. It closes the numeric seam between the gap function (derived from the phi-ladder) and the shift corrections (derived from cube geometry and the eight-tick octave). No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.