gap
plain-language theorem explainer
The gap function supplies the closed-form display F(Z) = ln(1 + Z/φ) / ln(φ) that equates the integrated mass anomalous dimension to a logarithmic ratio at the anchor scale μ⋆. Modelers of fermion mass hierarchies in the Recognition Science framework cite this when mapping charge indices Z to residue values. The definition is a direct one-line expression in terms of the framework's golden ratio constant.
Claim. $F(Z) = (1 / ln φ) ln(1 + Z/φ)$ for integer charge index $Z$, where $φ$ is the golden ratio fixed point.
background
The RSBridge Anchor module defines the bridge from the recognition framework to particle physics via the 12 Standard Model fermions, the ZOf map that computes an integer Z_i = q̃² + q̃⁴ (+4 for quarks) from the tilde charge in each sector, and the gap function as the display F(Z). The module states that F(Z) is the closed form claimed to equal the integrated RG residue f_i(μ⋆) at the anchor scale, with Single Anchor Phenomenology asserting that (1/ln φ) ∫ γ_i(μ) d(ln μ) ≈ gap(ZOf i) to tolerance ~1e-6. Upstream results supply the Constants structure holding the golden ratio φ and related framework values.
proof idea
The definition is a direct algebraic expression that implements the logarithmic ratio using Real.log applied to the scaled charge index divided by the logarithm of the golden ratio constant.
why it matters
This definition supplies the target closed form for the display_identity_at_anchor claim in AnchorPolicy and the Single Anchor Phenomenology statement in the module doc. It supports downstream massAtAnchor and residue calculations that feed into aesthetics modules via related J-cost bands and into archaeology via adjacencyGap constructions. It connects directly to the phi-ladder mass formula and the T5 J-uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.