G014 · F02
Euler's theorem for units
Follow the constructed multiplier permutation, the weighted finite product, and the count-prefix induction to an actual power congruent to one.
32 verified checkpoint theorems · 23 conservative definitions
Enter proof family →Explore the proof and definition DAG →
View unchanged published G014 roadmap →
The exact G014 theorem is proved in this research checkpoint for m>1 and genuinely invertible a. Phi counts coprime residues independently of the conclusion. The broader coprime theorem also handles m=1 by congruence, not by asserting that one is a canonical remainder. No multiplicative-order or RSA theorem is claimed. The published atlas and Alpha membership are unchanged.
G091 · F10
Prime-field arithmetic and finite tables
Construct the actual operations on representatives below a prime, complete beta-coded tables, a finite enumeration, and addition-of-one histories proving exact characteristic.
87 verified checkpoint theorems · 31 conservative definitions
Enter proof family →Explore the proof and definition DAG →
View unchanged published G091 roadmap →
This checkpoint constructs prime-order fields (k=1), with genuine finite arithmetic tables, cardinality, and characteristic. Inversion is proved only for nonzero elements; the table's zero entry is a zero-to-zero convention. G091 for every prime power p^k, with an irreducible polynomial of degree k, remains open. No extension-field construction or G091 closure is claimed.
G007 · F01
Möbius values and prime adjunction
Define Möbius values from squarefreeness and the parity of actual prime-factor lists, prove unique values, and trace how a fresh prime changes the sign.
21 verified checkpoint theorems · 20 conservative definitions
Enter proof family →Explore the proof and definition DAG →
View unchanged published G007 roadmap →
Mobius(n,z) is defined only for positive n. The canonical signed codes are 0 for zero, 2 for +1, and 1 for −1. The function is defined independently of any divisor-sum identity. These values and prime-step lemmas are prerequisites for G007; divisor-sum cancellation and full Möbius inversion remain open in this checkpoint. No signed-table proof is included here.
G007 · F01
Signed arithmetic tables and finite sums
Construct finite signed tables, form their actual prefix sums, and prove that a witnessed permutation preserves the signed sum.
30 verified checkpoint theorems · 16 conservative definitions
Enter proof family →Explore the proof and definition DAG →
View unchanged published G007 roadmap →
These are genuine signed-table and finite-sum foundations, not full divisor-sum cancellation or Möbius inversion. G007 remains open. The historical MatrixMinorFourCode definition is reused solely as generic nested pairing of four beta parameters; no matrix-specific hypothesis is imported. Equality is equality of represented signed values, not equality of arbitrary component codes.