bottom_Z_eq
plain-language theorem explainer
ZOf assigns the integer 24 to the bottom quark on the Recognition Science phi-ladder. Heavy-quark mass derivations cite this value when confirming the anchor-scale formula produces RS-native masses without PDG inputs. The proof is immediate reflexivity on the ZOf definition for the down-sector fermion b.
Claim. $Z(b) = 24$, where $b$ is the bottom quark constructor in the Fermion type and $Z$ is the integer returned by the ZOf function from the squared and fourth-power charge terms in the down sector.
background
The Heavy Quark Anchor Derivation module computes masses via massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap (ZOf f)) * log φ) with no external data. Fermion is the inductive enumeration containing the constructor b for the bottom quark. ZOf f first extracts tildeQ f then matches on sector: for down quarks it evaluates to 4 + q² + q⁴.
proof idea
The proof is a one-line reflexivity that unfolds the ZOf definition for Fermion.b and matches the resulting integer against 24.
why it matters
bottom_Z_eq supplies the bottom_Z field inside the QuarkAnchorDerivationCert record used by quarkAnchorDerivationCert_holds. It thereby completes the rung and Z assignments required for the three heavy-quark anchors in the phi-ladder construction. The result sits inside the T5–T8 forcing chain that fixes D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.