refineCell
plain-language theorem explainer
Reassembles a fine recognition cell from a coarsening refinement record by multiset-adding retained per-block internal events to the original cross-block events. Cosmogenesis T-1 round-trip and idle-cell lemmas cite it as the refine half of coarsen/refine. The body is literally multiset sum: no filtering or relabeling.
Claim. Given multisets $I$ (per-block internal recognition events) and $C$ (original cross-block events), define $\mathrm{refine}(I,C) := C + I$ as multisets of directed postings $(s\to t,r)$ with positive ratio $r$.
background
Module T-1 formalizes rung-coarsening for the scale-adaptive Cosmogenesis engine: a recognition cell at one $\varphi$-rung is a multiset of canonical events. An event is a directed posting $\mathrm{source}\to\mathrm{target}$ carrying a positive real ratio; double-entry reciprocity is implicit.
A block map $\mathbb{N}\to\mathbb{N}$ partitions fine events into internals (both endpoints in one coarse block) and crosses (endpoints in different blocks). Coarsening promotes crosses via site relabeling; the refinement record keeps the original crosses plus the per-block internals so nothing determined by the fine cell is discarded.
This definition is the reassembly map that mirrors the Python refine / Refinement path in rung_coarsen.py. Conserved functionals (count, cost, spectrum, net flow $\sigma$) are functions of the multiset alone, so exact reassembly is the structural reason coarsening can be called literal.
proof idea
Pure definition: return the multiset sum of the two arguments (crossOrigin + internal). No lemmas, tactics, or side conditions. Downstream proofs unfold this name and rewrite with add_zero or the partition identity cross_add_internal.
why it matters
This is the refine half of the T-1 coarsen/refine pair. roundtrip is defined as refineCell (internalOf block m) (crossOf block m); roundtrip_eq then shows the round-trip is the identity on every cell, which is the Lean discharge of paper theorem T-1 (build_spine.T1_coarsening_exact): the coarse representation is lossless.
Because reassembly returns the identical multiset, every conserved functional is automatically preserved (count, total cost, log-ratio spectrum, $\sigma$). idle_carries_nothing uses the same unfold: when internals vanish, refinement memory is empty and the round-trip collapses to the cross part, so storage scales with recognition activity rather than site count.
In the broader RS ladder picture, exact rung-coarsening supports multi-scale cosmogenesis without inventing or losing ledger content between $\varphi$-rungs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.