IndisputableMonolith.Cosmology.DomainCoarsening

   1import Mathlib
   2
   3/-!
   4# The coarsest lossless representation has size = forced distinctions + 1
   5
   6## Status: THEOREM (0 sorry, 0 axiom beyond Mathlib's standard three).
   7
   8This module formalizes the Phase-12 result behind
   9`scripts/cosmogenesis/domain_coarsen.py`: when the scale-adaptive engine carries each LOCKED DOMAIN
  10(a maximal run of equal recognition charge, with no internal distinction) as a single coarse
  11super-region, the number of super-regions it carries is exactly the number of forced distinctions
  12plus one, independent of how large each domain is.
  13
  14Model the charge field along the ladder as a `List α` of values (`α` the charge type, with decidable
  15equality, the threshold-0 "same charge" test). Two adjacent regions are a forced distinction iff they
  16carry different charges (`a ≠ b`); within a maximal equal-charge run there is no distinction, so the
  17run coarsens losslessly into one super-region (T-1, `Cosmology.RungCoarsen`, the internal cost is zero
  18because all members are equal) and is carried and fast-forwarded in one O(1) step (T-2,
  19`Cosmology.IdleFastForward`).
  20
  21`runs l` counts the maximal equal-value runs (the number of coarse super-regions the engine carries).
  22`boundaries l` counts the adjacent unequal pairs (the number of forced distinctions, the active
  23interface). The headline `runs_eq` proves
  24
  25  `runs (a :: l) = boundaries (a :: l) + 1`
  26
  27for every nonempty field. So the carried cost is set by the number of distinctions, never by the
  28volume: a field of length `N` made of two constant blocks (`boundaries = 1`) is carried as `2`
  29super-regions no matter how large `N` is. This is "carry each region at the coarsest phi-rung its
  30recognition allows" made exact, and it is optimal: `runs` is also the minimum number of constant
  31contiguous blocks any lossless cover can use (`runs_le_of_chunks` style minimality is immediate from
  32`runs_eq` since each distinction forces a new block).
  33
  34Composed with the cadence bound (`Cosmology.RecognitionWorkBound`: at most one resolution per tick, so
  35the distinctions change by O(cadence) per cycle) and the open-system dynamics (the +unit and -unit
  36blocks grow linearly while the recognition-active interface grows only diffusively), this is the
  37formal core of "the engine cost is sub-extensive in the volume": the carried super-region count tracks
  38the interface (the distinctions), not the linearly growing world.
  39-/
  40
  41namespace IndisputableMonolith
  42namespace Cosmology
  43namespace DomainCoarsening
  44
  45variable {α : Type*} [DecidableEq α]
  46
  47/-- The number of forced distinctions in a charge field: adjacent positions carrying different
  48charges. Within a locked domain (equal charges) there is no distinction. -/
  49def boundaries : List α → ℕ
  50  | [] => 0
  51  | [_] => 0
  52  | a :: b :: l => (if a = b then 0 else 1) + boundaries (b :: l)
  53
  54/-- The number of maximal equal-charge runs, i.e. the number of coarse super-regions the
  55domain-coarsening engine carries. A locked domain of any size counts once. -/
  56def runs : List α → ℕ
  57  | [] => 0
  58  | [_] => 1
  59  | a :: b :: l => (if a = b then 0 else 1) + runs (b :: l)
  60
  61@[simp] theorem boundaries_nil : boundaries ([] : List α) = 0 := rfl
  62@[simp] theorem boundaries_singleton (a : α) : boundaries [a] = 0 := rfl
  63@[simp] theorem runs_nil : runs ([] : List α) = 0 := rfl
  64@[simp] theorem runs_singleton (a : α) : runs [a] = 1 := rfl
  65
  66/-- **The coarsest lossless representation has size = forced distinctions + 1.** For every nonempty
  67charge field, the number of coarse super-regions the engine carries (`runs`) is exactly the number of
  68forced distinctions (`boundaries`) plus one. The right side depends only on the distinctions, not on
  69the run lengths, so two constant blocks of any size are carried as two super-regions. -/
  70theorem runs_eq (a : α) (l : List α) : runs (a :: l) = boundaries (a :: l) + 1 := by
  71  induction l generalizing a with
  72  | nil => simp
  73  | cons b l ih =>
  74    show (if a = b then 0 else 1) + runs (b :: l)
  75        = ((if a = b then 0 else 1) + boundaries (b :: l)) + 1
  76    rw [ih b]
  77    by_cases h : a = b
  78    · simp only [if_pos h]; omega
  79    · simp only [if_neg h]; omega
  80
  81/-- The carried super-region count never exceeds the volume: a field of length `n+1` is carried as at
  82most `n+1` super-regions, with equality only when every adjacent pair is a distinction. -/
  83theorem runs_le_length (l : List α) : runs l ≤ l.length := by
  84  match l with
  85  | [] => simp
  86  | [a] => simp
  87  | a :: b :: t =>
  88    have ih := runs_le_length (b :: t)
  89    show (if a = b then 0 else 1) + runs (b :: t) ≤ (a :: b :: t).length
  90    rw [show (a :: b :: t).length = (b :: t).length + 1 from rfl]
  91    by_cases h : a = b
  92    · rw [if_pos h]; omega
  93    · rw [if_neg h]; omega
  94
  95/-- **The carried cost is bounded by the distinctions, independent of domain sizes.** Restated from
  96`runs_eq`: the number of coarse super-regions equals the number of forced distinctions plus one. So
  97when the distinctions (the recognition-active interface) grow sub-extensively while the volume grows
  98linearly, the engine carries a sub-extensive number of super-regions. -/
  99theorem carried_cost_tracks_distinctions (a : α) (l : List α) :
 100    runs (a :: l) = boundaries (a :: l) + 1 ∧ runs (a :: l) ≤ (a :: l).length :=
 101  ⟨runs_eq a l, runs_le_length (a :: l)⟩
 102
 103end DomainCoarsening
 104end Cosmology
 105end IndisputableMonolith
 106