Encyclopedia Foundation Foundation Phi Closure Selection
ARTICLE 4 claims 4 theorems
Foundation Phi Closure Selection
When a scale ladder must be closed by composition, only the golden ratio ladder has no orphan rungs.
The closure selection
The golden ratio φ ≈ 1.618 is the positive solution of r² = r + 1. It appears throughout mathematics: in the regular pentagon, in the Fibonacci sequence, and as the limit of ratios of consecutive terms. The number also satisfies a family of related equations, r^k = r + 1 for k = 2, 3, 4, ..., each with a unique real root above 1. The k = 2 root is φ; the k = 3 root is the plastic constant ≈ 1.3247; higher k give further roots approaching 1.
In Recognition Science, the framework models a ledger (a discrete record of events) whose scales form a ladder: each level is r times the previous one, with a fixed ratio r > 1. The ladder is closed (every posted scale is earned by composing smaller scales) when it satisfies 1 + r = r^k for some integer k ≥ 2. The framework's library, a machine-checked collection of formal theorems, proves that if the second rung r² must itself be a composition of two rungs, then k = 2 and r = φ. The theorem closure_level_two_of_rung_two_composed shows that among all adjacent-closed ladders, the ones where r² is a sum of two rungs are exactly the k = 2 ladders. The selecting premise is generation completeness: no orphan scales.
The framework also proves a direct forcing result: a positive scale sequence with a constant ratio r > 1 satisfying the adjacent additive recurrence s_{n+2} = s_{n+1} + s_n must have r = φ. No closure hypothesis is needed; the recurrence and uniform ratio force the golden equation algebraically. On a φ ladder, every rung beyond the first two is the adjacent composition of the two preceding rungs, so no scale is orphaned. In contrast, for any k ≥ 3, the second rung r² cannot be written as a sum of two rungs: it is an orphan scale, postable but never produced by composition.
One tempting alternative, choosing k by minimizing a cost function, fails. The framework defines a recognition cost J(x) = (x + 1/x)/2 - 1. The theorem closure_cost_strictly_decreasing shows the per-closure cost J(1 + r) strictly decreases as k increases; the k = 3 plastic ladder exists and is strictly cheaper than the φ ladder. Cost minimization over closure levels selects nothing finite. The selection of k = 2 is therefore structural, not variational: it comes from the requirement that every posted scale be earned by composition.
What this means in plain language: if you insist that a scale ladder have no unearned rungs, the golden ratio is forced. The framework's library proves this from composition structure alone, without assuming closure or appealing to minimality. The uniform-ratio premise (one scaling ratio, no free parameters) remains a hypothesis; its own discharge is a separate open problem.
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 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_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 framework does not claim the uniform-ratio premise is itself derived from more basic principles. The framework does not claim cost minimization selects the golden ratio closure level. The framework does not claim the golden ratio appears in nature because of this selection alone.
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 structural condition, if any, discharges the uniform-ratio premise and forces the ladder form itself?
- How does the no-orphan requirement generalize to ladders with more than one base scale?
- What physical interpretation does the framework assign to an orphan scale, if one were observed?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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]Among all adjacent-closed ladders, the ones where r² is a sum of two rungs are exactly the k = 2 ladders. closure_level_two_of_rung_two_composed · IndisputableMonolith/Foundation/PhiClosureSelection.leanTHEOREM 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 ratio r > 1 satisfying the adjacent additive recurrence must have 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]For any k ≥ 3, the second rung r² cannot be written as a sum of two rungs. high_closure_orphan · 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) strictly decreases as k increases. closure_cost_strictly_decreasing · IndisputableMonolith/Foundation/PhiClosureSelection.lean