lawGivenTrigger
plain-language theorem explainer
For every block map and multiset of ledger events, the law-given refinement trigger holds: lossless reconstruction forces descent exactly on active blocks, and the rule "descend iff a posting is forced" is both lossless and minimal. Authors of the scale-adaptive Cosmogenesis spine cite this as the Lean packing of paper theorem T-3 (threshold structurally zero, no free ε). The proof is a three-field term constructor wiring the forced-threshold equivalence, law-given losslessness, and minimality lemmas.
Claim. For every block assignment $\mathrm{block}:\mathbb{N}\to\mathbb{N}$ and every multiset $m$ of events, the law-given trigger model holds: (i) reconstructing under a descent predicate $D$ recovers $m$ if and only if $D$ holds on every block carrying an internal posting of $m$; (ii) the law-given rule (descend a block exactly when it carries a forced internal posting) reconstructs $m$ losslessly; (iii) every lossless descent predicate must contain that law-given rule.
background
Module T-3 removes the free refinement knob from the scale-adaptive Cosmogenesis engine. A naive refiner descends wherever a scalar exceeds a tuned tolerance $\varepsilon$; that $\varepsilon$ is exactly the free parameter the north star forbids. Sigma is identically zero at every rung (double-entry), so imbalance never triggers. What forces descent is a posted distinction inside a block.
The cell model lives in RungCoarsen: an Event carries source, target, and a positive ratio; internalOf / crossOf split postings by whether source and target share a block; cost is the J-cost of a ratio (the Recognition cost $J(x)=(x+x^{-1})/2-1$); demand of a block is the total J-cost of its forced internal postings. Reconstruction under a descent set $D$ keeps only events whose block is selected by $D$.
Upstream, lossless_iff states that reconstruction under $D$ recovers $m$ exactly when $D$ covers every active block. lossless_law shows the concrete rule "descend iff the block carries an internal posting" is lossless. descendLaw_necessary shows every lossless $D$ must contain that rule. (A sibling, epsilon_unsafe, separately kills every positive threshold via arbitrarily small positive J-cost.)
proof idea
Pure term-mode structure constructor: no tactics. The goal is an instance of the three-field record LawGivenTrigger block m.
threshold_forcedis filled byfun D => lossless_iff block D m, the biconditional that lossless reconstruction under $D$ is equivalent to $D$ covering every internal posting's block.law_losslessis filled bylossless_law block m, which already proves reconstruction under the law-given descent predicate recovers $m$.law_minimalis filled byfun D => descendLaw_necessary block D m, which already proves any lossless $D$ must contain every law-given active block.
Each field is therefore a direct application (or eta-expansion) of a prior theorem in the same module; nothing new is proved here beyond packaging.
why it matters
This is the named Lean witness for Cosmogenesis T-3 (build_spine.T3_law_derived_refinement): the refinement threshold is structurally zero, read off the ledger, with no knob to choose. The module headline states the three guarantees packed here (forced descent set, lossless law-given rule, minimality) together with the sibling fact that no positive $\varepsilon$ is safe.
In the Recognition framework this closes the "knob risk" for scale-adaptive refinement: descent is forced exactly where a distinction is posted, so the engine cannot smuggle a free tolerance into the rung-coarsening dynamics. It sits on the T-1 cell model (Event, internal/cross split, J-cost demand) and feeds the law-derived refinement claim of the north-star plan. No downstream Lean consumers are recorded yet; the declaration is the terminal packaging of the T-3 record itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.