demand
plain-language theorem explainer
Per-block recognition demand is the total J-cost of internal postings whose source lands in a given coarse block. Cosmogenesis T-3 cites it as the scalar the law-given refine rule reads: descend exactly when demand is positive. The definition filters internal events to that block and sums the RS cost J on their ratios. No proof content; pure construction used by the zero-threshold and epsilon-unsafe arguments.
Claim. Given a block map $B:\mathbb{N}\to\mathbb{N}$, a multiset $m$ of recognition events (directed postings with positive ratios), and a block index $b$, the recognition demand is the total cost $$\mathrm{demand}(B,m,b)=\sum J(r_e)$$ over internal events $e\in m$ with both endpoints in one block and $B(\mathrm{source}(e))=b$, where $J(x)=(x+x^{-1})/2-1$.
background
Module T-3 removes the free tolerance knob from scale-adaptive cosmogenesis. A naive refiner descends when some scalar exceeds a tuned $\varepsilon$; the north-star plan forbids that parameter. Sigma imbalance is identically zero by double-entry, so the trigger must be a posted distinction inside a block.
An Event is a directed posting source$\to$target carrying a positive ratio. Under a block map, internalOf keeps events whose endpoints share a coarse block; cost sums a ratio weight over a multiset. The local weight is the RS recognition cost $J(x)=(x+x^{-1})/2-1$ (also written $\cosh(\log x)-1$), forced unique at T5 of the foundation chain and positive exactly when the ratio is not one.
Demand packages those pieces: take internal events, keep those whose source block equals $b$, and sum $J$ on their ratios. That scalar is what the law-given rule reads.
proof idea
Definition only: compose three upstream constructors. Restrict the multiset to internal events via internalOf, filter further to those with block e.source = b, then apply cost at weight Jcost. No lemmas, no tactics; the body is a one-line composition of filter and sum.
why it matters
This is the quantity named in the T-3 law: descend a block iff recognition demand is strictly positive (threshold structurally zero, read off the ledger). Downstream, epsilon_unsafe and jcost_arbitrarily_small_positive show every positive $\varepsilon$ skips some active block of demand in $(0,\varepsilon)$, so reconstruction is lossy. The headline t3_law_derived_refinement packages that with lossless_iff and lossless_law / descendLaw_necessary: lossless reconstruction forces descent exactly on blocks carrying internal postings.
In the broader RS frame this closes the cosmogenesis refine trigger without introducing a free scale. $J$ is the T5 unique cost; the argument uses that $J$ can be arbitrarily small and positive near ratio one. Sibling uses include cost_singleton (single-event reduction) and cross-module references that need the same demand scalar.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.