phi_zpow_ne_one
plain-language theorem explainer
phi_zpow_ne_one shows that the golden ratio to any nonzero integer power differs from one. Workers on the StillnessGenerative module cite it to separate the phi-ladder from the ground state x=1. The term proof assumes equality to one, invokes the zero-power identity, and extracts a contradiction from strict monotonicity of the integer zpow map.
Claim. Let $n$ be a nonzero integer and let $φ > 1$ be the golden ratio. Then $φ^n ≠ 1$.
background
The StillnessGenerative module derives from the T0–T8 chain that the unique zero-defect state x=1 is unstable and must generate non-trivial content. The phi-ladder is the sequence of states φ^k for k ∈ ℤ, where φ is the self-similar fixed point forced by the Recognition Composition Law. PhiForcing.phi_gt_one supplies φ > 1, which is required for monotonicity of the power map. The local setting is the claim that a uniform ledger violates the eight-tick period of T7 and therefore forces departure from unity.
proof idea
The proof is a term-mode argument. It obtains φ > 1 from PhiForcing.phi_gt_one. It assumes φ^n = 1 for contradiction and recalls φ^0 = 1 via zpow_zero. Strict monotonicity of m ↦ φ^m on ℤ follows from zpow_right_strictMono₀. Injectivity of this map then forces n = 0, contradicting the hypothesis.
why it matters
The lemma is invoked directly by phi_ladder_ne_one to show the ladder avoids unity and by unity_has_no_phi_structure to prove that the uniform initial condition carries no phi-structure. It fills the module step that every non-trivial entry must be of the form φ^n with n ≠ 0, consistent with T6 closure and the eight-tick octave of T7. No open scaffolding remains at this point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.