IndisputableMonolith.Cosmology.RungCoarsen

   1import Mathlib
   2
   3/-!
   4# T-1: Rung-coarsening is sigma-exact and cost-exact (the "literal" theorem)
   5
   6This is the Lean statement of theorem T-1 of the scale-adaptive Cosmogenesis engine
   7(`plans/Cosmogenesis_North_Star_Reality_Simulation_Plan_20260602.html`,
   8`simulation/manifest.json` `build_spine.T1_coarsening_exact`). The Python side
   9(`scripts/cosmogenesis/rung_coarsen.py`) discharged it numerically (round-trip exact
  10on the voxel battery and the idle cell); this module discharges the statement itself.
  11
  12## The model
  13
  14A recognition cell at one phi-rung is its multiset of canonical recognition events
  15(`Multiset Event`); order is irrelevant, every conserved functional is a function of
  16the multiset. A block map `block : ℕ → ℕ` sends fine sites to coarse sites. Coarsening
  17one rung up partitions the events:
  18
  19* `internalOf` : both endpoints land in one block, absorbed into that block's summary;
  20* `crossOf` : the endpoints differ, promoted to coarse events between coarse sites
  21  with the same ratio (`coarseLedger = (crossOf).map (relabel block)`).
  22
  23A refinement record keeps exactly the original cross events and the per-block internal
  24events, and `refineCell` reassembles them. This mirrors `rung_coarsen.py`'s
  25`coarsen` / `refine` / `Refinement`.
  26
  27## The content of T-1
  28
  29* **round-trip is the identity** (`roundtrip_eq`): `refine (coarsen m) = m`, because the
  30  partition recombines to the original multiset (`Multiset.filter_add_not`). Coarsening
  31  loses nothing reality has determined; this is what earns the word "literal."
  32* **every conserved functional is preserved** (`conserved`): because the round-trip
  33  returns the identical multiset, ANY functional of the cell is unchanged. Instances:
  34  event count (`count_preserved`), total cost (`cost_preserved`), the log-ratio
  35  spectrum (`spectrum_preserved`), and net flow / sigma (`sigma_preserved`).
  36* **cost partitions exactly** (`cost_partition`): the coarse cross-block cost plus the
  37  sum of block-internal cost equals the fine cost, since relabeling preserves ratios
  38  and the events partition.
  39* **sigma is preserved** (`sigma_preserved`): the round-trip returns identical net flow
  40  at every site. (The structural sigma = 0 of double-entry is proved at the
  41  LedgerForcing layer, `Cosmology.FirstTick.cosmic_ledger_conserves`.)
  42* **idle cells carry nothing** (`idle_carries_nothing`): a cell with no internal events
  43  keeps an empty refinement, so refinement memory scales with recognition activity,
  44  not with the number of sites.
  45
  46## Status
  47
  48Theorem-backed by `coarseningExact` / `t1_coarsening_exact`. Cost is stated for an
  49arbitrary ratio weight `wr : ℝ → ℝ` (so it holds for the RS recognition cost J and any
  50other). Zero `sorry`, zero new `axiom`.
  51-/
  52
  53namespace IndisputableMonolith
  54namespace Cosmology
  55namespace RungCoarsen
  56
  57/-- A canonical recognition event: a directed posting `source → target` carrying a
  58positive ratio. The double-entry reciprocal is implicit (see `doubled`). -/
  59structure Event where
  60  source : ℕ
  61  target : ℕ
  62  ratio : ℝ
  63
  64/-- Both endpoints of an event land in the same coarse block. -/
  65def sameBlock (block : ℕ → ℕ) (e : Event) : Prop := block e.source = block e.target
  66
  67instance (block : ℕ → ℕ) : DecidablePred (sameBlock block) :=
  68  fun e => inferInstanceAs (Decidable (block e.source = block e.target))
  69
  70/-- The internal events: both endpoints in one block, absorbed into the block summary. -/
  71def internalOf (block : ℕ → ℕ) (m : Multiset Event) : Multiset Event :=
  72  m.filter (sameBlock block)
  73
  74/-- The cross-block events: endpoints in different blocks, promoted to the coarse cell. -/
  75def crossOf (block : ℕ → ℕ) (m : Multiset Event) : Multiset Event :=
  76  m.filter (fun e => ¬ sameBlock block e)
  77
  78/-- A cross-block event with its endpoints relabeled to their coarse sites. The ratio,
  79the recognition content, is carried unchanged. -/
  80def relabel (block : ℕ → ℕ) (e : Event) : Event :=
  81  { source := block e.source, target := block e.target, ratio := e.ratio }
  82
  83/-- The coarse cell's canonical events: the cross-block events relabeled to coarse
  84sites. This is the object you evolve at the coarser rung. -/
  85def coarseLedger (block : ℕ → ℕ) (m : Multiset Event) : Multiset Event :=
  86  (crossOf block m).map (relabel block)
  87
  88/-- Reassemble the fine cell from the refinement: the original cross events together
  89with the retained per-block internal events. -/
  90def refineCell (internal crossOrigin : Multiset Event) : Multiset Event :=
  91  crossOrigin + internal
  92
  93/-- Coarsen one rung, then refine one rung, using the refinement record. -/
  94def roundtrip (block : ℕ → ℕ) (m : Multiset Event) : Multiset Event :=
  95  refineCell (internalOf block m) (crossOf block m)
  96
  97/-! ## §1. The round-trip is the identity -/
  98
  99/-- The cross and internal parts recombine to the whole cell. -/
 100theorem cross_add_internal (block : ℕ → ℕ) (m : Multiset Event) :
 101    crossOf block m + internalOf block m = m := by
 102  unfold crossOf internalOf
 103  rw [add_comm]
 104  exact Multiset.filter_add_not (sameBlock block) m
 105
 106/-- **T-1 round-trip.** Coarsening then refining returns the cell unchanged. The coarse
 107representation is lossless: it carries everything reality has determined with zero loss. -/
 108theorem roundtrip_eq (block : ℕ → ℕ) (m : Multiset Event) :
 109    roundtrip block m = m := by
 110  unfold roundtrip refineCell
 111  exact cross_add_internal block m
 112
 113/-! ## §2. Every conserved functional is preserved -/
 114
 115/-- Because the round-trip returns the identical multiset, ANY functional of the cell
 116is preserved. Sigma, totals, cost, and spectrum are all instances of this. -/
 117theorem conserved {X : Type*} (F : Multiset Event → X) (block : ℕ → ℕ) (m : Multiset Event) :
 118    F (roundtrip block m) = F m :=
 119  congrArg F (roundtrip_eq block m)
 120
 121/-- Event count. -/
 122def count (m : Multiset Event) : ℕ := Multiset.card m
 123
 124/-- The log-ratio spectrum, the recognition content as an (unordered) multiset. -/
 125noncomputable def spectrum (m : Multiset Event) : Multiset ℝ := m.map (fun e => Real.log e.ratio)
 126
 127/-- Total recognition cost under a ratio weight `wr` (the doubled J-cost in the engine). -/
 128def cost (wr : ℝ → ℝ) (m : Multiset Event) : ℝ := (m.map (fun e => wr e.ratio)).sum
 129
 130theorem count_preserved (block : ℕ → ℕ) (m : Multiset Event) :
 131    count (roundtrip block m) = count m := conserved count block m
 132
 133theorem spectrum_preserved (block : ℕ → ℕ) (m : Multiset Event) :
 134    spectrum (roundtrip block m) = spectrum m := conserved spectrum block m
 135
 136theorem cost_preserved (wr : ℝ → ℝ) (block : ℕ → ℕ) (m : Multiset Event) :
 137    cost wr (roundtrip block m) = cost wr m := conserved (cost wr) block m
 138
 139/-! ## §3. Cost partitions exactly across the rung change -/
 140
 141theorem cost_add (wr : ℝ → ℝ) (a b : Multiset Event) :
 142    cost wr (a + b) = cost wr a + cost wr b := by
 143  unfold cost
 144  rw [Multiset.map_add, Multiset.sum_add]
 145
 146/-- Relabeling endpoints to coarse sites preserves the ratio, hence the cost. -/
 147theorem cost_coarse_eq_cross (wr : ℝ → ℝ) (block : ℕ → ℕ) (m : Multiset Event) :
 148    cost wr (coarseLedger block m) = cost wr (crossOf block m) := by
 149  unfold cost coarseLedger
 150  rw [Multiset.map_map]
 151  rfl
 152
 153/-- **Cost partition.** Coarse cross-block cost plus block-internal cost equals the fine
 154cost. Cost is split exactly across the rung change, with no leakage. -/
 155theorem cost_partition (wr : ℝ → ℝ) (block : ℕ → ℕ) (m : Multiset Event) :
 156    cost wr (coarseLedger block m) + cost wr (internalOf block m) = cost wr m := by
 157  rw [cost_coarse_eq_cross, ← cost_add, cross_add_internal]
 158
 159/-! ## §4. Sigma (net flow) is preserved by the round-trip -/
 160
 161/-- Net flow at site `a`: out-postings minus in-postings, the sigma the engine carries.
 162(The structural sigma = 0 of the double-entry ledger is proved at the LedgerForcing
 163layer, `Cosmology.FirstTick.cosmic_ledger_conserves`; here we show the round-trip
 164returns identical net flow, which is the T-1 conserved-quantity claim.) -/
 165def netFlow (m : Multiset Event) (a : ℕ) : ℤ :=
 166  ((m.filter (fun e => e.source = a)).card : ℤ) - ((m.filter (fun e => e.target = a)).card : ℤ)
 167
 168/-- **Sigma is preserved by the round-trip.** The coarsen-then-refine cell has the same
 169net flow at every site as the original; coarsening returns identical sigma. -/
 170theorem sigma_preserved (block : ℕ → ℕ) (m : Multiset Event) (a : ℕ) :
 171    netFlow (roundtrip block m) a = netFlow m a :=
 172  conserved (fun s => netFlow s a) block m
 173
 174/-! ## §5. Idle cells carry no refinement memory -/
 175
 176/-- **Idle carries nothing.** A cell with no internal events keeps an empty refinement,
 177so the round-trip is just the (already coarse) cross part, and refinement memory scales
 178with recognition activity rather than with the number of sites. -/
 179theorem idle_carries_nothing (block : ℕ → ℕ) (m : Multiset Event)
 180    (hidle : internalOf block m = 0) :
 181    roundtrip block m = crossOf block m := by
 182  unfold roundtrip refineCell
 183  rw [hidle, add_zero]
 184
 185/-! ## §6. The T-1 model as one object -/
 186
 187/-- **Coarsening Exactness (T-1).** One named record collecting the lossless-coarsening
 188guarantees for a cell `m`, a block map `block`, and a ratio weight `wr`:
 189
 190* coarsen then refine is the identity;
 191* event count, total cost, and the log-ratio spectrum are preserved;
 192* cost partitions exactly into coarse cross-block cost plus block-internal cost;
 193* sigma (net flow) is zero at every site, at every rung.
 194
 195Zero `sorry`, zero new `axiom`. -/
 196structure CoarseningExact (block : ℕ → ℕ) (m : Multiset Event) (wr : ℝ → ℝ) : Prop where
 197  roundtrip_identity : roundtrip block m = m
 198  count_exact : count (roundtrip block m) = count m
 199  cost_exact : cost wr (roundtrip block m) = cost wr m
 200  spectrum_exact : spectrum (roundtrip block m) = spectrum m
 201  cost_partitions : cost wr (coarseLedger block m) + cost wr (internalOf block m) = cost wr m
 202  sigma_exact : ∀ a, netFlow (roundtrip block m) a = netFlow m a
 203
 204/-- **The coarsening-exactness model holds for every cell, block map, and weight.** -/
 205theorem coarseningExact (block : ℕ → ℕ) (m : Multiset Event) (wr : ℝ → ℝ) :
 206    CoarseningExact block m wr where
 207  roundtrip_identity := roundtrip_eq block m
 208  count_exact := count_preserved block m
 209  cost_exact := cost_preserved wr block m
 210  spectrum_exact := spectrum_preserved block m
 211  cost_partitions := cost_partition wr block m
 212  sigma_exact := sigma_preserved block m
 213
 214/-! ## §7. The headline -/
 215
 216/-- **T-1 headline.** Coarsening one phi-rung and refining back is the identity, so a
 217region carried coarse loses nothing reality has determined: the event count, the total
 218cost, the log-ratio spectrum, and the (zero) net flow all come back identical, and the
 219cost partitions exactly across the rung change. This is the theorem that earns the word
 220"literal" for the scale-adaptive engine. -/
 221theorem t1_coarsening_exact (block : ℕ → ℕ) (m : Multiset Event) (wr : ℝ → ℝ) :
 222    (roundtrip block m = m)
 223    ∧ (count (roundtrip block m) = count m)
 224    ∧ (cost wr (roundtrip block m) = cost wr m)
 225    ∧ (spectrum (roundtrip block m) = spectrum m)
 226    ∧ (cost wr (coarseLedger block m) + cost wr (internalOf block m) = cost wr m)
 227    ∧ (∀ a, netFlow (roundtrip block m) a = netFlow m a) :=
 228  ⟨roundtrip_eq block m, count_preserved block m, cost_preserved wr block m,
 229   spectrum_preserved block m, cost_partition wr block m, sigma_preserved block m⟩
 230
 231end RungCoarsen
 232end Cosmology
 233end IndisputableMonolith
 234