Holography
Holography modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
Holography.CellInjection |
16 | 0 | 11 | 228 | - |
Holography.CoefficientBridge |
11 | 0 | 5 | 148 | - |
Holography.DeficitFreePeriod |
14 | 0 | 5 | 312 | - |
Holography.EdgeSectorBridge |
6 | 0 | 2 | 142 | - |
Holography.EightTickSubperiodExclusion |
5 | 0 | 5 | 137 | - |
Holography.HorizonClockRate |
7 | 0 | 2 | 97 | - |
Holography.HorizonOneSidedCut |
24 | 0 | 13 | 348 | - |
Holography.KeystoneFactorThree |
10 | 0 | 1 | 214 | - |
Holography.LocalRecognitionHorizonCut |
9 | 0 | 7 | 204 | - |
Holography.PixelGluedPlaquette |
3 | 0 | 6 | 107 | - |
Holography.PixelLocal |
5 | 0 | 6 | 119 | - |
Holography.RecognitionEventCapacity |
8 | 0 | 4 | 189 | - |
Holography.RecognitionMultiplicity |
11 | 0 | 8 | 230 | - |
Holography.RecordCostAsymmetry |
19 | 0 | 5 | 400 | - |
Holography.RecordMonotonicity |
27 | 0 | 17 | 398 | - |
Holography.SeamLedgerDischarge |
18 | 0 | 2 | 408 | - |
Holography.SeamTransferCore |
24 | 3 | 7 | 471 | - |
Holography.TurnRatioCarrier |
28 | 0 | 10 | 450 | - |