count_preserved
plain-language theorem explainer
Event cardinality is invariant under one-rung coarsen-then-refine: the multiset of recognition events returns with the same card. Cosmogenesis and scale-adaptive ledger work cite it as the count instance of T-1 exactness. The proof is a one-line specialization of the general conserved-functional lemma to Multiset.card.
Claim. For any block map $b:\mathbb{N}\to\mathbb{N}$ and any multiset $m$ of recognition events, $\mathrm{card}(\mathrm{roundtrip}(b,m))=\mathrm{card}(m)$, where roundtrip coarsens one $\varphi$-rung by $b$ and then refines back.
background
Module T-1 formalizes rung-coarsening for the scale-adaptive Cosmogenesis engine: a recognition cell is a multiset of canonical events (directed postings source→target with positive ratio). A block map $b:\mathbb{N}\to\mathbb{N}$ partitions fine sites into coarse sites. Events split into internal (both endpoints in one block) and cross (endpoints in different blocks); coarsening promotes cross events by relabeling endpoints, and refinement reassembles the original multiset from the refinement record.
The key upstream fact is that roundtrip is the identity on multisets (roundtrip_eq), so every functional of the cell is unchanged. The general lemma conserved states: for any $F$, $F(\mathrm{roundtrip}(b,m))=F(m)$. Here $F$ is event count, defined as multiset cardinality. That is the content of T-1's "count exact" clause in the Cosmogenesis spine.
proof idea
One-line wrapper: apply conserved at the functional count (i.e. Multiset.card). Under the hood, conserved is congrArg F (roundtrip_eq block m), so the equality of cards is just transport of the round-trip identity along cardinality. No separate counting argument is needed.
why it matters
Feeds the count field of coarseningExact and the second conjunct of the T-1 headline t1_coarsening_exact: coarsen one phi-rung and refine back, and event count (with cost, spectrum, and net flow) returns identical. That is what earns "literal" for the scale-adaptive engine: a region carried coarse loses nothing reality has determined about how many recognition events it holds.
In the Cosmogenesis plan this is the Lean discharge of the Python-checked round-trip exactness on voxel batteries. It sits under the broader Recognition ledger picture (double-entry, conserved functionals) rather than the T0–T8 forcing chain itself, but it is the count instance that makes rung changes sigma- and cost-exact in the cosmology layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.