FP0049

prime_field_right_table_distributive

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.

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

Actual finite addition and multiplication table entries satisfy right distributivity, with all intermediate bounds derived.

Exact expanded first-order arithmetic statement

forall p A D M E a b c s x y u v. (forall pft_index_righttable_distributive_add. (exists pfa_gap_righttable_distributive_addprefix. pfa_gap_righttable_distributive_addprefix + S (pft_index_righttable_distributive_add) = ((p) * (p))) -> exists pft_value_righttable_distributive_add. (((((exists ff_h_pft_righttable_distributive_addpointentry. ff_h_pft_righttable_distributive_addpointentry + S (pft_value_righttable_distributive_add) = S ((S (pft_index_righttable_distributive_add)) * D)) /\ exists ff_q_pft_righttable_distributive_addpointentry. A = ff_q_pft_righttable_distributive_addpointentry * S ((S (pft_index_righttable_distributive_add)) * D) + (pft_value_righttable_distributive_add))) /\ ((exists pft_row_righttable_distributive_addpointvalue pft_column_righttable_distributive_addpointvalue. (((pft_index_righttable_distributive_add) = pft_row_righttable_distributive_addpointvalue * (p) + pft_column_righttable_distributive_addpointvalue) /\ ((((exists pfa_gap_righttable_distributive_addpointvalueoperationleft. pfa_gap_righttable_distributive_addpointvalueoperationleft + S (pft_row_righttable_distributive_addpointvalue) = (p)) /\ (((exists pfa_gap_righttable_distributive_addpointvalueoperationright. pfa_gap_righttable_distributive_addpointvalueoperationright + S (pft_column_righttable_distributive_addpointvalue) = (p)) /\ ((((exists pfa_gap_righttable_distributive_addpointvalueoperationresultbound. pfa_gap_righttable_distributive_addpointvalueoperationresultbound + S (pft_value_righttable_distributive_add) = (p)) /\ ((exists pfa_offset_left_righttable_distributive_addpointvalueoperationresultcongruence pfa_offset_right_righttable_distributive_addpointvalueoperationresultcongruence. ((pft_row_righttable_distributive_addpointvalue) + (pft_column_righttable_distributive_addpointvalue)) + (p) * pfa_offset_left_righttable_distributive_addpointvalueoperationresultcongruence = (pft_value_righttable_distributive_add) + (p) * pfa_offset_right_righttable_distributive_addpointvalueoperationresultcongruence)))))))))))))))) -> (forall pft_index_righttable_distributive_mul. (exists pfa_gap_righttable_distributive_mulprefix. pfa_gap_righttable_distributive_mulprefix + S (pft_index_righttable_distributive_mul) = ((p) * (p))) -> exists pft_value_righttable_distributive_mul. (((((exists ff_h_pft_righttable_distributive_mulpointentry. ff_h_pft_righttable_distributive_mulpointentry + S (pft_value_righttable_distributive_mul) = S ((S (pft_index_righttable_distributive_mul)) * E)) /\ exists ff_q_pft_righttable_distributive_mulpointentry. M = ff_q_pft_righttable_distributive_mulpointentry * S ((S (pft_index_righttable_distributive_mul)) * E) + (pft_value_righttable_distributive_mul))) /\ ((exists pft_row_righttable_distributive_mulpointvalue pft_column_righttable_distributive_mulpointvalue. (((pft_index_righttable_distributive_mul) = pft_row_righttable_distributive_mulpointvalue * (p) + pft_column_righttable_distributive_mulpointvalue) /\ ((((exists pfa_gap_righttable_distributive_mulpointvalueoperationleft. pfa_gap_righttable_distributive_mulpointvalueoperationleft + S (pft_row_righttable_distributive_mulpointvalue) = (p)) /\ (((exists pfa_gap_righttable_distributive_mulpointvalueoperationright. pfa_gap_righttable_distributive_mulpointvalueoperationright + S (pft_column_righttable_distributive_mulpointvalue) = (p)) /\ ((((exists pfa_gap_righttable_distributive_mulpointvalueoperationresultbound. pfa_gap_righttable_distributive_mulpointvalueoperationresultbound + S (pft_value_righttable_distributive_mul) = (p)) /\ ((exists pfa_offset_left_righttable_distributive_mulpointvalueoperationresultcongruence pfa_offset_right_righttable_distributive_mulpointvalueoperationresultcongruence. ((pft_row_righttable_distributive_mulpointvalue) * (pft_column_righttable_distributive_mulpointvalue)) + (p) * pfa_offset_left_righttable_distributive_mulpointvalueoperationresultcongruence = (pft_value_righttable_distributive_mul) + (p) * pfa_offset_right_righttable_distributive_mulpointvalueoperationresultcongruence)))))))))))))))) -> (exists pfa_gap_righttable_distributive_a. pfa_gap_righttable_distributive_a + S (a) = (p)) -> (exists pfa_gap_righttable_distributive_b. pfa_gap_righttable_distributive_b + S (b) = (p)) -> (exists pfa_gap_righttable_distributive_c. pfa_gap_righttable_distributive_c + S (c) = (p)) -> (((exists ff_h_pft_righttable_distributive_sum. ff_h_pft_righttable_distributive_sum + S (s) = S ((S (b*p+c)) * D)) /\ exists ff_q_pft_righttable_distributive_sum. A = ff_q_pft_righttable_distributive_sum * S ((S (b*p+c)) * D) + (s))) -> (((exists ff_h_pft_righttable_distributive_left. ff_h_pft_righttable_distributive_left + S (u) = S ((S (s*p+a)) * E)) /\ exists ff_q_pft_righttable_distributive_left. M = ff_q_pft_righttable_distributive_left * S ((S (s*p+a)) * E) + (u))) -> (((exists ff_h_pft_righttable_distributive_first. ff_h_pft_righttable_distributive_first + S (x) = S ((S (b*p+a)) * E)) /\ exists ff_q_pft_righttable_distributive_first. M = ff_q_pft_righttable_distributive_first * S ((S (b*p+a)) * E) + (x))) -> (((exists ff_h_pft_righttable_distributive_second. ff_h_pft_righttable_distributive_second + S (y) = S ((S (c*p+a)) * E)) /\ exists ff_q_pft_righttable_distributive_second. M = ff_q_pft_righttable_distributive_second * S ((S (c*p+a)) * E) + (y))) -> (((exists ff_h_pft_righttable_distributive_right. ff_h_pft_righttable_distributive_right + S (v) = S ((S (x*p+y)) * D)) /\ exists ff_q_pft_righttable_distributive_right. A = ff_q_pft_righttable_distributive_right * S ((S (x*p+y)) * D) + (v))) -> u = v

