gap_lepton_theory
plain-language theorem explainer
The declaration supplies the theoretical gap value for leptons by evaluating the closed-form residue function at the electron Z-value of 1332. Mass-spectrum researchers in Recognition Science cite it when checking that lepton residues cluster at the anchor scale. It is realized as a direct one-line application of the gap expression to the lepton ZOf definition.
Claim. The theoretical lepton gap is defined by $F(1332)$ where $F(Z) := (1/2) (Z/φ) / ln(φ)$ no, precisely $F(Z) = ln(1 + Z/φ) / ln(φ)$ with $φ$ the golden ratio and $Z = 1332$ for the electron.
background
The ResidueData module supplies audit certificates that bound the integrated RG residues of fermions at the anchor scale μ⋆, each required to equal gap(ZOf i) under the display_identity_at_anchor axiom of AnchorPolicy. The gap function is the closed-form expression gap(Z) = ln(1 + Z/φ)/ln(φ), introduced in RSBridge.Anchor as the target residue for any fermion species. ZOf maps a fermion to its integer rung via charge: for leptons it reduces to q² + q⁴, yielding 1332 for the electron. Upstream results include the gap definition in Masses.RSBridge.Anchor and the alias F in Physics.AnchorPolicy, both confirming the same logarithmic form.
proof idea
One-line wrapper that applies the gap function from RSBridge.Anchor directly to the ZOf value of the electron fermion.
why it matters
This definition provides the lepton target F(1332) ≈ 13.954 inside the residue-certificate audit, enabling direct comparison against transported experimental masses. It supports verification of the display_identity_at_anchor axiom and instantiates the integer-rung model for the lepton sector. The module observations note that lepton residues cluster tightly around this value, while charm anomalously matches it rather than the up-quark target F(276). It therefore quantifies the Quarter-Ladder versus Integer-Rung tension within the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.