FP0043

prime_field_add_table_associative

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

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

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 B C a b c x y u v. (forall pft_index_addassoc_table. (exists pfa_gap_addassoc_tableprefix. pfa_gap_addassoc_tableprefix + S (pft_index_addassoc_table) = ((p) * (p))) -> exists pft_value_addassoc_table. (((((exists ff_h_pft_addassoc_tablepointentry. ff_h_pft_addassoc_tablepointentry + S (pft_value_addassoc_table) = S ((S (pft_index_addassoc_table)) * C)) /\ exists ff_q_pft_addassoc_tablepointentry. B = ff_q_pft_addassoc_tablepointentry * S ((S (pft_index_addassoc_table)) * C) + (pft_value_addassoc_table))) /\ ((exists pft_row_addassoc_tablepointvalue pft_column_addassoc_tablepointvalue. (((pft_index_addassoc_table) = pft_row_addassoc_tablepointvalue * (p) + pft_column_addassoc_tablepointvalue) /\ ((((exists pfa_gap_addassoc_tablepointvalueoperationleft. pfa_gap_addassoc_tablepointvalueoperationleft + S (pft_row_addassoc_tablepointvalue) = (p)) /\ (((exists pfa_gap_addassoc_tablepointvalueoperationright. pfa_gap_addassoc_tablepointvalueoperationright + S (pft_column_addassoc_tablepointvalue) = (p)) /\ ((((exists pfa_gap_addassoc_tablepointvalueoperationresultbound. pfa_gap_addassoc_tablepointvalueoperationresultbound + S (pft_value_addassoc_table) = (p)) /\ ((exists pfa_offset_left_addassoc_tablepointvalueoperationresultcongruence pfa_offset_right_addassoc_tablepointvalueoperationresultcongruence. ((pft_row_addassoc_tablepointvalue) + (pft_column_addassoc_tablepointvalue)) + (p) * pfa_offset_left_addassoc_tablepointvalueoperationresultcongruence = (pft_value_addassoc_table) + (p) * pfa_offset_right_addassoc_tablepointvalueoperationresultcongruence)))))))))))))))) -> (exists pfa_gap_addassoc_a. pfa_gap_addassoc_a + S (a) = (p)) -> (exists pfa_gap_addassoc_b. pfa_gap_addassoc_b + S (b) = (p)) -> (exists pfa_gap_addassoc_c. pfa_gap_addassoc_c + S (c) = (p)) -> (((exists ff_h_pft_addtable_assoc0. ff_h_pft_addtable_assoc0 + S (x) = S ((S (a*p+b)) * C)) /\ exists ff_q_pft_addtable_assoc0. B = ff_q_pft_addtable_assoc0 * S ((S (a*p+b)) * C) + (x))) -> (((exists ff_h_pft_addtable_assoc1. ff_h_pft_addtable_assoc1 + S (u) = S ((S (x*p+c)) * C)) /\ exists ff_q_pft_addtable_assoc1. B = ff_q_pft_addtable_assoc1 * S ((S (x*p+c)) * C) + (u))) -> (((exists ff_h_pft_addtable_assoc2. ff_h_pft_addtable_assoc2 + S (y) = S ((S (b*p+c)) * C)) /\ exists ff_q_pft_addtable_assoc2. B = ff_q_pft_addtable_assoc2 * S ((S (b*p+c)) * C) + (y))) -> (((exists ff_h_pft_addtable_assoc3. ff_h_pft_addtable_assoc3 + S (v) = S ((S (a*p+y)) * C)) /\ exists ff_q_pft_addtable_assoc3. B = ff_q_pft_addtable_assoc3 * S ((S (a*p+y)) * C) + (v))) -> u = v

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 81 exact native proof lines.

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

Proof neighborhood

Direct dependencies

FP0039 prime_field_add_table_lookup FP0010 prime_field_add_associative

Direct dependents

none

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

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.

