IndependentRecognizers
plain-language theorem explainer
IndependentRecognizers defines when two recognizers on event spaces E1 and E2 each distinguish a configuration pair that the other leaves indistinguishable. Dimension theorists cite it to establish that the minimal count of such recognizers equals the geometric dimension of the configuration space. The definition is a direct conjunction of two existential statements on asymmetric distinguishability with no auxiliary lemmas.
Claim. Recognizers $r_1$ and $r_2$ are independent when there exist configurations $c_1,c_2$ such that $r_1.R(c_1)≠r_1.R(c_2)$ yet $r_2.R(c_1)=r_2.R(c_2)$, and there exist configurations distinguished by $r_2$ but not by $r_1$.
background
Recognition Geometry defines dimension as the smallest number of independent recognizers required to separate every pair of configurations. An EventSpace is any type containing at least two distinct observable events. A Recognizer supplies a map from configurations in C to events in its event space, acting as a measurement channel.
proof idea
This is a direct definition. The body is the explicit conjunction of two existential propositions, one for each direction of asymmetric distinguishability. No lemmas or tactics are invoked.
why it matters
The definition supplies the key predicate for the independent_strict_refines theorem, which shows that an independent pair yields a composite recognizer strictly finer than either factor. It also anchors the dimension_status summary that equates quantum Hilbert-space dimension with the count of independent observables. In the broader framework it realizes the operational meaning of dimension as the minimal number of independent recognizers, directly supporting the claim that spacetime requires four such measurements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.