Cosmology Rung Coarsen Cross Add Internal

The partition lemma

In the Recognition Science framework, a ledger is a discrete record of events, each event a directed posting from a source site to a target site carrying a positive ratio. When the framework coarsens such a ledger, moving from a fine scale to a coarser one, it groups sites into blocks. Each event then falls into one of two classes: an internal event, with both endpoints in the same block, or a cross event, whose endpoints land in different blocks. The declaration cross_add_internal states the simplest possible fact about this partition: the cross events plus the internal events, taken together as multisets, exactly equal the original set of events.

This is not a numerical approximation. The theorem, proved in the framework's machine-checked library of formal theorems, says that the multiset union of the two parts recombines to the original multiset, with no event duplicated and none dropped. Because the equality is exact at the level of multisets, every function of the ledger is preserved under the round trip of coarsening and refining. Event count, total cost for any ratio weight, the log-ratio spectrum, and net flow at each site all come back unchanged. The partition lemma is the hinge on which the whole exactness result turns.

The lemma also yields a clean accounting identity. The cost of the coarse ledger, which keeps only cross events relabeled to their blocks, plus the cost of the internal events, equals the cost of the original fine ledger. This holds for any cost function that assigns a value to each event's ratio, not only for the framework's own recognition cost. The partition is therefore a structural fact about the ledger, independent of how cost is defined.

What the declaration does not claim is equally important. It does not say that coarsening preserves the spatial arrangement of events, only their multiset of ratios and endpoints at the block level. It does not assert that the coarse ledger alone, without the internal events, carries all information; the cross events alone lose the internal structure. And it does not claim that the partition lemma holds for arbitrary groupings of events into blocks; it holds for the specific partition into same-block and different-block classes defined by a block map.

/-- The cross and internal parts recombine to the whole cell. -/
theorem cross_add_internal (block : ℕ → ℕ) (m : Multiset Event) :
    crossOf block m + internalOf block m = m := by
  unfold crossOf internalOf
  rw [add_comm]
  exact Multiset.filter_add_not (sameBlock 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)

/-- **Cost partition.** Coarse cross-block cost plus block-internal cost equals the fine
cost. Cost is split exactly across the rung change, with no leakage. -/
theorem cost_partition (wr : ℝ → ℝ) (block : ℕ → ℕ) (m : Multiset Event) :
    cost wr (coarseLedger block m) + cost wr (internalOf block m) = cost wr m := by
  rw [cost_coarse_eq_cross, ← cost_add, cross_add_internal]

What this page does not claim

Coarsening preserves the fine-grained spatial arrangement of events, only their multiset of ratios and block-level endpoints. The coarse ledger alone, without internal events, carries all information about the original ledger. The partition lemma holds for arbitrary groupings of events into blocks; it holds for the specific same-block versus different-block partition.

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: