composite_cell_subset_left
plain-language theorem explainer
Composite resolution cells sit inside each component cell. Researchers establishing the Refinement Theorem in Recognition Geometry cite this when showing that joint recognition distinguishes at least as much as either factor alone. The proof is a one-line reduction that invokes the intersection characterization of composite cells and the elementary inclusion of an intersection into its left factor.
Claim. Let $r_1$ and $r_2$ be recognizers on configuration space $C$. For any $c$ in $C$, the resolution cell of $c$ under the composite recognizer $r_1$ tensor $r_2$ is contained in the resolution cell of $c$ under $r_1$.
background
A recognizer maps configurations in $C$ to events. The resolution cell of a configuration $c$ under recognizer $r$ is the set of all configurations indistinguishable from $c$ under $r$, i.e., the equivalence class under the indistinguishability relation induced by $r$ (ResolutionCell definition). The composite recognizer $r_1$ tensor $r_2$ pairs the events produced by each factor, so two configurations are indistinguishable under the composite precisely when they are indistinguishable under both factors. Consequently the composite resolution cell equals the intersection of the two component cells (composite_resolutionCell theorem). This module develops the theory of such composites and proves the Refinement Theorem, which asserts that the composite quotient refines both component quotients.
proof idea
The proof is a one-line wrapper. It rewrites the composite resolution cell via the composite_resolutionCell lemma, which supplies the intersection equality, and then applies the standard set inclusion Set.inter_subset_left.
why it matters
This result supplies one direction of the subset relation required by the Refinement Theorem stated in the module documentation. It confirms that the composite indistinguishability relation is finer than either factor, consistent with the module's key insight that richer geometry emerges from paired measurements. The lemma sits among the basic subset facts that support the full refinement statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.