Ethics
Ethics modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
Ethics.ConsentInterfaceFromJCost |
5 | 0 | 3 | 93 | — |
Ethics.CostModel |
3 | 2 | 5 | 96 | — |
Ethics.LoveUniquenessDerivation |
4 | 0 | 1 | 108 | — |
Ethics.MoralDebt |
5 | 0 | 6 | 84 | — |
Ethics.SigmaEquilibrationAsDrive |
4 | 0 | 5 | 97 | — |
Ethics.SigmaExternalizationAudit |
3 | 0 | 3 | 33 | — |
Ethics.StakeGraph |
0 | 0 | 5 | 44 | — |
Ethics.ThermodynamicInstabilityOfExtraction |
19 | 0 | 3 | 300 | — |
Ethics.Truth |
0 | 0 | 0 | 49 | — |
Ethics.VirtueComposition |
3 | 0 | 4 | 61 | — |
Ethics.VirtueGeneratorsFromJCost |
6 | 0 | 3 | 89 | — |
Ethics.VirtueLatticeEffect |
4 | 0 | 3 | 64 | — |
Ethics.VirtueSignatures |
6 | 0 | 4 | 98 | — |
Ethics.Virtues.FiniteLatticeEnumeration |
7 | 0 | 8 | 180 | — |
Ethics.Virtues.Independence |
15 | 0 | 18 | 194 | — |
Ethics.Virtues.NormalForm |
11 | 11 | 6 | 517 | — |
Ethics.Virtues.SigmaPreservingProof |
4 | 0 | 1 | 129 | — |