F
plain-language theorem explainer
F(Z) maps integer charge index Z to the logarithmic gap ln(1 + Z/φ)/ln φ. Researchers modeling fermion masses on the Recognition Science phi-ladder cite this alias when equating the integrated RG residue f_i(μ⋆) to the closed-form gap at the anchor scale. The definition is a one-line alias to the imported gap function from RSBridge.
Claim. $F(Z) := (1 / ln φ) ln(1 + Z/φ)$ for integer $Z$, where $φ$ is the self-similar fixed point satisfying the Recognition Composition Law.
background
The module supplies a clean interface for single-anchor RG phenomenology in the mass framework. It reuses Constants.phi (the golden-ratio fixed point) and the gap display function imported from RSBridge.Anchor. Upstream, gap(Z) is defined as (ln(1 + Z/φ))/ln φ and is described as the closed form that the integrated RG residue is claimed to equal at the anchor scale μ⋆, with f_i(μ⋆) := (1/ln φ) ∫ γ_i(μ') d(ln μ') from the RG equation d(ln m)/d(ln μ) = -γ_m(μ). The module states the identity f_i(μ⋆) = F(Z_i) as a hypothesis for downstream use while keeping the actual QCD/QED kernels external.
proof idea
One-line wrapper that applies the gap definition imported from RSBridge.Anchor.
why it matters
The alias supplies the explicit display function required by the single-anchor policy, feeding the standard Lagrangian in Action.QuadraticLimit and the RCL verification in CostAlgebra.SatisfiesRCL. It closes the interface described in the module doc for linking the phi-ladder (T6) to RG transport and the eight-tick octave structure. It touches the open question of explicit anomalous-dimension integration, which is left to external tools or the certified variant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.