pith. machine review for the scientific record. sign in
def definition def or abbrev high

lambda

show as:
view Lean formalization →

The normalization constant λ is defined as the natural logarithm of the golden ratio φ. Researchers deriving structural masses via RG transport in Recognition Science cite this when normalizing the integrated anomalous dimension in the residue formula f(μ₀, μ₁). It enters the balance condition that fixes the unique positive root lambda_0. The declaration is a direct one-line assignment of Real.log phi.

claim$λ := ln(φ)$, where $φ = (1 + √5)/2$ is the golden ratio fixed point of the Recognition Composition Law.

background

The module formalizes RG transport for mass residues in the Standard Model setting. Fermion masses run according to d(ln m)/d(ln μ) = −γ_m(μ), and the integrated residue is f(μ₀, μ₁) = (1/λ) ∫ γ_m(μ') d(ln μ') with λ = ln φ. This yields the relation m_phys = m_struct · φ^{−f} between the anchor-scale structural mass and the observed physical mass.

proof idea

One-line definition that directly assigns Real.log phi. No lemmas or tactics are invoked; the declaration is a primitive constant binding.

why it matters in Recognition Science

λ supplies the normalization factor required by the mass formula and appears in every downstream balance theorem (balance_determines_lambda, balance_unique_positive_root, J_curv). It closes the link between the J-uniqueness fixed point (T5) and the eight-tick octave scale, fixing the RS-native unit in which G = φ^5/π and the alpha band are expressed.

scope and limits

formal statement (Lean)

  92def lambda : ℝ := Real.log phi

proof body

Definition body.

  93
  94/-- λ is positive. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

… and 10 more

depends on (4)

Lean names referenced from this declaration's body.