FP0045

prime_field_multiply_table_associative

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.

Both parenthesizations of three actual multiply table lookups agree, with intermediate bounds proved.

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

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. ∀ B. ∀ C. ∀ a. ∀ b. ∀ c. ∀ x. ∀ y. ∀ u. ∀ v. FpMulPrefix(p,B,C,p · p) → Lt(a,p) → Lt(b,p) → Lt(c,p) → BetaAt(B,C,a · p + b,x) → BetaAt(B,C,x · p + c,u) → BetaAt(B,C,b · p + c,y) → BetaAt(B,C,a · p + y,v) → u = v

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

Definition DAG

FpMul(p,a,b,c) · 2FpMulPrefix(p,b,c,l) · 1Lt(a,b) · 3BetaAt(b,c,i,x) · 4

Actual proof prerequisites

prime_field_multiply_table_lookupprime_field_multiply_associative
Original expanded first-order statement 
forall p B C a b c x y u v. (forall pft_index_multiplyassoc_table. (exists pfa_gap_multiplyassoc_tableprefix. pfa_gap_multiplyassoc_tableprefix + S (pft_index_multiplyassoc_table) = ((p) * (p))) -> exists pft_value_multiplyassoc_table. (((((exists ff_h_pft_multiplyassoc_tablepointentry. ff_h_pft_multiplyassoc_tablepointentry + S (pft_value_multiplyassoc_table) = S ((S (pft_index_multiplyassoc_table)) * C)) /\ exists ff_q_pft_multiplyassoc_tablepointentry. B = ff_q_pft_multiplyassoc_tablepointentry * S ((S (pft_index_multiplyassoc_table)) * C) + (pft_value_multiplyassoc_table))) /\ ((exists pft_row_multiplyassoc_tablepointvalue pft_column_multiplyassoc_tablepointvalue. (((pft_index_multiplyassoc_table) = pft_row_multiplyassoc_tablepointvalue * (p) + pft_column_multiplyassoc_tablepointvalue) /\ ((((exists pfa_gap_multiplyassoc_tablepointvalueoperationleft. pfa_gap_multiplyassoc_tablepointvalueoperationleft + S (pft_row_multiplyassoc_tablepointvalue) = (p)) /\ (((exists pfa_gap_multiplyassoc_tablepointvalueoperationright. pfa_gap_multiplyassoc_tablepointvalueoperationright + S (pft_column_multiplyassoc_tablepointvalue) = (p)) /\ ((((exists pfa_gap_multiplyassoc_tablepointvalueoperationresultbound. pfa_gap_multiplyassoc_tablepointvalueoperationresultbound + S (pft_value_multiplyassoc_table) = (p)) /\ ((exists pfa_offset_left_multiplyassoc_tablepointvalueoperationresultcongruence pfa_offset_right_multiplyassoc_tablepointvalueoperationresultcongruence. ((pft_row_multiplyassoc_tablepointvalue) * (pft_column_multiplyassoc_tablepointvalue)) + (p) * pfa_offset_left_multiplyassoc_tablepointvalueoperationresultcongruence = (pft_value_multiplyassoc_table) + (p) * pfa_offset_right_multiplyassoc_tablepointvalueoperationresultcongruence)))))))))))))))) -> (exists pfa_gap_multiplyassoc_a. pfa_gap_multiplyassoc_a + S (a) = (p)) -> (exists pfa_gap_multiplyassoc_b. pfa_gap_multiplyassoc_b + S (b) = (p)) -> (exists pfa_gap_multiplyassoc_c. pfa_gap_multiplyassoc_c + S (c) = (p)) -> (((exists ff_h_pft_multiplytable_assoc0. ff_h_pft_multiplytable_assoc0 + S (x) = S ((S (a*p+b)) * C)) /\ exists ff_q_pft_multiplytable_assoc0. B = ff_q_pft_multiplytable_assoc0 * S ((S (a*p+b)) * C) + (x))) -> (((exists ff_h_pft_multiplytable_assoc1. ff_h_pft_multiplytable_assoc1 + S (u) = S ((S (x*p+c)) * C)) /\ exists ff_q_pft_multiplytable_assoc1. B = ff_q_pft_multiplytable_assoc1 * S ((S (x*p+c)) * C) + (u))) -> (((exists ff_h_pft_multiplytable_assoc2. ff_h_pft_multiplytable_assoc2 + S (y) = S ((S (b*p+c)) * C)) /\ exists ff_q_pft_multiplytable_assoc2. B = ff_q_pft_multiplytable_assoc2 * S ((S (b*p+c)) * C) + (y))) -> (((exists ff_h_pft_multiplytable_assoc3. ff_h_pft_multiplytable_assoc3 + S (v) = S ((S (a*p+y)) * C)) /\ exists ff_q_pft_multiplytable_assoc3. B = ff_q_pft_multiplytable_assoc3 * S ((S (a*p+y)) * C) + (v))) -> u = v

