lambda_pos
plain-language theorem explainer
Positivity of the RG normalization constant lambda, equal to the natural logarithm of the golden ratio, is established here. Researchers building mass residue bounds or coupling band certificates in Recognition Science cite this when verifying positivity in optimization or cosmological contexts. The proof reduces to applying the logarithm positivity property once phi > 1 is obtained from an upstream lemma.
Claim. The RG normalization constant satisfies $lambda := ln phi > 0$.
background
The RGTransport module formalizes renormalization group transport for mass residues. Fermion masses run with scale mu according to d(ln m)/d(ln mu) = -gamma_m(mu), and the integrated residue is f(mu0, mu1) = (1/lambda) integral gamma_m d(ln mu'), where lambda = ln phi normalizes the transport in the structural-to-physical mass relation m(mu*) = m_phys * phi^f.
proof idea
The proof is a term-mode one-line wrapper. It obtains 1 < phi from the upstream lemma one_lt_phi, then applies Real.log_pos to conclude lambda > 0.
why it matters
This result feeds OmegaLambdaBandCert, CosmologicalConstantCert, and HydrideSCOptimizationCert, supplying the lambda_pos clause in each certificate structure. It anchors the basic positivity requirement for the normalization constant in the phi-ladder mass formula, consistent with T5 J-uniqueness and T6 phi fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.