roundtrip_eq
plain-language theorem explainer
Coarsening a recognition cell one phi-rung and refining it back recovers the original multiset of events exactly. Anyone citing T-1 of the scale-adaptive Cosmogenesis engine needs this identity as the lossless core. The proof unfolds the round-trip definition and applies the cross/internal partition recombination lemma.
Claim. For any block map $b:\mathbb{N}\to\mathbb{N}$ and any multiset $m$ of recognition events, coarsening $m$ by $b$ and then refining recovers $m$ exactly: $\mathrm{refine}(\mathrm{coarsen}_b(m))=m$.
background
In the Cosmogenesis T-1 model, a recognition cell at one phi-rung is a multiset of canonical events. Each event is a directed posting source → target carrying a positive ratio; order is irrelevant, and every conserved functional is a function of that multiset.
A block map $b:\mathbb{N}\to\mathbb{N}$ sends fine sites to coarse sites. Coarsening partitions events into internals (both endpoints land in one block) and cross events (endpoints differ, promoted to coarse edges with the same ratio). Refinement keeps the original cross events plus the per-block internals and reassembles them by multiset sum.
The local claim is that this partition is lossless. Upstream, the cross and internal parts recombine to the whole cell by the multiset filter identity: filtering by the same-block predicate and its complement, then adding, returns the original multiset.
proof idea
Term-mode one-liner after unfolding. Unfold the round-trip (coarsen then refine) and the refine-cell sum, which exposes exactly the cross multiset plus the internal multiset. Discharge by the recombination lemma: cross and internal parts add back to the original cell, itself proved by commuting the sum and applying Multiset.filter_add_not on the same-block predicate.
why it matters
This is the identity half of T-1 in the scale-adaptive Cosmogenesis engine: the coarse representation carries everything reality has determined with zero loss, which is what earns the word "literal." Downstream, every conserved functional is preserved by congruence on this identity (count, total cost under a ratio weight, log-ratio spectrum, net flow/sigma). The same fact is the roundtrip_identity field of the coarsening-exactness model and the first conjunct of the T-1 headline theorem. Cost partition and idle-cell memory bounds sit beside it in the same module; the structural sigma = 0 of double-entry is handled at the LedgerForcing layer, not here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.