IndisputableMonolith.Cosmology.RefineTrigger

   1import Mathlib
   2import IndisputableMonolith.Cosmology.RungCoarsen
   3
   4/-!
   5# T-3: the refinement trigger is law-derived (threshold = 0, no knob)
   6
   7This is the Lean statement of theorem T-3 of the scale-adaptive Cosmogenesis engine
   8(`plans/Cosmogenesis_North_Star_Reality_Simulation_Plan_20260602.html`,
   9`simulation/manifest.json` `build_spine.T3_law_derived_refinement`). The Python side
  10(`scripts/cosmogenesis/refine_trigger.py`) discharged it numerically; this module
  11discharges the statement itself. It builds on the T-1 cell model in
  12`Cosmology.RungCoarsen` (`Event`, `internalOf`, `crossOf`, `cost`, `cross_add_internal`).
  13
  14## The knob risk and how it is removed
  15
  16A naive refiner descends wherever some scalar exceeds a tuned tolerance `ε`. That `ε`
  17is exactly the free parameter the north star forbids. Sigma is identically zero at
  18every rung (double-entry), so a sigma imbalance is never the trigger. What forces a
  19descent is a posted distinction inside a block. The block's recognition demand is the
  20J-cost of its forced internal postings, and the law-given rule is:
  21
  22  descend a block iff recognition_demand(block) > 0,
  23
  24i.e. descend exactly where a distinction is forced. The threshold is structurally
  25zero, read off the ledger. There is no `ε` to choose.
  26
  27## The content of T-3
  28
  29* **the threshold is forced to zero** (`lossless_iff`): reconstructing while refining
  30  only the blocks in a decision `D` is lossless if and only if `D` covers every block
  31  that carries an internal posting. There is no freedom: lossless forces you to descend
  32  exactly the active blocks.
  33* **the law-given rule is lossless and minimal** (`lossless_law`,
  34  `descendLaw_necessary`): descend iff the block carries an internal posting; this is
  35  lossless, and any lossless decision must contain it.
  36* **no positive threshold is safe** (`jcost_arbitrarily_small_positive`,
  37  `epsilon_unsafe`): a forced posting can have arbitrarily small positive J-cost (ratio
  38  near one), so for every `ε > 0` there is a cell with an active block of demand below
  39  `ε` that the `ε`-rule skips, breaking losslessness. Zero is the unique law-given
  40  threshold.
  41
  42## Status
  43
  44Theorem-backed by `lawGivenTrigger` / `t3_law_derived_refinement`. The cost / demand is
  45the explicit RS recognition cost `Jcost x = (x + x⁻¹)/2 - 1`. Zero `sorry`, zero new
  46`axiom`.
  47-/
  48
  49namespace IndisputableMonolith
  50namespace Cosmology
  51namespace RefineTrigger
  52
  53open RungCoarsen
  54
  55open scoped Classical
  56
  57/-- Reconstruct the fine cell while refining only the blocks the decision `D` selects:
  58keep all cross-block events, but expand a block's internal postings only if `D` holds
  59of that block. A block left coarse contributes none of its internal postings. -/
  60def reconstructUnder (block : ℕ → ℕ) (D : ℕ → Prop) [DecidablePred D]
  61    (m : Multiset Event) : Multiset Event :=
  62  crossOf block m + (internalOf block m).filter (fun e => D (block e.source))
  63
  64/-! ## §1. The threshold is forced to zero -/
  65
  66/-- **The descent set is forced.** Refining only the blocks in `D` is lossless if and
  67only if `D` covers every block that carries an internal posting. There is no tunable
  68slack: lossless reconstruction requires descending exactly the active blocks. -/
  69theorem lossless_iff (block : ℕ → ℕ) (D : ℕ → Prop) [DecidablePred D] (m : Multiset Event) :
  70    reconstructUnder block D m = m ↔ ∀ e ∈ internalOf block m, D (block e.source) := by
  71  unfold reconstructUnder
  72  rw [← Multiset.filter_eq_self]
  73  constructor
  74  · intro h
  75    have h2 : crossOf block m + (internalOf block m).filter (fun e => D (block e.source))
  76            = crossOf block m + internalOf block m := by
  77      rw [h]; exact (cross_add_internal block m).symm
  78    exact add_left_cancel h2
  79  · intro h
  80    rw [h]
  81    exact cross_add_internal block m
  82
  83/-! ## §2. The law-given rule is lossless and minimal -/
  84
  85/-- The law-given descent predicate: descend a block iff it carries an internal
  86posting (positive recognition activity). -/
  87def descendLaw (block : ℕ → ℕ) (m : Multiset Event) (b : ℕ) : Prop :=
  88  b ∈ (internalOf block m).map (fun e => block e.source)
  89
  90/-- **The law-given rule is lossless.** Descending exactly the active blocks
  91reconstructs the cell with zero loss. -/
  92theorem lossless_law (block : ℕ → ℕ) (m : Multiset Event) :
  93    reconstructUnder block (descendLaw block m) m = m := by
  94  rw [lossless_iff]
  95  intro e he
  96  exact Multiset.mem_map.mpr ⟨e, he, rfl⟩
  97
  98/-- **The law-given rule is minimal.** Any lossless decision must descend every active
  99block; you cannot skip a block that carries a posting. -/
 100theorem descendLaw_necessary (block : ℕ → ℕ) (D : ℕ → Prop) [DecidablePred D]
 101    (m : Multiset Event) (h : reconstructUnder block D m = m) :
 102    ∀ b, descendLaw block m b → D b := by
 103  intro b hb
 104  obtain ⟨e, he, hbe⟩ := Multiset.mem_map.mp hb
 105  have hD := (lossless_iff block D m).mp h e he
 106  rwa [hbe] at hD
 107
 108/-! ## §3. The recognition cost and demand -/
 109
 110/-- The RS recognition cost of a positive ratio. -/
 111noncomputable def Jcost (x : ℝ) : ℝ := (x + x⁻¹) / 2 - 1
 112
 113/-- A genuine distinction (ratio not one) has strictly positive cost. -/
 114theorem jcost_pos {x : ℝ} (hx : 0 < x) (hne : x ≠ 1) : 0 < Jcost x := by
 115  have hx0 : x ≠ 0 := hx.ne'
 116  have key : Jcost x = (x - 1) ^ 2 / (2 * x) := by
 117    unfold Jcost; field_simp; ring
 118  rw [key]
 119  have hsq : 0 < (x - 1) ^ 2 := by
 120    have hne' : x - 1 ≠ 0 := sub_ne_zero.mpr hne
 121    positivity
 122  have hden : 0 < 2 * x := by linarith
 123  exact div_pos hsq hden
 124
 125/-- **Forced postings have arbitrarily small positive cost.** For every `ε > 0` there is
 126a ratio above one whose recognition cost is positive but below `ε`. This is why no
 127positive threshold is safe: a forced distinction can sit just under any `ε`. -/
 128theorem jcost_arbitrarily_small_positive (ε : ℝ) (hε : 0 < ε) :
 129    ∃ x : ℝ, 1 < x ∧ 0 < Jcost x ∧ Jcost x < ε := by
 130  have hδpos : 0 < min 1 ε := lt_min (by norm_num) hε
 131  have hδ1 : min 1 ε ≤ 1 := min_le_left _ _
 132  have hδε : min 1 ε ≤ ε := min_le_right _ _
 133  have hx1 : (1 : ℝ) < 1 + min 1 ε := by linarith
 134  have hpos : (0 : ℝ) < 1 + min 1 ε := by linarith
 135  have hne0 : (1 + min 1 ε) ≠ 0 := hpos.ne'
 136  refine ⟨1 + min 1 ε, hx1, jcost_pos hpos hx1.ne', ?_⟩
 137  have key : Jcost (1 + min 1 ε) = (min 1 ε) ^ 2 / (2 * (1 + min 1 ε)) := by
 138    unfold Jcost; field_simp; ring
 139  rw [key, div_lt_iff₀ (by nlinarith : (0 : ℝ) < 2 * (1 + min 1 ε))]
 140  nlinarith [hδpos, hδ1, hδε, hε,
 141    mul_nonneg hδpos.le (by linarith : (0 : ℝ) ≤ 1 - min 1 ε), mul_pos hε hδpos]
 142
 143/-- Per-block recognition demand: the recognition cost of the block's internal
 144postings, the quantity the law-given rule reads. -/
 145noncomputable def demand (block : ℕ → ℕ) (m : Multiset Event) (b : ℕ) : ℝ :=
 146  cost Jcost ((internalOf block m).filter (fun e => block e.source = b))
 147
 148/-! ## §4. No positive threshold is safe -/
 149
 150/-- A two-site block map: sites `0,1` to coarse block `0`, everything else to block `1`. -/
 151def b01 : ℕ → ℕ := fun s => if s ≤ 1 then 0 else 1
 152
 153@[simp] theorem b01_zero : b01 0 = 0 := by simp [b01]
 154@[simp] theorem b01_one : b01 1 = 0 := by simp [b01]
 155
 156theorem cost_singleton (wr : ℝ → ℝ) (e : Event) : cost wr {e} = wr e.ratio := by
 157  unfold cost; simp
 158
 159/-- **No positive threshold is safe.** For every `ε > 0` there is a cell with a single
 160internal posting whose demand is positive but below `ε`. The threshold rule "descend
 161iff demand exceeds `ε`" therefore skips that active block, and the reconstruction is
 162lossy. Only the zero threshold (descend iff a distinction is forced) is law-given. -/
 163theorem epsilon_unsafe (ε : ℝ) (hε : 0 < ε) :
 164    ∃ (m : Multiset Event) (b : ℕ),
 165      0 < demand b01 m b ∧ demand b01 m b < ε
 166      ∧ reconstructUnder b01 (fun c => ε < demand b01 m c) m ≠ m := by
 167  obtain ⟨r, hr1, hrpos, hrlt⟩ := jcost_arbitrarily_small_positive ε hε
 168  refine ⟨{(⟨0, 1, r⟩ : Event)}, 0, ?_, ?_, ?_⟩
 169  · -- demand b01 {⟨0,1,r⟩} 0 = Jcost r
 170    have hd : demand b01 {(⟨0, 1, r⟩ : Event)} 0 = Jcost r := by
 171      unfold demand internalOf
 172      simp [sameBlock, b01, Multiset.filter_singleton, cost_singleton]
 173    rw [hd]; exact hrpos
 174  · have hd : demand b01 {(⟨0, 1, r⟩ : Event)} 0 = Jcost r := by
 175      unfold demand internalOf
 176      simp [sameBlock, b01, Multiset.filter_singleton, cost_singleton]
 177    rw [hd]; exact hrlt
 178  · -- the epsilon-rule skips block 0, so reconstruction drops the only posting
 179    have hd : demand b01 {(⟨0, 1, r⟩ : Event)} 0 = Jcost r := by
 180      unfold demand internalOf
 181      simp [sameBlock, b01, Multiset.filter_singleton, cost_singleton]
 182    have hnotsel : ¬ (ε < demand b01 {(⟨0, 1, r⟩ : Event)} 0) := by rw [hd]; linarith
 183    -- reconstructUnder = crossOf (empty) + internal filtered by a false predicate = 0
 184    have hrecon : reconstructUnder b01 (fun c => ε < demand b01 {(⟨0, 1, r⟩ : Event)} c)
 185        {(⟨0, 1, r⟩ : Event)} = 0 := by
 186      unfold reconstructUnder crossOf internalOf
 187      simp [sameBlock, b01, Multiset.filter_singleton, hnotsel]
 188    rw [hrecon]
 189    -- 0 ≠ {⟨0,1,r⟩}
 190    intro hcontra
 191    have : Multiset.card (0 : Multiset Event) = Multiset.card {(⟨0, 1, r⟩ : Event)} :=
 192      congrArg Multiset.card hcontra
 193    simp at this
 194
 195/-! ## §5. The T-3 model as one object -/
 196
 197/-- **Law-Given Trigger (T-3).** One named record collecting the refinement-trigger
 198guarantees:
 199
 200* lossless reconstruction forces the descent set to be exactly the active blocks
 201  (`lossless_iff`);
 202* the law-given rule (descend iff a posting is forced) is lossless and minimal;
 203* no positive threshold is safe: a forced posting can have demand below any `ε > 0`.
 204
 205Zero `sorry`, zero new `axiom`. -/
 206structure LawGivenTrigger (block : ℕ → ℕ) (m : Multiset Event) : Prop where
 207  threshold_forced : ∀ (D : ℕ → Prop) [DecidablePred D],
 208    reconstructUnder block D m = m ↔ ∀ e ∈ internalOf block m, D (block e.source)
 209  law_lossless : reconstructUnder block (descendLaw block m) m = m
 210  law_minimal : ∀ (D : ℕ → Prop) [DecidablePred D],
 211    reconstructUnder block D m = m → ∀ b, descendLaw block m b → D b
 212
 213/-- **The law-given trigger model holds for every cell and block map.** -/
 214theorem lawGivenTrigger (block : ℕ → ℕ) (m : Multiset Event) : LawGivenTrigger block m where
 215  threshold_forced := fun D => lossless_iff block D m
 216  law_lossless := lossless_law block m
 217  law_minimal := fun D => descendLaw_necessary block D m
 218
 219/-! ## §6. The headline -/
 220
 221/-- **T-3 headline.** Lossless reconstruction forces the descent set to be exactly the
 222blocks that carry a forced posting (`lossless_iff`), the law-given rule realizing that
 223set is itself lossless (`lossless_law`), and no positive tolerance is safe because a
 224forced posting can have arbitrarily small positive cost (`epsilon_unsafe`). The
 225refinement threshold is therefore structurally zero, read off the ledger, with no knob
 226to choose. -/
 227theorem t3_law_derived_refinement (block : ℕ → ℕ) (m : Multiset Event) :
 228    (∀ (D : ℕ → Prop) [DecidablePred D],
 229        reconstructUnder block D m = m ↔ ∀ e ∈ internalOf block m, D (block e.source))
 230    ∧ (reconstructUnder block (descendLaw block m) m = m)
 231    ∧ (∀ ε : ℝ, 0 < ε → ∃ (m' : Multiset Event) (b : ℕ),
 232        0 < demand b01 m' b ∧ demand b01 m' b < ε
 233        ∧ reconstructUnder b01 (fun c => ε < demand b01 m' c) m' ≠ m') :=
 234  ⟨fun D => lossless_iff block D m, lossless_law block m,
 235   fun ε hε => epsilon_unsafe ε hε⟩
 236
 237end RefineTrigger
 238end Cosmology
 239end IndisputableMonolith
 240