IsSeparating
plain-language theorem explainer
IsSeparating declares that a recognizer distinguishes every pair of configurations precisely when its recognition map is injective. Researchers deriving spacetime dimension from operational separation would cite this when counting the minimal independent maps required to locate events uniquely. The declaration is a direct abbreviation of injectivity on the recognizer's output function.
Claim. A recognizer $r$ from configuration space $C$ to event space $E$ separates configurations when the map $r.R : C → E$ is injective.
background
Recognition Geometry defines a recognizer as a structure pairing a configuration space $C$ with an event space $E$ via a recognition map that assigns events to configurations. The module develops dimension as the smallest number of independent recognizers whose composite map distinguishes every configuration, supplying an operational account of why four coordinates locate events in spacetime. Upstream results supply the active-edge count $A$ per tick and the edge cardinality $E(D) = D · 2^{D-1}$ of the $D$-cube, which fix the geometric scaffolding for the recognition maps.
proof idea
This is a one-line definition that sets IsSeparating r to the proposition Function.Injective r.R.
why it matters
The definition anchors the dimension theory developed in the module and is invoked by isSeparating_iff, PairSeparates, separating_quotient_bijective, and dimension_status. It supplies the precise condition under which a collection of recognizers realizes the framework's claim that spacetime dimension equals four because exactly four independent maps separate events, consistent with the eight-tick octave and the forced value D = 3. The same notion appears in the quantum-dimension discussion where the number of independent observables equals the dimension of the state space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.