Complete tactic proof in conservative notation

All 81 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

81 script commands · 12 reading checkpoints · 2 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 (2)
prime field multiply table lookupprime field multiply associative
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro B
  3. L3
    intro C
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro x
  8. L8
    intro y
  9. L9
    intro u
  10. L10
    intro v
02Fix variables and assumptionsL11–18

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

  1. L11
    intro htable
  2. L12
    intro ha
  3. L13
    intro hb
  4. L14
    intro hc
  5. L15
    intro hatfirst
  6. L16
    intro hatleft
  7. L17
    intro hatsecond
  8. L18
    intro hatright
03Establish hfirstL19–28

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

  1. L19
    have hfirst : FpMul(p,a,b,x)Definitions: FpMul(p,a,b,x)Original native command in the exact edition
  2. L20
    specialize prime_field_multiply_table_lookup (p)
  3. L21
    specialize prime_field_multiply_table_lookup (B)
  4. L22
    specialize prime_field_multiply_table_lookup (C)
  5. L23
    specialize prime_field_multiply_table_lookup (a)
  6. L24
    specialize prime_field_multiply_table_lookup (b)
  7. L25
    specialize prime_field_multiply_table_lookup (x)
  8. L26
    apply prime_field_multiply_table_lookup
  9. L27
    exact htable
  10. L28
    exact ha
04Use earlier factsL29–30

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

  1. L29
    exact hb
  2. L30
    exact hatfirst
05Separate the logical casesL31–33

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

  1. L31
    cases hfirst
  2. L32
    cases hfirst_right
  3. L33
    cases hfirst_right_right
06Establish hsecondL34–43

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

  1. L34
    have hsecond : FpMul(p,b,c,y)Definitions: FpMul(p,b,c,y)Original native command in the exact edition
  2. L35
    specialize prime_field_multiply_table_lookup (p)
  3. L36
    specialize prime_field_multiply_table_lookup (B)
  4. L37
    specialize prime_field_multiply_table_lookup (C)
  5. L38
    specialize prime_field_multiply_table_lookup (b)
  6. L39
    specialize prime_field_multiply_table_lookup (c)
  7. L40
    specialize prime_field_multiply_table_lookup (y)
  8. L41
    apply prime_field_multiply_table_lookup
  9. L42
    exact htable
  10. L43
    exact hb
07Use earlier factsL44–45

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

  1. L44
    exact hc
  2. L45
    exact hatsecond
08Separate the logical casesL46–48

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

  1. L46
    cases hsecond
  2. L47
    cases hsecond_right
  3. L48
    cases hsecond_right_right
09Use earlier factsL49–58

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

  1. L49
    specialize prime_field_multiply_associative (p)
  2. L50
    specialize prime_field_multiply_associative (a)
  3. L51
    specialize prime_field_multiply_associative (b)
  4. L52
    specialize prime_field_multiply_associative (c)
  5. L53
    specialize prime_field_multiply_associative (x)
  6. L54
    specialize prime_field_multiply_associative (y)
  7. L55
    specialize prime_field_multiply_associative (u)
  8. L56
    specialize prime_field_multiply_associative (v)
  9. L57
    apply prime_field_multiply_associative
  10. L58
    exact hfirst
10Use earlier factsL59–68

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

  1. L59
    specialize prime_field_multiply_table_lookup (p)
  2. L60
    specialize prime_field_multiply_table_lookup (B)
  3. L61
    specialize prime_field_multiply_table_lookup (C)
  4. L62
    specialize prime_field_multiply_table_lookup (x)
  5. L63
    specialize prime_field_multiply_table_lookup (c)
  6. L64
    specialize prime_field_multiply_table_lookup (u)
  7. L65
    apply prime_field_multiply_table_lookup
  8. L66
    exact htable
  9. L67
    exact hfirst_right_right_left
  10. L68
    exact hc
