IndisputableMonolith.Cosmology.RecognitionWorkBound

   1import Mathlib
   2
   3/-!
   4# Recognition work per cycle is bounded by the cadence, independent of the population
   5
   6## Status: THEOREM (0 sorry, 0 axiom beyond Mathlib's standard three).
   7
   8This module formalizes the Phase-11 result behind
   9`scripts/cosmogenesis/driven_forward.py`: when the open-system (expanding) dynamics drives the
  10scale-adaptive cell engine over a GROWING world, the recognition cost per cadence cycle stays
  11bounded while the world grows linearly, so the engine cost localizes to a sub-extensive interface.
  12
  13The forced law posts at most one recognition event per tick (the cadence, T-7,
  14`Cosmology.FirstTick.cosmogenesisCadence = 8`). Model a cycle as `T` ticks, with at most one resolved
  15edge per tick: `res : Fin T → Option (ι × ι)` over an arbitrary region-index type `ι`. Each resolved
  16edge activates its two endpoints (a double-entry posting), so a tick contributes at most two
  17region-activations and, when each endpoint costs at most `P` forced postings to expand, at most
  18`2 * P` units of recognition work.
  19
  20The theorems below bound the per-cycle activations by `2 * T` and the per-cycle recognition work by
  21`2 * P * T`. Crucially the bounds mention only the tick count `T` (the cadence) and the per-region
  22cost ceiling `P`, never the number of regions: the type `ι` can be arbitrarily large and does not
  23enter. So recognition cost per cycle does not grow with the world. Composed with a world that grows
  24by a fixed number of regions per cycle (the conjugate births of `expanding_dynamics.py`), this is the
  25formal core of "the recognition-active fraction falls toward zero and the engine never expands the
  26locked interior": the numerator (recognition work) is capped while the denominator (volume) grows.
  27
  28This sits beside the schedule-independence corollary
  29(`Cosmology.ScaleAdaptiveSchedule.engine_run_literal_under_any_schedule`, which gives that the engine
  30stays literal under any schedule, hence the emergent open-system one) and the conjugate-birth charge
  31conservation (`Cosmology.RecognitionEquilibrium.manyBirths_chargeSum`, which gives sigma = 0 through
  32every birth). Together those three say: the driven engine is literal, conserves sigma through growth,
  33and pays a per-cycle recognition cost bounded by the cadence regardless of how large reality grows.
  34-/
  35
  36namespace IndisputableMonolith
  37namespace Cosmology
  38namespace RecognitionWorkBound
  39
  40variable {ι : Type*}
  41
  42/-- The recognition work a single tick contributes, given a per-region forced-posting cost. A tick
  43that resolves nothing costs `0`; a tick that resolves an edge `(a, b)` costs `cost a + cost b` (its
  44two endpoints are expanded). At most one edge is resolved per tick, the forced cadence law. -/
  45def tickWork (e : Option (ι × ι)) (cost : ι → ℕ) : ℕ :=
  46  match e with
  47  | none => 0
  48  | some (a, b) => cost a + cost b
  49
  50/-- The number of region-activations a single tick contributes: `0` if it resolves nothing, `2` if it
  51resolves an edge (its two endpoints). It is `tickWork` with the unit cost. -/
  52def tickActivations (e : Option (ι × ι)) : ℕ := tickWork e (fun _ => 1)
  53
  54/-- A tick costs at most `2 * P` recognition work when every endpoint costs at most `P` to expand. -/
  55theorem tickWork_le (e : Option (ι × ι)) (P : ℕ) (cost : ι → ℕ) (hcost : ∀ i, cost i ≤ P) :
  56    tickWork e cost ≤ 2 * P := by
  57  cases e with
  58  | none => simp [tickWork]
  59  | some ab =>
  60    obtain ⟨a, b⟩ := ab
  61    calc tickWork (some (a, b)) cost = cost a + cost b := rfl
  62      _ ≤ P + P := Nat.add_le_add (hcost a) (hcost b)
  63      _ = 2 * P := (two_mul P).symm
  64
  65/-- A tick contributes at most `2` region-activations. -/
  66theorem tickActivations_le_two (e : Option (ι × ι)) : tickActivations e ≤ 2 := by
  67  simpa using tickWork_le e 1 (fun _ => 1) (fun _ => le_rfl)
  68
  69/-- **Recognition work per cycle is bounded by the cadence, independent of the population.** Over a
  70cycle of `T` ticks with at most one resolved edge per tick and per-region expansion cost at most `P`,
  71the engine's total recognition work in the cycle is at most `2 * P * T`. The bound mentions only the
  72tick count `T` and the per-region ceiling `P`; the region-index type `ι` (the population) does not
  73appear, so the per-cycle recognition cost does not grow with the world. -/
  74theorem cycle_work_le (T : ℕ) (res : Fin T → Option (ι × ι)) (P : ℕ)
  75    (cost : ι → ℕ) (hcost : ∀ i, cost i ≤ P) :
  76    (∑ t, tickWork (res t) cost) ≤ 2 * P * T := by
  77  have h : (∑ t : Fin T, tickWork (res t) cost) ≤ ∑ _t : Fin T, 2 * P :=
  78    Finset.sum_le_sum (fun t _ => tickWork_le (res t) P cost hcost)
  79  have hconst : (∑ _t : Fin T, 2 * P) = 2 * P * T := by
  80    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul, Nat.mul_comm]
  81  exact h.trans (le_of_eq hconst)
  82
  83/-- **Region-activations per cycle are bounded by twice the cadence, independent of the population.**
  84A specialization of `cycle_work_le` with unit cost: at most `2 * T` region-activations occur in a
  85`T`-tick cycle, regardless of the number of regions. -/
  86theorem cycle_activations_le (T : ℕ) (res : Fin T → Option (ι × ι)) :
  87    (∑ t, tickActivations (res t)) ≤ 2 * T := by
  88  have := cycle_work_le T res 1 (fun _ => 1) (fun _ => le_rfl)
  89  simpa [tickActivations] using this
  90
  91/-- **Phase-11 cost-localization headline.** In a `T`-tick cadence cycle with at most one forced
  92resolution per tick, the engine's recognition work is at most `2 * P * T` and the region-activations
  93are at most `2 * T`, both independent of the population `ι`. So when the world grows by a fixed number
  94of regions per cycle, the recognition-cost numerator is capped while the volume denominator grows: the
  95recognition-active fraction falls toward zero and the cost localizes to a sub-extensive interface. -/
  96theorem recognition_work_localizes (T : ℕ) (res : Fin T → Option (ι × ι)) (P : ℕ)
  97    (cost : ι → ℕ) (hcost : ∀ i, cost i ≤ P) :
  98    (∑ t, tickWork (res t) cost) ≤ 2 * P * T
  99    ∧ (∑ t, tickActivations (res t)) ≤ 2 * T :=
 100  ⟨cycle_work_le T res P cost hcost, cycle_activations_le T res⟩
 101
 102end RecognitionWorkBound
 103end Cosmology
 104end IndisputableMonolith
 105