Foundation Phi Closure Selection Closure Cost Strictly Decreasing

/-- **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 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

/-- **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]

/-- **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