F
plain-language theorem explainer
F(Z) is the display function log(1 + Z/φ)/log(φ) that equals the claimed integrated RG residue at the anchor scale. Mass-spectrum and RG-transport modelers cite this alias when wiring single-anchor phenomenology into downstream calculations. The definition is a direct one-line re-export of the gap function from RSBridge.
Claim. $F(Z) := (1 / ln φ) ln(1 + Z/φ)$ for integer $Z$, where $φ$ denotes the golden ratio from Constants.
background
The AnchorPolicy module supplies a Lean surface for single-anchor RG policy and stability scaffolding. It reuses Constants.phi (proven) and re-exports the gap function so that downstream modules can depend on a clean interface for the anchor scale and the residue hypothesis. The module states the phenomenological claim that the integrated RG residue equals F(Z_i) at μ⋆ while leaving the actual QCD/QED kernels to external tools.
proof idea
One-line wrapper that applies the gap definition from IndisputableMonolith.Masses.RSBridge.Anchor.
why it matters
The alias feeds standardLagrangian in Action.QuadraticLimit and SatisfiesRCL in CostAlgebra, plus multiple chemistry results on atomic radii and electronegativity. It fills the single-anchor display function required by the mass framework and the RG residue hypothesis in RGTransport. It touches the phi-ladder mass formula and the T5 J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.