pairSeparates_iff
plain-language theorem explainer
Pair separation for two recognizers holds precisely when identical joint outputs imply identical configurations. Dimension theorists cite the equivalence when bounding the minimal recognizer count needed to separate events in a geometry. The proof reduces directly by unfolding the composite map and injectivity definitions.
Claim. Let $r_1$ and $r_2$ be recognizers over event spaces $E_1$ and $E_2$. Then $r_1$ and $r_2$ are pair-separating if and only if, for all configurations $c_1$ and $c_2$, $r_1(c_1) = r_1(c_2)$ and $r_2(c_1) = r_2(c_2)$ together imply $c_1 = c_2$.
background
Recognition Geometry defines dimension operationally as the smallest number of independent recognizers whose joint outputs distinguish every configuration. PairSeparates is the predicate that the composite recognizer $r_1 ⊗ r_2$ is separating, i.e., its map is injective. The composite map satisfies $(r_1 ⊗ r_2).R(c) = (r_1.R(c), r_2.R(c))$ by the upstream composite_R_eq theorem.
proof idea
The term proof applies simp only to the definitions of PairSeparates, IsSeparating, Function.Injective, the composite map equality, and the product equality Prod.mk.injEq, collapsing the statement to the desired universal quantification.
why it matters
The equivalence supplies the separation criterion used by dimension_status to characterize quantum and geometric dimension. It supports the Recognition Science claim that four independent recognizers are required for spacetime events and contributes to the forcing chain step that fixes spatial dimension at three. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.