Constructive proof overview

Generated structural guide

Actual finite addition and multiplication table entries satisfy right distributivity, with all intermediate bounds derived.

The unchanged tactic script uses 3 declared prerequisites and contains 103 exact native proof lines.

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

Proof neighborhood

Direct dependencies

FP0039 prime_field_add_table_lookup FP003C prime_field_multiply_table_lookup FP0013 prime_field_right_distributive

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. The literal dependency-closed bundle is checked by original HA and the independently compiled Lean verifier. Public delivery grants no Alpha checked-use authority or Stable membership.

Read the argument

Proof checkpoints

103 script commands · 16 reading checkpoints · 3 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 (3)
prime field add table lookupprime field multiply table lookupprime field right distributive
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro A
  3. L3
    intro D
  4. L4
    intro M
  5. L5
    intro E
  6. L6
    intro a
  7. L7
    intro b
  8. L8
    intro c
  9. L9
    intro s
  10. L10
    intro x
02Fix variables and assumptionsL11–20

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

  1. L11
    intro y
  2. L12
    intro u
  3. L13
    intro v
  4. L14
    intro haddtable
  5. L15
    intro hmultable
  6. L16
    intro ha
  7. L17
    intro hb
  8. L18
    intro hc
  9. L19
    intro hatsum
  10. L20
    intro hatleft
03Fix variables and assumptionsL21–23

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

  1. L21
    intro hatfirst
  2. L22
    intro hatsecond
  3. L23
    intro hatright
