FP0011

prime_field_multiply_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.

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

Both bracketings of three canonical multiply operands give the same actual result.

Exact expanded first-order arithmetic statement

forall p a b c x y u v. (((exists pfa_gap_multiplyassoc_firstleft. pfa_gap_multiplyassoc_firstleft + S (a) = (p)) /\ (((exists pfa_gap_multiplyassoc_firstright. pfa_gap_multiplyassoc_firstright + S (b) = (p)) /\ ((((exists pfa_gap_multiplyassoc_firstresultbound. pfa_gap_multiplyassoc_firstresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_multiplyassoc_firstresultcongruence pfa_offset_right_multiplyassoc_firstresultcongruence. ((a) * (b)) + (p) * pfa_offset_left_multiplyassoc_firstresultcongruence = (x) + (p) * pfa_offset_right_multiplyassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_multiplyassoc_leftleft. pfa_gap_multiplyassoc_leftleft + S (x) = (p)) /\ (((exists pfa_gap_multiplyassoc_leftright. pfa_gap_multiplyassoc_leftright + S (c) = (p)) /\ ((((exists pfa_gap_multiplyassoc_leftresultbound. pfa_gap_multiplyassoc_leftresultbound + S (u) = (p)) /\ ((exists pfa_offset_left_multiplyassoc_leftresultcongruence pfa_offset_right_multiplyassoc_leftresultcongruence. ((x) * (c)) + (p) * pfa_offset_left_multiplyassoc_leftresultcongruence = (u) + (p) * pfa_offset_right_multiplyassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_multiplyassoc_secondleft. pfa_gap_multiplyassoc_secondleft + S (b) = (p)) /\ (((exists pfa_gap_multiplyassoc_secondright. pfa_gap_multiplyassoc_secondright + S (c) = (p)) /\ ((((exists pfa_gap_multiplyassoc_secondresultbound. pfa_gap_multiplyassoc_secondresultbound + S (y) = (p)) /\ ((exists pfa_offset_left_multiplyassoc_secondresultcongruence pfa_offset_right_multiplyassoc_secondresultcongruence. ((b) * (c)) + (p) * pfa_offset_left_multiplyassoc_secondresultcongruence = (y) + (p) * pfa_offset_right_multiplyassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_multiplyassoc_rightleft. pfa_gap_multiplyassoc_rightleft + S (a) = (p)) /\ (((exists pfa_gap_multiplyassoc_rightright. pfa_gap_multiplyassoc_rightright + S (y) = (p)) /\ ((((exists pfa_gap_multiplyassoc_rightresultbound. pfa_gap_multiplyassoc_rightresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_multiplyassoc_rightresultcongruence pfa_offset_right_multiplyassoc_rightresultcongruence. ((a) * (y)) + (p) * pfa_offset_left_multiplyassoc_rightresultcongruence = (v) + (p) * pfa_offset_right_multiplyassoc_rightresultcongruence))))))))) -> u = v

Constructive proof overview

Generated structural guide

Both bracketings of three canonical multiply operands give the same actual result.

The unchanged tactic script uses 6 declared prerequisites and contains 78 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

mod_eq_mul Alpha theorem; checked-use authorized mod_eq_refl Alpha theorem; checked-use authorized mod_eq_trans Alpha theorem; checked-use authorized mul_assoc Alpha theorem; checked-use authorized binary_canonical_residue_functional Alpha theorem; checked-use authorized FP0004 prime_field_residue_input_equal

Direct dependents

FP002A prime_field_arithmetic_laws FP0045 prime_field_multiply_table_associative

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

78 script commands · 14 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 (1)
prime field residue input equal
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 b
  4. L4
    intro c
  5. L5
    intro x
  6. L6
    intro y
  7. L7
    intro u
  8. L8
    intro v
  9. L9
    intro hfirst
  10. L10
    intro hleft
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hsecond
  2. L12
    intro hright
03Separate the logical casesL13–22

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

  1. L13
    cases hfirst
  2. L14
    cases hfirst_right
  3. L15
    cases hfirst_right_right
  4. L16
    cases hleft
  5. L17
    cases hleft_right
  6. L18
    cases hleft_right_right
  7. L19
    cases hsecond
  8. L20
    cases hsecond_right
  9. L21
    cases hsecond_right_right
  10. L22
    cases hright
04Separate the logical casesL23–24

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

  1. L23
    cases hright_right
  2. L24
    cases hright_right_right
05Establish hlL25–25

Establish this local claim before using it. It is not an additional assumption.

  1. L25
    have hl : ((exists pfa_gap_multiplyassoc_raw_leftbound. pfa_gap_multiplyassoc_raw_leftbound + S (u) = (p)) /\ ((exists pfa_offset_left_multiplyassoc_raw_leftcongruence pfa_offset_right_multiplyassoc_raw_leftcongruence. ((a * b) * c) + (p) * pfa_offset_left_multiplyassoc_raw_leftcongruence = (u) + (p) * pfa_offset_right_multiplyassoc_raw_leftcongruence)))
06Separate the logical casesL26–26

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

  1. L26
    split
07Use earlier factsL27–36

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

  1. L27
    exact hleft_right_right_left
  2. L28
    specialize mod_eq_trans (p)
  3. L29
    specialize mod_eq_trans ((a * b) * c)
  4. L30
    specialize mod_eq_trans (x * c)
  5. L31
    specialize mod_eq_trans (u)
  6. L32
    apply mod_eq_trans
  7. L33
    specialize mod_eq_mul (p)
  8. L34
    specialize mod_eq_mul (a * b)
  9. L35
    specialize mod_eq_mul (x)
  10. L36
    specialize mod_eq_mul (c)
08Use earlier factsL37–43

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

  1. L37
    specialize mod_eq_mul (c)
  2. L38
    apply mod_eq_mul
  3. L39
    exact hfirst_right_right_right
  4. L40
    specialize mod_eq_refl (p)
  5. L41
    specialize mod_eq_refl (c)
  6. L42
    apply mod_eq_refl
  7. L43
    exact hleft_right_right_right
09Establish hrL44–44

Establish this local claim before using it. It is not an additional assumption.

  1. L44
    have hr : ((exists pfa_gap_multiplyassoc_raw_rightbound. pfa_gap_multiplyassoc_raw_rightbound + S (v) = (p)) /\ ((exists pfa_offset_left_multiplyassoc_raw_rightcongruence pfa_offset_right_multiplyassoc_raw_rightcongruence. (a * (b * c)) + (p) * pfa_offset_left_multiplyassoc_raw_rightcongruence = (v) + (p) * pfa_offset_right_multiplyassoc_raw_rightcongruence)))
10Separate the logical casesL45–45

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

  1. L45
    split
11Use earlier factsL46–55

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

  1. L46
    exact hright_right_right_left
  2. L47
    specialize mod_eq_trans (p)
  3. L48
    specialize mod_eq_trans (a * (b * c))
  4. L49
    specialize mod_eq_trans (a * y)
  5. L50
    specialize mod_eq_trans (v)
  6. L51
    apply mod_eq_trans
  7. L52
    specialize mod_eq_mul (p)
  8. L53
    specialize mod_eq_mul (a)
  9. L54
    specialize mod_eq_mul (a)
  10. L55
    specialize mod_eq_mul (b * c)
12Use earlier factsL56–65

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

  1. L56
    specialize mod_eq_mul (y)
  2. L57
    apply mod_eq_mul
  3. L58
    specialize mod_eq_refl (p)
  4. L59
    specialize mod_eq_refl (a)
  5. L60
    apply mod_eq_refl
  6. L61
    exact hsecond_right_right_right
  7. L62
    exact hright_right_right_right
  8. L63
    specialize binary_canonical_residue_functional (p)
  9. L64
    specialize binary_canonical_residue_functional ((a * b) * c)
  10. L65
    specialize binary_canonical_residue_functional (u)
13Use earlier factsL66–75

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

  1. L66
    specialize binary_canonical_residue_functional (v)
  2. L67
    apply binary_canonical_residue_functional
  3. L68
    exact hl
  4. L69
    specialize prime_field_residue_input_equal (p)
  5. L70
    specialize prime_field_residue_input_equal ((a * b) * c)
  6. L71
    specialize prime_field_residue_input_equal (a * (b * c))
  7. L72
    specialize prime_field_residue_input_equal (v)
  8. L73
    apply prime_field_residue_input_equal
  9. L74
    specialize mul_assoc (a)
  10. L75
    specialize mul_assoc (b)
14Use earlier factsL76–78

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

  1. L76
    specialize mul_assoc (c)
  2. L77
    apply mul_assoc
  3. L78
    exact hr

Library-wide reading audit

Original exact command ledger · 78 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro x
  6. 0006intro y
  7. 0007intro u
  8. 0008intro v
  9. 0009intro hfirst
  10. 0010intro hleft
  11. 0011intro hsecond
  12. 0012intro hright
  13. 0013cases hfirst
  14. 0014cases hfirst_right
  15. 0015cases hfirst_right_right
  16. 0016cases hleft
  17. 0017cases hleft_right
  18. 0018cases hleft_right_right
  19. 0019cases hsecond
  20. 0020cases hsecond_right
  21. 0021cases hsecond_right_right
  22. 0022cases hright
  23. 0023cases hright_right
  24. 0024cases hright_right_right
  25. 0025have hl : ((exists pfa_gap_multiplyassoc_raw_leftbound. pfa_gap_multiplyassoc_raw_leftbound + S (u) = (p)) /\ ((exists pfa_offset_left_multiplyassoc_raw_leftcongruence pfa_offset_right_multiplyassoc_raw_leftcongruence. ((a * b) * c) + (p) * pfa_offset_left_multiplyassoc_raw_leftcongruence = (u) + (p) * pfa_offset_right_multiplyassoc_raw_leftcongruence)))
  26. 0026split
  27. 0027exact hleft_right_right_left
  28. 0028specialize mod_eq_trans (p)
  29. 0029specialize mod_eq_trans ((a * b) * c)
  30. 0030specialize mod_eq_trans (x * c)
  31. 0031specialize mod_eq_trans (u)
  32. 0032apply mod_eq_trans
  33. 0033specialize mod_eq_mul (p)
  34. 0034specialize mod_eq_mul (a * b)
  35. 0035specialize mod_eq_mul (x)
  36. 0036specialize mod_eq_mul (c)
  37. 0037specialize mod_eq_mul (c)
  38. 0038apply mod_eq_mul
  39. 0039exact hfirst_right_right_right
  40. 0040specialize mod_eq_refl (p)
  41. 0041specialize mod_eq_refl (c)
  42. 0042apply mod_eq_refl
  43. 0043exact hleft_right_right_right
  44. 0044have hr : ((exists pfa_gap_multiplyassoc_raw_rightbound. pfa_gap_multiplyassoc_raw_rightbound + S (v) = (p)) /\ ((exists pfa_offset_left_multiplyassoc_raw_rightcongruence pfa_offset_right_multiplyassoc_raw_rightcongruence. (a * (b * c)) + (p) * pfa_offset_left_multiplyassoc_raw_rightcongruence = (v) + (p) * pfa_offset_right_multiplyassoc_raw_rightcongruence)))
  45. 0045split
  46. 0046exact hright_right_right_left
  47. 0047specialize mod_eq_trans (p)
  48. 0048specialize mod_eq_trans (a * (b * c))
  49. 0049specialize mod_eq_trans (a * y)
  50. 0050specialize mod_eq_trans (v)
  51. 0051apply mod_eq_trans
  52. 0052specialize mod_eq_mul (p)
  53. 0053specialize mod_eq_mul (a)
  54. 0054specialize mod_eq_mul (a)
  55. 0055specialize mod_eq_mul (b * c)
  56. 0056specialize mod_eq_mul (y)
  57. 0057apply mod_eq_mul
  58. 0058specialize mod_eq_refl (p)
  59. 0059specialize mod_eq_refl (a)
  60. 0060apply mod_eq_refl
  61. 0061exact hsecond_right_right_right
  62. 0062exact hright_right_right_right
  63. 0063specialize binary_canonical_residue_functional (p)
  64. 0064specialize binary_canonical_residue_functional ((a * b) * c)
  65. 0065specialize binary_canonical_residue_functional (u)
  66. 0066specialize binary_canonical_residue_functional (v)
  67. 0067apply binary_canonical_residue_functional
  68. 0068exact hl
  69. 0069specialize prime_field_residue_input_equal (p)
  70. 0070specialize prime_field_residue_input_equal ((a * b) * c)
  71. 0071specialize prime_field_residue_input_equal (a * (b * c))
  72. 0072specialize prime_field_residue_input_equal (v)
  73. 0073apply prime_field_residue_input_equal
  74. 0074specialize mul_assoc (a)
  75. 0075specialize mul_assoc (b)
  76. 0076specialize mul_assoc (c)
  77. 0077apply mul_assoc
  78. 0078exact hr