FP0037

prime_field_operation_tables_exists

Every prime has four actual finite beta-coded arithmetic tables; zero is only a totalized inverse-table convention.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

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

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.

Exact theorem in conservative defined notation

∀ p. Prime(p) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. ∃ i. ∃ j. FpOperationTables(p,x,y,z,n,m,k,i,j)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

FpAddPrefix(p,b,c,l) · 1FpMulPrefix(p,b,c,l) · 1FpNegPrefix(p,b,c,l) · 1FpInvPrefix(p,b,c,l) · 1FpOperationTables(p,ab,ac,mb,mc,nb,nc,ib,ic) · 1Prime(p) · 1

Actual proof prerequisites

prime_field_add_table_existsprime_field_multiply_table_existsprime_field_negate_table_existsprime_field_inverse_table_exists
Original expanded first-order statement 
forall p. (~((p) = 1) /\ forall pfa_factor_left_all_tables_domain pfa_factor_right_all_tables_domain. (p) = pfa_factor_left_all_tables_domain * pfa_factor_right_all_tables_domain -> pfa_factor_left_all_tables_domain = 1 \/ pfa_factor_right_all_tables_domain = 1) -> exists ab ac mb mc nb nc ib ic. (((forall pft_index_all_tablesadd. (exists pfa_gap_all_tablesaddprefix. pfa_gap_all_tablesaddprefix + S (pft_index_all_tablesadd) = ((p) * (p))) -> exists pft_value_all_tablesadd. (((((exists ff_h_pft_all_tablesaddpointentry. ff_h_pft_all_tablesaddpointentry + S (pft_value_all_tablesadd) = S ((S (pft_index_all_tablesadd)) * ac)) /\ exists ff_q_pft_all_tablesaddpointentry. ab = ff_q_pft_all_tablesaddpointentry * S ((S (pft_index_all_tablesadd)) * ac) + (pft_value_all_tablesadd))) /\ ((exists pft_row_all_tablesaddpointvalue pft_column_all_tablesaddpointvalue. (((pft_index_all_tablesadd) = pft_row_all_tablesaddpointvalue * (p) + pft_column_all_tablesaddpointvalue) /\ ((((exists pfa_gap_all_tablesaddpointvalueoperationleft. pfa_gap_all_tablesaddpointvalueoperationleft + S (pft_row_all_tablesaddpointvalue) = (p)) /\ (((exists pfa_gap_all_tablesaddpointvalueoperationright. pfa_gap_all_tablesaddpointvalueoperationright + S (pft_column_all_tablesaddpointvalue) = (p)) /\ ((((exists pfa_gap_all_tablesaddpointvalueoperationresultbound. pfa_gap_all_tablesaddpointvalueoperationresultbound + S (pft_value_all_tablesadd) = (p)) /\ ((exists pfa_offset_left_all_tablesaddpointvalueoperationresultcongruence pfa_offset_right_all_tablesaddpointvalueoperationresultcongruence. ((pft_row_all_tablesaddpointvalue) + (pft_column_all_tablesaddpointvalue)) + (p) * pfa_offset_left_all_tablesaddpointvalueoperationresultcongruence = (pft_value_all_tablesadd) + (p) * pfa_offset_right_all_tablesaddpointvalueoperationresultcongruence)))))))))))))))) /\ (((forall pft_index_all_tablesmultiply. (exists pfa_gap_all_tablesmultiplyprefix. pfa_gap_all_tablesmultiplyprefix + S (pft_index_all_tablesmultiply) = ((p) * (p))) -> exists pft_value_all_tablesmultiply. (((((exists ff_h_pft_all_tablesmultiplypointentry. ff_h_pft_all_tablesmultiplypointentry + S (pft_value_all_tablesmultiply) = S ((S (pft_index_all_tablesmultiply)) * mc)) /\ exists ff_q_pft_all_tablesmultiplypointentry. mb = ff_q_pft_all_tablesmultiplypointentry * S ((S (pft_index_all_tablesmultiply)) * mc) + (pft_value_all_tablesmultiply))) /\ ((exists pft_row_all_tablesmultiplypointvalue pft_column_all_tablesmultiplypointvalue. (((pft_index_all_tablesmultiply) = pft_row_all_tablesmultiplypointvalue * (p) + pft_column_all_tablesmultiplypointvalue) /\ ((((exists pfa_gap_all_tablesmultiplypointvalueoperationleft. pfa_gap_all_tablesmultiplypointvalueoperationleft + S (pft_row_all_tablesmultiplypointvalue) = (p)) /\ (((exists pfa_gap_all_tablesmultiplypointvalueoperationright. pfa_gap_all_tablesmultiplypointvalueoperationright + S (pft_column_all_tablesmultiplypointvalue) = (p)) /\ ((((exists pfa_gap_all_tablesmultiplypointvalueoperationresultbound. pfa_gap_all_tablesmultiplypointvalueoperationresultbound + S (pft_value_all_tablesmultiply) = (p)) /\ ((exists pfa_offset_left_all_tablesmultiplypointvalueoperationresultcongruence pfa_offset_right_all_tablesmultiplypointvalueoperationresultcongruence. ((pft_row_all_tablesmultiplypointvalue) * (pft_column_all_tablesmultiplypointvalue)) + (p) * pfa_offset_left_all_tablesmultiplypointvalueoperationresultcongruence = (pft_value_all_tablesmultiply) + (p) * pfa_offset_right_all_tablesmultiplypointvalueoperationresultcongruence)))))))))))))))) /\ (((forall pft_index_all_tablesnegate. (exists pfa_gap_all_tablesnegateprefix. pfa_gap_all_tablesnegateprefix + S (pft_index_all_tablesnegate) = (p)) -> exists pft_value_all_tablesnegate. (((((exists ff_h_pft_all_tablesnegatepointentry. ff_h_pft_all_tablesnegatepointentry + S (pft_value_all_tablesnegate) = S ((S (pft_index_all_tablesnegate)) * nc)) /\ exists ff_q_pft_all_tablesnegatepointentry. nb = ff_q_pft_all_tablesnegatepointentry * S ((S (pft_index_all_tablesnegate)) * nc) + (pft_value_all_tablesnegate))) /\ ((((exists pfa_gap_all_tablesnegatepointvalueadditionleft. pfa_gap_all_tablesnegatepointvalueadditionleft + S (pft_index_all_tablesnegate) = (p)) /\ (((exists pfa_gap_all_tablesnegatepointvalueadditionright. pfa_gap_all_tablesnegatepointvalueadditionright + S (pft_value_all_tablesnegate) = (p)) /\ ((((exists pfa_gap_all_tablesnegatepointvalueadditionresultbound. pfa_gap_all_tablesnegatepointvalueadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_all_tablesnegatepointvalueadditionresultcongruence pfa_offset_right_all_tablesnegatepointvalueadditionresultcongruence. ((pft_index_all_tablesnegate) + (pft_value_all_tablesnegate)) + (p) * pfa_offset_left_all_tablesnegatepointvalueadditionresultcongruence = (0) + (p) * pfa_offset_right_all_tablesnegatepointvalueadditionresultcongruence))))))))))))) /\ ((forall pft_index_all_tablesinverse. (exists pfa_gap_all_tablesinverseprefix. pfa_gap_all_tablesinverseprefix + S (pft_index_all_tablesinverse) = (p)) -> exists pft_value_all_tablesinverse. (((((exists ff_h_pft_all_tablesinversepointentry. ff_h_pft_all_tablesinversepointentry + S (pft_value_all_tablesinverse) = S ((S (pft_index_all_tablesinverse)) * ic)) /\ exists ff_q_pft_all_tablesinversepointentry. ib = ff_q_pft_all_tablesinversepointentry * S ((S (pft_index_all_tablesinverse)) * ic) + (pft_value_all_tablesinverse))) /\ ((((exists pfa_gap_all_tablesinversepointvalueinput. pfa_gap_all_tablesinversepointvalueinput + S (pft_index_all_tablesinverse) = (p)) /\ (((exists pfa_gap_all_tablesinversepointvalueoutput. pfa_gap_all_tablesinversepointvalueoutput + S (pft_value_all_tablesinverse) = (p)) /\ ((((pft_index_all_tablesinverse) = 0 /\ (pft_value_all_tablesinverse) = 0) \/ (((~((pft_index_all_tablesinverse) = 0)) /\ ((((exists pfa_gap_all_tablesinversepointvaluenonzeromultiplicationleft. pfa_gap_all_tablesinversepointvaluenonzeromultiplicationleft + S (pft_index_all_tablesinverse) = (p)) /\ (((exists pfa_gap_all_tablesinversepointvaluenonzeromultiplicationright. pfa_gap_all_tablesinversepointvaluenonzeromultiplicationright + S (pft_value_all_tablesinverse) = (p)) /\ ((((exists pfa_gap_all_tablesinversepointvaluenonzeromultiplicationresultbound. pfa_gap_all_tablesinversepointvaluenonzeromultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_all_tablesinversepointvaluenonzeromultiplicationresultcongruence pfa_offset_right_all_tablesinversepointvaluenonzeromultiplicationresultcongruence. ((pft_index_all_tablesinverse) * (pft_value_all_tablesinverse)) + (p) * pfa_offset_left_all_tablesinversepointvaluenonzeromultiplicationresultcongruence = (1) + (p) * pfa_offset_right_all_tablesinversepointvaluenonzeromultiplicationresultcongruence)))))))))))))))))))))))))))))

