cross_add_internal
plain-language theorem explainer
Cross-block and internal events of a recognition cell form a partition of the cell multiset: their multiset sum is the original cell. Cosmology and scale-adaptive Cosmogenesis proofs cite this as the algebraic recombination step behind T-1. The argument is a short filter identity after unfolding the two parts and commuting addition.
Claim. For any block map $b:\mathbb{N}\to\mathbb{N}$ and any multiset $m$ of recognition events, the multiset of cross-block events (endpoints in different blocks) plus the multiset of internal events (both endpoints in one block) equals $m$.
background
Module T-1 formalizes rung-coarsening for the scale-adaptive Cosmogenesis engine: a recognition cell is a multiset of canonical events, each a directed posting source→target carrying a positive ratio. A block map $b$ sends fine sites to coarse sites and induces a decidable predicate sameBlock: both endpoints land in one coarse block.
From that predicate the cell splits into two filters. Internal events are absorbed into the block summary; cross events are promoted to the coarse ledger (after relabeling endpoints) with the ratio unchanged. The module claim is that this partition is exact, so coarsen/refine is lossless and every multiset functional is conserved.
Upstream, internalOf and crossOf are exactly the complementary filters of $m$ by sameBlock and its negation. Multiset algebra then supplies the recombination identity used here.
proof idea
Unfold crossOf and internalOf to the complementary filters of $m$. Rewrite with commutativity of multiset addition so the order matches the library lemma. Finish by Multiset.filter_add_not applied to the predicate sameBlock b: filtering by a predicate and by its negation, then adding, recovers the original multiset.
why it matters
This is the partition identity that makes T-1 literal. Downstream, roundtrip_eq is a one-line application: refine after coarsen returns the cell unchanged precisely because cross and internal recombine to $m$. That round-trip is what the module means by lossless coarse representation.
cost_partition rewrites through the same identity (after equating coarse cost with cross cost) so fine cost splits exactly into coarse cross-block cost plus internal cost, with no leakage. RefineTrigger.lossless_iff sits on the same partition language: lossless partial refine is forced exactly on blocks that carry internal postings.
In the Cosmogenesis spine this discharges the Lean half of build_spine.T1_coarsening_exact already checked numerically in rung_coarsen.py. It is bookkeeping for the phi-rung ladder rather than a forcing-chain step (T5–T8), but it is the algebraic reason conserved quantities (count, cost, spectrum, sigma) survive a rung change.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.