finite_resolution_mono
plain-language theorem explainer
Finite resolution at a configuration is inherited by any smaller neighborhood. Researchers building discrete models from recognition axioms cite this to confirm that local finiteness propagates downward in the neighborhood system. The proof is a one-line wrapper applying image monotonicity under inclusion followed by the subset property of finite sets.
Claim. Let $U$ and $V$ be neighborhoods of a configuration $c$ with $Vsubseteq U$. If the image of $U$ under the recognizer map $R$ is finite, then the image of $V$ under $R$ is finite.
background
The module formalizes axiom RG4: every configuration $c$ admits a neighborhood $U$ such that the recognizer image $R(U)$ is finite. This encodes the finite local resolution enforced by the eight-tick cycle of the recognition lattice. The present theorem records the monotonicity of that finiteness under neighborhood inclusion.
proof idea
One-line wrapper that applies Set.Finite.subset to the supplied finiteness hypothesis together with Set.image_mono on the inclusion $Vsubseteq U$.
why it matters
The result feeds the finite_resolution_status definition, which links finite resolution to 8-tick atomicity and the bound on distinguishable states in any local region. It completes the inheritance step required by RG4 and aligns with the T7 eight-tick octave landmark that supplies the underlying discreteness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.