lossless_iff
plain-language theorem explainer
Lossless reconstruction under a block decision D holds exactly when D covers every block that carries an internal posting. Cosmogenesis and scale-adaptive refinement cite this as the forcing that the descent set is unique: no tunable slack. The proof unfolds the reconstruction, rewrites equality as a filter-identity, and cancels the cross-block summand via the cross/internal partition.
Claim. For a block map $\mathrm{block}:\mathbb{N}\to\mathbb{N}$, a decidable predicate $D$ on blocks, and a multiset $m$ of recognition events, the reconstruction that keeps all cross-block events and expands internal postings only on blocks in $D$ recovers $m$ if and only if every internal event $e\in m$ has $D(\mathrm{block}(e.\mathrm{source}))$.
background
Module T-3 discharges the claim that the cosmogenesis refinement trigger is law-derived: the threshold is structurally zero, with no free $\varepsilon$. The cell model lives in RungCoarsen. An Event is a directed posting $\mathrm{source}\to\mathrm{target}$ carrying a positive ratio. Given a block map, crossOf keeps events whose endpoints lie in different blocks; internalOf keeps same-block postings. Their sum is the whole cell: cross_add_internal states $\mathrm{crossOf}+\mathrm{internalOf}=m$.
reconstructUnder rebuilds the fine cell while refining only blocks selected by $D$: it always keeps the cross part, and filters the internal part to those $e$ with $D(\mathrm{block}(e.\mathrm{source}))$. A block left coarse contributes none of its internal postings. The module doc frames the knob risk: a naive refiner descends where a scalar exceeds a tuned tolerance; here sigma is identically zero by double-entry, so only a posted distinction inside a block can force descent.
proof idea
Unfold reconstructUnder to $\mathrm{crossOf}+(\mathrm{internalOf}).\mathrm{filter},D$. Rewrite the target equality as the Multiset identity that a filter equals the original multiset. Split the biconditional.
Forward: from reconstruction equals $m$, replace the filtered internal summand and use cross_add_internal (symmetrized) to obtain $\mathrm{cross}+\mathrm{filter}=\mathrm{cross}+\mathrm{internal}$; cancel the common cross summand by left-cancellation of multiset addition.
Reverse: if every internal event already satisfies $D$ on its source block, the filter is the identity on internalOf, so reconstruction collapses exactly to cross_add_internal.
why it matters
This is the first bullet of T-3 in the scale-adaptive Cosmogenesis spine: the threshold is forced to zero. Doc-comment: "There is no tunable slack: lossless reconstruction requires descending exactly the active blocks."
Downstream, lossless_law instantiates $D$ as the law-given descent predicate (descend iff the block carries an internal posting) and gets zero loss in one rewrite. descendLaw_necessary uses the forward direction to prove minimality: any lossless $D$ must contain every active block. Both feed lawGivenTrigger, whose threshold_forced field is literally this biconditional, and the headline t3_law_derived_refinement. Together with epsilon_unsafe (no positive J-cost threshold is safe), it removes the free $\varepsilon$ from the refiner and pins the recognition demand trigger at structural zero on the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.