QuarkAnchorDerivationCert
plain-language theorem explainer
QuarkAnchorDerivationCert packages the rung levels and ZOf values for charm, bottom, and top quarks with positivity of their native anchor masses from the RSBridge formula. Researchers deriving RS-native quark scales on the phi-ladder would cite it to confirm consistency without PDG inputs. The definition is a direct record bundling six equalities and three inequalities from sibling lemmas.
Claim. The certificate asserts rung(c) = 15, rung(b) = 21, rung(t) = 21, ZOf(c) = 276, ZOf(b) = 24, ZOf(t) = 276 together with 0 < charm_anchor_native, 0 < bottom_anchor_native, 0 < top_anchor_native, where rung is the phi-ladder level, ZOf supplies the gap integer, and the anchor terms are the native masses at the anchor scale.
background
The module derives heavy-quark anchor-scale masses from the RSBridge formula massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap (ZOf f)) * log φ). Rung assigns each fermion to a discrete level on the phi-ladder; upstream definitions in CKMHierarchyFromPhiLadder supply base values for charm, bottom, and top. ZOf provides the integer gap that adjusts the exponent. The structure collects these assignments for the three heavy quarks to certify the derivation in RS-native dimensionless units.
proof idea
This is a structure definition that directly records the rung equalities, ZOf values, and positivity conditions on the three anchor masses. No lemmas or tactics are invoked; the fields are populated by the equalities and inequalities supplied by the sibling definitions bottom_anchor_native, charm_anchor_native, top_anchor_native and their rung and ZOf companions.
why it matters
The certificate is instantiated by the theorem quarkAnchorDerivationCert_holds, which applies the component equalities to produce the full record. It supports the heavy-quark sector of the mass formula yardstick * φ^(rung - 8 + gap(Z)), consistent with the eight-tick octave and phi self-similarity. The construction keeps the result internal to Recognition Science by excluding external mass data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.