ResidueCert
ResidueCert packages each of the twelve Standard Model fermions with a rational interval asserted to contain the value of its gap function at the charge index. Researchers tabulating mass hierarchies from the recognition framework cite these certificates when checking computed gaps against the single-anchor phenomenology. The definition is a direct record construction whose validity predicate performs the real-number containment test.
claimA residue certificate for fermion $f$ consists of rationals $l,h$ with $l≤h$ such that $l ≤ gap(Z(f)) ≤ h$, where $Z(f)$ is the charge-indexed integer of $f$ and $gap(z) = ln(1 + z/φ)/ln φ$.
background
The RSBridge.Anchor module defines the twelve fermions as an inductive type with constructors d, s, b, u, c, t, e, mu, tau, nu1, nu2, nu3. The gap function, drawn from AnchorPolicy, evaluates to ln(1 + Z/φ)/ln φ for the charge index Z produced by ZOf; this expression is the closed form claimed to equal the integrated RG residue at the anchor scale. Upstream results include the rung and Generation abbrevs that organize fermions into families, together with the gap derivation that fixes the numerical target 45 in related contexts.
proof idea
The valid predicate is a direct one-line definition that casts the rational bounds to reals and asserts the conjunction of the two inequalities around gap(ZOf c.f). No lemmas or tactics are invoked.
why it matters in Recognition Science
ResidueCert supplies the data consumed by allCerts, cert_b, cert_c, cert_d and certificateWithinTolerance in ResidueData, enabling systematic verification that each fermion gap lies inside its prescribed tolerance. It operationalizes the module claim that the integrated RG residue approximates gap(ZOf i) within ~1e-6, thereby anchoring the phi-ladder mass formula and the eight-tick octave structure for the twelve fermions.
scope and limits
- Does not derive the gap function or the ZOf map.
- Does not prove that the supplied bounds are tightest possible.
- Does not address physical interpretation of the tolerance.
- Does not extend to bosons or other particles.
formal statement (Lean)
134structure ResidueCert where
135 f : Fermion
136 lo : ℚ
137 hi : ℚ
138 lo_le_hi : lo ≤ hi
139
140def ResidueCert.valid (c : ResidueCert) : Prop :=
proof body
Definition body.
141 (c.lo : ℝ) ≤ gap (ZOf c.f) ∧ gap (ZOf c.f) ≤ (c.hi : ℝ)
142
143/-! ### Generation indexing (three disjoint families) -/
144
145/-- Generation index (0,1,2) assigned by rung/sector ordering. -/