phi_ladder_ratio
plain-language theorem explainer
Adjacent rungs on the golden-ratio ladder differ by exactly the factor φ. Researchers deriving discrete spectra from J-cost minimization cite this algebraic identity when closing the ladder under scaling. The proof rewrites the exponent sum, cancels the common power after confirming nonzeroness, and finishes by field simplification.
Claim. For every integer $n$, $φ^{n+1}/φ^n = φ$, where $φ$ is the golden ratio.
background
The PhiEmergence module shows how the golden ratio arises from minimizing J-cost under self-similar scaling. The phi-ladder is the discrete set of positive reals closed under multiplication by φ, generated as powers of the fixed point of the Recognition Composition Law. Upstream results supply the positivity of φ and the nonzeroness of its integer powers; the same identity appears in the UV-cutoff energy ladder.
proof idea
One-line wrapper that first invokes phi_pos to obtain φ ≠ 0, then zpow_ne_zero to obtain φ^n ≠ 0, rewrites the exponent via zpow_add_one₀, and cancels via field_simp.
why it matters
The identity feeds the downstream claim that stable positions coincide exactly with the phi-ladder. It supplies the algebraic closure step required by the self-similar fixed-point forcing (T6) and is reused verbatim in the QFT UV-cutoff construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.