gap
plain-language theorem explainer
Gap supplies the closed-form display function F(Z) = ln(1 + Z/φ)/ln(φ) that the integrated renormalization-group residue is claimed to match at the anchor scale for each fermion species. Mass-hierarchy modelers cite this when placing Standard Model fermions on the phi-ladder via the ZOf charge index. The implementation is a direct one-line transcription of the logarithmic ratio using the phi constant from the Constants bundle.
Claim. $F(Z) = (1/2) ln(1 + Z/φ) / ln(φ) for integer charge index Z, where φ is the golden ratio constant from the Constants bundle and Z is obtained from the ZOf map on fermions.
background
The RSBridge.Anchor module bridges recognition forcing to particle physics by defining the 12 Standard Model fermions, the ZOf charge index, and the gap display function. ZOf assigns to each fermion an integer Z = q̃² + q̃⁴ (plus 4 for quarks) from its tildeQ charge. Gap then gives the explicit closed form claimed to equal the integrated RG residue f_i(μ⋆) at the anchor scale, per the module statement: (1/ln φ) ∫ γ_i(μ) d(ln μ) ≈ gap(ZOf i) with tolerance ~1e-6.
proof idea
This is a one-line definition that directly transcribes the logarithmic ratio using Real.log applied to (1 + Z/φ) divided by Real.log of the phi constant imported from Constants. No lemmas or tactics are applied beyond the primitive real-arithmetic operations.
why it matters
Gap completes the anchor identification required by Single Anchor Phenomenology in the RSBridge module and supplies the explicit residue for the phi-ladder mass formula. It is invoked downstream in visualBeautyCert, Jphi_numerical_band, and potterySerialCert for band and positivity checks. It operationalizes the T5 J-uniqueness and T6 phi fixed point by furnishing the concrete rung offset in the mass expression yardstick * φ^(rung - 8 + gap(Z)).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.