sameBlock
plain-language theorem explainer
A recognition event is internal to a coarse block when the block map sends its source and target to the same coarse site. Cosmogenesis T-1 uses this predicate to partition a cell's multiset into absorbed internal postings versus promoted cross-block edges. The definition is a bare equality of block labels, with a decidability instance for Multiset.filter.
Claim. Given a block map $b:\mathbb{N}\to\mathbb{N}$ and a recognition event $e$ with endpoints $\mathrm{source}(e)$ and $\mathrm{target}(e)$, the predicate $\mathrm{sameBlock}(b,e)$ holds if and only if $b(\mathrm{source}(e))=b(\mathrm{target}(e))$.
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:\mathbb{N}\to\mathbb{N}$ sends fine sites to coarse sites. Coarsening one phi-rung partitions that multiset into internal postings (both endpoints in one block) and cross postings (endpoints in different blocks).
An Event is a directed posting $\mathrm{source}\to\mathrm{target}$ carrying a positive real ratio; the double-entry reciprocal is implicit. The block map is an arbitrary function on site indices; equality of the two images is exactly the internal/cross cut used by the Python reference (rung_coarsen.py).
This predicate is the Boolean test that Multiset.filter applies when building the internal and cross parts of a cell.
proof idea
Definitional: the body is the propositional equality block e.source = block e.target. A companion DecidablePred instance reduces decidability to equality of natural numbers, so Multiset.filter can split a cell without classical choice.
why it matters
This cut is the structural hinge of T-1 (rung-coarsening is sigma-exact and cost-exact). Downstream, internalOf filters with the predicate and crossOf filters with its negation; cross_add_internal then recovers the original multiset via Multiset.filter_add_not, which is the algebraic engine of the round-trip identity and of every conserved functional (count, cost, spectrum, sigma).
RefineTrigger.epsilon_unsafe also depends on internal postings: it shows that any positive demand threshold skips some active internal block, so only the zero threshold is law-given. In the broader RS picture this is the discrete bookkeeping that lets coarsening climb the phi-ladder without losing ledger content.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.