gap_down_theory
gap_down_theory defines the theoretical residue gap for down quarks as the closed-form expression F(24). A physicist auditing fermion mass residues at the anchor scale would cite it when checking RG-transported experimental data against the predicted value. The definition is a direct one-line application of the gap function to the integer Z value for the down sector.
claimThe theoretical gap for down quarks is the value $F(24) = (Real.log(1 + 24 / phi)) / (Real.log phi) approx 5.74$, where $F(Z)$ is the display function and 24 is the integer rung assigned to the down quark sector.
background
The ResidueData module holds audit certificates that bound experimental fermion residues after RG transport to the anchor scale, verifying the display_identity_at_anchor axiom. The gap function is defined in RSBridge.Anchor as the closed-form residue $F(Z) = ln(1 + Z/phi)/ln phi$, with notation $F(Z)$. This rests on the Z integer map in Masses.Anchor (sector-dependent quadratic in charge) and the gap definition in AnchorPolicy that applies the same expression to charge-derived Z values. Upstream canonical arithmetic objects from ArithmeticOf supply realization-independent integer arithmetic for the rung assignments.
proof idea
One-line definition that applies the gap function from RSBridge.Anchor to the ZOf d value for the down quark sector.
why it matters in Recognition Science
This definition supplies the theoretical target F(24) for the down quark residue certificate inside the audit payload. It instantiates the phi-ladder rung assignment for down quarks and supports verification of the display_identity_at_anchor axiom from AnchorPolicy. In the Recognition framework it connects to the mass formula using phi-ladder rungs and the gap function, though the used_by edges list no direct parent theorems.
scope and limits
- Does not evaluate the expression to a floating-point number.
- Does not compare the value against experimental residue data.
- Does not derive or prove the Z assignment of 24 for down quarks.
- Does not address residue certificates for leptons or up quarks.
formal statement (Lean)
45noncomputable def gap_down_theory : ℝ := gap (ZOf d)
proof body
Definition body.
46
47/-! ## Verification: Z values match canonical bands -/
48