Encyclopedia Foundation Foundation Phi Closure Selection Ratio Eq Phi Of Uniform Adjacent Composition
ARTICLE 4 claims 4 theorems
Foundation Phi Closure Selection Ratio Eq Phi Of Uniform Adjacent Composition
A scale sequence that grows by one fixed ratio and composes each level from its two neighbors must have the golden ratio as that ratio.
The golden ratio from two premises
A ladder of levels, each level a number. The ladder is uniform: every step up multiplies the level by the same ratio r, with r greater than 1. The ladder is also adjacent-composed: each level, from the third onward, is the sum of the two levels below it. The theorem ratio_eq_phi_of_uniform_adjacent_composition proves that these two conditions alone force r to equal the golden ratio φ, about 1.618. No further assumption about closure, minimality, or cost is needed. The proof is algebraic: from the recurrence s(n+2) = s(n+1) + s(n) and the uniform ratio s(n+1) = r·s(n), the equation 1 + r = r² follows directly, and its positive root is φ.
The golden ratio has a long classical history. Euclid called it the extreme and mean ratio, the division of a segment so that the whole is to the longer part as the longer part is to the shorter. It solves r² = r + 1, has the continued fraction [1; 1, 1, 1, ...], and appears in the pentagon's geometry and in the Fibonacci sequence, where successive terms approach φ. The framework's contribution is not the number itself but a structural route to it: two plain premises about how a scale ladder behaves force the golden equation, with no appeal to a pre-chosen closure level.
In Recognition Science, the framework models reality as a ledger, a discrete record of recognition events where each event has a cost. The ladder here is a scale of levels, and the recurrence says each level is composed from its two neighbors. The theorem removes a prior assumption: earlier derivations took closure, the equation 1 + r = r², as a hypothesis. This result derives it from the uniform ratio and adjacent composition instead. The framework's machine-checked library of formal theorems contains this proof, kernel-verified with no framework-specific axioms.
The theorem also clarifies what does not select the golden ratio. A separate result shows that higher closure levels, like 1 + r = r³ (the plastic constant), leave orphan rungs: the second rung r² is not the sum of any two earlier rungs. And cost minimization does not select level 2; the per-closure cost J(1 + r) strictly decreases as the closure level rises, approaching a trivial limit. The selection of φ is structural, from generation completeness, not variational. The ladder form itself, a single uniform ratio, remains a premise, not yet derived from more basic principles.
THEOREM ratio_eq_phi_of_uniform_adjacent_composition · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- **Direct forcing.** A positive scale sequence with a constant inter-level
ratio `r > 1` (uniform scaling: one ratio, no free parameters) satisfying the
adjacent additive recurrence (each level composes its two neighbours: binary
posting) has ratio `φ`. Closure is not assumed; the golden equation falls
out of the two premises algebraically. -/
theorem ratio_eq_phi_of_uniform_adjacent_composition {s : ℕ → ℝ} {r : ℝ}
(h0 : 0 < s 0) (hr : 1 < r)
(hunif : ∀ n, s (n + 1) = r * s n)
(hadj : ∀ n, s (n + 2) = s (n + 1) + s n) :
r = phi := by
have h1 : s 1 = r * s 0 := hunif 0
have h2u : s 2 = r * s 1 := hunif 1
have h2a : s 2 = s 1 + s 0 := hadj 0
rw [h1] at h2a h2u
-- r * (r * s 0) = r * s 0 + s 0
have hs0 : s 0 ≠ 0 := ne_of_gt h0
have hfact : s 0 * (r ^ 2 - r - 1) = 0 := by nlinarith [h2u, h2a]
rcases mul_eq_zero.mp hfact with h | h
· exact absurd h hs0
· have hsq : 1 + r = r ^ 2 := by nlinarith [h]
exact PhiForcingDerived.phi_forcing_complete r (by linarith) (by linarith) hsq
THEOREM high_closure_orphan · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- **Orphan theorem.** If the ladder closes at level `k ≥ 3` (`1 + r = r^k`),
then `r²` is not the composition of any two rungs: it is an orphan scale,
postable but never produced by composing ledger events. -/
theorem high_closure_orphan {r : ℝ} {k : ℕ} (hr : 1 < r) (hk : 3 ≤ k)
(hclose : 1 + r = r ^ k) (a b : ℕ) :
r ^ a + r ^ b ≠ r ^ 2 := by
intro hab
rcases rung_two_sum_cases hr hab with ⟨_, _, h2⟩ | ⟨_, _, h12⟩ | ⟨_, _, h12⟩ | ⟨_, _, hr2⟩
· -- r² = 2, so r³ = 2r ≤ r^k, giving 1 + r ≥ 2r, i.e. 1 ≥ r.
have hk3 : r ^ 3 ≤ r ^ k := pow_le_pow_of_le (le_of_lt hr) hk
have hr3 : r ^ 3 = 2 * r := by
calc r ^ 3 = r * r ^ 2 := by ring
_ = r * 2 := by rw [h2]
_ = 2 * r := by ring
linarith [hk3, hr3, hclose, hr]
· -- 1 + r = r² and 1 + r = r^k force k = 2.
have hkk : r ^ k = r ^ 2 := by rw [← h12, hclose]
have := pow_inj_right hr hkk
omega
· have hkk : r ^ k = r ^ 2 := by rw [← h12, hclose]
have := pow_inj_right hr hkk
omega
· -- r = 2: closure gives 3 = 2^k ≥ 8.
have hk3 : r ^ 3 ≤ r ^ k := pow_le_pow_of_le (le_of_lt hr) hk
rw [hr2] at hk3 hclose
norm_num at hk3 hclose
linarith [hk3, hclose]
THEOREM closure_level_two_of_rung_two_composed · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- **Selection theorem.** Among adjacent-closed ladders (`1 + r = r^k`,
`k ≥ 2`), the ones in which the second rung is a composition of two rungs
are exactly the `k = 2` ladders, and then `r = φ`. The selecting premise is
generation completeness (no orphan scales), not minimality. -/
theorem closure_level_two_of_rung_two_composed {r : ℝ} {k : ℕ}
(hr : 1 < r) (hk : 2 ≤ k) (hclose : 1 + r = r ^ k)
(a b : ℕ) (hab : r ^ a + r ^ b = r ^ 2) :
k = 2 ∧ r = phi := by
rcases rung_two_sum_cases hr hab with ⟨_, _, h2⟩ | ⟨_, _, h12⟩ | ⟨_, _, h12⟩ | ⟨_, _, hr2⟩
· -- r² = 2: exclude both k = 2 and k ≥ 3.
rcases (le_iff_eq_or_lt.mp hk) with hkk | hkk
· -- k = 2: closure gives 1 + r = 2, i.e. r = 1.
subst hkk
exfalso
linarith [hclose, h2, hr]
· -- k ≥ 3: r³ = 2r ≤ r^k gives 1 ≥ r.
have hk3 : r ^ 3 ≤ r ^ k := pow_le_pow_of_le (le_of_lt hr) hkk
have hr3 : r ^ 3 = 2 * r := by
calc r ^ 3 = r * r ^ 2 := by ring
_ = r * 2 := by rw [h2]
_ = 2 * r := by ring
exfalso
linarith [hk3, hr3, hclose, hr]
· -- 1 + r = r²: closure gives r^k = r², so k = 2; then r = φ.
have hkk : r ^ k = r ^ 2 := by rw [← h12, hclose]
have hk2 := pow_inj_right hr hkk
exact ⟨hk2, PhiForcingDerived.phi_forcing_complete r (by linarith) (by linarith) h12⟩
· have hkk : r ^ k = r ^ 2 := by rw [← h12, hclose]
have hk2 := pow_inj_right hr hkk
exact ⟨hk2, PhiForcingDerived.phi_forcing_complete r (by linarith) (by linarith) h12⟩
· -- r = 2: exclude both k = 2 and k ≥ 3.
rcases (le_iff_eq_or_lt.mp hk) with hkk | hkk
· subst hkk
rw [hr2] at hclose
norm_num at hclose
· have hk3 : r ^ 3 ≤ r ^ k := pow_le_pow_of_le (le_of_lt hr) hkk
rw [hr2] at hk3 hclose
norm_num at hk3 hclose
linarith [hk3, hclose]
THEOREM closure_cost_strictly_decreasing · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- **Route-kill measurement.** The per-closure cost `J(1 + r)` is strictly
decreasing as the closure level rises: for any two closure ladders at
consecutive levels, the higher-level ladder has the cheaper closure.
Cost-minimization therefore does not select `k = 2`; it selects nothing
finite. This kills the sub-route "the J-cost excess selects the closure
level by minimization." -/
theorem closure_cost_strictly_decreasing {r s : ℝ} {k : ℕ}
(hr : 1 < r) (hrc : 1 + r = r ^ (k + 2))
(hs : 1 < s) (hsc : 1 + s = s ^ (k + 3)) :
Cost.Jcost (1 + s) < Cost.Jcost (1 + r) := by
have hsr : s < r := by
by_contra h
push_neg at h
rcases lt_or_eq_of_le h with hlt | heq
· -- r < s: strict monotonicity of the closure polynomial gives
-- f_{k+3}(r) < f_{k+3}(s) = 0, but f_{k+3}(r) = r² - 1 > 0.
have h1 : r ^ (k + 3) - r - 1 < s ^ (k + 3) - s - 1 :=
closurePoly_strictMono (le_of_lt hr) hlt (by omega)
have hfs : s ^ (k + 3) - s - 1 = 0 := by
have e : s ^ (k + 3) = 1 + s := by rw [← hsc]
linarith
have hfr : r ^ (k + 3) - r - 1 = r ^ 2 - 1 := by
have e0 : k + 3 = (k + 2) + 1 := by omega
have e : r ^ (k + 3) = r * r ^ (k + 2) := by rw [e0, pow_succ']
rw [e, ← hrc]
ring
nlinarith [h1, hfs, hfr, hr,
mul_pos (sub_pos.mpr hr) (by linarith : (0 : ℝ) < r + 1)]
· -- r = s: then r^{k+2} = r^{k+3}, impossible.
rw [← heq] at hsc
have e1 : r ^ (k + 2) = r ^ (k + 3) := by rw [← hrc, ← hsc]
have := pow_inj_right hr e1
omega
have hlog : Real.log (1 + s) < Real.log (1 + r) :=
Real.log_lt_log (by linarith) (by linarith)
have hc : Real.cosh (Real.log (1 + s)) < Real.cosh (Real.log (1 + r)) :=
cosh_strictMono_on_nonneg (Real.log_nonneg (by linarith)) hlog
have e1 : Cost.Jcost (1 + s) = Real.cosh (Real.log (1 + s)) - 1 :=
Cost.GeometricRoot.jcost_eq_cosh_log_sub_one (by linarith)
have e2 : Cost.Jcost (1 + r) = Real.cosh (Real.log (1 + r)) - 1 :=
Cost.GeometricRoot.jcost_eq_cosh_log_sub_one (by linarith)
linarith [e1, e2, hc]
What this page does not claim
The uniform-ratio premise is not derived; it remains an assumption in this theorem. Cost minimization does not select the golden ratio; the theorem does not claim a variational route. The theorem does not derive the golden ratio from the cost function J alone, only from the two ladder premises.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Foundation/PhiClosureSelection.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What more basic principle would discharge the uniform-ratio premise itself?
- How does the φ ladder connect to the eight-tick recognition cycle and the forcing of three spatial dimensions?
- Does the structural selection of k = 2 extend to other composition laws beyond adjacent sums?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM ratio_eq_phi_of_uniform_adjacent_composition · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- **Direct forcing.** A positive scale sequence with a constant inter-level ratio `r > 1` (uniform scaling: one ratio, no free parameters) satisfying the adjacent additive recurrence (each level composes its two neighbours: binary posting) has ratio `φ`. Closure is not assumed; the golden equation falls out of the two premises algebraically. -/ theorem ratio_eq_phi_of_uniform_adjacent_composition {s : ℕ → ℝ} {r : ℝ} (h0 : 0 < s 0) (hr : 1 < r) (hunif : ∀ n, s (n + 1) = r * s n) (hadj : ∀ n, s (n + 2) = s (n + 1) + s n) : r = phi := by have h1 : s 1 = r * s 0 := hunif 0 have h2u : s 2 = r * s 1 := hunif 1 have h2a : s 2 = s 1 + s 0 := hadj 0 rw [h1] at h2a h2u -- r * (r * s 0) = r * s 0 + s 0 have hs0 : s 0 ≠ 0 := ne_of_gt h0 have hfact : s 0 * (r ^ 2 - r - 1) = 0 := by nlinarith [h2u, h2a] rcases mul_eq_zero.mp hfact with h | h · exact absurd h hs0 · have hsq : 1 + r = r ^ 2 := by nlinarith [h] exact PhiForcingDerived.phi_forcing_complete r (by linarith) (by linarith) hsqA positive scale sequence with a constant inter-level ratio r > 1 satisfying the adjacent additive recurrence s(n+2) = s(n+1) + s(n) has r = φ. ratio_eq_phi_of_uniform_adjacent_composition · IndisputableMonolith/Foundation/PhiClosureSelection.leanTHEOREM high_closure_orphan · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- **Orphan theorem.** If the ladder closes at level `k ≥ 3` (`1 + r = r^k`), then `r²` is not the composition of any two rungs: it is an orphan scale, postable but never produced by composing ledger events. -/ theorem high_closure_orphan {r : ℝ} {k : ℕ} (hr : 1 < r) (hk : 3 ≤ k) (hclose : 1 + r = r ^ k) (a b : ℕ) : r ^ a + r ^ b ≠ r ^ 2 := by intro hab rcases rung_two_sum_cases hr hab with ⟨_, _, h2⟩ | ⟨_, _, h12⟩ | ⟨_, _, h12⟩ | ⟨_, _, hr2⟩ · -- r² = 2, so r³ = 2r ≤ r^k, giving 1 + r ≥ 2r, i.e. 1 ≥ r. have hk3 : r ^ 3 ≤ r ^ k := pow_le_pow_of_le (le_of_lt hr) hk have hr3 : r ^ 3 = 2 * r := by calc r ^ 3 = r * r ^ 2 := by ring _ = r * 2 := by rw [h2] _ = 2 * r := by ring linarith [hk3, hr3, hclose, hr] · -- 1 + r = r² and 1 + r = r^k force k = 2. have hkk : r ^ k = r ^ 2 := by rw [← h12, hclose] have := pow_inj_right hr hkk omega · have hkk : r ^ k = r ^ 2 := by rw [← h12, hclose] have := pow_inj_right hr hkk omega · -- r = 2: closure gives 3 = 2^k ≥ 8. have hk3 : r ^ 3 ≤ r ^ k := pow_le_pow_of_le (le_of_lt hr) hk rw [hr2] at hk3 hclose norm_num at hk3 hclose linarith [hk3, hclose]If 1 + r = r^k with k ≥ 3, then no pair of rungs composes to r². high_closure_orphan · IndisputableMonolith/Foundation/PhiClosureSelection.leanTHEOREM closure_level_two_of_rung_two_composed · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- **Selection theorem.** Among adjacent-closed ladders (`1 + r = r^k`, `k ≥ 2`), the ones in which the second rung is a composition of two rungs are exactly the `k = 2` ladders, and then `r = φ`. The selecting premise is generation completeness (no orphan scales), not minimality. -/ theorem closure_level_two_of_rung_two_composed {r : ℝ} {k : ℕ} (hr : 1 < r) (hk : 2 ≤ k) (hclose : 1 + r = r ^ k) (a b : ℕ) (hab : r ^ a + r ^ b = r ^ 2) : k = 2 ∧ r = phi := by rcases rung_two_sum_cases hr hab with ⟨_, _, h2⟩ | ⟨_, _, h12⟩ | ⟨_, _, h12⟩ | ⟨_, _, hr2⟩ · -- r² = 2: exclude both k = 2 and k ≥ 3. rcases (le_iff_eq_or_lt.mp hk) with hkk | hkk · -- k = 2: closure gives 1 + r = 2, i.e. r = 1. subst hkk exfalso linarith [hclose, h2, hr] · -- k ≥ 3: r³ = 2r ≤ r^k gives 1 ≥ r. have hk3 : r ^ 3 ≤ r ^ k := pow_le_pow_of_le (le_of_lt hr) hkk have hr3 : r ^ 3 = 2 * r := by calc r ^ 3 = r * r ^ 2 := by ring _ = r * 2 := by rw [h2] _ = 2 * r := by ring exfalso linarith [hk3, hr3, hclose, hr] · -- 1 + r = r²: closure gives r^k = r², so k = 2; then r = φ. have hkk : r ^ k = r ^ 2 := by rw [← h12, hclose] have hk2 := pow_inj_right hr hkk exact ⟨hk2, PhiForcingDerived.phi_forcing_complete r (by linarith) (by linarith) h12⟩ · have hkk : r ^ k = r ^ 2 := by rw [← h12, hclose] have hk2 := pow_inj_right hr hkk exact ⟨hk2, PhiForcingDerived.phi_forcing_complete r (by linarith) (by linarith) h12⟩ · -- r = 2: exclude both k = 2 and k ≥ 3. rcases (le_iff_eq_or_lt.mp hk) with hkk | hkk · subst hkk rw [hr2] at hclose norm_num at hclose · have hk3 : r ^ 3 ≤ r ^ k := pow_le_pow_of_le (le_of_lt hr) hkk rw [hr2] at hk3 hclose norm_num at hk3 hclose linarith [hk3, hclose]Among adjacent-closed ladders (1 + r = r^k, k ≥ 2), requiring r² to be a composition of two rungs forces k = 2 and r = φ. closure_level_two_of_rung_two_composed · IndisputableMonolith/Foundation/PhiClosureSelection.leanTHEOREM closure_cost_strictly_decreasing · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- **Route-kill measurement.** The per-closure cost `J(1 + r)` is strictly decreasing as the closure level rises: for any two closure ladders at consecutive levels, the higher-level ladder has the cheaper closure. Cost-minimization therefore does not select `k = 2`; it selects nothing finite. This kills the sub-route "the J-cost excess selects the closure level by minimization." -/ theorem closure_cost_strictly_decreasing {r s : ℝ} {k : ℕ} (hr : 1 < r) (hrc : 1 + r = r ^ (k + 2)) (hs : 1 < s) (hsc : 1 + s = s ^ (k + 3)) : Cost.Jcost (1 + s) < Cost.Jcost (1 + r) := by have hsr : s < r := by by_contra h push_neg at h rcases lt_or_eq_of_le h with hlt | heq · -- r < s: strict monotonicity of the closure polynomial gives -- f_{k+3}(r) < f_{k+3}(s) = 0, but f_{k+3}(r) = r² - 1 > 0. have h1 : r ^ (k + 3) - r - 1 < s ^ (k + 3) - s - 1 := closurePoly_strictMono (le_of_lt hr) hlt (by omega) have hfs : s ^ (k + 3) - s - 1 = 0 := by have e : s ^ (k + 3) = 1 + s := by rw [← hsc] linarith have hfr : r ^ (k + 3) - r - 1 = r ^ 2 - 1 := by have e0 : k + 3 = (k + 2) + 1 := by omega have e : r ^ (k + 3) = r * r ^ (k + 2) := by rw [e0, pow_succ'] rw [e, ← hrc] ring nlinarith [h1, hfs, hfr, hr, mul_pos (sub_pos.mpr hr) (by linarith : (0 : ℝ) < r + 1)] · -- r = s: then r^{k+2} = r^{k+3}, impossible. rw [← heq] at hsc have e1 : r ^ (k + 2) = r ^ (k + 3) := by rw [← hrc, ← hsc] have := pow_inj_right hr e1 omega have hlog : Real.log (1 + s) < Real.log (1 + r) := Real.log_lt_log (by linarith) (by linarith) have hc : Real.cosh (Real.log (1 + s)) < Real.cosh (Real.log (1 + r)) := cosh_strictMono_on_nonneg (Real.log_nonneg (by linarith)) hlog have e1 : Cost.Jcost (1 + s) = Real.cosh (Real.log (1 + s)) - 1 := Cost.GeometricRoot.jcost_eq_cosh_log_sub_one (by linarith) have e2 : Cost.Jcost (1 + r) = Real.cosh (Real.log (1 + r)) - 1 := Cost.GeometricRoot.jcost_eq_cosh_log_sub_one (by linarith) linarith [e1, e2, hc]The per-closure cost J(1 + r) is strictly decreasing in the closure level k. closure_cost_strictly_decreasing · IndisputableMonolith/Foundation/PhiClosureSelection.lean