down_Z_is_24
plain-language theorem explainer
The theorem fixes the down-quark rung index at 24 on the Recognition Science phi-ladder. Modelers of fermion masses via the integer-rung construction cite this to anchor the down-sector residue in the mass formula. The proof is a direct native_decide reduction on the computable ZOf definition for the down identifier.
Claim. $Z(d) = 24$, where $Z$ is the rung index function on the down-quark sector of the phi-ladder.
background
The module supplies audit certificates that bound fermion residues at the anchor scale and verify the display_identity_at_anchor axiom from AnchorPolicy. ZOf maps a sector identifier such as d (down quark) to its integer rung, drawing on the sector-specific mappings in Masses.RSBridge.Anchor (Integers.r_down) and AnchorPolicy.rung. Upstream results include the CPM2D model construction and the Lepton inductive type, which together embed the rung assignments into the broader cost and connection framework.
proof idea
The proof is a one-line term-mode wrapper that applies native_decide to evaluate the definition of ZOf on the down-quark case, reducing it to the literal constant 24.
why it matters
This pins the down-quark rung at 24, feeding the mass formula yardstick * phi^(rung - 8 + gap(Z)) and supporting the integer-rung model for quarks. It aligns with the T5 J-uniqueness and T6 phi fixed-point steps in the forcing chain, while highlighting the quark tension noted in the module's audit data. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.