Foundation Recurrence Bridge

/-- **The recurrence bridge.** A ratio floor ρ above the plastic constant
(ρ³ > ρ + 1), together with adjacent closure (the composition of rungs n and
n+1 is always a rung), forces the adjacent recurrence: the composition
cannot reach rung n+3, so it is rung n+2. -/
theorem recurrence_of_floor_above_plastic (hpos : ∀ n, 0 < s n)
    {ρ : ℝ} (hρ : 1 < ρ) (hρ3 : ρ + 1 < ρ ^ 3)
    (hfloor : ∀ n, ρ * s n ≤ s (n + 1))
    (hclosure : ∀ n, ∃ m, m ≥ n + 2 ∧ s m = s n + s (n + 1)) :
    ∀ n, s (n + 2) = s (n + 1) + s n := by
  have hmono := monotone_of_floor hpos hρ hfloor
  have hρpos : 0 < ρ := by linarith
  intro n
  obtain ⟨m, hm, hsm⟩ := hclosure n
  have hmle : m ≤ n + 2 := by
    by_contra h
    push_neg at h
    have hm3 : n + 3 ≤ m := by omega
    have hs3 : s (n + 3) ≤ s m := hmono hm3
    have hf2 : ρ ^ 2 * s (n + 1) ≤ s (n + 3) :=
      calc ρ ^ 2 * s (n + 1) = ρ * (ρ * s (n + 1)) := by ring
        _ ≤ ρ * s (n + 2) :=
          mul_le_mul_of_nonneg_left (hfloor (n + 1)) (le_of_lt hρpos)
        _ ≤ s (n + 3) := hfloor (n + 2)
    have hsn : s n ≤ s (n + 1) / ρ := by
      rw [le_div_iff₀ hρpos, mul_comm]
      exact hfloor n
    have hsp : 0 < s (n + 1) := hpos (n + 1)
    have h1 : ρ ^ 2 * s (n + 1) ≤ s n + s (n + 1) := by
      linarith [hs3, hf2, hsm]
    have h2 : s n + s (n + 1) ≤ s (n + 1) / ρ + s (n + 1) := by
      linarith [hsn]
    have h3 : ρ ^ 2 * s (n + 1) ≤ (1 / ρ + 1) * s (n + 1) := by
      have e : s (n + 1) / ρ + s (n + 1) = (1 / ρ + 1) * s (n + 1) := by ring
      rw [e] at h2
      exact le_trans h1 h2
    have h4 : ρ ^ 2 ≤ 1 / ρ + 1 := le_of_mul_le_mul_right h3 hsp
    have h5 : ρ ^ 2 * ρ ≤ (1 / ρ + 1) * ρ :=
      mul_le_mul_of_nonneg_right h4 (le_of_lt hρpos)
    have h6 : (1 / ρ + 1) * ρ = 1 + ρ := by field_simp [hρpos.ne']
    have h7 : ρ ^ 2 * ρ = ρ ^ 3 := by ring
    rw [h7] at h5
    rw [h6] at h5
    linarith [h5, hρ3]
  have hmeq : m = n + 2 := by omega
  subst hmeq
  linarith [hsm]

/-- The threshold is exact: at ρ = plastic (ρ³ = ρ + 1, the non-strict
boundary), the plastic ladder satisfies the ratio floor with equality,
satisfies adjacent closure (its composition lands at rung n+3, skipping
rung n+2), and violates the adjacent recurrence. The strict inequality
ρ³ > ρ + 1 in the bridge theorem cannot be relaxed to ≥. -/
theorem plastic_sharpness :
    ∃ (s : ℕ → ℝ) (ρ : ℝ), (∀ n, 0 < s n) ∧ 1 < ρ ∧ ρ ^ 3 = ρ + 1 ∧
      (∀ n, ρ * s n ≤ s (n + 1)) ∧
      (∀ n, ∃ m, m ≥ n + 2 ∧ s m = s n + s (n + 1)) ∧
      ¬ (∀ n, s (n + 2) = s (n + 1) + s n) := by
  obtain ⟨r, hr1, hr3⟩ := PhiClosureSelection.plastic_ladder_exists
  have hr0 : 0 < r := by linarith
  refine ⟨fun n => r ^ n, r, (fun n => pow_pos hr0 n), hr1, by linarith [hr3],
    ?_, ?_, ?_⟩
  · intro n
    exact le_of_eq (pow_succ' r n).symm
  · intro n
    refine ⟨n + 3, by omega, ?_⟩
    show r ^ (n + 3) = r ^ n + r ^ (n + 1)
    rw [pow_add, mul_comm, ← hr3, pow_succ']
    ring
  · intro hall
    have h0 := hall 0
    dsimp only at h0
    norm_num at h0
    have e : r ^ 3 = 2 * r + 1 := by
      calc r ^ 3 = r ^ 2 * r := by ring
        _ = (r + 1) * r := by rw [h0]
        _ = r ^ 2 + r := by ring
        _ = 2 * r + 1 := by rw [h0]; ring
    linarith [e, hr3, hr1]

/-- The countermodel, packaged: strict monotonicity, adjacent closure, full
generation, ledger additivity (composition is addition), and an absolute
minimum step of 1 all hold for the integer ladder, yet the adjacent
recurrence fails and no ratio floor above 1 exists. Closure + generation +
absolute tick (the banked tick's form) do not force the recurrence. -/
theorem closure_generation_tick_insufficient :
    ∃ s : ℕ → ℝ, StrictMono s ∧
      (∀ n, ∃ m, m ≥ n + 2 ∧ s m = s n + s (n + 1)) ∧
      (∀ n, n ≥ 2 → ∃ a b, a ≤ b ∧ b < n ∧ s n = s a + s b) ∧
      (∀ n, s (n + 1) - s n = 1) ∧
      ¬ (∀ n, s (n + 2) = s (n + 1) + s n) ∧
      (∀ ρ : ℝ, 1 < ρ → ∃ n, s (n + 1) < ρ * s n) :=
  ⟨intLadder, intLadder_strictMono, intLadder_adjacent_closure,
    intLadder_generation, intLadder_tick, intLadder_recurrence_fails,
    intLadder_no_ratio_floor⟩

/-- **T6 assembly, bridge form.** A ratio floor above the plastic constant
plus adjacent closure forces the recurrence (this module), hence the
asymptotic inter-level ratio is φ (PhiForcingUnconditional). No geometric
ladder, no uniform ratio, no minimality posture. -/
theorem phi_of_floor_above_plastic (hpos : ∀ n, 0 < s n)
    {ρ : ℝ} (hρ : 1 < ρ) (hρ3 : ρ + 1 < ρ ^ 3)
    (hfloor : ∀ n, ρ * s n ≤ s (n + 1))
    (hclosure : ∀ n, ∃ m, m ≥ n + 2 ∧ s m = s n + s (n + 1)) :
    Tendsto (fun n => s (n + 1) / s n) atTop (nhds phi) :=
  ratio_tendsto_phi hpos
    (recurrence_of_floor_above_plastic hpos hρ hρ3 hfloor hclosure)