pairBitFamily_projection_injective
plain-language theorem explainer
The projection of the two-bit toy space onto its physical quotient by the two-coordinate Boolean family is injective: equal full signatures force equal states. Anyone citing the T0 Boolean-shadow completeness boundary uses this as the positive half of the story (two bits separate; one bit does not). The proof is a one-line application of the general separating-family injectivity lemma to the already-proved separation of the pair-bit family.
Claim. The gauge projection $\mathrm{proj}_{F}$ associated to the two-coordinate Boolean family $F=\{\pi_1,\pi_2\}$ on $\mathrm{Bool}\times\mathrm{Bool}$ is injective: if two two-bit states have the same recognition signature under $F$, then they are equal.
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 of an admitted family of observables; the forced quotient collapses exactly the indistinguishable pairs.
The projection $\mathrm{proj},F:X\to\mathrm{PhysicalQuotient},F$ sends a state to its gauge class under the indistinguishability setoid of $F$. Upstream, if $F$ separates points (equal signatures imply equal states), then $\mathrm{proj},F$ is injective. That is the precise complete-recognizer-family condition.
Here $X=\mathrm{Bool}\times\mathrm{Bool}$ and $F$ is the two-coordinate family ${\mathrm{firstBit},\mathrm{secondBit}}$. A sibling lemma already shows this $F$ separates every pair of two-bit states. One Boolean coordinate alone fails to separate, which is the negative half of the same boundary.
proof idea
One-line term wrapper. Apply the general lemma that a separating recognition family yields an injective quotient projection, instantiated at the two-coordinate Boolean family, using the already-established fact that those two coordinate recognizers separate all states of $\mathrm{Bool}\times\mathrm{Bool}$. No further case analysis is needed at this site.
why it matters
This is the positive injectivity half of the corrected T0 Boolean-shadow completeness boundary. Downstream it is wired directly into the audit certificate booleanShadowCompletenessBoundary_holds, which packages: one bit is atomic not complete; scalar-cost equality is not a complete gauge invariant without an extra hypothesis; the two-bit signature projection is injective; and the full-signature quotient is exact.
In the Recognition forcing chain this sits at the T0 floor: recognition begins with Boolean distinctions, but completeness of the physical quotient requires a separating family, not a single bit. The result closes the Lean-level correction that one Boolean coordinate is incomplete on the two-bit toy space while the two-coordinate family recovers the whole state.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.