Cosmology Recognition Work Bound Tick Work Le

The cost of a tick

The declaration tickWork_le is a proved theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes a bound on the recognition work, the framework's term for the cost of updating a discrete record of events, that occurs in a single tick, the smallest unit of the framework's eight-tick cosmic cadence. The theorem states that if each region of the world costs at most P units of work to expand, then one tick, which resolves at most one edge between two regions, costs at most 2P units of work. The proof is a simple calculation: resolving an edge activates its two endpoints, each costing at most P, so the total is at most P plus P, which equals 2P.

The significance of this bound is that it does not depend on the number of regions in the world. The type of region indices, which could be arbitrarily large, does not appear in the bound. This means the cost of a single tick is capped by the per-region cost ceiling, not by the size of the population. A companion theorem, cycle_work_le, extends this to a full cycle of T ticks, bounding the total recognition work by 2PT. Together these theorems show that when the world grows by a fixed number of regions per cycle, the recognition cost stays capped while the volume grows, so the cost localizes to a sub-extensive interface, a boundary whose cost does not scale with the whole.

In Recognition Science, this result supports the claim that a driven, expanding universe can be simulated without the cost of bookkeeping exploding. The theorem is formalized in the file RecognitionWorkBound.lean with zero axioms beyond the standard three of the ambient type theory. It is a statement about the framework's model of cosmic dynamics, not a statement about any specific physical universe.

/-- A tick costs at most `2 * P` recognition work when every endpoint costs at most `P` to expand. -/
theorem tickWork_le (e : Option (ι × ι)) (P : ℕ) (cost : ι → ℕ) (hcost : ∀ i, cost i ≤ P) :
    tickWork e cost ≤ 2 * P := by
  cases e with
  | none => simp [tickWork]
  | some ab =>
    obtain ⟨a, b⟩ := ab
    calc tickWork (some (a, b)) cost = cost a + cost b := rfl
      _ ≤ P + P := Nat.add_le_add (hcost a) (hcost b)
      _ = 2 * P := (two_mul P).symm

/-- **Recognition work per cycle is bounded by the cadence, independent of the population.** Over a
cycle of `T` ticks with at most one resolved edge per tick and per-region expansion cost at most `P`,
the engine's total recognition work in the cycle is at most `2 * P * T`. The bound mentions only the
tick count `T` and the per-region ceiling `P`; the region-index type `ι` (the population) does not
appear, so the per-cycle recognition cost does not grow with the world. -/
theorem cycle_work_le (T : ℕ) (res : Fin T → Option (ι × ι)) (P : ℕ)
    (cost : ι → ℕ) (hcost : ∀ i, cost i ≤ P) :
    (∑ t, tickWork (res t) cost) ≤ 2 * P * T := by
  have h : (∑ t : Fin T, tickWork (res t) cost) ≤ ∑ _t : Fin T, 2 * P :=
    Finset.sum_le_sum (fun t _ => tickWork_le (res t) P cost hcost)
  have hconst : (∑ _t : Fin T, 2 * P) = 2 * P * T := by
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, smul_eq_mul, Nat.mul_comm]
  exact h.trans (le_of_eq hconst)

/-- A tick costs at most `2 * P` recognition work when every endpoint costs at most `P` to expand. -/
theorem tickWork_le (e : Option (ι × ι)) (P : ℕ) (cost : ι → ℕ) (hcost : ∀ i, cost i ≤ P) :
    tickWork e cost ≤ 2 * P := by
  cases e with
  | none => simp [tickWork]
  | some ab =>
    obtain ⟨a, b⟩ := ab
    calc tickWork (some (a, b)) cost = cost a + cost b := rfl
      _ ≤ P + P := Nat.add_le_add (hcost a) (hcost b)
      _ = 2 * P := (two_mul P).symm

What this page does not claim

The theorem does not claim that recognition work is zero, only that it is bounded per cycle. The theorem does not claim that the framework's model of cosmic dynamics is the actual physics of the universe. The theorem does not claim that the per-region cost P is a constant across all regions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/RecognitionWorkBound.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: