phi_ladder_hierarchy
plain-language theorem explainer
The theorem establishes that the φ-ladder scale at any positive integer rung n exceeds unity. Researchers deriving renormalization-group flows from Recognition Science scaling would cite it to justify exponential hierarchies among coupling constants. The proof is a short term-mode derivation that unfolds the scale definition, rewrites the exponent, and applies the standard power inequality for bases greater than one.
Claim. Let $n$ be a positive integer. Then the φ-ladder scale function at rung $n$ satisfies scale$(n) > 1$, where the scale is realized as a positive power of the golden ratio φ.
background
In the QFT.RunningCouplings module the φ-ladder supplies discrete energy scales for running couplings, with each rung corresponding to a distinct J-cost optimum. The phiLadderScale function maps a natural-number rung to the associated scale factor, conventionally a power of φ. Upstream, phi_gt_one' asserts φ > 1 (derived from φ > 1.5 via linarith in the HiggsMechanism context) and supplies the base needed for the power inequality. Related rung definitions in mass anchors and asteroid spectroscopy assign integer positions on the same ladder to particles and material classes.
proof idea
The proof is a short term-mode derivation. It unfolds phiLadderScale, rewrites the natural-number exponent via zpow_natCast, and applies the lemma one_lt_pow₀ instantiated with phi_gt_one' together with the positivity of n.
why it matters
This result supplies the elementary inequality required for the one-loop running-coupling formulas presented later in the same module, such as α(n) = α₀ / (1 + b · n · ln φ). It sits inside the Recognition Science forcing chain once φ has been fixed as the self-similar point (T6), furnishing the discrete scales that drive renormalization-group evolution. No downstream uses are recorded yet, but the theorem closes a basic prerequisite for the QFT-011 development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.