G007 · F01
Actual divisor sums and Möbius tables
Construct signed tables, tabulate independently defined Möbius values, and mask positive divisors before taking the actual signed prefix sum.
37 genuinely new checkpoint theorems · 30 conservative definitions
Enter proof family →Explore actual proof and definition dependencies →
View unchanged G007 campaign roadmap →
These are constructed divisor-sum and Möbius-table prerequisites, not full Möbius inversion. A divisor mask has S n entries indexed 0 through n, with entry zero forced to zero regardless of F(0). Mobius itself remains positive-domain only. Prime-toggle divisor cancellation and G007 inversion remain open.
G007 · F01
Signed weighted sums and linearity
Construct real pointwise sum, product and scalar tables and prove algebraic laws for their actual finite signed sums, including empty windows.
40 genuinely new checkpoint theorems · 18 conservative definitions
Enter proof family →Explore actual proof and definition dependencies →
View unchanged G007 campaign roadmap →
All operation tables contain actual beta-coded entries and theorems compare represented signed values, not arbitrary encodings. The strict sum window is i<l; the separately certified endpoint i=l is unused. Rectangular row/column Fubini, divisor cancellation, convolution inversion and full G007 remain open.
G091 · F10
Prime-field coefficient tables and Horner evaluation
Normalize finite coefficient data, construct coefficientwise arithmetic, and execute an actual modular Horner trace using the already proved canonical field operations.
49 genuinely new checkpoint theorems · 21 conservative definitions
Enter proof family →Explore actual proof and definition dependencies →
View unchanged G091 campaign roadmap →
Length is representation length, not polynomial degree. Leading zeros and the empty zero polynomial are allowed; the canonical argument guard x<p also applies to the empty case. Evaluation is defined by actual field-operation steps, not an assumed residue invariant. Polynomial division, gcd, irreducibles and general prime-power extension fields remain open; this does not close G091.