phi_zpow_ne_one
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not extend the claim to real exponents.
- Does not compute explicit numerical values of φ^n.
- Does not establish existence or positivity of costs on the ladder.
- Does not address stability under small perturbations.
Lean usage
example {n : ℤ} (hn : n ≠ 0) : PhiForcing.φ ^ n ≠ 1 := phi_zpow_ne_one hnformal statement (Lean)
49theorem phi_zpow_ne_one {n : ℤ} (hn : n ≠ 0) : PhiForcing.φ ^ n ≠ 1 := by
proof body
Term-mode proof.
50 have hφ_gt := PhiForcing.phi_gt_one
51 intro heq
52 have h0 : PhiForcing.φ ^ (0 : ℤ) = 1 := zpow_zero _
53 have hmono : StrictMono fun m : ℤ => PhiForcing.φ ^ m :=
54 zpow_right_strictMono₀ hφ_gt
55 exact hn (hmono.injective (heq.trans h0.symm))
56