Complete tactic proof in conservative notation

All 41 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

41 script commands · 16 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (4)
prime field add table existsprime field multiply table existsprime field negate table existsprime field inverse table exists
01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro hp
02Establish haddL3–6

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field add table exists.

  1. L3
    have hadd : ∃ b. ∃ c. FpAddPrefix(p,b,c,p · p)Definitions: FpAddPrefix(p,b,c,p · p)Original native command in the exact edition
  2. L4
    specialize prime_field_add_table_exists (p)
  3. L5
    apply prime_field_add_table_exists
  4. L6
    exact hp
03Separate the logical casesL7–8

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L7
    cases hadd
  2. L8
    cases hadd_witness
04Establish hmultiplyL9–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field multiply table exists.

  1. L9
    have hmultiply : ∃ b. ∃ c. FpMulPrefix(p,b,c,p · p)Definitions: FpMulPrefix(p,b,c,p · p)Original native command in the exact edition
  2. L10
    specialize prime_field_multiply_table_exists (p)
  3. L11
    apply prime_field_multiply_table_exists
  4. L12
    exact hp
05Separate the logical casesL13–14

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L13
    cases hmultiply
  2. L14
    cases hmultiply_witness
06Establish hnegateL15–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field negate table exists.

  1. L15
    have hnegate : ∃ b. ∃ c. FpNegPrefix(p,b,c,p)Definitions: FpNegPrefix(p,b,c,p)Original native command in the exact edition
  2. L16
    specialize prime_field_negate_table_exists (p)
  3. L17
    apply prime_field_negate_table_exists
  4. L18
    exact hp
