`complete_summary`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Integration
domain: RecogGeom
line: 102 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.RecogGeom.Integration on GitHub at line 102.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  99/-! ## Module Summary -/
 100
 101/-- Summary of all Recognition Geometry modules -/
 102def complete_summary : String :=
 103  "╔══════════════════════════════════════════════════════════════════╗\n" ++
 104  "║         RECOGNITION GEOMETRY - COMPLETE SUMMARY                  ║\n" ++
 105  "╠══════════════════════════════════════════════════════════════════╣\n" ++
 106  "║                                                                  ║\n" ++
 107  "║  MODULE                   │ AXIOM │ STATUS                       ║\n" ++
 108  "║ ─────────────────────────┼───────┼───────────────────────────── ║\n" ++
 109  "║  Core.lean               │ RG0   │ ✅ ConfigSpace, EventSpace   ║\n" ++
 110  "║  Locality.lean           │ RG1   │ ✅ LocalConfigSpace          ║\n" ++
 111  "║  Recognizer.lean         │ RG2   │ ✅ Recognizer structure      ║\n" ++
 112  "║  Indistinguishable.lean  │ RG3   │ ✅ Equivalence relation      ║\n" ++
 113  "║  Quotient.lean           │ -     │ ✅ Recognition quotient      ║\n" ++
 114  "║  FiniteResolution.lean   │ RG4   │ ✅ Finite local resolution   ║\n" ++
 115  "║  Connectivity.lean       │ RG5   │ ✅ Local regularity          ║\n" ++
 116  "║  Composition.lean        │ RG6   │ ✅ Composite recognizers     ║\n" ++
 117  "║  Comparative.lean        │ RG7   │ ✅ Order emergence           ║\n" ++
 118  "║  Symmetry.lean           │ -     │ ✅ Automorphisms, gauge      ║\n" ++
 119  "║  Charts.lean             │ -     │ ✅ Recognition charts        ║\n" ++
 120  "║  Dimension.lean          │ -     │ ✅ Separation, dimension     ║\n" ++
 121  "║  RSBridge.lean           │ -     │ ✅ RS instantiation          ║\n" ++
 122  "║  Examples.lean           │ -     │ ✅ Concrete examples          ║\n" ++
 123  "║  Foundations.lean        │ -     │ ✅ Fundamental theorems       ║\n" ++
 124  "║                                                                  ║\n" ++
 125  "╠══════════════════════════════════════════════════════════════════╣\n" ++
 126  "║                    KEY THEOREMS PROVED                           ║\n" ++
 127  "╠══════════════════════════════════════════════════════════════════╣\n" ++
 128  "║  • indistinguishable_equivalence - ~ is equivalence relation    ║\n" ++
 129  "║  • quotientEventMap_injective - Event map is injective          ║\n" ++
 130  "║  • refinement_theorem - Composite refines both components       ║\n" ++
 131  "║  • symmetry_group_structure - Automorphisms form group          ║\n" ++
 132  "║  • no_injection_on_infinite_finite - Finite blocks injection    ║\n" ++

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.