phi_ladder_ratio
plain-language theorem explainer
The theorem establishes that energies at consecutive rungs of the phi-ladder, scaled from a nonzero base E0, stand in exact ratio phi. Researchers modeling natural UV cutoffs in QFT from discrete spacetime would cite this identity to justify finite loop integrals. The proof is a direct term-mode algebraic reduction that unfolds the ladder energy definition and cancels via exponent addition and division rules.
Claim. Let $E_0$ be a nonzero real number serving as the fundamental energy scale. For any integer $n$, the ratio of the energy at rung $n+1$ to the energy at rung $n$ on the phi-ladder equals the golden ratio: $E_0 phi^{n+1} / (E_0 phi^n) = phi$.
background
The module derives a physical UV cutoff for QFT from Recognition Science discreteness at the tau0 scale, with momenta bounded by p_max = hbar/tau0. The base energy E0 is the fundamental scale hbar/tau0. Upstream results include the scale function returning phi^k and the phi-ladder ratio theorem in PhiEmergence, which states that adjacent rungs satisfy phi^(n+1)/phi^n = phi. The local setting treats renormalization as finite because the cutoff is physical rather than artificial.
proof idea
The term proof unfolds phiLadderEnergy, invokes phi nonzero from Constants.phi_pos, commutes the E0 factors, applies mul_div_mul_right, rewrites via zpow_add_one0, cancels the common phi^n term with div_self, and reduces the remainder to phi via mul_one.
why it matters
This identity feeds the hypothesis H_StableIffPhiLadder that stable positions coincide exactly with the phi-ladder under self-similar J-cost minimization. It supplies the phi-forcing step (T6) in the unified forcing chain and supports the natural UV regularization claim in the module, where discrete rungs render all loop integrals convergent. The result also connects to the eight-tick octave structure through the ladder's self-similar spacing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.