independent_strict_refines
plain-language theorem explainer
Independent recognizers that each fail to be injective have a composite map separating some pairs they equate. Researchers deriving spacetime dimension from recognizer structure cite this to show why single or redundant measurements leave events indistinguishable. The proof extracts the relevant witness pair from the independence definition and uses the product equality on the composite to reach a contradiction.
Claim. Let $r_1$ and $r_2$ be recognizers on a shared configuration space. If they are independent (each distinguishes a pair the other equates) and neither is injective, then there exist configurations $c_1,c_2$ such that $r_1(c_1)=r_1(c_2)$ yet the composite recognizer satisfies $(r_1⊗r_2)(c_1)≠(r_1⊗r_2)(c_2)$.
background
Recognition geometry defines dimension as the minimal number of independent recognizers required to separate all configurations. A recognizer is separating precisely when its map is injective on the configuration space. Two recognizers are independent when each supplies distinctions the other lacks: there exist pairs equated by one but separated by the other, and vice versa. The module states that spacetime dimension equals four because exactly four independent recognizers (corresponding to x, y, z, t) are needed to locate every event.
proof idea
The proof is a direct term-mode extraction. It introduces the non-separating assumption, obtains from the independence hypothesis the pair where the first recognizer equates the configurations while the second distinguishes them, applies the composite equality to rewrite the product map, and derives a contradiction by assuming the composite equates the pair (which forces equality on the second component).
why it matters
This lemma supports the operational definition of recognition dimension as the size of a minimal independent separating family. It is invoked by the dimension_status definition in the same module, which records the link between recognizer independence and the four-dimensional structure of spacetime. Within the Recognition Science framework it supplies the step showing why three or fewer independent measurements cannot separate all events, consistent with the requirement of four coordinates and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.