11Use earlier factsL69–78

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

  1. L69
    exact hatleft
  2. L70
    exact hsecond
  3. L71
    specialize prime_field_multiply_table_lookup (p)
  4. L72
    specialize prime_field_multiply_table_lookup (B)
  5. L73
    specialize prime_field_multiply_table_lookup (C)
  6. L74
    specialize prime_field_multiply_table_lookup (a)
  7. L75
    specialize prime_field_multiply_table_lookup (y)
  8. L76
    specialize prime_field_multiply_table_lookup (v)
  9. L77
    apply prime_field_multiply_table_lookup
  10. L78
    exact htable
12Use earlier factsL79–81

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

  1. L79
    exact ha
  2. L80
    exact hsecond_right_right_left
  3. L81
    exact hatright

Library-wide reading audit

Original defined command ledger · 81 lines
  1. 0001intro p
  2. 0002intro B
  3. 0003intro C
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro x
  8. 0008intro y
  9. 0009intro u
  10. 0010intro v
  11. 0011intro htable
  12. 0012intro ha
  13. 0013intro hb
  14. 0014intro hc
  15. 0015intro hatfirst
  16. 0016intro hatleft
  17. 0017intro hatsecond
  18. 0018intro hatright
  19. 0019have hfirst : FpMul(p,a,b,x)
  20. 0020specialize prime_field_multiply_table_lookup (p)
  21. 0021specialize prime_field_multiply_table_lookup (B)
  22. 0022specialize prime_field_multiply_table_lookup (C)
  23. 0023specialize prime_field_multiply_table_lookup (a)
  24. 0024specialize prime_field_multiply_table_lookup (b)
  25. 0025specialize prime_field_multiply_table_lookup (x)
  26. 0026apply prime_field_multiply_table_lookup
  27. 0027exact htable
  28. 0028exact ha
  29. 0029exact hb
  30. 0030exact hatfirst
  31. 0031cases hfirst
  32. 0032cases hfirst_right
  33. 0033cases hfirst_right_right
  34. 0034have hsecond : FpMul(p,b,c,y)
  35. 0035specialize prime_field_multiply_table_lookup (p)
  36. 0036specialize prime_field_multiply_table_lookup (B)
  37. 0037specialize prime_field_multiply_table_lookup (C)
  38. 0038specialize prime_field_multiply_table_lookup (b)
  39. 0039specialize prime_field_multiply_table_lookup (c)
  40. 0040specialize prime_field_multiply_table_lookup (y)
  41. 0041apply prime_field_multiply_table_lookup
  42. 0042exact htable
  43. 0043exact hb
  44. 0044exact hc
  45. 0045exact hatsecond
  46. 0046cases hsecond
  47. 0047cases hsecond_right
  48. 0048cases hsecond_right_right
  49. 0049specialize prime_field_multiply_associative (p)
  50. 0050specialize prime_field_multiply_associative (a)
  51. 0051specialize prime_field_multiply_associative (b)
  52. 0052specialize prime_field_multiply_associative (c)
  53. 0053specialize prime_field_multiply_associative (x)
  54. 0054specialize prime_field_multiply_associative (y)
  55. 0055specialize prime_field_multiply_associative (u)
  56. 0056specialize prime_field_multiply_associative (v)
  57. 0057apply prime_field_multiply_associative
  58. 0058exact hfirst
  59. 0059specialize prime_field_multiply_table_lookup (p)
  60. 0060specialize prime_field_multiply_table_lookup (B)
  61. 0061specialize prime_field_multiply_table_lookup (C)
  62. 0062specialize prime_field_multiply_table_lookup (x)
  63. 0063specialize prime_field_multiply_table_lookup (c)
  64. 0064specialize prime_field_multiply_table_lookup (u)
  65. 0065apply prime_field_multiply_table_lookup
  66. 0066exact htable
  67. 0067exact hfirst_right_right_left
  68. 0068exact hc
  69. 0069exact hatleft
  70. 0070exact hsecond
  71. 0071specialize prime_field_multiply_table_lookup (p)
  72. 0072specialize prime_field_multiply_table_lookup (B)
  73. 0073specialize prime_field_multiply_table_lookup (C)
  74. 0074specialize prime_field_multiply_table_lookup (a)
  75. 0075specialize prime_field_multiply_table_lookup (y)
  76. 0076specialize prime_field_multiply_table_lookup (v)
  77. 0077apply prime_field_multiply_table_lookup
  78. 0078exact htable
  79. 0079exact ha
  80. 0080exact hsecond_right_right_left
  81. 0081exact hatright