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

examples_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)

 176def examples_status : String :=

proof body

Definition body.

 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

depends on (20)

Lean names referenced from this declaration's body.