lossless_law
plain-language theorem explainer
Descending exactly the blocks that carry internal postings reconstructs the fine cell with zero loss. Cosmogenesis and T-3 cite this as the positive half of the law-given refinement rule (threshold structurally zero). The proof is a short rewrite through the lossless characterization plus the definition of the law-given descent predicate.
Claim. For any block map $\mathrm{block}:\mathbb{N}\to\mathbb{N}$ and any multiset $m$ of recognition events, reconstructing under the law-given descent rule (descend a block iff it carries an internal posting) recovers $m$ exactly: $\mathrm{reconstruct}(\mathrm{block},\,D_{\mathrm{law}},\,m)=m$.
background
Module T-3 removes the free tolerance $\varepsilon$ from scale-adaptive cosmogenesis refinement. A cell is a multiset of directed recognition events (source, target, positive ratio). The block map coarsens endpoints; internal postings stay inside one coarse block, cross-block postings bridge blocks.
Reconstruction under a decision $D$ keeps every cross event and expands internal postings only for blocks where $D$ holds. A skipped active block drops its internals, so the reconstructed multiset is strictly smaller than $m$.
Upstream, lossless_iff states that reconstruction equals $m$ if and only if $D$ covers every block that carries an internal posting. The law-given predicate descendLaw is exactly membership in the image of those internal sources under the block map: descend iff the block is active.
proof idea
One short term/tactic proof. Rewrite the goal with lossless_iff, reducing losslessness to: every internal event $e$ has $D(\mathrm{block},e.\mathrm{source})$ for $D=\mathrm{descendLaw}$. Unfolding that predicate, the goal is membership of $\mathrm{block},e.\mathrm{source}$ in the mapped multiset of internal sources. Discharge by Multiset.mem_map with witness $e$, the given membership, and rfl on the block image.
why it matters
This is the constructive half of T-3: the ledger-read rule (descend exactly where recognition demand is positive) is lossless, so the refinement threshold is forced to zero with no knob. It is packaged into lawGivenTrigger as the law_lossless field, and into the headline t3_law_derived_refinement as the second conjunct (law-given reconstruction equals $m$). Together with necessity (descendLaw_necessary) and the arbitrarily-small positive J-cost argument (epsilon_unsafe), it closes the claim that only the zero threshold is safe. In the Cosmogenesis spine this is build_spine.T3_law_derived_refinement; it sits on the T-1 cell model from RungCoarsen and the J-cost demand of forced internal postings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.