Z_down
plain-language theorem explainer
The Z_down theorem fixes the integer Z-value of the down fermion at 24 under the ZOf map. Physicists calibrating the Recognition Science phi-ladder for quark masses cite this when setting the down-quark rung in the mass formula. The proof is a one-line native_decide that evaluates the definition of ZOf directly on Fermion.d.
Claim. $Z(f_d) = 24$, where $f_d$ denotes the down-type fermion and $Z$ is the integer rung assignment on the phi-ladder.
background
The AnchorPolicy module supplies a Lean interface for single-anchor RG phenomenology. ZOf maps each Fermion species to its integer Z on the ladder, while gap(Z) implements the display function F(Z) drawn from RSBridge. Fermion.d is the down quark entry in the Fermion inductive type. The module reuses Constants.phi and RSBridge.anchor_ratio; the integrated residue hypothesis $f_i(μ⋆) = gap(ZOf i)$ is stated explicitly in the module documentation as an empirical calibration imported from external QCD/QED transport.
proof idea
The proof is a term-mode one-liner that applies native_decide to the computable definition of ZOf on Fermion.d, reducing the equality to a decidable numerical check.
why it matters
Z_down anchors the down-quark position in the mass formula yardstick * phi^(rung - 8 + gap(Z)), completing the flavor set alongside sibling declarations Z_up and Z_electron. It supports the anchor residue hypothesis in the module documentation and connects to upstream results on phi-tiers (NucleosynthesisTiers.of) and scale factors (LargeScaleStructureFromRS.scale). In the broader framework it contributes to the phi-ladder mass assignments and the eight-tick octave structure, though no downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.