SameRecognitionSignature
plain-language theorem explainer
Two states share the same recognition signature under a family of observables precisely when every admitted observable returns the same value on both. This is the T0-language name for observational equivalence, used wherever the physical gauge quotient is identified with full-signature equality. The definition is a one-line alias of that equivalence relation.
Claim. For a family $F$ of maps $X\to C$ and states $x,y\in X$, $x$ and $y$ have the same recognition signature under $F$ if and only if $\forall f\in F$, $f(x)=f(y)$.
background
The module fixes the T-1/T0 Boolean-shadow correction: 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 the full signature it induces.
Observational equivalence under a family $F\subseteq{X\to C}$ means every $f\in F$ agrees on the two states. That relation is the kernel of the joint map $x\mapsto(f(x))_{f\in F}$. The present definition simply names that kernel in T0 language as equality of the full recognition signature.
Upstream, the quotient-selection layer already treats physical identification as this observational equivalence and proves that admitted observables descend to the quotient and that a separating family yields an injective projection. Scalar-cost equality is a separate completeness hypothesis, not automatic.
proof idea
One-line definitional alias: the predicate is definitionally equal to observational equivalence under $F$ (every $f\in F$ returns the same value on the two states). No proof obligations.
why it matters
This name is the hinge of the gauge story in the module. The recognition-signature gauge certificate states that the physical projection identifies states exactly when they share the same recognition signature, that every admitted observable descends, and that a separating family gives an injective projection.
Downstream uses include the Boolean-shadow completeness boundary (one Boolean coordinate fails to separate Bool×Bool while the two-coordinate family does), the scalar-cost completeness hypothesis (scalar equality matches full-signature equality only under an extra assumption), and the forced-quotient and injective-projection lemmas. In the forcing chain this is the T0-level correction: physical gauge is full-signature equality, not a single bit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.