crossOf
plain-language theorem explainer
Cross-block events are the subset of a recognition cell whose endpoints fall in different blocks under a site-to-block map. Cosmogenesis coarsening cites this partition half when building the coarse ledger and when proving round-trip identity. The body is a one-line multiset filter: keep events that fail the same-block predicate.
Claim. Given a block map $\mathrm{block}:\mathbb{N}\to\mathbb{N}$ and a multiset $m$ of recognition events (each a directed posting $\mathrm{source}\to\mathrm{target}$ with ratio $r>0$), the cross-block part is $\{e\in m:\mathrm{block}(e.\mathrm{source})\neq\mathrm{block}(e.\mathrm{target})\}$ as a multiset.
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 sends fine sites to coarse sites. Coarsening one phi-rung partitions that multiset into internal events (both endpoints in one block, absorbed into a block summary) and cross-block events (endpoints in different blocks).
An event is a directed posting source → target carrying a positive real ratio; double-entry reciprocity is implicit. The same-block predicate holds exactly when the two endpoints map to one coarse site. Cross-block events are the complementary filter: they are promoted to the coarser rung, with ratios kept as recognition content.
The companion internal filter and the recombination identity (cross plus internal equals the original multiset) are the partition that makes coarsening "literal": nothing reality has determined is discarded.
proof idea
Definitional one-liner. Unfold to multiset filter of $m$ by the negation of the same-block predicate on the given block map. Decidability of same-block (equality of natural numbers after applying the block map to source and target) supplies the filter instance. No lemmas beyond that predicate and Multiset.filter.
why it matters
This is one half of the T-1 partition in the Cosmogenesis north-star plan (build_spine.T1_coarsening_exact). The coarse ledger is exactly the image of these cross events under endpoint relabeling to coarse sites, so every coarser-rung evolution step is built from this set.
Downstream, recombination (cross_add_internal) and round-trip identity rest on filter-plus-complement; cost equality for the coarse ledger reduces to cost on the cross multiset because relabeling preserves ratios. Refine-trigger reconstruction keeps all cross events unconditionally and only selectively expands internals, so lossless descent theorems (lossless_iff, epsilon_unsafe) quantify over this fixed cross skeleton.
In the broader RS picture this is bookkeeping for exact rung moves on the phi-ladder: conserved functionals (count, cost, spectrum, net flow/sigma) survive coarsening because the partition is multiset-exact, not approximate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.