phi_ladder_pos
Every rung on the φ-ladder is strictly positive for any integer tier. Researchers deriving the instability of the ground state x=1 and the resulting positive costs would cite this to guarantee all non-trivial entries contribute positively. The proof is a one-line wrapper applying the positivity of integer powers to the golden-ratio base.
claimFor every integer $n$, $0 < φ^n$, where $φ$ is the golden-ratio fixed point.
background
The φ-ladder is the function sending each integer tier $n$ to $φ^n$, where $φ$ is the self-similar fixed point forced by T6. This appears upstream both as the set of all such powers and as the tiered value used in nucleosynthesis calculations. The StillnessGenerative module places the ladder inside the derivation that x=1 cannot remain uniform because recognition and the eight-tick cycle require non-trivial content, which T6 closure forces to be exactly the powers $φ^n$ for $n ≠ 0$.
proof idea
The proof is a one-line wrapper that applies the zpow_pos lemma to the established positivity of $φ$.
why it matters in Recognition Science
It is invoked by the parent theorem phi_ladder_positive_cost to obtain $0 < Jcost(φ^n)$ for $n ≠ 0$. This supplies the positivity step in the T6 closure argument of the module, confirming that every non-trivial ledger entry generated from the ground state carries positive cost and that the Fibonacci cascade can populate the entire ladder. The result therefore supports the claim that x=1 is the maximally creative source rather than a passive equilibrium.
scope and limits
- Does not give the numerical magnitude of any ladder entry.
- Does not address the J-cost function itself.
- Does not extend positivity to non-integer exponents.
- Does not prove that the ladder exhausts all possible non-trivial states.
Lean usage
have hpos : 0 < phi_ladder n := phi_ladder_pos nformal statement (Lean)
46theorem phi_ladder_pos (n : ℤ) : 0 < phi_ladder n :=
proof body
One-line wrapper that applies zpow_pos.
47 zpow_pos PhiForcing.phi_pos n
48