04Establish hsumL24–33

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

  1. L24
    have hsum : ((exists pfa_gap_righttable_sum_graphleft. pfa_gap_righttable_sum_graphleft + S (b) = (p)) /\ (((exists pfa_gap_righttable_sum_graphright. pfa_gap_righttable_sum_graphright + S (c) = (p)) /\ ((((exists pfa_gap_righttable_sum_graphresultbound. pfa_gap_righttable_sum_graphresultbound + S (s) = (p)) /\ ((exists pfa_offset_left_righttable_sum_graphresultcongruence pfa_offset_right_righttable_sum_graphresultcongruence. ((b) + (c)) + (p) * pfa_offset_left_righttable_sum_graphresultcongruence = (s) + (p) * pfa_offset_right_righttable_sum_graphresultcongruence))))))))
  2. L25
    specialize prime_field_add_table_lookup (p)
  3. L26
    specialize prime_field_add_table_lookup (A)
  4. L27
    specialize prime_field_add_table_lookup (D)
  5. L28
    specialize prime_field_add_table_lookup (b)
  6. L29
    specialize prime_field_add_table_lookup (c)
  7. L30
    specialize prime_field_add_table_lookup (s)
  8. L31
    apply prime_field_add_table_lookup
  9. L32
    exact haddtable
  10. L33
    exact hb
05Use earlier factsL34–35

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

  1. L34
    exact hc
  2. L35
    exact hatsum
06Separate the logical casesL36–38

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

  1. L36
    cases hsum
  2. L37
    cases hsum_right
  3. L38
    cases hsum_right_right
07Establish hfirstL39–48

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

  1. L39
    have hfirst : ((exists pfa_gap_righthfirstgraphleft. pfa_gap_righthfirstgraphleft + S (b) = (p)) /\ (((exists pfa_gap_righthfirstgraphright. pfa_gap_righthfirstgraphright + S (a) = (p)) /\ ((((exists pfa_gap_righthfirstgraphresultbound. pfa_gap_righthfirstgraphresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_righthfirstgraphresultcongruence pfa_offset_right_righthfirstgraphresultcongruence. ((b) * (a)) + (p) * pfa_offset_left_righthfirstgraphresultcongruence = (x) + (p) * pfa_offset_right_righthfirstgraphresultcongruence))))))))
  2. L40
    specialize prime_field_multiply_table_lookup (p)
  3. L41
    specialize prime_field_multiply_table_lookup (M)
  4. L42
    specialize prime_field_multiply_table_lookup (E)
  5. L43
    specialize prime_field_multiply_table_lookup (b)
  6. L44
    specialize prime_field_multiply_table_lookup (a)
  7. L45
    specialize prime_field_multiply_table_lookup (x)
  8. L46
    apply prime_field_multiply_table_lookup
  9. L47
    exact hmultable
  10. L48
    exact hb
08Use earlier factsL49–50

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

  1. L49
    exact ha
  2. L50
    exact hatfirst
09Separate the logical casesL51–53

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

  1. L51
    cases hfirst
  2. L52
    cases hfirst_right
  3. L53
    cases hfirst_right_right
10Establish hsecondL54–63

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

  1. L54
    have hsecond : ((exists pfa_gap_righthsecondgraphleft. pfa_gap_righthsecondgraphleft + S (c) = (p)) /\ (((exists pfa_gap_righthsecondgraphright. pfa_gap_righthsecondgraphright + S (a) = (p)) /\ ((((exists pfa_gap_righthsecondgraphresultbound. pfa_gap_righthsecondgraphresultbound + S (y) = (p)) /\ ((exists pfa_offset_left_righthsecondgraphresultcongruence pfa_offset_right_righthsecondgraphresultcongruence. ((c) * (a)) + (p) * pfa_offset_left_righthsecondgraphresultcongruence = (y) + (p) * pfa_offset_right_righthsecondgraphresultcongruence))))))))
  2. L55
    specialize prime_field_multiply_table_lookup (p)
  3. L56
    specialize prime_field_multiply_table_lookup (M)
  4. L57
    specialize prime_field_multiply_table_lookup (E)
  5. L58
    specialize prime_field_multiply_table_lookup (c)
  6. L59
    specialize prime_field_multiply_table_lookup (a)
  7. L60
    specialize prime_field_multiply_table_lookup (y)
  8. L61
    apply prime_field_multiply_table_lookup
  9. L62
    exact hmultable
  10. L63
    exact hc
11Use earlier factsL64–65

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

  1. L64
    exact ha
  2. L65
    exact hatsecond
12Separate the logical casesL66–68

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

  1. L66
    cases hsecond
  2. L67
    cases hsecond_right
  3. L68
    cases hsecond_right_right
