FP0037

prime_field_operation_tables_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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 expanded first-order arithmetic 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)))))))))))))))))))))))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 41 exact native proof lines.

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

Proof neighborhood

Direct dependencies

FP0033 prime_field_add_table_exists FP0034 prime_field_multiply_table_exists FP0035 prime_field_negate_table_exists FP0036 prime_field_inverse_table_exists

Direct dependents

FP0057 prime_field_of_prime_order_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (4)
prime field add table existsprime field multiply table existsprime field negate table existsprime field inverse table exists

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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
  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
  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
  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 exact command ledger · 41 lines
  1. 0001intro p
  2. 0002intro hp
  3. 0003have hadd : exists b c. (forall pft_index_addall_tables. (exists pfa_gap_addall_tablesprefix. pfa_gap_addall_tablesprefix + S (pft_index_addall_tables) = ((p) * (p))) -> exists pft_value_addall_tables. (((((exists ff_h_pft_addall_tablespointentry. ff_h_pft_addall_tablespointentry + S (pft_value_addall_tables) = S ((S (pft_index_addall_tables)) * c)) /\ exists ff_q_pft_addall_tablespointentry. b = ff_q_pft_addall_tablespointentry * S ((S (pft_index_addall_tables)) * c) + (pft_value_addall_tables))) /\ ((exists pft_row_addall_tablespointvalue pft_column_addall_tablespointvalue. (((pft_index_addall_tables) = pft_row_addall_tablespointvalue * (p) + pft_column_addall_tablespointvalue) /\ ((((exists pfa_gap_addall_tablespointvalueoperationleft. pfa_gap_addall_tablespointvalueoperationleft + S (pft_row_addall_tablespointvalue) = (p)) /\ (((exists pfa_gap_addall_tablespointvalueoperationright. pfa_gap_addall_tablespointvalueoperationright + S (pft_column_addall_tablespointvalue) = (p)) /\ ((((exists pfa_gap_addall_tablespointvalueoperationresultbound. pfa_gap_addall_tablespointvalueoperationresultbound + S (pft_value_addall_tables) = (p)) /\ ((exists pfa_offset_left_addall_tablespointvalueoperationresultcongruence pfa_offset_right_addall_tablespointvalueoperationresultcongruence. ((pft_row_addall_tablespointvalue) + (pft_column_addall_tablespointvalue)) + (p) * pfa_offset_left_addall_tablespointvalueoperationresultcongruence = (pft_value_addall_tables) + (p) * pfa_offset_right_addall_tablespointvalueoperationresultcongruence))))))))))))))))
  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 : exists b c. (forall pft_index_multiplyall_tables. (exists pfa_gap_multiplyall_tablesprefix. pfa_gap_multiplyall_tablesprefix + S (pft_index_multiplyall_tables) = ((p) * (p))) -> exists pft_value_multiplyall_tables. (((((exists ff_h_pft_multiplyall_tablespointentry. ff_h_pft_multiplyall_tablespointentry + S (pft_value_multiplyall_tables) = S ((S (pft_index_multiplyall_tables)) * c)) /\ exists ff_q_pft_multiplyall_tablespointentry. b = ff_q_pft_multiplyall_tablespointentry * S ((S (pft_index_multiplyall_tables)) * c) + (pft_value_multiplyall_tables))) /\ ((exists pft_row_multiplyall_tablespointvalue pft_column_multiplyall_tablespointvalue. (((pft_index_multiplyall_tables) = pft_row_multiplyall_tablespointvalue * (p) + pft_column_multiplyall_tablespointvalue) /\ ((((exists pfa_gap_multiplyall_tablespointvalueoperationleft. pfa_gap_multiplyall_tablespointvalueoperationleft + S (pft_row_multiplyall_tablespointvalue) = (p)) /\ (((exists pfa_gap_multiplyall_tablespointvalueoperationright. pfa_gap_multiplyall_tablespointvalueoperationright + S (pft_column_multiplyall_tablespointvalue) = (p)) /\ ((((exists pfa_gap_multiplyall_tablespointvalueoperationresultbound. pfa_gap_multiplyall_tablespointvalueoperationresultbound + S (pft_value_multiplyall_tables) = (p)) /\ ((exists pfa_offset_left_multiplyall_tablespointvalueoperationresultcongruence pfa_offset_right_multiplyall_tablespointvalueoperationresultcongruence. ((pft_row_multiplyall_tablespointvalue) * (pft_column_multiplyall_tablespointvalue)) + (p) * pfa_offset_left_multiplyall_tablespointvalueoperationresultcongruence = (pft_value_multiplyall_tables) + (p) * pfa_offset_right_multiplyall_tablespointvalueoperationresultcongruence))))))))))))))))
  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 : exists b c. (forall pft_index_negateall_tables. (exists pfa_gap_negateall_tablesprefix. pfa_gap_negateall_tablesprefix + S (pft_index_negateall_tables) = (p)) -> exists pft_value_negateall_tables. (((((exists ff_h_pft_negateall_tablespointentry. ff_h_pft_negateall_tablespointentry + S (pft_value_negateall_tables) = S ((S (pft_index_negateall_tables)) * c)) /\ exists ff_q_pft_negateall_tablespointentry. b = ff_q_pft_negateall_tablespointentry * S ((S (pft_index_negateall_tables)) * c) + (pft_value_negateall_tables))) /\ ((((exists pfa_gap_negateall_tablespointvalueadditionleft. pfa_gap_negateall_tablespointvalueadditionleft + S (pft_index_negateall_tables) = (p)) /\ (((exists pfa_gap_negateall_tablespointvalueadditionright. pfa_gap_negateall_tablespointvalueadditionright + S (pft_value_negateall_tables) = (p)) /\ ((((exists pfa_gap_negateall_tablespointvalueadditionresultbound. pfa_gap_negateall_tablespointvalueadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negateall_tablespointvalueadditionresultcongruence pfa_offset_right_negateall_tablespointvalueadditionresultcongruence. ((pft_index_negateall_tables) + (pft_value_negateall_tables)) + (p) * pfa_offset_left_negateall_tablespointvalueadditionresultcongruence = (0) + (p) * pfa_offset_right_negateall_tablespointvalueadditionresultcongruence)))))))))))))
  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 : exists b c. (forall pft_index_inverseall_tables. (exists pfa_gap_inverseall_tablesprefix. pfa_gap_inverseall_tablesprefix + S (pft_index_inverseall_tables) = (p)) -> exists pft_value_inverseall_tables. (((((exists ff_h_pft_inverseall_tablespointentry. ff_h_pft_inverseall_tablespointentry + S (pft_value_inverseall_tables) = S ((S (pft_index_inverseall_tables)) * c)) /\ exists ff_q_pft_inverseall_tablespointentry. b = ff_q_pft_inverseall_tablespointentry * S ((S (pft_index_inverseall_tables)) * c) + (pft_value_inverseall_tables))) /\ ((((exists pfa_gap_inverseall_tablespointvalueinput. pfa_gap_inverseall_tablespointvalueinput + S (pft_index_inverseall_tables) = (p)) /\ (((exists pfa_gap_inverseall_tablespointvalueoutput. pfa_gap_inverseall_tablespointvalueoutput + S (pft_value_inverseall_tables) = (p)) /\ ((((pft_index_inverseall_tables) = 0 /\ (pft_value_inverseall_tables) = 0) \/ (((~((pft_index_inverseall_tables) = 0)) /\ ((((exists pfa_gap_inverseall_tablespointvaluenonzeromultiplicationleft. pfa_gap_inverseall_tablespointvaluenonzeromultiplicationleft + S (pft_index_inverseall_tables) = (p)) /\ (((exists pfa_gap_inverseall_tablespointvaluenonzeromultiplicationright. pfa_gap_inverseall_tablespointvaluenonzeromultiplicationright + S (pft_value_inverseall_tables) = (p)) /\ ((((exists pfa_gap_inverseall_tablespointvaluenonzeromultiplicationresultbound. pfa_gap_inverseall_tablespointvaluenonzeromultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_inverseall_tablespointvaluenonzeromultiplicationresultcongruence pfa_offset_right_inverseall_tablespointvaluenonzeromultiplicationresultcongruence. ((pft_index_inverseall_tables) * (pft_value_inverseall_tables)) + (p) * pfa_offset_left_inverseall_tablespointvaluenonzeromultiplicationresultcongruence = (1) + (p) * pfa_offset_right_inverseall_tablespointvaluenonzeromultiplicationresultcongruence))))))))))))))))))))))
  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