canonical_mass_law_formula
plain-language theorem explainer
The master mass predictor coincides definitionally with the canonical φ-ladder: sector yardstick times φ raised to (rung − 8 + gap(Z)). Anyone wiring T6 (φ forced) into the mass ladder cites this identification. The proof is pure reflexivity after introducing sector, rung, and Z.
Claim. The existing master mass assignment obeys the canonical ladder formula relative to its gap correction: for every sector, rung $r\in\mathbb{Z}$, and integer $Z$, the predicted mass equals the sector yardstick times $\varphi^{(r-8)+g(Z)}$, where $g$ is the gap-correction map.
background
In the Unified Forcing Chain, T0–T8 are forced from the Recognition Composition Law plus normalization and calibration. T6 forces φ as the self-similar fixed point of the discrete ledger; the mass sector then lives on a φ-ladder.
MassLadderFormula is the Prop that a mass map mass : Sector → ℤ → ℤ → ℝ equals, for every sector, rung, and Z,
yardstick(sector) · φ^(rung − 8 + gap(Z)).
The offset −8 is the RS rung convention; gap absorbs the Z-dependent correction used by the master mass law.
This declaration simply records that the already-defined master predictor and its gap correction inhabit that Prop, so later bridge theorems can quote a single canonical shape rather than the concrete names.
proof idea
Term/tactic proof with two steps: introduce the three universal arguments (sector, rung, Z), then rfl. The equality is definitional: unfolding MassLadderFormula and the master mass/gap definitions yields identical terms, so no algebraic lemma is required.
why it matters
Closes the identification step on the T6 → mass-ladder bridge. Downstream, t6_to_canonical_mass_ladder_bridge_holds packages three facts under the hypothesis that T6 holds: uniqueness of φ, this canonical formula, and rung scaling by φ. Its doc-comment states "T6 supplies the canonical Mass Ladder bridge"; the canonical_formula field is exactly this theorem.
In the primer mass law, masses sit on yardstick · φ^(rung − 8 + gap(Z)). Pinning the master predictor to that shape lets the forcing chain treat particle masses as forced φ-ladder data once φ is forced (T6), rather than an independent phenomenological fit. No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.