FP0011

prime_field_multiply_associative

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

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. ∀ a. ∀ b. ∀ c. ∀ x. ∀ y. ∀ u. ∀ v. FpMul(p,a,b,x) → FpMul(p,x,c,u) → FpMul(p,b,c,y) → FpMul(p,a,y,v) → u = v

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

Definition DAG

CanonicalModularResidue(m,a,r) · 2FpMul(p,a,b,c) · 4

Actual proof prerequisites

mod_eq_mul · checked external prerequisitemod_eq_refl · checked external prerequisitemod_eq_trans · checked external prerequisitemul_assoc · checked external prerequisitebinary_canonical_residue_functional · checked external prerequisiteprime_field_residue_input_equal
Original expanded first-order 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

Complete tactic proof in conservative notation

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

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.

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 (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 : CanonicalModularResidue(p,a · b · c,u)Definitions: CanonicalModularResidue(p,a · b · c,u)Original native command in the exact edition
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 : CanonicalModularResidue(p,a · (b · c),v)Definitions: CanonicalModularResidue(p,a · (b · c),v)Original native command in the exact edition
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 defined 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 : CanonicalModularResidue(p,a · b · c,u)
  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 : CanonicalModularResidue(p,a · (b · c),v)
  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