Fgap
plain-language theorem explainer
Fgap supplies the closed-form gap function on integer Z values for the certified anchor interface. Physicists replacing axiomatic RG-residue equalities with external certificate bounds would cite this when deriving per-species inequalities. The declaration is a one-line abbreviation forwarding to the underlying gap computation from the masses anchor modules.
Claim. $F(z) := g(z)$ for integer $z$, where $g$ denotes the closed-form residue display obtained from the charge-to-Z map and the golden-ratio logarithm.
background
This module remedies the axiomatic treatment of Standard-Model RG residues in AnchorPolicy.lean. Instead of asserting a global axiom of the form $|f_ residue(f, μ^⋆) - gap(ZOf f)| < 1e-6$, it encodes the dependency via an external certificate consisting of residue intervals $Ires$ and gap intervals $Igap$ together with a validity proof. Fgap is the integer-argument version of the gap function that supplies the closed-form display against which certified residues are compared. Upstream results include the gap definition in Masses.AnchorPolicy (the logarithmic expression involving ChargeIndex.Z and phi) and the integer Z map in Masses.Anchor that converts sector and charge to the integer rung used by the phi-ladder.
proof idea
One-line abbreviation that re-exports the gap function from the masses anchor modules for use as a parameter in certified statements.
why it matters
Fgap supplies the reference closed-form used by the parent theorems anchor_identity_from_cert and equalZ_residue_from_cert, which derive residue bounds directly from a Valid certificate. It also appears in the ablation predicates AnchorEq and ablation_contradictions to enforce that any transformed Z map must reproduce the original residues. In the Recognition framework this definition closes the interface between the integer Z map (Masses.Anchor) and the phi-based gap computation, allowing the mass-ladder and eight-tick octave structure to be checked against external data without an equality axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.