firstBit
plain-language theorem explainer
The first-coordinate projection on the toy space Bool × Bool, used as a single Boolean recognizer. Anyone citing the one-bit incompleteness counterexample or the two-bit separating family needs this map. The body is the pure first-projection lambda.
Claim. Define the first-coordinate recognizer $b_1 : \mathrm{Bool}\times\mathrm{Bool}\to\mathrm{Bool}$ by $b_1(x_1,x_2)=x_1$.
background
The module fixes the T-1/T0 Boolean-shadow audit: a single Boolean distinction is an atomic recognition floor, not a complete encoding of an arbitrary state space. Physical identification is equality of the full recognition signature; observables must descend to that quotient; only a separating family yields an injective projection.
PairBoolState is the toy carrier $\mathrm{Bool}\times\mathrm{Bool}$ built exactly for the counterexample that one Boolean cannot encode everything. A recognizer here is any map from that carrier into $\mathrm{Bool}$. The first-coordinate map is the simplest nontrivial such recognizer.
Downstream, the one-element family generated by this map fails to separate states that share the first bit, while adjoining the second-coordinate map restores separation.
proof idea
Pure definition: the function is the first projection $\pi_1$ on the product type, written as fun x => x.1. No lemmas or tactics.
why it matters
This map is the generator of the one-coordinate family used to prove that a single Boolean coordinate is not complete on $\mathrm{Bool}\times\mathrm{Bool}$. It also appears in the two-coordinate family that does separate all states.
Those two facts underwrite the module's T0 boundary claim: the complete observable object is a family of recognizers and its full signature, not one bit. The result feeds the gauge-quotient story already present in PrimitiveRecognitionCalculus.QuotientSelection (signature equality as physical identification, descent of observables, injectivity from separating families). It is the concrete witness that scalar or one-bit data is incomplete without an extra completeness hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.