BooleanShadowCompletenessBoundary
plain-language theorem explainer
A Prop-valued audit certificate packaging four T0 Boolean-shadow boundary facts: one Boolean coordinate fails to separate Bool×Bool; first-bit scalar cost likewise fails completeness; the two-bit family projects injectively; and full-signature equality is exactly the recognition quotient. Anyone citing the corrected T0 atomic-floor claim references this package. As a structure definition it has no proof body; the companion theorem discharges each field.
Claim. The Boolean-shadow completeness boundary is the conjunction of four statements: (i) there exist distinct $x,y\in\mathrm{Bool}\times\mathrm{Bool}$ with the same one-bit recognition signature; (ii) there exist distinct states with equal first-bit scalar cost; (iii) the quotient projection induced by the two-bit recognizer family is injective; (iv) for any family $F$ of observables on a type $X$, the projection identifies $x$ and $y$ if and only if they share the full recognition signature under $F$.
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.
Observational equivalence under a family $F$ of maps $X\to C$ is written as equality of the full recognition signature: two states are identified precisely when every admitted observable agrees on them. The physical quotient is that equivalence relation; every admitted observable descends to it, and a separating family yields an injective projection.
The toy state space is $\mathrm{Bool}\times\mathrm{Bool}$. One coordinate recognizer (and the scalar cost built from it) fails to separate; the two-coordinate family does separate. Scalar-cost equality is a complete gauge invariant only under an extra completeness hypothesis, not by default.
proof idea
No proof body: this is a structure extending Prop whose four fields are named hypotheses. The companion theorem booleanShadowCompletenessBoundary_holds fills them by applying existing lemmas: the one-bit incompleteness counterexample on PairBoolState, the first-bit scalar-cost collision, injectivity of the two-bit family projection, and the general quotient exactness statement that projection equality coincides with full-signature equivalence. The structure itself only packages the boundary; it performs no reduction.
why it matters
This certificate is the machine-checkable statement of the corrected T0 boundary in the forcing chain: one bit is atomic, not complete; a full signature quotient is theorem-grade; scalar-cost completeness needs an extra hypothesis. Downstream, booleanShadowCompletenessBoundary_holds instantiates every field, so the audit is zero-sorry and axiom-free.
It ties the T0 floor to the existing quotient theorem in PrimitiveRecognitionCalculus.QuotientSelection: physical identification is full-signature equality, observables descend, and separating families inject. Without this package, the one-bit shadow could be misread as a complete gauge, collapsing the distinction between atomic recognition and complete encoding that later steps (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick) rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.