Complexity
Complexity modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
Complexity.BalancedParityHidden |
2 | 7 | 3 | 117 | — |
Complexity.CellularAutomata |
7 | 0 | 11 | 270 | — |
Complexity.CircuitLedger |
10 | 0 | 6 | 353 | — |
Complexity.CircuitLowerBound |
4 | 0 | 2 | 262 | — |
Complexity.ComputationBridge |
5 | 0 | 1 | 409 | — |
Complexity.JCostLaplacian |
13 | 0 | 8 | 241 | — |
Complexity.JFrustration |
4 | 0 | 3 | 99 | — |
Complexity.NonNaturalness |
7 | 0 | 4 | 168 | — |
Complexity.PvsNPAssembly |
2 | 0 | 2 | 123 | — |
Complexity.PvsNPFromBIT |
11 | 0 | 4 | 154 | — |
Complexity.RSVC |
1 | 1 | 6 | 67 | — |
Complexity.RSatEncoding |
9 | 0 | 2 | 273 | — |
Complexity.SAT.BWD3SchurPinch |
5 | 0 | 3 | 109 | — |
Complexity.SAT.Backprop |
2 | 16 | 10 | 462 | — |
Complexity.SAT.CNF |
0 | 0 | 5 | 51 | — |
Complexity.SAT.Completeness |
5 | 2 | 5 | 218 | — |
Complexity.SAT.GeoFamily |
1 | 8 | 11 | 180 | — |
Complexity.SAT.Isolation |
0 | 0 | 2 | 29 | — |
Complexity.SAT.PC |
5 | 0 | 13 | 276 | — |
Complexity.SAT.Runtime |
0 | 0 | 4 | 45 | — |
Complexity.SAT.SmallBias |
0 | 4 | 5 | 84 | — |
Complexity.SAT.XOR |
0 | 5 | 5 | 110 | — |
Complexity.SpectralGap |
5 | 0 | 2 | 99 | — |
Complexity.TuringBridge |
2 | 0 | 3 | 163 | — |
Complexity.VertexCover |
0 | 6 | 5 | 66 | — |