ResidueCert
plain-language theorem explainer
ResidueCert is a record structure pairing one of the twelve Standard Model fermions with rational bounds lo and hi together with an ordering proof, plus a validity predicate that checks containment of the gap function at the fermion's Z-index. Downstream code assembling complete fermion certificate lists for mass-ladder comparisons cites it directly. The definition is a straightforward record whose validity clause performs a direct real-interval check after coercion.
Claim. A residue certificate for fermion $f$ consists of rationals $l,h$ with $l≤h$ such that $l ≤ gap(Z(f)) ≤ h$ after embedding into the reals, where $Z(f)$ is the charge-indexed integer $Z_i=˜q^2+˜q^4$ (+4 for quarks) and $gap(Z)=ln(1+Z/φ)/lnφ$.
background
The module defines the bridge from the recognition framework to particle physics. Fermion is the inductive type enumerating the twelve Standard Model species (six quarks, three charged leptons, three neutrinos). ZOf maps each fermion to its charge-indexed integer. The gap function, drawn from AnchorPolicy, is the closed-form display $F(Z)=ln(1+Z/φ)/lnφ$ conjectured to equal the integrated RG residue at the anchor scale. Upstream results include the rung definition in Compat.Constants, the Generation type as Fin 3 from SpectralEmergence, and the gap derivation in Gap45 that fixes the numerical value 45. The module doc states the Single Anchor Phenomenology claim: the integrated RG residue approximates gap(ZOf i) with tolerance ~1e-6.
proof idea
The declaration is a structure definition whose four fields directly record the fermion, the rational bounds, and their ordering proof. The accompanying valid predicate is a one-line conjunction that coerces lo and hi to reals and asserts interval containment of gap(ZOf f).
why it matters
ResidueCert supplies the data type used to populate allCerts in ResidueData and the individual cert_b, cert_c, cert_d, cert_e instances that feed certificateWithinTolerance. It realizes the anchor-scale identification step in the RSBridge, linking the phi-ladder mass formula to observed fermion masses via the gap function. The construction supports the T7 eight-tick octave and T8 D=3 landmarks by providing concrete Z-values for the twelve fermions that populate the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.