reconstructUnder
plain-language theorem explainer
Partial reconstruction of a fine multiset of recognition events under a block map and a descent decision D: keep every cross-block posting, and keep an internal posting only when D holds of its block. Cosmology T-3 cites it as the reconstruction operator whose equality with the original multiset forces D to cover every active block. The body is a one-line multiset sum of crossOf with a filtered internalOf.
Claim. Given a block assignment $\mathrm{block}:\mathbb{N}\to\mathbb{N}$, a decidable predicate $D$ on blocks, and a multiset $m$ of recognition events, form the multiset consisting of all cross-block events of $m$ together with those internal events whose source block satisfies $D$. Blocks with $\neg D$ contribute none of their internal postings.
background
Module T-3 (law-derived refinement trigger) removes the free tolerance $\varepsilon$ from scale-adaptive cosmogenesis. The cell model lives in RungCoarsen: an Event is a directed posting $\mathrm{source}\to\mathrm{target}$ carrying a positive ratio; double-entry is implicit. Relative to a block map, internalOf keeps events whose endpoints share a block, while crossOf keeps events that cross blocks and are promoted to the coarse cell.
A naive refiner would descend wherever some scalar exceeds a tuned $\varepsilon$. Sigma imbalance cannot be the trigger (identically zero by double-entry). What forces descent is a posted distinction inside a block. The reconstruction operator below is the bookkeeping device that makes "lossless iff $D$ covers every active block" a pure multiset identity, with threshold structurally zero.
proof idea
Definition, not a proof. The right-hand side is the multiset sum of crossOf block m with the filter of internalOf block m on events $e$ such that $D(\mathrm{block}, e.\mathrm{source})$. Cross postings always survive; internal postings survive only on blocks selected by $D$. Downstream theorems unfold this definition and rewrite with multiset filter identities (notably filter_eq_self).
why it matters
This is the reconstruction map that T-3 is about. lossless_iff states that reconstructUnder block D m = m if and only if every internal event has $D$ true on its block, so lossless reconstruction forces the descent set with no slack. lossless_law and descendLaw_necessary then show the law-given rule (descend exactly the active blocks) is lossless and minimal. epsilon_unsafe builds a one-event cell where a positive $\varepsilon$-threshold skips an active block and the reconstruction is lossy. Those facts package into LawGivenTrigger and the headline t3_law_derived_refinement: the refinement threshold is structurally zero, read off the ledger, with no knob. Framework role: closes the free-parameter risk in the scale-adaptive Cosmogenesis spine (build_spine.T3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.