b01
plain-language theorem explainer
Canonical two-site block partition on natural-number sites: 0 and 1 collapse to coarse block 0, every larger site goes to block 1. Cosmology and forcing-bridge proofs cite it as the concrete block map when stating demand, lossless reconstruction, and the T-3 zero-threshold claim. The body is a one-line piecewise definition.
Claim. Define $b_{01}:\mathbb{N}\to\mathbb{N}$ by $b_{01}(s)=0$ whenever $s\le 1$, and $b_{01}(s)=1$ for all $s\ge 2$. Sites $0$ and $1$ share one coarse block; every other site is its own second block.
background
Module T-3 treats law-derived refinement in the scale-adaptive cosmogenesis engine. A naive refiner would descend when a scalar exceeds a tuned tolerance $\varepsilon$; that $\varepsilon$ is the free knob the north star forbids. Double-entry keeps sigma identically zero, so imbalance never triggers descent. What forces descent is a posted distinction inside a block: recognition demand is the J-cost of forced internal postings, and the law-given rule is descend exactly when that demand is positive (threshold structurally zero).
The block map is the partition of event sites into coarse blocks. Demand, reconstruction under a decision predicate, and the lossless characterizations are all parameterized by such a map. The two-site map $b_{01}$ is the standard concrete instance used to exhibit arbitrarily small positive J-cost and to discharge the T-3 headline.
proof idea
Pure definition: the function is the piecewise rule if s ≤ 1 then 0 else 1. No lemmas, no tactics. Downstream simp lemmas unfold the two base cases at 0 and 1.
why it matters
Feeds the concrete witnesses in epsilon_unsafe (no positive threshold is safe) and the T-3 headline t3_law_derived_refinement, which packages lossless-iff, the law-given descent rule, and the zero-threshold uniqueness. Those results close the cosmogenesis build-spine item that the refinement trigger is law-derived with no knob. The same identifier also appears in the T-minus-1-to-T1 and complete T-minus-1-to-T8 forcing-chain certificates as the bridge object carrying the T0 fragment, so the two-site map is the running example that links the cosmology refinement story into the global forcing chain (T0 onward).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.