composite_info_monotone_left

formal source

 189
 190/-- The composite recognizer has at least as much information as either component.
 191    "Information" here means the ability to distinguish configurations. -/
 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₂ :=
 195  composite_distinguishes r₁ r₂ (Or.inl h)
 196
 197theorem composite_info_monotone_right (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂)
 198    {c₁ c₂ : C} (h : Distinguishable r₂ c₁ c₂) :
 199    Distinguishable (r₁ ⊗ r₂) c₁ c₂ :=
 200  composite_distinguishes r₁ r₂ (Or.inr h)
 201
 202/-! ## Module Status -/
 203
 204def composition_status : String :=
 205  "✓ CompositeRecognizer defined (RG6)\n" ++
 206  "✓ composite_indistinguishable_iff: c₁ ~₁₂ c₂ ↔ (c₁ ~₁ c₂) ∧ (c₁ ~₂ c₂)\n" ++
 207  "✓ composite_refines_left/right: composite refines both components\n" ++
 208  "✓ composite_resolutionCell: cells are intersections\n" ++
 209  "✓ quotientMapLeft/Right: surjective quotient maps\n" ++
 210  "✓ REFINEMENT THEOREM: composite quotient refines both components\n" ++
 211  "✓ composite_comm: composition is commutative\n" ++
 212  "✓ Information monotonicity theorems\n" ++
 213  "\n" ++
 214  "COMPOSITION (RG6) COMPLETE"
 215
 216#eval composition_status
 217
 218end RecogGeom
 219end IndisputableMonolith