phiRung_add
The φ-ladder scaling function obeys the additive homomorphism φ^{m+n} = φ^m · φ^n for integers m and n. Researchers deriving combined masses or energies from multiple rungs in the Recognition Science framework cite this when superposing independent contributions. The proof is a direct term reduction to the definition of integer exponentiation followed by the standard nonzero-base power-addition identity.
claimLet φ denote the golden ratio. For the ladder scaling function defined by f(k) := φ^k with k ∈ ℤ, one has f(m + n) = f(m) · f(n) for all m, n ∈ ℤ.
background
In the RS-native unit system the φ-ladder organizes all measures so that rung n scales any quantity by φ^n. The function phiRung computes this factor directly as φ raised to the integer argument. Upstream results supply the fact that φ ≠ 0, which is the sole hypothesis needed for the power-addition rule to hold on the integers.
proof idea
The term proof first simplifies the definition of the scaling function, then applies the lemma phi_ne_zero to confirm the base is nonzero and invokes the standard zpow addition identity.
why it matters in Recognition Science
The result supplies the algebraic closure property for rung arithmetic that appears in every mass formula of the form yardstick · φ^(rung - 8 + gap(Z)). It supports the T5 J-uniqueness step and the T6 self-similar fixed point by guaranteeing that independent rung contributions combine without extra factors. No immediate downstream theorems are recorded, yet the identity is presupposed by any later theorem that adds or subtracts rungs.
scope and limits
- Does not extend to real-valued rung additions without continuity assumptions.
- Does not derive the numerical value of φ or its positivity.
- Does not address convergence of the ladder for non-integer exponents.
formal statement (Lean)
168lemma phiRung_add (m n : ℤ) : phiRung (m + n) = phiRung m * phiRung n := by
proof body
Term-mode proof.
169 simp only [phiRung]
170 exact zpow_add₀ phi_ne_zero m n
171