netFlow
plain-language theorem explainer
Net flow at a site is the integer excess of outgoing recognition postings over incoming ones in a multiset of directed events. Cosmology and ledger arguments cite it as the local sigma the scale-adaptive engine carries. The body is a two-filter cardinality difference cast to integers; no proof content beyond the definition.
Claim. For a multiset $m$ of directed recognition events and a site $a\in\mathbb{N}$, the net flow is $\mathrm{netFlow}(m,a) := \#\{e\in m: e.\mathrm{source}=a\} - \#\{e\in m: e.\mathrm{target}=a\}\in\mathbb{Z}$.
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. Events partition into internal (both ends in one block) and cross (promoted to the coarse ledger); refine reassembles the original multiset.
An Event is a directed posting source → target carrying a positive ratio; the double-entry reciprocal is implicit. Net flow is the local bookkeeping quantity (out-count minus in-count) that the engine treats as sigma. Structural global conservation sigma = 0 lives at the LedgerForcing layer (cosmic_ledger_conserves); this definition only names the per-site integer used in the T-1 conserved-quantity claims.
proof idea
Pure definition: filter the multiset for events with source equal to the site, take cardinality as an integer, subtract the analogous in-count (target equal to the site). No lemmas, no tactics.
why it matters
Supplies the sigma functional that T-1 must preserve under coarsen-then-refine. Downstream, sigma_preserved is the one-line instance conserved (fun s => netFlow s a), and the T-1 headline plus the CoarseningExact record package that identity with count, cost, spectrum, and cost-partition exactness. The module doc ties this to the North-Star build spine item T1_coarsening_exact: round-trip exactness means a region carried coarse loses nothing reality has determined, including net flow. Structural vanishing of sigma is not proved here; it is imported from FirstTick ledger forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.