phi_ladder_mul_closed
plain-language theorem explainer
The theorem shows that the set of all integer powers of φ is closed under multiplication by φ itself. Researchers building discrete spectra or mass ladders in Recognition Science cite this when scaling stable positions along the phi-ladder. The proof extracts the integer exponent from membership and shifts it by one using the zpow addition rule.
Claim. If $x = φ^n$ for some $n ∈ ℤ$, then $x φ$ also equals $φ^k$ for some integer $k$.
background
PhiLadder is the set {x ∈ ℝ | ∃ n : ℤ, x = φ^n}. The PhiEmergence module derives φ from J-cost minimization and establishes basic properties of this ladder. Upstream results supply the positivity of φ (phi_pos) and the ladder definition itself, which is reused across unification and game-theory modules.
proof idea
The term proof obtains the witness integer n from the membership hypothesis hx, then rewrites x * φ as φ^{n+1} via zpow_add_one₀ applied to the positivity of φ.
why it matters
Closure under multiplication by φ is required to keep the ladder invariant under the self-similar scaling that appears in the forcing chain (T5–T8) and in the mass formula yardstick * φ^(rung). It directly supports downstream constructions of stable positions even though no immediate used_by edges are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.