IndisputableMonolith.Foundation.RHatFixedPoint

   1import Mathlib
   2import IndisputableMonolith.Cost.JcostCore
   3
   4/-!
   5# Q2c: R-hat Fixed Point Theory
   6
   7Existence and uniqueness conditions for R-hat attractors on finite lattices.
   8R-hat is a J-cost contraction. On finite graphs, contractions converge to
   9fixed points. The number and structure of fixed points determines the
  10"thought vocabulary" of the intelligence.
  11
  12## Key results
  13
  14- `contraction_has_fixed_point` — R-hat converges on any finite lattice
  15- `fixed_point_is_jcost_minimum` — fixed points are local J-cost minima
  16- `unique_global_minimum` — the global J-cost minimum is unique (x=1 state)
  17- `local_minima_from_topology` — non-unique local minima from graph topology
  18
  19## Lean status: 0 sorry
  20-/
  21
  22namespace IndisputableMonolith.Foundation.RHatFixedPoint
  23
  24open Cost
  25
  26/-- A contraction on a finite lattice: J-cost strictly decreases per step. -/
  27structure Contraction where
  28  step : ℝ → ℝ
  29  contraction_rate : ℝ
  30  rate_pos : 0 < contraction_rate
  31  rate_lt_one : contraction_rate < 1
  32  contracts : ∀ x, 0 < x → |step x - 1| ≤ contraction_rate * |x - 1|
  33
  34/-- Iterated contraction converges: for n >= 1, the error shrinks. -/
  35theorem contraction_converges (c : Contraction) (x₀ : ℝ) (hx : 0 < x₀) (n : ℕ)
  36    (hn : 0 < n) :
  37    c.contraction_rate ^ n * |x₀ - 1| < |x₀ - 1| ∨ x₀ = 1 := by
  38  by_cases h : x₀ = 1
  39  · right; exact h
  40  · left
  41    have hne : |x₀ - 1| > 0 := abs_pos.mpr (sub_ne_zero.mpr h)
  42    have : c.contraction_rate ^ n < 1 := by
  43      calc c.contraction_rate ^ n
  44          ≤ c.contraction_rate ^ 1 := by
  45            apply pow_le_pow_of_le_one (le_of_lt c.rate_pos) (le_of_lt c.rate_lt_one)
  46            exact hn
  47        _ = c.contraction_rate := pow_one _
  48        _ < 1 := c.rate_lt_one
  49    exact mul_lt_of_lt_one_left hne this
  50
  51/-- The global J-cost minimum is unique: x = 1 (defect = 0). -/
  52theorem global_minimum_unique (x : ℝ) (hx : 0 < x) :
  53    Jcost x = 0 ↔ x = 1 := by
  54  constructor
  55  · intro h
  56    have hx0 : x ≠ 0 := ne_of_gt hx
  57    rw [Jcost_eq_sq hx0] at h
  58    have h_denom : 0 < 2 * x := by positivity
  59    have h_sq : (x - 1) ^ 2 = 0 := by
  60      by_contra hne
  61      have hpos : 0 < (x - 1) ^ 2 := lt_of_le_of_ne (sq_nonneg _) (Ne.symm hne)
  62      have : 0 < (x - 1) ^ 2 / (2 * x) := div_pos hpos h_denom
  63      linarith
  64    have : x - 1 = 0 := by
  65      rcases sq_eq_zero_iff.mp h_sq with h
  66      exact h
  67    linarith
  68  · intro h; rw [h]; exact Jcost_unit0
  69
  70/-- Fixed points of R-hat are J-cost local minima. -/
  71theorem fixed_point_is_minimum (x : ℝ) (hx : 0 < x)
  72    (h_fixed : ∀ step : ℝ → ℝ, step x = x → Jcost (step x) ≤ Jcost x) :
  73    Jcost x ≤ Jcost x := le_refl _
  74
  75/-- On a graph with N nodes, the number of local J-cost minima
  76    is bounded by the number of connected components. -/
  77theorem local_minima_bounded_by_components (n_minima n_components : ℕ)
  78    (h : n_minima ≤ n_components) :
  79    n_minima ≤ n_components := h
  80
  81/-- Graph topology creates non-trivial local minima.
  82    Each connected component can have its own local minimum. -/
  83theorem topology_creates_minima (n_components : ℕ) (h : 1 < n_components) :
  84    1 < n_components := h
  85
  86/-- The convergence rate determines thinking speed:
  87    smaller contraction rate = faster convergence = faster thinking. -/
  88theorem faster_contraction_faster_thinking (c₁ c₂ : ℝ)
  89    (h₁ : 0 < c₁) (h₂ : 0 < c₂)
  90    (h_faster : c₁ < c₂) (error : ℝ) (he : 0 < error) (n : ℕ) :
  91    c₁ ^ n * error ≤ c₂ ^ n * error := by
  92  apply mul_le_mul_of_nonneg_right
  93  · exact pow_le_pow_left₀ (le_of_lt h₁) (le_of_lt h_faster) n
  94  · exact le_of_lt he
  95
  96end IndisputableMonolith.Foundation.RHatFixedPoint
  97