Z_down
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 in Recognition Science
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.
scope and limits
- Does not derive the numerical value 24 from the RG integral or anomalous dimensions.
- Does not prove radiative stability or flavor mixing.
- Does not compute physical masses or coupling constants.
- Does not address the full RG transport kernel; that remains external.
formal statement (Lean)
108theorem Z_down : ZOf Fermion.d = 24 := by native_decide
proof body
Term-mode proof.
109
110/-! ## Abstract RG Residue -/
111
112/-- **ANCHOR RESIDUE THEOREM**
113
114 Abstract RG residue for species at scale μ matches val.
115
116 **Proof Structure**:
117 1. The mass of a fermion species $i$ evolves as $m_i(\mu) = m_i(\mu_0) \exp(-\int_{\ln \mu_0}^{\ln \mu} \gamma_i(t) dt)$.
118 2. The integrated residue $f_i$ is defined using `RGTransport.integratedResidue`.
119 3. External RG transport calculations (QCD 4L/QED 2L) provide the specific values for each species.
120 4. This theorem maps these computed residues to the canonical SI units.
121
122 **STATUS**: HYPOTHESIS (empirical calibration) -/