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

Prime-field arithmetic and finite tables

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

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

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: research checkpoint map → 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.
Public research checkpoint, independently verified: 87 theorems in a complete dependency-closed HA bundle · 254 proof prerequisites · 31 linked definitions · 57 definition-dependency arrows · 3160 exact tactic lines. Not Alpha-enrolled; no Alpha checked-use authority; not Stable. Alpha v30 remains 3222 theorems and Stable remains 432. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 228 bundle nodes; SHA-256 688e7141106c19adec6fa52a0ae77af3d389b77df512622adc93bd3b0c7ba04e. Inspect the checkpoint receipt, literal bundle, and source files →
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.