secondBit
plain-language theorem explainer
Extracts the second Boolean coordinate from a two-bit toy state. Used to build the two-coordinate recognizer family that separates Bool × Bool, showing one bit is incomplete while two bits suffice. Pure projection definition: second component of the product.
Claim. The second-coordinate recognizer is the map $s \colon \{0,1\} \times \{0,1\} \to \{0,1\}$ given by $s(b_1,b_2) = b_2$.
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; admitted observables descend to the quotient; a separating family yields an injective projection.
PairBoolState is the toy product $\mathrm{Bool} \times \mathrm{Bool}$, introduced precisely as a counterexample space where one Boolean cannot encode everything. The first- and second-coordinate maps are the elementary recognizers on that space. Scalar-cost equality is complete only under an extra hypothesis; one coordinate alone fails separation on this product.
proof idea
Definitional projection: the function sends a pair to its second component. No lemmas or tactics; the body is fun x => x.2.
why it matters
Feeds the two-coordinate family pairBitFamily = {firstBit, secondBit} and the separation theorem that this family separates all states of $\mathrm{Bool} \times \mathrm{Bool}$. That pair of facts is the concrete witness that one Boolean coordinate is incomplete while the full two-bit signature is separating, which is the module's T0-boundary correction: the complete observable object is a family of recognizers, not a single bit. Lands in the foundation layer that links recognition signatures to the quotient theorem in PrimitiveRecognitionCalculus.QuotientSelection.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.