composite_info_monotone_left
If one recognizer distinguishes two configurations, the composite with any second recognizer distinguishes them as well. Researchers proving the refinement theorem in recognition geometry cite this monotonicity. The proof is a one-line wrapper that feeds the left distinguishability hypothesis into the general composite_distinguishes lemma.
claimLet $r_1$ be a recognizer from configurations $C$ to events $E_1$ and $r_2$ a recognizer from $C$ to $E_2$. For $c_1,c_2$ in $C$, if $r_1.R(c_1)neq r_1.R(c_2)$ then $(r_1otimes r_2).R(c_1)neq(r_1otimes r_2).R(c_2)$.
background
In the Recognition Geometry module on composition, a Recognizer is a map sending configurations in $C$ to events in some space $E$. Distinguishability of $c_1$ and $c_2$ under recognizer $r$ means $r.R(c_1)neq r.R(c_2)$. The composite $r_1otimes r_2$ is the recognizer that returns the ordered pair of events from both components, so its recognition map satisfies the equality recorded in composite_R_eq.
proof idea
One-line wrapper that applies composite_distinguishes to the disjunction formed by injecting the given left distinguishability hypothesis via Or.inl.
why it matters in Recognition Science
The result is invoked directly by pillar2_distinguish_monotone in Foundations, which records the corollary that distinguishability is monotonic under composition. It supplies the left half of the Refinement Theorem whose module documentation states that the composite quotient refines both component quotients. In the Recognition Science framework this supports emergence of richer geometry from multiple measurements, consistent with the Recognition Composition Law.
scope and limits
- Does not claim distinguishability when only the right recognizer distinguishes the pair.
- Does not quantify the increase in distinguishable pairs.
- Applies only to the stated left component; the symmetric right case uses a separate declaration.
- Holds for arbitrary event spaces with no further structure assumed.
formal statement (Lean)
192theorem composite_info_monotone_left (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
193 {c₁ c₂ : C} (h : Distinguishable r₁ c₁ c₂) :
194 Distinguishable (r₁ ⊗ r₂) c₁ c₂ :=
proof body
One-line wrapper that applies composite_distinguishes.
195 composite_distinguishes r₁ r₂ (Or.inl h)
196