lambda_from_phi
plain-language theorem explainer
The RG normalization constant equals the natural log of the golden-ratio fixed point φ. Anchor-scale non-circularity and baryogenesis certificates cite this to lock transport scales to Recognition-native units. The proof is pure reflexivity: the constant is defined to be ln φ, so equality holds by unfolding.
Claim. The RG normalization constant satisfies $\lambda = \ln\varphi$, where $\varphi$ is the self-similar fixed point forced by the Recognition cost.
background
This module certifies that the anchor scale $\mu_\star = 182.201,\mathrm{GeV}$ is fixed by PMS/BLM stationarity on the SM RG flow, using only gauge-group beta structure and no measured fermion masses. Among the structural claims, P3 is the $\varphi$-connection: the transport normalization must be $\lambda = \ln\varphi$.
Upstream, lambda in RG transport is introduced exactly as $\lambda := \ln\varphi$. Here $\varphi$ is the unique self-similar fixed point of the Recognition cost (forcing chain T5–T6: $J(x)=\cosh(\log x)-1$, with $\varphi$ solving the fixed-point equation). Related scale maps in the codebase are pure $\varphi$-powers, so log-$\varphi$ is the natural additive step on that ladder.
The certificate draws a hard line between structure proved in Lean (P1–P4) and numerics certified externally (C1–C3). P3 sits entirely on the structural side.
proof idea
One-line term proof by rfl. The definition of the RG normalization constant is already $\lambda := \mathrm{Real.log},\varphi$, so the equality goal is definitional and closes by reflexivity. No lemmas are applied; no arithmetic is performed.
why it matters
P3 of the Anchor Scale Non-Circularity Certificate: it records that the transport normalization is not a free fit parameter but is forced by the cost-function fixed point $\varphi$ (primer T5 J-uniqueness, T6 $\varphi$ fixed point). Without this lock, stationarity bounds on $\mu_\star$ could silently reintroduce mass-dependent scales.
Downstream, the baryogenesis certificate structure exposes a lambda_from_phi field (bounds on the CP-sector $\lambda$) and the packaged baryogenesis_cert theorem; both sit in the same $\varphi$-normalized unit system this identity underwrites. Sibling claims in the module (mass-independent betas, positivity of $\mu_\star$, dispersion-minimum certification) rely on the same non-circular scaffolding.
The result does not compute $\mu_\star$ numerically; it only pins the log-$\varphi$ yardstick that makes the structural half of the honesty principle hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.