quarkAnchorDerivationCert_holds
plain-language theorem explainer
The theorem certifies the rung and Z assignments for charm, bottom, and top quarks required by the RSBridge mass formula. Researchers deriving quark masses from the phi-ladder would cite it to fix the heavy anchors in RS-native units without PDG input. The proof is a direct term construction that assembles the certificate record from six equality lemmas and one positivity result.
Claim. The structure holds with rung(Fermion.c) = 15, ZOf(Fermion.c) = 276, rung(Fermion.b) = 21, ZOf(Fermion.b) = 24, rung(Fermion.t) = 21, ZOf(Fermion.t) = 276, and positive values for charm_anchor_native, bottom_anchor_native, and top_anchor_native.
background
The module derives heavy-quark anchor masses from the RSBridge formula massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap(ZOf f)) * log φ), staying dimensionless and free of external mass data. QuarkAnchorDerivationCert bundles the required rung and ZOf values for the three heavy fermions together with anchor positivity. Upstream rung definitions from CKMHierarchyFromPhiLadder supply initial values (charm_rung = 17, bottom_rung = 22, top_rung = 30) that are specialized here via local equalities.
proof idea
The proof is a term-mode record construction. It populates the seven fields of QuarkAnchorDerivationCert by substituting the equality theorems charm_rung_eq, bottom_rung_eq, top_rung_eq, charm_Z_eq, bottom_Z_eq, top_Z_eq and the positivity lemma heavy_anchor_positive.
why it matters
The result supplies the certified inputs for heavy-quark mass anchors inside the QuarkAnchorDerivation module, enabling direct phi-ladder computations. It supports the Recognition mass formula and is consistent with the phi fixed point and eight-tick octave. No downstream uses appear yet, so its integration into full CKM or spectrum derivations remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.