b01_zero
plain-language theorem explainer
The two-site coarsening map that sends sites 0 and 1 to coarse block 0 evaluates to 0 at site 0. Anyone working the T-3 refinement-trigger examples that use this fixed block partition will cite the simp fact. The proof is a one-line unfolding of the piecewise definition.
Claim. Let $b_{01}:\mathbb{N}\to\mathbb{N}$ be the two-site block map with $b_{01}(s)=0$ when $s\le 1$ and $b_{01}(s)=1$ otherwise. Then $b_{01}(0)=0$.
background
Module T-3 (law-derived refinement trigger) removes any free tolerance $\varepsilon$ from block descent: a block is refined exactly when its recognition demand is positive, i.e. when it carries a forced internal posting. Demand is the J-cost of those postings; the threshold is structurally zero.
The supporting cell model lives in RungCoarsen (events, internal and cross postings, cost). Inside this module, $b_{01}$ is a concrete two-site partition used as a test map: sites $0,1$ collapse to coarse block $0$, and every larger site goes to block $1$. The present fact pins the value of that map at the origin site.
proof idea
One-line wrapper: simp [b01] unfolds the definition $b_{01}(s)=\mathbf{1}_{s>1}$ (equivalently the if s ≤ 1 then 0 else 1 clause). The hypothesis $0\le 1$ fires the first branch, yielding $0$.
why it matters
T-3 asserts that lossless reconstruction forces descent exactly on blocks with positive internal demand, so the threshold is forced to zero with no knob (lossless_iff, lossless_law, descendLaw_necessary). The map $b_{01}$ is a minimal working partition for those arguments and for the companion facts that no positive $\varepsilon$ is safe.
This simp lemma is local plumbing: it keeps evaluations of $b_{01}$ at site $0$ automatic. No downstream theorem currently lists it as a dependency; it supports readable case analysis on the fixed two-site example rather than a named paper proposition by itself. Framework landmarks nearby are the J-cost demand and the zero-threshold rule, not the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.