composite_resolutionCell
plain-language theorem explainer
The composite resolution cell theorem asserts that for recognizers r1 and r2 on configuration space C the resolution cell of their composite at c equals the intersection of the two component resolution cells. Researchers modeling multi-measurement refinement in Recognition Geometry would cite this when deriving how paired observations produce strictly finer partitions. The proof reduces the equality to membership via set extensionality and applies the composite indistinguishability equivalence to obtain the intersection definition.
Claim. Let $r_1 : Recognizer(C, E_1)$ and $r_2 : Recognizer(C, E_2)$ be recognizers on configuration space $C$. For any $c : C$, the resolution cell of the composite recognizer satisfies $ResolutionCell(r_1 ⊗ r_2, c) = ResolutionCell(r_1, c) ∩ ResolutionCell(r_2, c)$.
background
In the Recognition Geometry module on composition (RG6), a Recognizer maps each configuration to an evidence value that encodes distinguishable outcomes. The composite recognizer is the product map sending c to the pair of individual evidences. ResolutionCell(r, c) is the set of all configurations that produce the same evidence as c under r, i.e., the equivalence class under the indistinguishability relation induced by r.
proof idea
The proof is a one-line term-mode wrapper. It applies set extensionality to equate the two sides by membership, then invokes simp with the definitions of ResolutionCell and the composite_indistinguishable_iff lemma. The lemma replaces the composite indistinguishability predicate with the conjunction of the two component predicates, which is precisely the membership condition for set intersection.
why it matters
This theorem supplies the intersection identity required by the refinement theorem in RG6. It is invoked directly by composite_cell_subset_left and composite_cell_subset_right, which establish that composite cells are subsets of each factor cell; those subset facts in turn support the composition_status definition asserting monotonic increase in distinguishing power. Within the Recognition Science framework the result illustrates how additional recognizers refine the quotient without changing the underlying J-cost structure or the eight-tick dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.