no_injection_on_infinite_finite
plain-language theorem explainer
If a neighborhood contains infinitely many configurations but the recognizer produces only finitely many distinct events from it, then the mapping from configurations to events cannot be one-to-one. Researchers modeling discrete geometries in recognition-based physics cite this to derive contradictions with continuous embeddings. The tactic proof assumes injectivity, shows the neighborhood must then be finite via image finiteness, and contradicts the infinitude assumption.
Claim. Let $C$ be a configuration space, $E$ an event space, $L$ a local configuration space, and $r$ a recognizer. For any configuration $c$ and neighborhood $U$ with $U$ belonging to the neighborhoods of $c$ under $L$, if $U$ is infinite but the image $r.R(U)$ is finite, then the restriction of $r.R$ to $U$ (composed with the subtype embedding) is not injective.
background
The module formalizes axiom RG4 of finite local resolution: every configuration has a neighborhood where the recognizer distinguishes only finitely many states. A neighborhood $U$ in $L.N(c)$ consists of all configurations sharing the same observed label under the recognizer, per the definition in RecognitionLatticeFromRecognizer.neighborhood. Upstream results include the RS-native units setting the gauge with one tick and one voxel, plus constructions of integers and rationals from logic primitives that support the underlying lattice.
proof idea
The proof proceeds by contradiction in tactic mode. It introduces the injectivity assumption, then applies Set.Finite.of_finite_image together with the subtype equality to conclude that $U$ must be finite. This directly contradicts the given infinitude of $U$.
why it matters
This supplies the core non-injectivity step invoked by finite_resolution_not_injective and pillar3_finite_resolution_obstruction. It realizes the RG4 axiom and the physical claim that the eight-tick cycle bounds local events, preventing continuous embeddings and separating recognition geometry from Euclidean space. The result closes the local obstruction argument in the finite-resolution module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.