PairSeparates
plain-language theorem explainer
PairSeparates declares that two recognizers jointly distinguish all configurations precisely when their composite map is injective. Dimension theorists cite the definition when bounding the number of independent measurements required to fix an event. It is a direct abbreviation that applies the separating predicate to the tensor product of the two recognizers.
Claim. Let $r_1 : C → E_1$ and $r_2 : C → E_2$ be recognizers on event spaces $E_1, E_2$. The pair separates if the map $c ↦ (r_1(c), r_2(c))$ is injective on the configuration space $C$.
background
EventSpace requires a type of observable outcomes to contain at least two distinct events. IsSeparating states that a recognizer separates configurations when its response function is injective. The module develops recognition dimension as the smallest number of independent recognizers whose joint responses distinguish every configuration, thereby accounting for the four-dimensional character of spacetime.
proof idea
One-line definition that sets PairSeparates r₁ r₂ to IsSeparating (r₁ ⊗ r₂).
why it matters
The definition supplies the predicate used by dimension_status to characterize quantum dimension and by the equivalence theorem pairSeparates_iff. It operationalizes the minimum recognizer count that explains four-dimensional spacetime, consistent with the forcing chain steps that fix D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.