one_bit_not_complete_boundary
plain-language theorem explainer
The corrected T0 boundary packages four facts: a single Boolean coordinate is atomic but not complete; scalar cost alone is not complete; a two-bit signature is injective; and the full recognition signature determines states exactly up to the forced quotient. Cite it when arguing that physical content lives in the admitted recognizer family, not in one bit. It is a one-line public alias of the machine-checked Boolean-shadow completeness boundary theorem.
Claim. The corrected T0 completeness boundary holds: (i) one Boolean coordinate does not separate states; (ii) a scalar cost functional alone does not separate states; (iii) a two-bit signature family is injective on the relevant projection; (iv) for any admitted recognizer family $F$, the full signature determines $x$ and $y$ up to the forced indistinguishability quotient. Scalar-cost completeness remains a separate hypothesis.
background
Recognition Core aggregates the T0/T4 layer of the forcing chain: recognizers, their indistinguishability quotients, recognition signatures, and the completeness condition under which a signature determines physically relevant states. The module's stated answer is that a single Boolean observable is atomic, not complete; physical content is carried by the admitted recognizer family.
Upstream, booleanShadowCompletenessBoundary_holds packages the boundary as a structure with four fields: one Boolean coordinate is not complete; first-bit scalar cost is not complete; the pair-bit family projection is injective; and the full signature quotient is exact via the forced-quotient equivalence. Related public targets include the forced quotient iff, gauge-from-indistinguishability, and completeness iff the family separates points.
Notation: a recognizer family induces an indistinguishability relation; the signature is the joint observable map; completeness means that map is injective on the physical quotient.
proof idea
One-line abbreviation wrapper. The body is exactly the upstream theorem that the Boolean-shadow completeness boundary holds, which assembles four already-proved components: non-completeness of one Boolean coordinate, non-completeness of first-bit scalar cost, injectivity of the two-bit pair-family projection, and exactness of the full signature quotient via the forced-quotient equivalence for every admitted family.
why it matters
This is a named public citation target in Recognition Core for the corrected T0 boundary. It anchors the claim that one bit is atomic rather than ontologically complete, so reconstruction requires a separating family and scalar-cost completeness is not free. That stance feeds the recognizer-family story: refinement by composition, observer forced by non-trivial recognition, logic induced by a recognizer, and the recognition lattice from kernel classes.
In the forcing chain it sits at T0 (and the T0/T4 signature layer), before J-uniqueness (T5), phi (T6), the eight-tick octave (T7), and D = 3 (T8). No downstream dependents are recorded yet; the value is as the stable export name for the boundary package rather than as a lemma inside a longer proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.