signature_complete_iff_separating
plain-language theorem explainer
Completeness of a recognition signature means the family separates states, so the physical quotient projection is injective. This is the public citation target for the necessary-and-sufficient completeness condition at the recognizer layer. The declaration is a one-line abbrev re-exporting the gauge-layer injectivity theorem.
Claim. If a recognition signature family $F$ separates points (equal signatures under $F$ imply equal states), then the physical quotient projection associated to $F$ is injective. This is the exact completeness condition for the admitted recognizer family.
background
RecognitionCore aggregates the T0/T4 recognizer layer: the admitted family of recognition maps, the indistinguishability relation they induce, and the quotient of physically relevant states. Two states are indistinguishable when every map in the family returns the same value; the quotient projection collapses exactly those pairs.
A family is separating when indistinguishability already forces equality of states. Completeness is the demand that this quotient carry no residual identification: the projection is injective, so distinct states remain distinct after all admitted recognition acts.
Upstream, signature_projection_injective_of_separating states the same fact at the gauge layer: "If the full recognition signature separates states, the quotient projection is injective. This is the precise complete recognizer family condition." The present abbrev surfaces that result as a named public target.
proof idea
One-line abbrev. The body is a direct alias of Foundation.RecognitionSignatureGauge.signature_projection_injective_of_separating, which itself reduces to the generic lemma that a separating family makes the induced quotient projection injective. No extra argument is introduced here.
why it matters
Listed in the module doc as a primary citation target: completeness (injective physical quotient) holds precisely when the family separates points. It anchors the corrected T0 boundary story next to the sibling claim that a single Boolean coordinate is atomic, not complete; scalar-cost completeness needs a separate hypothesis.
In the forcing chain this sits at the recognizer/signature layer before observer forcing and the multiplicative L4 composition law. Gauge is absence of a distinguishing recognition act; this abbrev packages the dual completeness side so downstream work can cite a stable name without reaching into the gauge module. No downstream dependents are recorded yet; the value is the stable public interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.