LawGivenTrigger
plain-language theorem explainer
Named Prop record packaging the three T-3 guarantees for law-derived refinement: lossless reconstruction forces descent exactly on active blocks; the law-given rule (descend iff a block carries an internal posting) is lossless and minimal. Cosmogenesis and scale-adaptive engine work cite it as the threshold-free trigger interface. Pure structure definition; the inhabiting theorem wires three prior lemmas into its fields.
Claim. For a block map $\beta:\mathbb{N}\to\mathbb{N}$ and a multiset $m$ of recognition events, the law-given trigger holds when three conditions are met: (i) reconstructing $m$ while refining only blocks selected by a decision $D$ recovers $m$ if and only if $D$ holds of every block that carries an internal posting; (ii) reconstructing under the law-given descent predicate (descend a block iff it has an internal posting) recovers $m$ exactly; (iii) every decision $D$ that reconstructs losslessly must contain the law-given descent set.
background
Module T-3 states that the refinement trigger of the scale-adaptive Cosmogenesis engine is law-derived: the threshold is structurally zero, with no free tolerance $\varepsilon$. The cell model comes from RungCoarsen. An Event is a directed posting source$\to$target carrying a positive ratio. Given a block map, internalOf keeps events whose endpoints lie in one block; crossOf keeps the rest. Reconstructing under a decision $D$ keeps all cross-block 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 marks a block active exactly when it appears as the block of some internal event (positive recognition activity). Recognition demand of a block is the J-cost of its forced internal postings. A naive refiner that descends only when demand exceeds a tuned $\varepsilon$ introduces a free parameter the north star forbids; sigma imbalance is identically zero by double-entry, so it never triggers descent.
Upstream, reconstructUnder is the selective fine-cell rebuild, and descendLaw is the zero-threshold rule. The three field obligations match lossless_iff, lossless_law, and descendLaw_necessary.
proof idea
No proof body: this is a Prop-valued structure, a named record of three fields. threshold_forced is the biconditional that selective reconstruction equals the original multiset iff $D$ covers every active block. law_lossless asserts reconstruction under the law-given descent predicate is the identity on $m$. law_minimal asserts every lossless decision contains the law-given descent set.
The inhabiting theorem lawGivenTrigger fills the fields by direct application of lossless_iff, lossless_law, and descendLaw_necessary respectively; no extra argument is needed beyond those lemmas.
why it matters
This is the Lean interface for theorem T-3 of the Cosmogenesis north-star plan (build_spine.T3_law_derived_refinement): the refinement trigger is law-derived, threshold identically zero, no knob. Downstream, lawGivenTrigger constructs an instance for every block map and every cell, discharging the headline that the model holds universally.
In the framework it removes the free $\varepsilon$ that would otherwise sit between rung coarsening and fine reconstruction. Descent is forced exactly where a distinction is posted inside a block, read off the ledger. Together with the companion facts that J-cost of a forced posting can be arbitrarily small positive, it pins zero as the unique safe threshold. It sits on the T-1 cell model (Event, internal/cross split, cost additivity) and feeds the scale-adaptive engine spine rather than the T0–T8 forcing chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.