structure
definition
RecognitionTriple
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.RecogGeom.Core on GitHub at line 74.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
71/-- A recognition triple bundles a configuration space, event space,
72 and the implicit structure connecting them. This is the basic
73 object of study in recognition geometry. -/
74structure RecognitionTriple where
75 /-- The type of configurations -/
76 Config : Type*
77 /-- The type of events -/
78 Event : Type*
79 /-- Configurations form a valid configuration space -/
80 configSpace : ConfigSpace Config
81 /-- Events form a valid event space -/
82 eventSpace : EventSpace Event
83
84/-! ## Module Status -/
85
86def core_status : String :=
87 "✓ ConfigSpace defined (RG0)\n" ++
88 "✓ EventSpace defined\n" ++
89 "✓ Nonemptiness axiom established\n" ++
90 "✓ Nontriviality axiom established\n" ++
91 "✓ RecognitionTriple bundle defined\n" ++
92 "\n" ++
93 "CORE FOUNDATION COMPLETE"
94
95#eval core_status
96
97end RecogGeom
98end IndisputableMonolith