firstBitFamily
plain-language theorem explainer
The one-coordinate Boolean family is the singleton set of recognizers consisting of the first-bit projection on Bool × Bool. It is the minimal counterexample family used to show that a single Boolean distinction does not separate states. Downstream completeness audits cite it when proving that one bit is not a complete recognition signature. The body is a direct set comprehension around the first-coordinate map.
Claim. Let the toy state space be $X = \mathbb{B} \times \mathbb{B}$. Write $\pi_1 : X \to \mathbb{B}$ for the first-coordinate projection. The one-coordinate Boolean family is the singleton $\mathcal{F}_1 = \{\pi_1\}$ of Boolean-valued recognizers on $X$.
background
This module records the Lean-level correction from 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, when it exists, is a family of recognizers and its full signature.
Physical identification is equality of the full recognition signature; every admitted observable descends to the quotient; a separating family gives an injective projection. Scalar-cost equality is a complete gauge invariant only under a separate completeness hypothesis, not by default.
The toy state space is $\mathrm{Bool} \times \mathrm{Bool}$, introduced for the "one Boolean cannot encode everything" counterexample. The first-coordinate recognizer is $\pi_1(x) = x.1$. This definition packages that single map as a family of observables, the object on which signature equality is later tested.
proof idea
Pure definition by set comprehension: the family is the singleton ${f \mid f = \pi_1}$, i.e. exactly the first-coordinate projection as a map $X \to \mathrm{Bool}$. No lemmas, no tactics, no proof obligations.
why it matters
Supplies the family argument to one_boolean_coordinate_not_complete, which exhibits two distinct two-bit states with equal first bit and therefore the same recognition signature under this family. That existence statement is the one_bit_not_complete field of the audit structure BooleanShadowCompletenessBoundary.
In the Recognition forcing chain, T0 is the atomic recognition floor. This definition is the concrete one-bit family showing that floor is incomplete as a full signature on a two-bit space, while the two-coordinate recognizers do separate. The module status is zero sorry and zero project axiom; the definition is scaffolding only in the sense that it is the named input to those completeness boundary certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.