RecogGeom
RecogGeom modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
RecogGeom.Charts |
8 | 0 | 7 | 256 | — |
RecogGeom.Comparative |
6 | 0 | 8 | 254 | — |
RecogGeom.Composition |
15 | 0 | 4 | 220 | — |
RecogGeom.Connectivity |
6 | 0 | 4 | 156 | — |
RecogGeom.Core |
2 | 0 | 1 | 99 | — |
RecogGeom.Dimension |
5 | 0 | 4 | 179 | — |
RecogGeom.EffectiveManifold |
5 | 0 | 2 | 166 | — |
RecogGeom.Examples |
14 | 0 | 5 | 201 | — |
RecogGeom.FiniteResolution |
10 | 0 | 6 | 183 | — |
RecogGeom.Foundations |
9 | 0 | 1 | 267 | — |
RecogGeom.Indistinguishable |
8 | 0 | 6 | 164 | — |
RecogGeom.Integration |
0 | 0 | 2 | 196 | — |
RecogGeom.Locality |
0 | 0 | 3 | 143 | — |
RecogGeom.Quotient |
6 | 0 | 8 | 139 | — |
RecogGeom.RSBridge |
2 | 0 | 5 | 253 | — |
RecogGeom.Recognizer |
1 | 0 | 1 | 137 | — |
RecogGeom.Symmetry |
22 | 0 | 7 | 293 | — |
RecogGeom.ZornRefinement |
14 | 0 | 6 | 261 | — |