lnphi
plain-language theorem explainer
lnphi defines the natural logarithm of the golden ratio phi. It supplies the explicit denominator in the display function F(Z) = log(1 + Z/phi)/log(phi) used for RG residues at single anchors. Mass framework users cite it when converting the integrated anomalous dimension hypothesis into the gap expression. The definition is a direct one-line alias to the real logarithm applied to the constant phi.
Claim. Let $phi$ be the golden ratio. Define $ln phi := log phi$, where $log$ denotes the natural logarithm.
background
The Single-Anchor RG Policy module supplies a Lean interface for mass anchors, importing the proven constant phi from Constants and reusing the gap function from RSBridge.Anchor. The display function F(Z) is written explicitly as log(1 + Z/phi) / log(phi) to isolate the RG residue hypothesis f_i(mu*) = F(Z_i) arising from the integral of the mass anomalous dimension. This lnphi extracts the denominator for clarity in stability and flavor calculations.
proof idea
The definition is a one-line wrapper that applies Real.log directly to the golden ratio constant phi.
why it matters
This definition supports the anchor policy scaffolding by making the logarithmic base explicit for the F(Z) = gap identity. It connects to the phi-ladder mass formula and the RG transport integral in the module. The construction fills the interface role between Constants.phi and downstream stability bounds at anchors, consistent with the self-similar fixed point for phi in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.