13Use earlier factsL69–78

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

  1. L69
    specialize prime_field_right_distributive (p)
  2. L70
    specialize prime_field_right_distributive (a)
  3. L71
    specialize prime_field_right_distributive (b)
  4. L72
    specialize prime_field_right_distributive (c)
  5. L73
    specialize prime_field_right_distributive (s)
  6. L74
    specialize prime_field_right_distributive (x)
  7. L75
    specialize prime_field_right_distributive (y)
  8. L76
    specialize prime_field_right_distributive (u)
  9. L77
    specialize prime_field_right_distributive (v)
  10. L78
    apply prime_field_right_distributive
14Use earlier factsL79–88

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

  1. L79
    exact hsum
  2. L80
    specialize prime_field_multiply_table_lookup (p)
  3. L81
    specialize prime_field_multiply_table_lookup (M)
  4. L82
    specialize prime_field_multiply_table_lookup (E)
  5. L83
    specialize prime_field_multiply_table_lookup (s)
  6. L84
    specialize prime_field_multiply_table_lookup (a)
  7. L85
    specialize prime_field_multiply_table_lookup (u)
  8. L86
    apply prime_field_multiply_table_lookup
  9. L87
    exact hmultable
  10. L88
    exact hsum_right_right_left
15Use earlier factsL89–98

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

  1. L89
    exact ha
  2. L90
    exact hatleft
  3. L91
    exact hfirst
  4. L92
    exact hsecond
  5. L93
    specialize prime_field_add_table_lookup (p)
  6. L94
    specialize prime_field_add_table_lookup (A)
  7. L95
    specialize prime_field_add_table_lookup (D)
  8. L96
    specialize prime_field_add_table_lookup (x)
  9. L97
    specialize prime_field_add_table_lookup (y)
  10. L98
    specialize prime_field_add_table_lookup (v)
16Use earlier factsL99–103

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

  1. L99
    apply prime_field_add_table_lookup
  2. L100
    exact haddtable
  3. L101
    exact hfirst_right_right_left
  4. L102
    exact hsecond_right_right_left
  5. L103
    exact hatright

Library-wide reading audit

