F
plain-language theorem explainer
The declaration supplies the base generating functional F(z) = log(1 + z/φ) inside the Pipelines module. Gap and mass derivations in Recognition Science cite it as the un-normalized logarithmic map that later feeds normalized anchor residues. The definition is a direct one-line assignment of the Real logarithm applied to a linear fractional argument in the golden ratio.
Claim. $F(z) = log(1 + z/φ)$ for real $z$, where $φ$ denotes the golden ratio.
background
The module fixes the golden ratio as a concrete real constant. The functional form matches the un-normalized core of several gap maps: RSBridge.Anchor.gap normalizes the identical expression by an extra log(φ) factor to obtain the residue at the anchor scale, while Physics.AnchorPolicy.F simply aliases that normalized version. Upstream structure as from SimplicialLedger.ContinuumBridge supplies the Laplacian-to-action identification that motivates logarithmic cost functions throughout the framework.
proof idea
Direct definition; the body is a single Real.log application with no lemmas or tactics.
why it matters
The function supplies the primitive logarithmic generator used by downstream declarations including SatisfiesRCL in CostAlgebra (which encodes the Recognition Composition Law) and multiple chemistry results on electronegativity trends and atomic radii. It therefore sits at the base of the phi-ladder constructions that realize T5 J-uniqueness and the gap-45 derivation. No open scaffolding is closed here; the definition remains a reusable building block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.