Understand the argument.
Inspect every detail.

What this layer does—and does not claim

Each reading checkpoint cites its original commands. Definitions keep their original links; long formulas and the original command ledger remain expandable. Every defined page is bound to its paired exact edition, with direct links to native commands. Structural groups are consecutive commands, not reconstructed proof-tree branches.

The existing family definition DAGs reduce 0 long defined-edition local claims and 89 exact-edition reading claims. Each replacement passes an exact formula-and-free-context expansion comparison. Large defined claims fall from 0 to 0; no new definition is invented.

There are script-bound mathematical notes for 0 distinct theorem names, appearing on 0 pages. Other pages explicitly use structural guides. This is not a claim that every proof now has a human-authored explanation. No additional theorem or definition has been admitted to Alpha or Stable.

Coverage by family

Next mathematical exposition priorities

These pages still contain large compound conditions even after existing conservative definitions are applied. They are visible priorities for further definition work and mathematical explanation, not silently declared solved.

1. jordan rectangle crt pair value · 334 characters in the largest defined local claim
2. jordan enumeration index map exists · 312 characters in the largest defined local claim
3. jordan enumeration cardinality le · 307 characters in the largest defined local claim
4. jordan rectangle crt append · 287 characters in the largest defined local claim
5. jordan rectangle crt actual entry · 284 characters in the largest defined local claim
6. jordan rectangle crt enumeration · 284 characters in the largest defined local claim
7. jordan rectangle crt distinct · 274 characters in the largest defined local claim
8. jordan enumeration index map append · 167 characters in the largest defined local claim
9. jordan enumeration index map entry · 167 characters in the largest defined local claim
10. jordan enumeration index map bounded injective · 167 characters in the largest defined local claim
11. jordan rectangle crt covers · 156 characters in the largest defined local claim
12. jordan primitive tuple decidable · 154 characters in the largest defined local claim
13. jordan tuple scan append · 131 characters in the largest defined local claim
14. jordan tuple primitive bounded decidable · 120 characters in the largest defined local claim
15. jordan crt tuple extend · 116 characters in the largest defined local claim
16. jordan enumeration actual value · 113 characters in the largest defined local claim
17. jordan enumeration position match exists · 113 characters in the largest defined local claim
18. jordan crt tuple left · 112 characters in the largest defined local claim
19. jordan crt tuple right · 112 characters in the largest defined local claim
20. jordan product enumeration exists · 104 characters in the largest defined local claim
21. jordan canonical crt tuple exists · 92 characters in the largest defined local claim
22. jordan tuple scan exists · 90 characters in the largest defined local claim
23. jordan rectangle crt exists · 87 characters in the largest defined local claim
24. jordan enumeration reduce primitive · 82 characters in the largest defined local claim
25. jordan tuple divisor test decidable · 80 characters in the largest defined local claim
26. jordan totient exists · 79 characters in the largest defined local claim
27. jordan tuple listed decidable · 73 characters in the largest defined local claim
28. jordan tuple outer append exists · 64 characters in the largest defined local claim
29. jordan primitive crt tuple exists · 64 characters in the largest defined local claim
30. jordan tuple normalize exists · 58 characters in the largest defined local claim