pith. machine review for the scientific record. sign in
def definition def or abbrev

composition_status

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 204def composition_status : String :=

proof body

Definition body.

 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

depends on (11)

Lean names referenced from this declaration's body.