descendLaw_necessary
plain-language theorem explainer
Any lossless reconstruction decision must cover every block that carries an internal posting; you cannot skip an active block. Cosmologists citing T-3 (law-derived refinement, threshold forced to zero) use this for minimality of the law-given rule. The proof unpacks the descent predicate via multiset membership and applies the lossless characterization.
Claim. Fix a block map, a decidable decision predicate $D$ on blocks, and a multiset $m$ of events. If reconstructing $m$ while refining only the blocks selected by $D$ recovers $m$ exactly, then every block $b$ that carries an internal posting (the law-given descent condition) satisfies $D(b)$.
background
Module T-3 removes the free tolerance $\varepsilon$ from scale-adaptive cosmogenesis refinement. A naive refiner descends wherever some scalar exceeds a tuned threshold; that $\varepsilon$ is forbidden by the north-star plan. Double-entry keeps sigma identically zero, so imbalance never triggers. What forces descent is a posted distinction inside a block.
Events split into cross-block and internal postings under a block map. Reconstruction under a decision $D$ keeps all cross events and expands internal postings only for blocks where $D$ holds; a block left coarse contributes none of its internals. The law-given descent predicate holds of a block exactly when that block appears as the image of some internal event's source (i.e., the block carries a posting).
Upstream, the lossless characterization states that reconstruction under $D$ recovers $m$ if and only if $D$ covers every block that carries an internal posting. Demand is the recognition cost (sum of $J$-costs of ratios) of a block's internal postings; the present lemma is the minimality half of the law-given package, before cost enters.
proof idea
Tactic proof, four steps. Introduce a block $b$ and the hypothesis that the law-given descent predicate holds of $b$. Unpack that hypothesis via multiset membership in the image: there is an internal event $e$ whose source maps to $b$. Apply the forward direction of the lossless characterization to the reconstruction hypothesis, at that event $e$, to obtain $D$ at the block of $e$'s source. Rewrite along the equality that identifies that block with $b$.
why it matters
This is the minimality half of T-3 in the scale-adaptive Cosmogenesis spine (build_spine.T3_law_derived_refinement). Together with the matching lossless half (descend exactly the active blocks recovers the cell), it shows the law-given rule is forced: threshold structurally zero, read off the ledger, no knob.
Downstream it is wired directly into the structure package lawGivenTrigger as the law_minimal field: for every cell and block map, any lossless decision contains the law-given descent set. That package is the theorem-backed discharge of T-3. The companion results (arbitrarily small positive $J$-cost; every positive $\varepsilon$ unsafe) then pin uniqueness of the zero threshold. Framework-wise this is local to the cosmology rung-coarsen engine, not a T0–T8 forcing step, but it removes the last free parameter from the refinement trigger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.