Encyclopedia Foundation Foundation Phi Closure Selection Closure Level Two Of Rung Two Composed
ARTICLE 5 claims 5 theorems
Foundation Phi Closure Selection Closure Level Two Of Rung Two Composed
A single structural condition, that every posted scale must be earned by composing smaller ones, forces the golden ratio and rules out all other closure levels.
The selection theorem
The golden ratio φ, about 1.618, is the unique positive number whose square equals itself plus one: φ² = φ + 1. This equation also describes a ladder of powers 1, φ, φ², φ³, ... where each rung is the sum of the two before it. The Recognition Science framework asks a sharper question: among all ladders whose rungs satisfy a closure relation of the form 1 + r = r^k, which one is actually generated by composition? The answer, proved in the framework's machine-checked library of formal theorems, is that only k = 2 survives.
The key premise is generation completeness, a structural condition rather than a preference for small numbers. The framework models recognition events as entries in a ledger, a discrete record of events, and a rung of the ladder is a scale at which events can be posted. The condition says every posted scale must be earned: it must be the composition, in the sense of addition, of two smaller rungs. The theorem closure_level_two_of_rung_two_composed proves that if the second rung r² is such a composition, then the closure level k must be 2 and r must be φ. No other closure level, such as k = 3 with the plastic constant, can satisfy this requirement.
The theorem also proves a negative result about higher closures. If the ladder closes at level k ≥ 3, then r² is an orphan scale: it can be posted but never produced by composing two rungs. This is the precise sense in which higher closures fail generation completeness. The framework's library shows that the φ ladder, by contrast, is fully generated: every rung beyond the first two is the adjacent composition of the two preceding rungs, so no posted scale is orphaned.
The selection is structural, not variational. The framework's library also proves that the per-closure cost J(1 + r) strictly decreases as k rises, so cost minimization would select no finite level at all. The k = 3 ladder exists and is strictly cheaper than the φ ladder, yet it is rejected because it leaves orphans. This is why the theorem's force comes from composition structure, not from any minimality posture.
What the theorem does not claim is equally precise. It assumes the ladder form itself, a constant inter-level ratio r > 1, as a premise; discharging that scaling assumption is a separate problem. It does not prove that the golden ratio is the unique self-similar scaling in any broader sense, only within this composition-generated ladder family. And it does not derive the cost function J; that is a separate theorem in the framework's foundation.
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 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 phi_rung_composed · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- **Generation theorem.** On a ladder closed at level 2 (`1 + r = r²`),
every rung beyond the first two is the adjacent composition of the two
preceding rungs. No orphans: every posted scale is earned. -/
theorem phi_rung_composed {r : ℝ} (h : 1 + r = r ^ 2) (m : ℕ) (hm : 2 ≤ m) :
r ^ m = r ^ (m - 1) + r ^ (m - 2) := by
have e : r ^ m = r ^ (m - 2) * r ^ 2 := by
rw [← pow_add]
congr 1
omega
have e3 : r ^ (m - 2) * r = r ^ (m - 1) := by
rw [← pow_succ]
congr 1
omega
rw [e, ← h, mul_add, mul_one, e3]
ring
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]
THEOREM plastic_cheaper_than_phi · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- The concrete witness for the route-kill: the plastic ladder exists and
its closure is strictly cheaper than the φ closure. -/
theorem plastic_cheaper_than_phi :
∃ r : ℝ, 1 < r ∧ 1 + r = r ^ 3 ∧
Cost.Jcost (1 + r) < Cost.Jcost (1 + phi) := by
obtain ⟨r, hr, hrc⟩ := plastic_ladder_exists
refine ⟨r, hr, hrc, ?_⟩
have hphi2 : 1 + phi = phi ^ 2 := by linarith [phi_sq_eq]
have h := closure_cost_strictly_decreasing (k := 0) one_lt_phi
(by simpa using hphi2) hr (by simpa using hrc)
exact h
What this page does not claim
The theorem does not prove that the golden ratio is the unique self-similar scaling outside this composition-generated ladder family. The theorem does not derive the cost function J, which is a separate result in the framework's foundation. The theorem does not claim that cost minimization selects the closure level; the library proves the opposite.
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 scaling premise that the ladder form assumes?
- Does the generation completeness condition extend to ladders with non-uniform inter-level ratios?
- How does the orphan-scale argument generalize to closure relations with more than two rungs composing a scale?
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]if the second rung r² is such a composition, then the closure level k must be 2 and r must be φ closure_level_two_of_rung_two_composed · 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 the ladder closes at level k ≥ 3, then r² is an orphan scale high_closure_orphan · IndisputableMonolith/Foundation/PhiClosureSelection.leanTHEOREM phi_rung_composed · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- **Generation theorem.** On a ladder closed at level 2 (`1 + r = r²`), every rung beyond the first two is the adjacent composition of the two preceding rungs. No orphans: every posted scale is earned. -/ theorem phi_rung_composed {r : ℝ} (h : 1 + r = r ^ 2) (m : ℕ) (hm : 2 ≤ m) : r ^ m = r ^ (m - 1) + r ^ (m - 2) := by have e : r ^ m = r ^ (m - 2) * r ^ 2 := by rw [← pow_add] congr 1 omega have e3 : r ^ (m - 2) * r = r ^ (m - 1) := by rw [← pow_succ] congr 1 omega rw [e, ← h, mul_add, mul_one, e3] ringthe φ ladder is fully generated phi_rung_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) strictly decreases as k rises closure_cost_strictly_decreasing · IndisputableMonolith/Foundation/PhiClosureSelection.leanTHEOREM plastic_cheaper_than_phi · IndisputableMonolith/Foundation/PhiClosureSelection.lean
/-- The concrete witness for the route-kill: the plastic ladder exists and its closure is strictly cheaper than the φ closure. -/ theorem plastic_cheaper_than_phi : ∃ r : ℝ, 1 < r ∧ 1 + r = r ^ 3 ∧ Cost.Jcost (1 + r) < Cost.Jcost (1 + phi) := by obtain ⟨r, hr, hrc⟩ := plastic_ladder_exists refine ⟨r, hr, hrc, ?_⟩ have hphi2 : 1 + phi = phi ^ 2 := by linarith [phi_sq_eq] have h := closure_cost_strictly_decreasing (k := 0) one_lt_phi (by simpa using hphi2) hr (by simpa using hrc) exact hthe k = 3 ladder exists and is strictly cheaper than the φ ladder plastic_cheaper_than_phi · IndisputableMonolith/Foundation/PhiClosureSelection.lean