descendLaw
plain-language theorem explainer
Defines the law-given descent predicate on a coarse block: a block is marked for descent exactly when it contains at least one internal recognition event. Cosmogenesis and T-3 cite it as the zero-threshold refine rule with no free ε. The body is a one-line membership check after mapping internal events to their block labels.
Claim. Given a block assignment $B:\mathbb{N}\to\mathbb{N}$ and a multiset $m$ of directed recognition events, a block label $b$ satisfies the law-given descent predicate if and only if $b=B(s)$ for the source $s$ of some event in $m$ whose both endpoints lie in the same $B$-block (an internal posting).
background
Module T-3 removes the free refine threshold from the scale-adaptive Cosmogenesis engine. A naive refiner descends when a scalar exceeds a tuned $\varepsilon$; that $\varepsilon$ is forbidden. Sigma imbalance is identically zero by double-entry, so the only forced trigger is a posted distinction inside a block.
From RungCoarsen, an Event is a directed posting $\mathrm{source}\to\mathrm{target}$ with positive ratio. internalOf keeps those events whose endpoints share one coarse block (absorbed into the block summary); cross-block events are promoted. Recognition demand of a block is the $J$-cost of its forced internal postings.
The law-given rule is: descend a block iff recognition demand is positive, i.e. iff a distinction is forced. The threshold is structurally zero, read off the ledger.
proof idea
Definition, not a proof. The predicate holds of block label $b$ precisely when $b$ appears in the image of internalOf block m under the map sending each internal event to the block of its source. Equivalently: there exists an internal event whose source lands in $b$. No tactics; pure Prop abbreviation of that membership.
why it matters
This is the named decision set that T-3 proves is forced. Downstream, lossless_law shows reconstructing under exactly this predicate recovers $m$ with zero loss; descendLaw_necessary shows every lossless decision must contain it (minimality). Both feed the LawGivenTrigger record and the headline t3_law_derived_refinement: lossless reconstruction forces descent on exactly the active blocks, the law-given rule is lossless and minimal, and no positive $\varepsilon$ is safe because $J$-cost of a forced posting can be arbitrarily small.
In the Cosmogenesis north-star spine this closes the knob risk: the refine trigger is law-derived at threshold zero, not a free parameter. It sits on the T-1 cell model (Event, internalOf, cost/cross decomposition) and underwrites scale-adaptive refinement without introducing new constants beyond the RS $J$-cost already fixed by the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.