booleanShadowCompletenessBoundary_holds
plain-language theorem explainer
Machine-checkable T0 Boolean-shadow certificate: one Boolean coordinate is atomic, not complete; scalar cost alone fails completeness; a two-bit separating family injects on the quotient; full signature equality is exactly the forced physical quotient. RecognitionCore cites it as the corrected one-bit boundary. Proof is a four-field structure assembly from prior lemmas.
Claim. The T0 Boolean-shadow completeness boundary holds: there exist distinct two-bit states with the same first-bit recognition signature; there exist distinct two-bit states with equal first-bit scalar cost; the two-coordinate bit family induces an injective quotient projection; and for any recognizer family $F$, the forced quotient identifies $x$ and $y$ if and only if they share the same full recognition signature under $F$.
background
This module records the Lean 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 (signature_forced_quotient_iff). Every admitted observable descends to that quotient; a separating family yields 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 PairBoolState (two Boolean coordinates). The one-coordinate family firstBitFamily fails to separate states that differ only in the second bit; the two-coordinate family does separate, so its projection is injective.
proof idea
Term-mode structure construction for BooleanShadowCompletenessBoundary. Four fields are filled by named lemmas: one_boolean_coordinate_not_complete supplies the one-bit incompleteness witness on PairBoolState; first_bit_scalar_cost_not_complete supplies the scalar-cost incompleteness witness; pairBitFamily_projection_injective (via the separating-family injectivity lemma) supplies two-bit injectivity; signature_forced_quotient_iff is eta-expanded as the exactness of the full signature quotient.
why it matters
Closes the corrected T0 boundary as a zero-sorry audit certificate. Downstream, RecognitionCore.one_bit_not_complete_boundary is literally an abbrev for this theorem, packaging the claim that one Boolean coordinate is atomic not complete, a separating family reconstructs the state, and scalar-cost completeness needs an extra hypothesis.
In the forcing chain, T0 is the recognition floor before J-uniqueness (T5), phi (T6), the eight-tick octave (T7), and D=3 (T8). The certificate blocks the false reading that a single bit, or bare scalar cost, already gives a complete physical quotient. Status of the module: 0 sorry, 0 project axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.