composite_cell_subset_right
The resolution cell of a composite recognizer is contained in the resolution cell of its second factor. Researchers establishing refinement properties of combined measurements in Recognition Geometry cite this when showing that composites distinguish at least as finely as their components. The proof is a one-line wrapper that rewrites the composite resolution cell definition and applies the set intersection subset property.
claimLet $r_1$ and $r_2$ be recognizers on configuration space $C$. For any configuration $c$, the resolution cell of the composite recognizer $r_1$ combined with $r_2$ at $c$ satisfies inclusion in the resolution cell of $r_2$ at $c$.
background
Recognition Geometry develops how recognizers induce partitions on configuration spaces. A recognizer maps each configuration to evidence; the resolution cell at $c$ is the set of configurations producing identical evidence, forming the equivalence class under the induced indistinguishability relation. The module introduces composite recognizers via the product construction, where the composite at $c$ returns the paired evidence from each factor. The sibling definition composite_resolutionCell expresses the composite resolution cell explicitly as the intersection of the two component cells. This inclusion is one half of the refinement relation needed for the module's Refinement Theorem, which states that the composite quotient refines both component quotients.
proof idea
The proof is a one-line wrapper. It rewrites the left side via the composite_resolutionCell definition, reducing the claim to the intersection of the two resolution cells, then applies the standard library fact that an intersection is a subset of its right operand.
why it matters in Recognition Science
This result supplies one inclusion direction for the refinement properties of composite recognizers, directly supporting the module's Refinement Theorem and the indistinguishability characterization. It fits the framework's emphasis on how richer geometry emerges from combining measurements, consistent with the eight-tick octave and phi-ladder structure in the broader Recognition Science chain. No open scaffolding remains here; the declaration closes a basic set-theoretic step required for downstream quotient comparisons.
scope and limits
- Does not claim equality of the two resolution cells.
- Does not establish the symmetric inclusion for the first component.
- Does not depend on specific structure of the evidence types.
- Does not address infinite or iterated composites.
formal statement (Lean)
106theorem composite_cell_subset_right (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) (c : C) :
107 ResolutionCell (r₁ ⊗ r₂) c ⊆ ResolutionCell r₂ c := by
proof body
Term-mode proof.
108 rw [composite_resolutionCell]
109 exact Set.inter_subset_right
110
111/-! ## Quotient Maps -/
112
113/-- There is a natural map from the composite quotient to the r₁ quotient -/