phi_ladder_ne_one
plain-language theorem explainer
The declaration shows that the φ-ladder at any nonzero integer rung differs from the ground state value 1. Researchers working on the generative instability of x=1 cite it to guarantee that the ladder populates only non-unit states. The proof is a direct one-line application of the upstream zpow non-equality lemma after the ladder definition identifies the two expressions.
Claim. For every integer $n ≠ 0$, the φ-ladder value at rung $n$, given by $φ^n$, satisfies $φ^n ≠ 1$.
background
The StillnessGenerative module derives that the unique zero-defect state x=1 generates all structure. The φ-ladder is defined locally as the map sending integer n to φ^n, where φ is the self-similar fixed point arising from T6 closure. Upstream, phi_zpow_ne_one proves φ^n ≠ 1 for n ≠ 0 by invoking φ > 1 together with strict monotonicity of the zpow map on integers.
proof idea
The proof is a one-line wrapper that applies the lemma phi_zpow_ne_one directly to the hypothesis hn : n ≠ 0 after the definition phi_ladder n := φ^n equates the two sides.
why it matters
This result is invoked by the downstream theorem phi_ladder_positive_cost to obtain positive J-cost on nonzero rungs. It realizes the module step that every non-trivial entry on the closed geometric sequence must be of the form φ^n for n ≠ 0, completing the T6 closure within the T0-T8 chain and the T7 eight-tick requirement that forces departure from x=1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.