phiLadderScale
The phiLadderScale definition maps each integer rung n to the energy scale phi raised to n, expressed in units of a reference energy E0. Physicists deriving renormalization-group flows from Recognition Science would cite it when discretizing scales via the golden-ratio fixed point. The definition is a direct exponentiation with no additional lemmas or reductions.
claimThe energy scale at φ-ladder rung n is given by E_n = φ^n (in units of reference scale E_0), where φ is the golden ratio.
background
The QFT module on running couplings treats different φ-ladder rungs as distinct energy scales at which J-cost optimization produces scale-dependent couplings. The Recognition Science framework obtains φ as the self-similar fixed point forced by T5 (J-uniqueness) and T6 in the unified forcing chain. This definition therefore supplies the basic map from rung index to scale that later theorems use to recover the observed running of α, α_s and α_W.
proof idea
The declaration is a direct definition that sets the function equal to the real power phi ^ n. No lemmas are invoked; the body is a one-line abbreviation.
why it matters in Recognition Science
The definition is the base scale map invoked by the downstream theorems scale_at_zero, scale_at_one, scale_at_two and phi_ladder_hierarchy. It supplies the concrete realization of the QFT-011 target (running couplings from φ-scaling) and connects to the eight-tick octave and D = 3 forced by T7-T8. It leaves open the precise derivation of the beta-function coefficients from rung-dependent J-cost.
scope and limits
- Does not specify a numerical value for the reference scale E0.
- Does not derive beta functions or explicit running equations.
- Does not restrict the rung index n to nonnegative integers.
- Does not incorporate loop corrections or renormalization-scheme dependence.
formal statement (Lean)
73noncomputable def phiLadderScale (n : ℤ) : ℝ := phi ^ n
proof body
Definition body.
74
75/-- φ is nonzero. -/