lambda
plain-language theorem explainer
The definition introduces the RG normalization constant λ as the natural logarithm of the golden ratio. Researchers deriving mass residues from integrated anomalous dimensions in the Recognition Science framework cite this to scale the transport integral. It is supplied as a direct abbreviation with no lemmas or computation required.
Claim. Define the normalization constant by $λ := ln φ$, where $φ$ denotes the golden ratio.
background
The RGTransport module formalizes renormalization-group transport of mass residues. The integrated residue is written $f(μ₀, μ₁) = (1/λ) ∫_{ln μ₀}^{ln μ₁} γ_m(μ') d(ln μ')$, and the structural-to-physical mass relation becomes $m_phys = m_struct · φ^{-f}$. The module doc states that λ = ln φ supplies the required normalization factor in the mass formula.
proof idea
The declaration is a direct abbreviation Real.log phi with an empty proof body.
why it matters
This λ enters the balance condition J_curv λ = J_bit_normalized whose unique positive root is proved in balance_determines_lambda and balance_unique_positive_root. It therefore anchors the curvature cost functional J_curv = 2λ² to the phi-ladder used for mass residues. The definition closes the normalization step required by the RG transport construction in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.