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 198 long defined-edition local claims and 3,543 exact-edition reading claims. Each replacement passes an exact formula-and-free-context expansion comparison. Large defined claims fall from 279 to 85; no new definition is invented.

There are script-bound mathematical notes for 5 distinct theorem names, appearing on 10 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. eisenstein product shuffle · 6,587 characters in the largest defined local claim
2. gaussian adjoint product is norm scale · 2,880 characters in the largest defined local claim
3. eisenstein coordinate norm product · 2,848 characters in the largest defined local claim
4. eisenstein product associate imaginary · 2,802 characters in the largest defined local claim
5. cf convergent old history successor elimination · 1,924 characters in the largest defined local claim
6. gaussian signed euclidean division exists · 1,712 characters in the largest defined local claim
7. eisenstein adjoint product is norm scale · 1,488 characters in the largest defined local claim
8. eisenstein signed euclidean division exists · 1,345 characters in the largest defined local claim
9. prime field polynomial normalized gcd bezout exists · 1,003 characters in the largest defined local claim
10. eisenstein successor row split prefix exists · 988 characters in the largest defined local claim
11. eisenstein transposed column count decoded partition · 968 characters in the largest defined local claim
12. eisenstein transposed column count prefix exists · 958 characters in the largest defined local claim
13. eisenstein successor rectangle row split prefix exists · 891 characters in the largest defined local claim
14. eisenstein successor row split choices · 872 characters in the largest defined local claim
15. cf convergent actual prefix error invariant · 866 characters in the largest defined local claim
16. prime field polynomial division execution aligned identity · 844 characters in the largest defined local claim
17. eisenstein transposed column count total exists · 829 characters in the largest defined local claim
18. gaussian multiply associative · 797 characters in the largest defined local claim
19. prime field polynomial gcd bezout division backward · 779 characters in the largest defined local claim
20. cf convergent matrix extend preserved prefix · 768 characters in the largest defined local claim
21. gaussian signed product shuffle · 762 characters in the largest defined local claim
22. prime terminal range two product mod one exists · 755 characters in the largest defined local claim
23. cf convergent full matrix is exact · 754 characters in the largest defined local claim
24. prime field polynomial bezout euclidean backward · 753 characters in the largest defined local claim
25. cf convergent actual prefix index bound · 752 characters in the largest defined local claim
26. eisenstein weighted norm product · 748 characters in the largest defined local claim
27. lucas terminating multidigit theorem · 728 characters in the largest defined local claim
28. four square signed conjugate quaternion · 711 characters in the largest defined local claim
29. gauss signed pointwise mul scale mod · 710 characters in the largest defined local claim
30. cf convergent second column is previous prefix · 707 characters in the largest defined local claim