Encyclopedia Foundation Foundation Phi Closure Selection Plastic Cheaper Than Phi
ARTICLE 3 claims 3 theorems
Foundation Phi Closure Selection Plastic Cheaper Than Phi
A machine-checked theorem shows that minimizing a certain cost function would choose no finite scaling ladder, so the golden ratio must be selected by structure, not by economy.
Why cost alone picks no ladder
The golden ratio φ ≈ 1.618 solves the equation 1 + r = r². It is also the root of a more general family: for any whole number k ≥ 2, the equation 1 + r = r^k has a solution above 1. For k = 3 that solution is the plastic constant, about 1.3247. Each such solution describes a possible ladder of scales, where each rung is the previous rung multiplied by r, and where the first two rungs add to make the third.
Recognition Science, a framework that derives structure from a forced cost of recognition, asks which ladder nature should pick. One tempting answer is economy: choose the ladder whose closure costs least. The theorem plastic_cheaper_than_phi (a machine-checked result in the framework's library of formal theorems) closes that route. It proves that the plastic ladder, at k = 3, has a strictly lower per-closure cost than the golden ladder at k = 2. The cost keeps falling as k rises, approaching a limit of 1/4 without ever reaching it. Minimizing cost therefore selects no finite ladder at all.
The proof works by showing the cost function J(x) = (x + 1/x)/2 − 1 is strictly decreasing in the closure level. A supporting theorem, closure_cost_strictly_decreasing, establishes this for any two consecutive levels. The concrete witness then feeds the plastic constant into that inequality and compares it against φ.
What the theorem does not claim is that the plastic ladder is preferable. It is a negative result: it kills the idea that cost minimization explains why the golden ratio appears. The framework's positive selection of φ comes from a different theorem, closure_level_two_of_rung_two_composed, which shows that requiring every rung to be composed from earlier rungs forces k = 2. That is a structural completeness condition, not a variational one.
The consequence is a sharper picture of the framework's logic. The golden ratio is not the cheapest option, and the framework does not pretend otherwise. Its derivation rests on the demand that no posted scale be an orphan, a condition about generation, not about thrift.
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
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 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]
What this page does not claim
The plastic ladder is preferable to the golden ladder. Cost minimization selects any finite closure level. The theorem proves the plastic constant is the root of 1 + r = r³; that existence is a separate theorem.
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 remains assumed in all ladder derivations?
- Does the plastic constant appear anywhere else in the framework's derivations, or is it only a counterexample to cost minimization?
- How does the generation-completeness selection of k = 2 relate to the eight-tick cycle derived elsewhere in the framework?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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 hThe plastic ladder, at k = 3, has a strictly lower per-closure cost than the golden ladder at k = 2. plastic_cheaper_than_phi · 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 cost keeps falling as k rises, approaching a limit of 1/4 without ever reaching it. closure_cost_strictly_decreasing · 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]The framework's positive selection of φ comes from a different theorem, closure_level_two_of_rung_two_composed, which shows that requiring every rung to be composed from earlier rungs forces k = 2. closure_level_two_of_rung_two_composed · IndisputableMonolith/Foundation/PhiClosureSelection.lean