t3_law_derived_refinement
plain-language theorem explainer
T-3 packages three facts: lossless reconstruction under a block map forces descent on exactly the blocks that carry internal postings; the law-given predicate (descend iff a block is active) is itself lossless; and every positive tolerance ε fails on some cell with arbitrarily small positive demand. Cosmogenesis and scale-adaptive ledger work cite it to kill free refinement knobs. The proof is a three-conjunct term that applies lossless_iff, lossless_law, and epsilon_unsafe.
Claim. For any block map $\mathrm{block}:\mathbb{N}\to\mathbb{N}$ and multiset of events $m$: (i) for every decidable predicate $D$ on blocks, reconstructing $m$ while refining only blocks in $D$ recovers $m$ if and only if $D$ holds on the block of every internal event of $m$; (ii) reconstructing under the law-given descent set (blocks that carry an internal posting) recovers $m$; (iii) for every $\varepsilon>0$ there exist a multiset $m'$ and a block $b$ such that the recognition demand of $b$ in $m'$ is positive and strictly less than $\varepsilon$, yet the $\varepsilon$-threshold rule fails to reconstruct $m'$.
background
Module T-3 states the law-derived refinement trigger for the scale-adaptive Cosmogenesis engine: the descent threshold is structurally zero, read off the ledger, with no free $\varepsilon$. It sits on the T-1 cell model (Event, internalOf, crossOf, cost) from RungCoarsen. Sigma is identically zero by double-entry, so imbalance never triggers refinement; what forces descent is a posted distinction inside a block.
Recognition demand of a block is the J-cost of its filtered internal postings. The law-given descent predicate holds exactly on blocks that appear as sources of internal events. Reconstruction under a decision $D$ keeps internal structure only on blocks satisfying $D$; losslessness means the reconstructed multiset equals the original.
Upstream: lossless_iff says refining only $D$ is lossless iff $D$ covers every active block. lossless_law says the law-given rule is lossless. epsilon_unsafe builds, via a two-site block map and arbitrarily small positive J-cost, a cell whose $\varepsilon$-rule skips an active block and loses information.
proof idea
Term-mode triple conjunction. First conjunct: for each decidable $D$, apply lossless_iff block D m (reconstruction equals $m$ iff $D$ holds on every internal event's block). Second conjunct: apply lossless_law block m (reconstruction under descendLaw recovers $m$). Third conjunct: for each $\varepsilon>0$, apply epsilon_unsafe ε hε, which itself uses jcost_arbitrarily_small_positive on the two-site map b01 to produce a singleton internal posting with demand in $(0,\varepsilon)$ that the threshold rule skips. No extra algebra in this wrapper.
why it matters
This is the Lean discharge of Cosmogenesis theorem T-3 (build_spine.T3_law_derived_refinement): the refinement trigger is law-derived, threshold identically zero, no knob. It closes the free-parameter risk that a naive refiner would introduce by tuning $\varepsilon$ against recognition demand. Demand is J-cost of forced internal postings; J is the unique cost from the forcing chain (T5), so the zero threshold is not an extra axiom but a readout of the ledger.
Together the three conjuncts say: losslessness forces the active-block set, the law-given rule realizes that set, and every positive cutoff is unsafe because J-cost can be arbitrarily small and positive near ratio one. Used_by is currently empty in the graph; the declaration is the headline packaging for the Python-side numerical check and for any later spine that imports a knob-free refiner. It does not itself invoke T6–T8 or the mass ladder, but it keeps cosmogenesis compatible with the no-free-parameter stance of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.