coarseLedger
plain-language theorem explainer
Defines the coarse-rung recognition cell as the multiset of cross-block events with endpoints mapped to coarse sites and ratios left unchanged. Cosmogenesis and rung-coarsening arguments cite it as the object evolved one phi-rung up. The body is a one-line composition of the cross-block filter with endpoint relabeling.
Claim. Given a block map $b:\mathbb{N}\to\mathbb{N}$ and a multiset $m$ of recognition events (each a directed posting $s\to t$ with positive ratio $r$), the coarse ledger is the multiset of those events whose endpoints lie in different blocks, each rewritten as $b(s)\to b(t)$ with the same ratio $r$.
background
Module T-1 formalizes rung-coarsening for the scale-adaptive Cosmogenesis engine: a recognition cell is a multiset of canonical events, and a block map $b$ sends fine sites to coarse sites. Events partition into internal (both endpoints in one block) and cross (endpoints in different blocks).
An Event is a directed posting source → target carrying a positive real ratio; double-entry reciprocity is implicit. crossOf b m keeps only events with endpoints in different blocks. relabel b sends those endpoints to $b(\mathrm{source})$ and $b(\mathrm{target})$ while leaving the ratio fixed, so recognition content is unchanged under the site map.
The coarse ledger is exactly that promoted cross multiset. It is the cell one evolves at the coarser phi-rung; refinement later reassembles original cross events with per-block internals so the round-trip can be the identity.
proof idea
Pure definition, not a proved theorem. The body is the composition
(crossOf block m).map (relabel block):
filter to cross-block events, then map each event by relabeling endpoints to coarse sites and retaining the ratio. No tactics or lemmas beyond those two sibling defs.
why it matters
This is the coarse cell in T-1 ("rung-coarsening is sigma-exact and cost-exact"). Downstream, cost_coarse_eq_cross shows relabeling preserves cost; cost_partition splits fine cost into coarse cross cost plus internal cost with no leakage; CoarseningExact and the headline t1_coarsening_exact package round-trip identity, count/cost/spectrum preservation, and that partition.
In the framework it is the object the scale-adaptive engine evolves one rung up on the phi-ladder: coarsening loses nothing reality has determined ("literal" coarsening). It supports conserved functionals (count, cost, log-ratio spectrum, net flow/sigma) under rung change, tying Cosmology.RungCoarsen to the ledger picture without invoking T5–T8 directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.