Original exact command ledger · 103 lines
  1. 0001intro p
  2. 0002intro A
  3. 0003intro D
  4. 0004intro M
  5. 0005intro E
  6. 0006intro a
  7. 0007intro b
  8. 0008intro c
  9. 0009intro s
  10. 0010intro x
  11. 0011intro y
  12. 0012intro u
  13. 0013intro v
  14. 0014intro haddtable
  15. 0015intro hmultable
  16. 0016intro ha
  17. 0017intro hb
  18. 0018intro hc
  19. 0019intro hatsum
  20. 0020intro hatleft
  21. 0021intro hatfirst
  22. 0022intro hatsecond
  23. 0023intro hatright
  24. 0024have hsum : ((exists pfa_gap_righttable_sum_graphleft. pfa_gap_righttable_sum_graphleft + S (b) = (p)) /\ (((exists pfa_gap_righttable_sum_graphright. pfa_gap_righttable_sum_graphright + S (c) = (p)) /\ ((((exists pfa_gap_righttable_sum_graphresultbound. pfa_gap_righttable_sum_graphresultbound + S (s) = (p)) /\ ((exists pfa_offset_left_righttable_sum_graphresultcongruence pfa_offset_right_righttable_sum_graphresultcongruence. ((b) + (c)) + (p) * pfa_offset_left_righttable_sum_graphresultcongruence = (s) + (p) * pfa_offset_right_righttable_sum_graphresultcongruence))))))))
  25. 0025specialize prime_field_add_table_lookup (p)
  26. 0026specialize prime_field_add_table_lookup (A)
  27. 0027specialize prime_field_add_table_lookup (D)
  28. 0028specialize prime_field_add_table_lookup (b)
  29. 0029specialize prime_field_add_table_lookup (c)
  30. 0030specialize prime_field_add_table_lookup (s)
  31. 0031apply prime_field_add_table_lookup
  32. 0032exact haddtable
  33. 0033exact hb
  34. 0034exact hc
  35. 0035exact hatsum
  36. 0036cases hsum
  37. 0037cases hsum_right
  38. 0038cases hsum_right_right
  39. 0039have hfirst : ((exists pfa_gap_righthfirstgraphleft. pfa_gap_righthfirstgraphleft + S (b) = (p)) /\ (((exists pfa_gap_righthfirstgraphright. pfa_gap_righthfirstgraphright + S (a) = (p)) /\ ((((exists pfa_gap_righthfirstgraphresultbound. pfa_gap_righthfirstgraphresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_righthfirstgraphresultcongruence pfa_offset_right_righthfirstgraphresultcongruence. ((b) * (a)) + (p) * pfa_offset_left_righthfirstgraphresultcongruence = (x) + (p) * pfa_offset_right_righthfirstgraphresultcongruence))))))))
  40. 0040specialize prime_field_multiply_table_lookup (p)
  41. 0041specialize prime_field_multiply_table_lookup (M)
  42. 0042specialize prime_field_multiply_table_lookup (E)
  43. 0043specialize prime_field_multiply_table_lookup (b)
  44. 0044specialize prime_field_multiply_table_lookup (a)
  45. 0045specialize prime_field_multiply_table_lookup (x)
  46. 0046apply prime_field_multiply_table_lookup
  47. 0047exact hmultable
  48. 0048exact hb
  49. 0049exact ha
  50. 0050exact hatfirst
  51. 0051cases hfirst
  52. 0052cases hfirst_right
  53. 0053cases hfirst_right_right
  54. 0054have hsecond : ((exists pfa_gap_righthsecondgraphleft. pfa_gap_righthsecondgraphleft + S (c) = (p)) /\ (((exists pfa_gap_righthsecondgraphright. pfa_gap_righthsecondgraphright + S (a) = (p)) /\ ((((exists pfa_gap_righthsecondgraphresultbound. pfa_gap_righthsecondgraphresultbound + S (y) = (p)) /\ ((exists pfa_offset_left_righthsecondgraphresultcongruence pfa_offset_right_righthsecondgraphresultcongruence. ((c) * (a)) + (p) * pfa_offset_left_righthsecondgraphresultcongruence = (y) + (p) * pfa_offset_right_righthsecondgraphresultcongruence))))))))
  55. 0055specialize prime_field_multiply_table_lookup (p)
  56. 0056specialize prime_field_multiply_table_lookup (M)
  57. 0057specialize prime_field_multiply_table_lookup (E)
  58. 0058specialize prime_field_multiply_table_lookup (c)
  59. 0059specialize prime_field_multiply_table_lookup (a)
  60. 0060specialize prime_field_multiply_table_lookup (y)
  61. 0061apply prime_field_multiply_table_lookup
  62. 0062exact hmultable
  63. 0063exact hc
  64. 0064exact ha
  65. 0065exact hatsecond
  66. 0066cases hsecond
  67. 0067cases hsecond_right
  68. 0068cases hsecond_right_right
  69. 0069specialize prime_field_right_distributive (p)
  70. 0070specialize prime_field_right_distributive (a)
  71. 0071specialize prime_field_right_distributive (b)
  72. 0072specialize prime_field_right_distributive (c)
  73. 0073specialize prime_field_right_distributive (s)
  74. 0074specialize prime_field_right_distributive (x)
  75. 0075specialize prime_field_right_distributive (y)
  76. 0076specialize prime_field_right_distributive (u)
  77. 0077specialize prime_field_right_distributive (v)
  78. 0078apply prime_field_right_distributive
  79. 0079exact hsum
  80. 0080specialize prime_field_multiply_table_lookup (p)
  81. 0081specialize prime_field_multiply_table_lookup (M)
  82. 0082specialize prime_field_multiply_table_lookup (E)
  83. 0083specialize prime_field_multiply_table_lookup (s)
  84. 0084specialize prime_field_multiply_table_lookup (a)
  85. 0085specialize prime_field_multiply_table_lookup (u)
  86. 0086apply prime_field_multiply_table_lookup
  87. 0087exact hmultable
  88. 0088exact hsum_right_right_left
  89. 0089exact ha
  90. 0090exact hatleft
  91. 0091exact hfirst
  92. 0092exact hsecond
  93. 0093specialize prime_field_add_table_lookup (p)
  94. 0094specialize prime_field_add_table_lookup (A)
  95. 0095specialize prime_field_add_table_lookup (D)
  96. 0096specialize prime_field_add_table_lookup (x)
  97. 0097specialize prime_field_add_table_lookup (y)
  98. 0098specialize prime_field_add_table_lookup (v)
  99. 0099apply prime_field_add_table_lookup
  100. 0100exact haddtable
  101. 0101exact hfirst_right_right_left
  102. 0102exact hsecond_right_right_left
  103. 0103exact hatright