Named ingredients (2)
prime field add table lookupprime field add 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 add table lookup.

  1. L19
    have hfirst : ((exists pfa_gap_addhfirstleft. pfa_gap_addhfirstleft + S (a) = (p)) /\ (((exists pfa_gap_addhfirstright. pfa_gap_addhfirstright + S (b) = (p)) /\ ((((exists pfa_gap_addhfirstresultbound. pfa_gap_addhfirstresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_addhfirstresultcongruence pfa_offset_right_addhfirstresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_addhfirstresultcongruence = (x) + (p) * pfa_offset_right_addhfirstresultcongruence))))))))
  2. L20
    specialize prime_field_add_table_lookup (p)
  3. L21
    specialize prime_field_add_table_lookup (B)
  4. L22
    specialize prime_field_add_table_lookup (C)
  5. L23
    specialize prime_field_add_table_lookup (a)
  6. L24
    specialize prime_field_add_table_lookup (b)
  7. L25
    specialize prime_field_add_table_lookup (x)
  8. L26
    apply prime_field_add_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 add table lookup.

  1. L34
    have hsecond : ((exists pfa_gap_addhsecondleft. pfa_gap_addhsecondleft + S (b) = (p)) /\ (((exists pfa_gap_addhsecondright. pfa_gap_addhsecondright + S (c) = (p)) /\ ((((exists pfa_gap_addhsecondresultbound. pfa_gap_addhsecondresultbound + S (y) = (p)) /\ ((exists pfa_offset_left_addhsecondresultcongruence pfa_offset_right_addhsecondresultcongruence. ((b) + (c)) + (p) * pfa_offset_left_addhsecondresultcongruence = (y) + (p) * pfa_offset_right_addhsecondresultcongruence))))))))
  2. L35
    specialize prime_field_add_table_lookup (p)
  3. L36
    specialize prime_field_add_table_lookup (B)
  4. L37
    specialize prime_field_add_table_lookup (C)
  5. L38
    specialize prime_field_add_table_lookup (b)
  6. L39
    specialize prime_field_add_table_lookup (c)
  7. L40
    specialize prime_field_add_table_lookup (y)
  8. L41
    apply prime_field_add_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_add_associative (p)
  2. L50
    specialize prime_field_add_associative (a)
  3. L51
    specialize prime_field_add_associative (b)
  4. L52
    specialize prime_field_add_associative (c)
  5. L53
    specialize prime_field_add_associative (x)
  6. L54
    specialize prime_field_add_associative (y)
  7. L55
    specialize prime_field_add_associative (u)
  8. L56
    specialize prime_field_add_associative (v)
  9. L57
    apply prime_field_add_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_add_table_lookup (p)
  2. L60
    specialize prime_field_add_table_lookup (B)
  3. L61
    specialize prime_field_add_table_lookup (C)
  4. L62
    specialize prime_field_add_table_lookup (x)
  5. L63
    specialize prime_field_add_table_lookup (c)
  6. L64
    specialize prime_field_add_table_lookup (u)
  7. L65
    apply prime_field_add_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_add_table_lookup (p)
  4. L72
    specialize prime_field_add_table_lookup (B)
  5. L73
    specialize prime_field_add_table_lookup (C)
  6. L74
    specialize prime_field_add_table_lookup (a)
  7. L75
    specialize prime_field_add_table_lookup (y)
  8. L76
    specialize prime_field_add_table_lookup (v)
  9. L77
    apply prime_field_add_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 exact 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 : ((exists pfa_gap_addhfirstleft. pfa_gap_addhfirstleft + S (a) = (p)) /\ (((exists pfa_gap_addhfirstright. pfa_gap_addhfirstright + S (b) = (p)) /\ ((((exists pfa_gap_addhfirstresultbound. pfa_gap_addhfirstresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_addhfirstresultcongruence pfa_offset_right_addhfirstresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_addhfirstresultcongruence = (x) + (p) * pfa_offset_right_addhfirstresultcongruence))))))))
  20. 0020specialize prime_field_add_table_lookup (p)
  21. 0021specialize prime_field_add_table_lookup (B)
  22. 0022specialize prime_field_add_table_lookup (C)
  23. 0023specialize prime_field_add_table_lookup (a)
  24. 0024specialize prime_field_add_table_lookup (b)
  25. 0025specialize prime_field_add_table_lookup (x)
  26. 0026apply prime_field_add_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 : ((exists pfa_gap_addhsecondleft. pfa_gap_addhsecondleft + S (b) = (p)) /\ (((exists pfa_gap_addhsecondright. pfa_gap_addhsecondright + S (c) = (p)) /\ ((((exists pfa_gap_addhsecondresultbound. pfa_gap_addhsecondresultbound + S (y) = (p)) /\ ((exists pfa_offset_left_addhsecondresultcongruence pfa_offset_right_addhsecondresultcongruence. ((b) + (c)) + (p) * pfa_offset_left_addhsecondresultcongruence = (y) + (p) * pfa_offset_right_addhsecondresultcongruence))))))))
  35. 0035specialize prime_field_add_table_lookup (p)
  36. 0036specialize prime_field_add_table_lookup (B)
  37. 0037specialize prime_field_add_table_lookup (C)
  38. 0038specialize prime_field_add_table_lookup (b)
  39. 0039specialize prime_field_add_table_lookup (c)
  40. 0040specialize prime_field_add_table_lookup (y)
  41. 0041apply prime_field_add_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_add_associative (p)
  50. 0050specialize prime_field_add_associative (a)
  51. 0051specialize prime_field_add_associative (b)
  52. 0052specialize prime_field_add_associative (c)
  53. 0053specialize prime_field_add_associative (x)
  54. 0054specialize prime_field_add_associative (y)
  55. 0055specialize prime_field_add_associative (u)
  56. 0056specialize prime_field_add_associative (v)
  57. 0057apply prime_field_add_associative
  58. 0058exact hfirst
  59. 0059specialize prime_field_add_table_lookup (p)
  60. 0060specialize prime_field_add_table_lookup (B)
  61. 0061specialize prime_field_add_table_lookup (C)
  62. 0062specialize prime_field_add_table_lookup (x)
  63. 0063specialize prime_field_add_table_lookup (c)
  64. 0064specialize prime_field_add_table_lookup (u)
  65. 0065apply prime_field_add_table_lookup
  66. 0066exact htable
  67. 0067exact hfirst_right_right_left
  68. 0068exact hc
  69. 0069exact hatleft
  70. 0070exact hsecond
  71. 0071specialize prime_field_add_table_lookup (p)
  72. 0072specialize prime_field_add_table_lookup (B)
  73. 0073specialize prime_field_add_table_lookup (C)
  74. 0074specialize prime_field_add_table_lookup (a)
  75. 0075specialize prime_field_add_table_lookup (y)
  76. 0076specialize prime_field_add_table_lookup (v)
  77. 0077apply prime_field_add_table_lookup
  78. 0078exact htable
  79. 0079exact ha
  80. 0080exact hsecond_right_right_left
  81. 0081exact hatright