pairBitFamily
plain-language theorem explainer
The two-coordinate Boolean family is the set of the two projections Bool×Bool → Bool. It is the complete recognizer family for the toy two-bit state space in the T0 Boolean-shadow audit. Anyone citing separation or injectivity of the full signature projection on that space uses this set. The body is a two-element set comprehension of the coordinate maps.
Claim. The two-coordinate Boolean family is the set $\{\pi_1,\pi_2\}$ of coordinate projections $\pi_i:\mathbb{B}\times\mathbb{B}\to\mathbb{B}$, where $\pi_1(x,y)=x$ and $\pi_2(x,y)=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. Physical identification is equality of the full recognition signature; admitted observables descend to the quotient; a separating family yields an injective projection.
The toy state space is $\mathbb{B}\times\mathbb{B}$. The first and second coordinate recognizers are the maps $(x,y)\mapsto x$ and $(x,y)\mapsto y$. The one-coordinate family is incomplete on this space; the two-coordinate family is the natural candidate for a complete signature.
Upstream quotient machinery from PrimitiveRecognitionCalculus.QuotientSelection supplies SameRecognitionSignature, projection, and the separating-implies-injective lemma used downstream.
proof idea
Pure definition: the set of functions $f:\mathbb{B}\times\mathbb{B}\to\mathbb{B}$ equal to either coordinate projection. No proof obligations; the body is the set comprehension ${f\mid f=\pi_1\lor f=\pi_2}$.
why it matters
This family is the positive half of the T0 Boolean-shadow correction. Downstream, pairBitFamily_separating shows the two coordinates separate all states of $\mathbb{B}\times\mathbb{B}$, and pairBitFamily_projection_injective concludes that the physical quotient map is injective: two Boolean recognizers recover the whole two-bit toy state.
BooleanShadowCompletenessBoundary packages the contrast: one Boolean coordinate is not complete in general, while this two-coordinate family is. That boundary is the Lean-level record that scalar-cost equality and single-bit shadows are incomplete gauge invariants unless a separate completeness hypothesis holds. It sits at the T0 floor of the forcing chain: one bit is atomic recognition, not a full signature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.