Canonical operations · actual tables · cardinality and characteristic · Constructive arithmetic

Prime-field arithmetic and finite tables

Prime(p) ⇒ ∃ab ac mb mc nb nc ib ic eb ec. FpFiniteStructure(p,ab,ac,mb,mc,nb,nc,ib,ic,eb,ec)

Construct the actual operations on representatives below a prime, complete beta-coded tables, a finite enumeration, and addition-of-one histories proving exact characteristic.

Open the definition-aware map Read the final theorem See campaign milestone G091

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact certificate

Fully expanded arithmetic

Inspect all 3160 native tactic lines and 254 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem FP0057 and follow only the lemmas and conservative definitions supporting prime_field_of_prime_order_exists.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G091 milestone → theorem and definition dependencies.
Major independently established statements: FP002A prime_field_arithmetic_laws · FP0037 prime_field_operation_tables_exists · FP0057 prime_field_of_prime_order_exists.
Independently verified Alpha v34 checked-use theorem family: 87 dependency-curried kernel-checked theorem bodies · 254 proof prerequisites · 31 linked definitions · 57 definition-dependency arrows · 3160 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 228 bundle nodes; SHA-256 688e7141106c19adec6fa52a0ae77af3d389b77df512622adc93bd3b0c7ba04e.
Exact mathematical boundary: 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.