roundtrip
plain-language theorem explainer
Defines the coarsen-then-refine map on a recognition cell: split events by a block map into internal and cross parts, then reassemble them. Cosmogenesis T-1 cites it as the carrier of lossless rung change. The body is a one-line composition of the partition and the refinement sum.
Claim. Given a block map $b:\mathbb{N}\to\mathbb{N}$ and a multiset $m$ of recognition events (directed postings $s\to t$ with positive ratio), the round-trip is $\mathrm{refine}(\mathrm{internal}_b(m),\mathrm{cross}_b(m))$, i.e. the multiset sum of the within-block events and the cross-block events of $m$.
background
Module T-1 formalizes rung-coarsening for the scale-adaptive Cosmogenesis engine: a recognition cell is a multiset of canonical events, and every conserved quantity is a functional of that multiset. A block map $b$ sends fine lattice sites to coarse sites one phi-rung up.
Events partition by endpoint placement. Internal events have both endpoints in one block and are absorbed into that block's summary; cross events have endpoints in different blocks and are promoted (after relabeling) to the coarse ledger. The refinement record keeps the original cross multiset and the per-block internals.
refineCell is multiset addition of those two parts. The round-trip composes the split with that sum, matching the Python coarsen/refine/Refinement path that already checked exactness numerically on the voxel battery.
proof idea
Definitional one-liner: apply internalOf block m and crossOf block m (filters by sameBlock), then feed both into refineCell, which is crossOrigin + internal. No tactics; the mathematical content lives in the later identity theorem that this equals $m$.
why it matters
This is the named operator behind Cosmogenesis T-1 ("literal" coarsening). Downstream, roundtrip_eq proves it is the identity via the partition lemma cross_add_internal; conserved then lifts that to every functional of the cell, yielding count_preserved, cost_preserved, spectrum_preserved, and sigma_preserved. The bundle structure CoarseningExact packages those guarantees, and idle_carries_nothing specializes the round-trip when internals vanish so refinement memory tracks activity, not site count.
In the RS ladder picture, lossless rung change means coarsening loses nothing reality has already fixed: cost, spectrum, and net flow survive the phi-rung step exactly. That underwrites scale-adaptive cosmogenesis without inventing or discarding ledger content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.