lnphi
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute a numerical value for ln phi.
- Does not prove any functional equation or inequality involving the logarithm.
- Does not implement the full RG transport kernels or anomalous dimensions.
formal statement (Lean)
55noncomputable def lnphi : ℝ := Real.log phi
proof body
Definition body.
56
57/-- Display function F(Z) = log(1 + Z/φ) / log(φ).
58 This is exactly `RSBridge.gap`. We provide an alias for clarity. -/