pairBitFamily_separating
plain-language theorem explainer
The two coordinate Boolean recognizers separate every state of Bool × Bool: equal full signatures force equal pairs. Anyone citing the T0 Boolean-shadow correction or the injectivity of the two-bit physical quotient needs this lemma. The proof is a short case split that reads each coordinate off the signature via the corresponding recognizer.
Claim. Let $X = \mathrm{Bool} \times \mathrm{Bool}$ and let $F = \{\pi_1, \pi_2\}$ be the family of the two coordinate projections $X \to \mathrm{Bool}$. If $x, y \in X$ have the same recognition signature under $F$ (i.e., $f(x) = f(y)$ for every $f \in F$), then $x = y$.
background
This 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. The complete observable object is a family of recognizers and the full signature it induces. Physical identification is equality of that signature; a separating family yields an injective projection onto the physical quotient.
PairBoolState is the toy space $\mathrm{Bool} \times \mathrm{Bool}$ used as the counterexample that one Boolean coordinate is incomplete. The two-coordinate family consists of the first- and second-coordinate projections. SameRecognitionSignature F x y is observational equivalence under every admitted observable in $F$ (named in the T0 language).
The surrounding quotient machinery (from QuotientSelection) already states that physical identification is signature equality and that every admitted observable descends. What remains for the two-bit toy is to prove the family actually separates.
proof idea
Introduce $x,y$ and the signature hypothesis. Destructure both as pairs $(x_1,x_2)$ and $(y_1,y_2)$. Instantiate the signature hypothesis at the first-coordinate recognizer (membership by left disjunct) to get $x_1 = y_1$, and at the second-coordinate recognizer (right disjunct) to get $x_2 = y_2$. Substitute both equalities and close by reflexivity. No external lemmas beyond the definitions of the family and the two bit maps.
why it matters
This is the positive half of the T0 Boolean-shadow correction: while one Boolean coordinate fails to separate $\mathrm{Bool} \times \mathrm{Bool}$, the two coordinate recognizers do. Downstream, pairBitFamily_projection_injective applies the generic lemma that a separating family gives an injective physical projection, concluding that two Boolean recognizers recover the whole two-bit toy state.
In the Recognition framework this pins the T0 boundary: the atomic recognition floor is one bit, but completeness of the gauge invariant requires a separating family, not a single scalar or single Boolean. It also underwrites the module certificate that scalar-cost equality is complete only under an extra hypothesis, not by default. Status is fully proved (0 sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.