Claim coverage and theorem index
On this page · Permalink · Source line 2
The source register has eight maintained claim groups. This reference expands the maintained arguments into individually numbered statements and adds the later register-product invariant. Prose statement counts and formal lemma counts have different meanings. The Lean guide lists all 115 formal declarations; the original theorem companion and its historical theorem map remain preserved.
E.1 Coverage of the maintained register
On this page · Permalink · Source line 6
| ID | Maintained subject | Results in this reference | Source location |
|---|---|---|---|
| C01 | Exact cut-comparison cover | Theorem 14.1 | Foundations F2 |
| C02 | Complete-cover bound and dual certificates | Results 15.1–15.7 | Theory §1; Foundations F4 |
| C03 | Unbalanced-OR calibration | Results 16.1–16.4 | Theory §2 |
| C04 | Optimal small restored oracles | Theorem 16.5 | Theory §2 |
| C05 | Projection cost and safety | Results 17.1–17.5 | Theory §3 |
| C06 | Faithful flat gluing dimension | Theorem 18.1; Corollary 18.2 | Theory §4 |
| C07 | Weighted witness fingerprint | Results 19.1–19.5 | Theory §5 |
| C08 | Overlap obstruction | Proposition 20.1; Counterexample 20.2 | Theory §5 |
The foundational simulation and degree results, Theorem 13.1 and Lemma 13.2, support the active claims. The conditional status of Proposition 19.5 is unchanged from C07. Counterexamples are deliberately indexed as counterexamples, rather than presented as successful universal compression theorems.