RecogSpec
RecogSpec modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
RecogSpec.Anchors |
0 | 1 | 0 | 23 | — |
RecogSpec.BridgeDerivation |
3 | 0 | 2 | 71 | — |
RecogSpec.Core |
0 | 17 | 3 | 146 | — |
RecogSpec.MassLawFromLedger |
3 | 0 | 1 | 63 | — |
RecogSpec.ObservablePayloads |
5 | 0 | 2 | 111 | — |
RecogSpec.PhiSelectionCore |
0 | 0 | 1 | 12 | — |
RecogSpec.RSBridge |
9 | 0 | 9 | 171 | — |
RecogSpec.RSLedger |
8 | 6 | 5 | 221 | — |
RecogSpec.Scales |
0 | 23 | 18 | 194 | — |
RecogSpec.Universe |
0 | 0 | 1 | 31 | — |
RecogSpec.Witness.Core |
0 | 0 | 0 | 15 | — |