b01_one
plain-language theorem explainer
The two-site block map sends natural-number site 1 to coarse block 0. Anyone simplifying identities that use this standard test partition of sites will cite the lemma. The proof is a one-line simp that unfolds the piecewise definition.
Claim. Let $b_{01}:\mathbb{N}\to\mathbb{N}$ be the two-site block map with $b_{01}(s)=0$ for $s\le 1$ and $b_{01}(s)=1$ otherwise. Then $b_{01}(1)=0$.
background
Module T-3 treats the refinement trigger of the scale-adaptive Cosmogenesis engine: a block is descended exactly when its recognition demand is positive, so the threshold is structurally zero and no free $\varepsilon$ appears. Demand is the J-cost of forced internal postings on the cell model from RungCoarsen (events, internal and cross postings, additive cost).
The two-site block map $b_{01}$ is a concrete test partition used in that development: sites $0$ and $1$ collapse to coarse block $0$, and every larger site goes to block $1$. Evaluating it at the boundary site $1$ is the elementary fact recorded here; the companion evaluation at $0$ is the sibling zero case.
proof idea
One-line wrapper: simp [b01] unfolds the definition $b_{01}(s)=\mathbf{1}{s\le 1}\cdot 0+\mathbf{1}{s>1}\cdot 1$ and discharges $1\le 1$, yielding $0$.
why it matters
T-3 removes the knob risk in refinement: descend iff recognition demand $>0$, equivalently iff the block carries an internal posting (lossless_iff, lossless_law, descendLaw_necessary). The map $b_{01}$ supplies a minimal two-block test geometry for those identities and for the claim that no positive threshold is safe (jcost_arbitrarily_small_positive). This simp fact keeps boundary evaluations of that geometry definitionally clean. No downstream theorems currently depend on it; it is local bookkeeping inside the T-3 module rather than a forcing-chain landmark (T5--T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.