one_boolean_coordinate_not_complete
plain-language theorem explainer
A single Boolean coordinate on the two-bit state space Bool × Bool fails to separate states: there exist distinct pairs that agree on the first bit. Anyone citing the T0 Boolean-shadow boundary or arguing that atomic recognition is not a complete gauge will use this. The proof is a direct witness: (false,false) and (false,true) differ, yet every observable in the first-bit family returns the same value.
Claim. There exist distinct states $x,y \in \{0,1\}\times\{0,1\}$ that are observationally equivalent under the one-coordinate family consisting of the first-bit map alone: every admitted observable in that family takes the same value at $x$ and at $y$.
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 of a family of observables; every admitted observable descends to that quotient; a separating family yields an injective projection.
PairBoolState is the toy space $\mathrm{Bool}\times\mathrm{Bool}$ used for the incompleteness counterexample. SameRecognitionSignature $F,x,y$ is observational equivalence under every map in the family $F$ (named in the T0 language). The first-bit family is the singleton family whose only recognizer reads the first coordinate.
The surrounding development stresses that scalar-cost equality is a complete gauge invariant only under an extra completeness hypothesis, not by default. One Boolean coordinate is incomplete on this space; the two-coordinate family does separate.
proof idea
Term-mode existence proof by explicit witness. Instantiate $x=(\mathsf{false},\mathsf{false})$ and $y=(\mathsf{false},\mathsf{true})$. Inequality is discharged by decide. Same-signature membership is an intro over the family: any $f$ in the first-bit family equals the first-bit map, and rewriting reduces both sides to rfl on the shared first coordinate.
why it matters
This is the concrete incompleteness half of the corrected T0 boundary. Downstream, booleanShadowCompletenessBoundary_holds packages it as the field one_bit_not_complete of BooleanShadowCompletenessBoundary, together with the matching scalar-cost incompleteness, two-bit injectivity, and exactness of the full-signature quotient.
In the Recognition forcing chain the point is foundational rather than numerical: T0-level recognition starts from atomic distinctions, but the physical quotient is the full signature, not a single bit. The result blocks the false claim that one Boolean coordinate (or its scalar cost) already gauges the state space. Status in-module is 0 sorry and 0 project axiom; the certificate theorem is the parent that cites this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.