additive_closure_golden
plain-language theorem explainer
Researchers deriving the golden ratio from additive closure on geometric scale ladders cite this result to justify the self-similar fixed point in Recognition Science hierarchies. Assuming a positive real-valued sequence that scales geometrically by factor σ > 1 and satisfies the additive relation at the second level, the theorem concludes that σ must satisfy the quadratic equation σ² = σ + 1. The proof rewrites the level-2 value in two equivalent forms using the uniform scaling and closure assumptions, subtracts them to obtain a factored zero,
Claim. Let $ℓ : ℕ → ℝ$ be a positive function and let $σ > 1$ be real. Suppose $ℓ(k+1) = σ ⋅ ℓ(k)$ for all natural $k$ and $ℓ(2) = ℓ(1) + ℓ(0)$. Then $σ² = σ + 1$.
background
The module derives additive scale composition from the Recognition Composition Law (RCL) without assuming linearity, closing Proposition 4.3 of the phi paper. It defines posting potential Π(x) := J(x) + 1 = ½(x + x⁻¹), which satisfies the multiplicative relation Π(ab) + Π(a/b) = 2Π(a)Π(b) from the RCL. A uniform scale ladder is a geometric sequence levels(k) = σ^k levels(0) with σ > 1. Additive closure requires levels(2) = levels(1) + levels(0). Upstream, mul_eq_zero states that LogicInt has no zero divisors: from a * b = 0, either a = 0 or b = 0.
proof idea
The proof first obtains levels(2) = σ² levels(0) by applying the uniform scaling twice and ring simplification. It next rewrites levels(2) = (σ + 1) levels(0) from the closure assumption and uniform scaling. Subtracting these expressions produces (σ² - σ - 1) levels(0) = 0. The mul_eq_zero theorem (applied after the real arithmetic) together with levels(0) ≠ 0 forces the quadratic factor to vanish.
why it matters
This result supports forcing phi as the self-similar fixed point (T6) in the UnifiedForcingChain by converting extensivity into the golden equation. It fills the additive-closure step in Proposition 4.3 on scale composition from the RCL. The declaration sits among sibling results such as posting_extensivity_forces_phi and closure_forces_additive, which together derive the phi-ladder recurrence without external linearity assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.