IndisputableMonolith.Cosmology.RecognitionEquilibrium

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cosmology.RefineTrigger
   4
   5/-!
   6# Recognition equilibrium: the forward dynamics descends to the J-cost ground state
   7
   8This module discharges, in Lean, the central convergence facts of the Phase-7 forward
   9dynamics (`scripts/cosmogenesis/forward_dynamics.py`). That dynamics evolves a field of
  10recognition levels `x : Fin n → ℝ` on a coupling graph by posting, each tick, one forced
  11recognition event: it resolves a coupled pair `(i, j)` by sending both endpoints to their
  12mean (the sigma = 0, J-minimal move; no relaxation rate, no knob). The Python checks these
  13facts numerically; here they are theorems.
  14
  15* `pairResolve_levelSum` : a resolution conserves the level sum (sigma is conserved).
  16* `variance_pairResolve` : a resolution lowers the spread by **exactly** `(x i - x j)^2 / 2`.
  17  So the level variance is a Lyapunov function with an exact, law-given decrement; the
  18  dynamics is a strict descent until every coupled pair is equal. (Total edge demand is
  19  *not* monotone and is not claimed to be; the variance is.)
  20* `variance_nonincreasing` : the immediate corollary (the spread never grows).
  21* `jcost_nonneg`, `jcost_eq_zero_iff` : the recognition cost is nonnegative, and zero only
  22  at ratio one.
  23* `totalCost_nonneg`, `totalCost_eq_zero_iff` : the total recognition cost over the
  24  coupling graph is nonnegative and vanishes **iff** the field is constant on every edge
  25  (consensus). So the recognition ground state is exactly the consensus configuration the
  26  descent converges to.
  27* `conjugateBirth_chargeSum`, `manyBirths_chargeSum` : the driven (open-system) extension
  28  (`scripts/cosmogenesis/expanding_dynamics.py`) grows the ladder by a conjugate pair
  29  `(+u, -u)` born at the horizon each cadence cycle. These show that a birth, and any number
  30  of births, conserves the charge sum, so sigma = 0 holds through the whole driven evolution:
  31  recognition resolutions conserve it by `pairResolve_levelSum`, births by these. Closed-
  32  system descent (above) provably relaxes to consensus; the conserved-sigma birth is the
  33  forced open input that keeps non-homogenizing structure alive.
  34
  35`Jcost` and `jcost_pos` are reused from `RefineTrigger` (T-3); `phi` and `one_lt_phi` from
  36`Constants`. The ratio of two regions is the forced `phi ^ (x i - x j)`. Zero `sorry`,
  37zero new `axiom`; the only axioms are the three standard ones.
  38-/
  39
  40namespace IndisputableMonolith
  41namespace Cosmology
  42namespace RecognitionEquilibrium
  43
  44open scoped BigOperators
  45open IndisputableMonolith.Cosmology.RefineTrigger
  46
  47/-! ## §1. The forced pair resolution and the conserved sum -/
  48
  49/-- The forced recognition resolution of one coupled pair: send both endpoints to their
  50mean. This is the sigma = 0, J-minimal move the forward dynamics posts each tick. -/
  51noncomputable def pairResolve {n : ℕ} (x : Fin n → ℝ) (i j : Fin n) : Fin n → ℝ :=
  52  fun k => if k = i ∨ k = j then (x i + x j) / 2 else x k
  53
  54@[simp] lemma pairResolve_at_i {n : ℕ} (x : Fin n → ℝ) (i j : Fin n) :
  55    pairResolve x i j i = (x i + x j) / 2 := by
  56  unfold pairResolve; rw [if_pos (Or.inl rfl)]
  57
  58@[simp] lemma pairResolve_at_j {n : ℕ} (x : Fin n → ℝ) (i j : Fin n) :
  59    pairResolve x i j j = (x i + x j) / 2 := by
  60  unfold pairResolve; rw [if_pos (Or.inr rfl)]
  61
  62lemma pairResolve_other {n : ℕ} (x : Fin n → ℝ) {i j k : Fin n}
  63    (hi : k ≠ i) (hj : k ≠ j) : pairResolve x i j k = x k := by
  64  unfold pairResolve
  65  rw [if_neg (by rintro (h | h); exact hi h; exact hj h)]
  66
  67/-- The sum of all levels (the conserved sigma quantity). -/
  68noncomputable def levelSum {n : ℕ} (x : Fin n → ℝ) : ℝ := ∑ k, x k
  69
  70/-- A helper: split `∑` over `univ` as `∑` over the pair `{i, j}` plus the rest, and prove
  71two configurations that agree off `{i, j}` have equal `∑` there. -/
  72private lemma sum_split_pair {n : ℕ} (f g : Fin n → ℝ) {i j : Fin n} (hij : i ≠ j)
  73    (hagree : ∀ k, k ≠ i → k ≠ j → f k = g k) :
  74    (∑ k, f k) - (∑ k, g k) = (f i + f j) - (g i + g j) := by
  75  have hsub : ({i, j} : Finset (Fin n)) ⊆ Finset.univ := Finset.subset_univ _
  76  have hf : (∑ k, f k) = (∑ k ∈ Finset.univ \ {i, j}, f k) + (f i + f j) := by
  77    rw [← Finset.sum_sdiff hsub, Finset.sum_pair hij]
  78  have hg : (∑ k, g k) = (∑ k ∈ Finset.univ \ {i, j}, g k) + (g i + g j) := by
  79    rw [← Finset.sum_sdiff hsub, Finset.sum_pair hij]
  80  have hrest : (∑ k ∈ Finset.univ \ {i, j}, f k) = (∑ k ∈ Finset.univ \ {i, j}, g k) := by
  81    apply Finset.sum_congr rfl
  82    intro k hk
  83    rw [Finset.mem_sdiff] at hk
  84    have hki : k ≠ i := by rintro rfl; exact hk.2 (by simp)
  85    have hkj : k ≠ j := by rintro rfl; exact hk.2 (by simp)
  86    exact hagree k hki hkj
  87  rw [hf, hg, hrest]; ring
  88
  89/-- **Sigma is conserved.** Resolving a pair leaves the total level unchanged. -/
  90theorem pairResolve_levelSum {n : ℕ} (x : Fin n → ℝ) {i j : Fin n} (h : i ≠ j) :
  91    levelSum (pairResolve x i j) = levelSum x := by
  92  unfold levelSum
  93  have hagree : ∀ k, k ≠ i → k ≠ j → pairResolve x i j k = x k :=
  94    fun k hi hj => pairResolve_other x hi hj
  95  have hsp := sum_split_pair (pairResolve x i j) x h hagree
  96  rw [pairResolve_at_i, pairResolve_at_j] at hsp
  97  -- hsp : (∑ resolved) - (∑ x) = ((xi+xj)/2 + (xi+xj)/2) - (x i + x j)
  98  have hzero : ((x i + x j) / 2 + (x i + x j) / 2) - (x i + x j) = 0 := by ring
  99  rw [hzero] at hsp
 100  linarith [hsp]
 101
 102/-! ## §2. The variance is a Lyapunov function with an exact, law-given decrement -/
 103
 104/-- Spread of the level field around a reference `c`. -/
 105noncomputable def varAround {n : ℕ} (x : Fin n → ℝ) (c : ℝ) : ℝ := ∑ k, (x k - c) ^ 2
 106
 107/-- **The exact variance drop (around any reference).** Resolving a pair lowers the spread
 108by exactly `(x i - x j)^2 / 2`, independent of the reference point. -/
 109theorem varAround_pairResolve {n : ℕ} (x : Fin n → ℝ) {i j : Fin n} (h : i ≠ j) (c : ℝ) :
 110    varAround (pairResolve x i j) c = varAround x c - (x i - x j) ^ 2 / 2 := by
 111  unfold varAround
 112  have hagree : ∀ k, k ≠ i → k ≠ j →
 113      (pairResolve x i j k - c) ^ 2 = (x k - c) ^ 2 :=
 114    fun k hi hj => by rw [pairResolve_other x hi hj]
 115  have hsplit := sum_split_pair (fun k => (pairResolve x i j k - c) ^ 2)
 116    (fun k => (x k - c) ^ 2) h hagree
 117  simp only [pairResolve_at_i, pairResolve_at_j] at hsplit
 118  -- hsplit : (∑ resolved sq) - (∑ x sq) = (2 * ((xi+xj)/2 - c)^2) - ((xi-c)^2 + (xj-c)^2)
 119  have hid : (((x i + x j) / 2 - c) ^ 2 + ((x i + x j) / 2 - c) ^ 2)
 120      - ((x i - c) ^ 2 + (x j - c) ^ 2) = -((x i - x j) ^ 2 / 2) := by ring
 121  rw [hid] at hsplit
 122  linarith [hsplit]
 123
 124/-- The mean level. -/
 125noncomputable def meanLevel {n : ℕ} (x : Fin n → ℝ) : ℝ := levelSum x / (n : ℝ)
 126
 127/-- The level variance (spread about the mean): the Lyapunov function of the descent. -/
 128noncomputable def variance {n : ℕ} (x : Fin n → ℝ) : ℝ := varAround x (meanLevel x)
 129
 130theorem meanLevel_pairResolve {n : ℕ} (x : Fin n → ℝ) {i j : Fin n} (h : i ≠ j) :
 131    meanLevel (pairResolve x i j) = meanLevel x := by
 132  unfold meanLevel; rw [pairResolve_levelSum x h]
 133
 134/-- **The variance Lyapunov law.** Each forced resolution lowers the level variance by
 135exactly `(x i - x j)^2 / 2`. The decrement is the recognition gap that was resolved, so
 136the descent is strict until every coupled pair is equal. -/
 137theorem variance_pairResolve {n : ℕ} (x : Fin n → ℝ) {i j : Fin n} (h : i ≠ j) :
 138    variance (pairResolve x i j) = variance x - (x i - x j) ^ 2 / 2 := by
 139  unfold variance
 140  rw [meanLevel_pairResolve x h, varAround_pairResolve x h (meanLevel x)]
 141
 142/-- The spread never grows under a forced resolution. -/
 143theorem variance_nonincreasing {n : ℕ} (x : Fin n → ℝ) {i j : Fin n} (h : i ≠ j) :
 144    variance (pairResolve x i j) ≤ variance x := by
 145  rw [variance_pairResolve x h]
 146  nlinarith [sq_nonneg (x i - x j)]
 147
 148/-! ## §3. The recognition cost ground state is exactly consensus -/
 149
 150/-- The recognition cost is nonnegative. -/
 151theorem jcost_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ Jcost x := by
 152  rcases eq_or_ne x 1 with h | h
 153  · subst h; norm_num [Jcost]
 154  · exact le_of_lt (RefineTrigger.jcost_pos hx h)
 155
 156/-- The recognition cost vanishes exactly at ratio one. -/
 157theorem jcost_eq_zero_iff {x : ℝ} (hx : 0 < x) : Jcost x = 0 ↔ x = 1 := by
 158  constructor
 159  · intro h0
 160    by_contra hne
 161    have hp : 0 < Jcost x := RefineTrigger.jcost_pos hx hne
 162    rw [h0] at hp
 163    exact lt_irrefl 0 hp
 164  · intro h; subst h; norm_num [Jcost]
 165
 166/-- `phi ^ t = 1` exactly when `t = 0` (phi is positive and not one). -/
 167theorem phi_rpow_eq_one_iff (t : ℝ) : (Constants.phi : ℝ) ^ t = 1 ↔ t = 0 := by
 168  rw [Real.rpow_def_of_pos Constants.phi_pos,
 169      show (1 : ℝ) = Real.exp 0 from (Real.exp_zero).symm, Real.exp_eq_exp]
 170  have hlog : Real.log Constants.phi ≠ 0 := ne_of_gt (Real.log_pos Constants.one_lt_phi)
 171  constructor
 172  · intro h
 173    rcases mul_eq_zero.mp h with h' | h'
 174    · exact absurd h' hlog
 175    · exact h'
 176  · intro h; rw [h, mul_zero]
 177
 178/-- Two regions carry no forced distinction exactly when their levels are equal. -/
 179theorem cost_phi_eq_zero_iff (a b : ℝ) :
 180    Jcost ((Constants.phi : ℝ) ^ (a - b)) = 0 ↔ a = b := by
 181  rw [jcost_eq_zero_iff (Real.rpow_pos_of_pos Constants.phi_pos _),
 182      phi_rpow_eq_one_iff, sub_eq_zero]
 183
 184/-- Total recognition cost over the coupling graph: the sum of the forced demands. -/
 185noncomputable def totalCost {n : ℕ} (x : Fin n → ℝ) (edges : Finset (Fin n × Fin n)) : ℝ :=
 186  ∑ e ∈ edges, Jcost ((Constants.phi : ℝ) ^ (x e.1 - x e.2))
 187
 188/-- The total recognition cost is nonnegative. -/
 189theorem totalCost_nonneg {n : ℕ} (x : Fin n → ℝ) (edges : Finset (Fin n × Fin n)) :
 190    0 ≤ totalCost x edges :=
 191  Finset.sum_nonneg (fun _ _ => jcost_nonneg (Real.rpow_pos_of_pos Constants.phi_pos _))
 192
 193/-- **The recognition ground state is consensus.** The total recognition cost vanishes if
 194and only if the level field is constant on every coupled pair. So the zero-cost
 195configuration the descent converges to is exactly graph consensus. -/
 196theorem totalCost_eq_zero_iff {n : ℕ} (x : Fin n → ℝ) (edges : Finset (Fin n × Fin n)) :
 197    totalCost x edges = 0 ↔ ∀ e ∈ edges, x e.1 = x e.2 := by
 198  rw [totalCost, Finset.sum_eq_zero_iff_of_nonneg
 199        (fun _ _ => jcost_nonneg (Real.rpow_pos_of_pos Constants.phi_pos _))]
 200  constructor
 201  · intro h e he; exact (cost_phi_eq_zero_iff _ _).mp (h e he)
 202  · intro h e he; exact (cost_phi_eq_zero_iff _ _).mpr (h e he)
 203
 204/-! ## §4. The bundled statement -/
 205
 206/-- The recognition-equilibrium package: the forced forward dynamics conserves sigma,
 207descends the level variance by an exact law-given decrement (so the spread is a Lyapunov
 208function and the descent is strict until consensus), and its zero-cost ground state is
 209exactly the consensus configuration. -/
 210structure Equilibrium {n : ℕ} (x : Fin n → ℝ)
 211    (edges : Finset (Fin n × Fin n)) : Prop where
 212  sigma_conserved : ∀ i j : Fin n, i ≠ j → levelSum (pairResolve x i j) = levelSum x
 213  variance_drop : ∀ i j : Fin n, i ≠ j →
 214    variance (pairResolve x i j) = variance x - (x i - x j) ^ 2 / 2
 215  variance_nonincreasing : ∀ i j : Fin n, i ≠ j → variance (pairResolve x i j) ≤ variance x
 216  cost_nonneg : 0 ≤ totalCost x edges
 217  ground_state_iff_consensus : totalCost x edges = 0 ↔ ∀ e ∈ edges, x e.1 = x e.2
 218
 219/-- **Recognition equilibrium holds for every level field and coupling graph.** -/
 220theorem recognitionEquilibrium {n : ℕ} (x : Fin n → ℝ)
 221    (edges : Finset (Fin n × Fin n)) : Equilibrium x edges where
 222  sigma_conserved := fun _ _ h => pairResolve_levelSum x h
 223  variance_drop := fun _ _ h => variance_pairResolve x h
 224  variance_nonincreasing := fun _ _ h => variance_nonincreasing x h
 225  cost_nonneg := totalCost_nonneg x edges
 226  ground_state_iff_consensus := totalCost_eq_zero_iff x edges
 227
 228/-! ## §5. Expansion: a conjugate birth at the horizon conserves sigma
 229
 230The driven (open-system) dynamics (`scripts/cosmogenesis/expanding_dynamics.py`) grows the
 231phi-ladder: each cadence cycle a conjugate pair `(+u, -u)` is born at the two frontiers, the
 232double-entry creation of a distinction at the horizon. The closed descent of §1-§4 provably
 233relaxes any connected world to consensus (the variance is a strict Lyapunov function), so a
 234forced open input is needed to keep structure alive; the conjugate birth is that input.
 235
 236Recognition resolutions conserve the level sum by `pairResolve_levelSum`. Here we show the
 237birth conserves it too, so sigma = 0 holds through the whole driven evolution, resolve and
 238grow alike. The charge field is a `List ℝ` here because a birth changes the number of
 239regions (the ladder grows). -/
 240
 241/-- **A conjugate birth conserves sigma.** Inserting `+u` at the fine frontier and `-u` at
 242the coarse frontier leaves the total charge unchanged: the net of the born pair is zero. -/
 243theorem conjugateBirth_chargeSum (u : ℝ) (xs : List ℝ) :
 244    ((u :: xs) ++ [-u]).sum = xs.sum := by
 245  simp only [List.sum_append, List.sum_cons, List.sum_nil]
 246  ring
 247
 248/-- **Any number of conjugate births conserves sigma.** After `k` cadence cycles of
 249expansion the ladder carries `k` extra `+u` charges at the fine frontier and `k` extra `-u`
 250charges at the coarse frontier; the total charge is still the initial total. So sigma = 0 is
 251preserved through the entire driven run. -/
 252theorem manyBirths_chargeSum (k : ℕ) (u : ℝ) (xs : List ℝ) :
 253    (List.replicate k u ++ xs ++ List.replicate k (-u)).sum = xs.sum := by
 254  simp only [List.sum_append, List.sum_replicate, nsmul_eq_mul]
 255  ring
 256
 257end RecognitionEquilibrium
 258end Cosmology
 259end IndisputableMonolith
 260