Cosmology Recognition Work Bound Tick Activations

The bounded tick

In the Recognition Science framework, reality keeps a ledger, a discrete record of events, and each event has a forced cost. The declaration tickActivations is the unit of that accounting for a single tick, one step of the framework's internal clock. The definition is plain: a tick that resolves nothing costs zero activations, and a tick that resolves an edge between two regions activates exactly two, one for each endpoint. This is the double-entry posting rule, the framework's way of saying that a connection touches both of its ends.

The theorem that matters is tickActivations_le_two: any tick contributes at most two region-activations. That bound is the first rung of a ladder. Sum it over a cycle of eight ticks, the framework's forced cadence, and the total activations in a cycle are at most sixteen, no matter how many regions the world contains. The proof is a short chain of inequalities in the machine-checked library of formal theorems: each tick's work is the sum of two endpoint costs, each cost is at most the ceiling, and a finite sum of ceilings is the ceiling times the count.

The payoff is the localization result. When the world grows by a fixed number of regions per cycle, the recognition work per cycle stays capped by the cadence while the volume of the ledger grows without bound. The recognition-active fraction, work divided by volume, falls toward zero. The engine never expands its locked interior; the cost concentrates on a thin boundary. This is the formal core of a cosmological claim: an expanding ledger can stay cheap to run.

What the declaration does not claim is just as important. It bounds activations, not the total work of expansion, which depends on a separate per-region cost ceiling. It assumes at most one resolved edge per tick, the forced cadence law, and does not model a tick that resolves several edges at once. It says nothing about which edges get resolved, only how many activations any resolution costs. The bound is a ceiling, not a prediction of what a real dynamics will do.

/-- The number of region-activations a single tick contributes: `0` if it resolves nothing, `2` if it
resolves an edge (its two endpoints). It is `tickWork` with the unit cost. -/
def tickActivations (e : Option (ι × ι)) : ℕ := tickWork e (fun _ => 1)

/-- A tick contributes at most `2` region-activations. -/
theorem tickActivations_le_two (e : Option (ι × ι)) : tickActivations e ≤ 2 := by
  simpa using tickWork_le e 1 (fun _ => 1) (fun _ => le_rfl)

/-- **Region-activations per cycle are bounded by twice the cadence, independent of the population.**
A specialization of `cycle_work_le` with unit cost: at most `2 * T` region-activations occur in a
`T`-tick cycle, regardless of the number of regions. -/
theorem cycle_activations_le (T : ℕ) (res : Fin T → Option (ι × ι)) :
    (∑ t, tickActivations (res t)) ≤ 2 * T := by
  have := cycle_work_le T res 1 (fun _ => 1) (fun _ => le_rfl)
  simpa [tickActivations] using this

/-- **Phase-11 cost-localization headline.** In a `T`-tick cadence cycle with at most one forced
resolution per tick, the engine's recognition work is at most `2 * P * T` and the region-activations
are at most `2 * T`, both independent of the population `ι`. So when the world grows by a fixed number
of regions per cycle, the recognition-cost numerator is capped while the volume denominator grows: the
recognition-active fraction falls toward zero and the cost localizes to a sub-extensive interface. -/
theorem recognition_work_localizes (T : ℕ) (res : Fin T → Option (ι × ι)) (P : ℕ)
    (cost : ι → ℕ) (hcost : ∀ i, cost i ≤ P) :
    (∑ t, tickWork (res t) cost) ≤ 2 * P * T
    ∧ (∑ t, tickActivations (res t)) ≤ 2 * T :=
  ⟨cycle_work_le T res P cost hcost, cycle_activations_le T res⟩

What this page does not claim

The declaration does not bound the total recognition work of a cycle, which also depends on the per-region cost ceiling P. It does not model ticks that resolve more than one edge at once. It does not predict which edges are resolved, only the maximum activations any resolution costs.

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: