certificateWithinTolerance
plain-language theorem explainer
The predicate checks whether a residue certificate's rational bounds encompass the theoretical gap value for its fermion after offset by anchorTolerance. Auditors validating RS mass residues against the anchor scale would cite it to confirm consistency of transported experimental data with the closed-form gap. The definition extracts ZOf from the certificate, applies the gap function, and performs the direct interval comparison.
Claim. For a residue certificate $c$ with fermion $f$, lower bound $l$ and upper bound $h$, the predicate holds if and only if $l - t ≤ F(Z(f)) ≤ h + t$, where $t$ is the anchor tolerance and $F(Z) = ln(1 + Z/φ)/ln φ$.
background
ResidueData supplies the audit payload of numerical bounds for fermion residues at the anchor scale, obtained from experimental masses via RG transport in tools/audit_masses.py. ResidueCert is the structure holding a Fermion $f$, rational bounds $lo$ and $hi$ with $lo ≤ hi$. The gap function, given by $F(Z) = ln(1 + Z/φ)/ln φ$, is the closed-form expression for the theoretical residue at μ⋆, as documented in the RSBridge.Anchor gap definition: 'The residue at the anchor for a fermion species.'
proof idea
The definition is realized by a let-binding that computes theoretical as gap(ZOf c.f), followed by the conjunction of the two inequalities that place this value inside the certificate interval offset by anchorTolerance. No lemmas are applied; it is a direct unfolding of the ResidueCert fields and the imported gap function.
why it matters
It supplies the tolerance predicate used to audit residue certificates against the gap formula that implements the mass ladder at the anchor. The module doc-comment positions it as the verifier for the display_identity_at_anchor axiom, noting lepton clustering around F(1332) ≈ 13.95 and quark discrepancies that quantify the integer-rung versus quarter-ladder tension. It therefore supports the phi-ladder and gap computations that descend from the forcing chain T5–T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.