Cosmology Rung Coarsen Count Preserved

Counting events across scales

A recognition event is a directed posting from one site to another, carrying a positive ratio; think of it as a single entry in a discrete ledger of happenings. The theorem count_preserved states that if you take a multiset of such events, coarsen it by grouping sites into blocks, and then refine it back, the total number of events is unchanged. Formally, count (roundtrip block m) = count m. This is not a physical claim about nature; it is a mathematical identity about a specific model.

The proof is almost trivial once you see the setup. Coarsening partitions the original multiset into two parts: events whose endpoints lie in the same block (internal) and events whose endpoints lie in different blocks (cross). Refining simply recombines these two parts. Because the partition is exact, the round-trip returns the identical multiset, so any function of that multiset, including its cardinality, is preserved. The theorem is a direct consequence of the round-trip identity, which is the real content.

In the Recognition Science framework, this result is one of several conservation properties that follow from the same round-trip identity. The library proves that total cost, the log-ratio spectrum, and net flow at every site are all preserved under the same coarsening and refinement. The theorem holds for an arbitrary ratio weight, so it applies to the framework's own recognition cost and to any other weighting. The statement is machine-checked, with zero axioms beyond the standard ones.

What the theorem does not claim is equally important. It does not say that coarsening loses no information in any physical sense; it only says that the multiset of events is recoverable from the coarse data plus the internal events. It does not assert that any particular quantity in nature is conserved; it is a statement about a formal model. It does not imply that the coarsening procedure is physically realizable or that the block map is meaningful. These are modeling choices, not consequences of the theorem.

theorem count_preserved (block : ℕ → ℕ) (m : Multiset Event) :
    count (roundtrip block m) = count m := conserved count block m

/-- **T-1 round-trip.** Coarsening then refining returns the cell unchanged. The coarse
representation is lossless: it carries everything reality has determined with zero loss. -/
theorem roundtrip_eq (block : ℕ → ℕ) (m : Multiset Event) :
    roundtrip block m = m := by
  unfold roundtrip refineCell
  exact cross_add_internal block m

/-- Because the round-trip returns the identical multiset, ANY functional of the cell
is preserved. Sigma, totals, cost, and spectrum are all instances of this. -/
theorem conserved {X : Type*} (F : Multiset Event → X) (block : ℕ → ℕ) (m : Multiset Event) :
    F (roundtrip block m) = F m :=
  congrArg F (roundtrip_eq block m)

theorem cost_preserved (wr : ℝ → ℝ) (block : ℕ → ℕ) (m : Multiset Event) :
    cost wr (roundtrip block m) = cost wr m := conserved (cost wr) block m

theorem spectrum_preserved (block : ℕ → ℕ) (m : Multiset Event) :
    spectrum (roundtrip block m) = spectrum m := conserved spectrum block m

/-- **Sigma is preserved by the round-trip.** The coarsen-then-refine cell has the same
net flow at every site as the original; coarsening returns identical sigma. -/
theorem sigma_preserved (block : ℕ → ℕ) (m : Multiset Event) (a : ℕ) :
    netFlow (roundtrip block m) a = netFlow m a :=
  conserved (fun s => netFlow s a) block m

What this page does not claim

The theorem does not claim that coarsening preserves all information about the original events. The theorem does not assert any physical conservation law in nature. The theorem does not justify the choice of block map or the model's physical relevance.

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/RungCoarsen.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: