`examples_status`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.Examples
domain: RecogGeom
line: 176 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.Examples on GitHub at line 176.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 173
 174/-! ## Module Status -/
 175
 176def examples_status : String :=
 177  "✓ Discrete Recognition on Fin n\n" ++
 178  "  • discrete_indist_iff_eq: indistinguishable ↔ equal\n" ++
 179  "  • discrete_singleton_cells: each config is its own cell\n" ++
 180  "\n" ++
 181  "✓ Sign Recognizer on ℤ\n" ++
 182  "  • sign_indistinguishable: same sign ↔ indistinguishable\n" ++
 183  "  • neg_indist, neg_pos_dist: concrete examples\n" ++
 184  "\n" ++
 185  "✓ Magnitude Recognizer on ℤ\n" ++
 186  "  • magnitude_indistinguishable: same |n| ↔ indistinguishable\n" ++
 187  "  • plus_minus_indist: 3 ~ -3\n" ++
 188  "\n" ++
 189  "✓ Composition Analysis\n" ++
 190  "  • sign_distinguishes_3_neg3 vs magnitude_indist_3_neg3\n" ++
 191  "  • sign_indist_3_5 vs magnitude_distinguishes_3_5\n" ++
 192  "  • composition_refines: combining gives finer resolution\n" ++
 193  "\n" ++
 194  "EXAMPLES COMPLETE"
 195
 196#eval examples_status
 197
 198end Examples
 199end RecogGeom
 200end IndisputableMonolith

papers checked against this theorem

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