07Separate the logical casesL19–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L19
    cases hnegate
  2. L20
    cases hnegate_witness
08Establish hinverseL21–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field inverse table exists.

  1. L21
    have hinverse : ∃ b. ∃ c. FpInvPrefix(p,b,c,p)Definitions: FpInvPrefix(p,b,c,p)Original native command in the exact edition
  2. L22
    specialize prime_field_inverse_table_exists (p)
  3. L23
    apply prime_field_inverse_table_exists
  4. L24
    exact hp
09Separate the logical casesL25–26

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L25
    cases hinverse
  2. L26
    cases hinverse_witness
10Construct an explicit witnessL27–34

Supply the displayed value, then prove that it has the required property.

  1. L27
    exists x
  2. L28
    exists x1
  3. L29
    exists x2
  4. L30
    exists x3
  5. L31
    exists x4
  6. L32
    exists x5
  7. L33
    exists x6
  8. L34
    exists x7
11Separate the logical casesL35–35

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L35
    split
12Use earlier factsL36–36

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L36
    exact hadd_witness_witness
13Separate the logical casesL37–37

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L37
    split
14Use earlier factsL38–38

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L38
    exact hmultiply_witness_witness
15Separate the logical casesL39–39

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    split
16Use earlier factsL40–41

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L40
    exact hnegate_witness_witness
  2. L41
    exact hinverse_witness_witness

Library-wide reading audit

Original defined command ledger · 41 lines
  1. 0001intro p
  2. 0002intro hp
  3. 0003have hadd : ∃ b. ∃ c. FpAddPrefix(p,b,c,p · p)
  4. 0004specialize prime_field_add_table_exists (p)
  5. 0005apply prime_field_add_table_exists
  6. 0006exact hp
  7. 0007cases hadd
  8. 0008cases hadd_witness
  9. 0009have hmultiply : ∃ b. ∃ c. FpMulPrefix(p,b,c,p · p)
  10. 0010specialize prime_field_multiply_table_exists (p)
  11. 0011apply prime_field_multiply_table_exists
  12. 0012exact hp
  13. 0013cases hmultiply
  14. 0014cases hmultiply_witness
  15. 0015have hnegate : ∃ b. ∃ c. FpNegPrefix(p,b,c,p)
  16. 0016specialize prime_field_negate_table_exists (p)
  17. 0017apply prime_field_negate_table_exists
  18. 0018exact hp
  19. 0019cases hnegate
  20. 0020cases hnegate_witness
  21. 0021have hinverse : ∃ b. ∃ c. FpInvPrefix(p,b,c,p)
  22. 0022specialize prime_field_inverse_table_exists (p)
  23. 0023apply prime_field_inverse_table_exists
  24. 0024exact hp
  25. 0025cases hinverse
  26. 0026cases hinverse_witness
  27. 0027exists x
  28. 0028exists x1
  29. 0029exists x2
  30. 0030exists x3
  31. 0031exists x4
  32. 0032exists x5
  33. 0033exists x6
  34. 0034exists x7
  35. 0035split
  36. 0036exact hadd_witness_witness
  37. 0037split
  38. 0038exact hmultiply_witness_witness
  39. 0039split
  40. 0040exact hnegate_witness_witness
  41. 0041exact hinverse_witness_witness