FP0010

prime_field_add_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 bracketings of three canonical add operands give the same actual result.

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

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

Definition DAG

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

Actual proof prerequisites

mod_eq_add · checked external prerequisitemod_eq_refl · checked external prerequisitemod_eq_trans · checked external prerequisiteadd_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_addassoc_firstleft. pfa_gap_addassoc_firstleft + S (a) = (p)) /\ (((exists pfa_gap_addassoc_firstright. pfa_gap_addassoc_firstright + S (b) = (p)) /\ ((((exists pfa_gap_addassoc_firstresultbound. pfa_gap_addassoc_firstresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_addassoc_firstresultcongruence pfa_offset_right_addassoc_firstresultcongruence. ((a) + (b)) + (p) * pfa_offset_left_addassoc_firstresultcongruence = (x) + (p) * pfa_offset_right_addassoc_firstresultcongruence))))))))) -> (((exists pfa_gap_addassoc_leftleft. pfa_gap_addassoc_leftleft + S (x) = (p)) /\ (((exists pfa_gap_addassoc_leftright. pfa_gap_addassoc_leftright + S (c) = (p)) /\ ((((exists pfa_gap_addassoc_leftresultbound. pfa_gap_addassoc_leftresultbound + S (u) = (p)) /\ ((exists pfa_offset_left_addassoc_leftresultcongruence pfa_offset_right_addassoc_leftresultcongruence. ((x) + (c)) + (p) * pfa_offset_left_addassoc_leftresultcongruence = (u) + (p) * pfa_offset_right_addassoc_leftresultcongruence))))))))) -> (((exists pfa_gap_addassoc_secondleft. pfa_gap_addassoc_secondleft + S (b) = (p)) /\ (((exists pfa_gap_addassoc_secondright. pfa_gap_addassoc_secondright + S (c) = (p)) /\ ((((exists pfa_gap_addassoc_secondresultbound. pfa_gap_addassoc_secondresultbound + S (y) = (p)) /\ ((exists pfa_offset_left_addassoc_secondresultcongruence pfa_offset_right_addassoc_secondresultcongruence. ((b) + (c)) + (p) * pfa_offset_left_addassoc_secondresultcongruence = (y) + (p) * pfa_offset_right_addassoc_secondresultcongruence))))))))) -> (((exists pfa_gap_addassoc_rightleft. pfa_gap_addassoc_rightleft + S (a) = (p)) /\ (((exists pfa_gap_addassoc_rightright. pfa_gap_addassoc_rightright + S (y) = (p)) /\ ((((exists pfa_gap_addassoc_rightresultbound. pfa_gap_addassoc_rightresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_addassoc_rightresultcongruence pfa_offset_right_addassoc_rightresultcongruence. ((a) + (y)) + (p) * pfa_offset_left_addassoc_rightresultcongruence = (v) + (p) * pfa_offset_right_addassoc_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_add (p)
  8. L34
    specialize mod_eq_add (a + b)
  9. L35
    specialize mod_eq_add (x)
  10. L36
    specialize mod_eq_add (c)
08Use earlier factsL37–43

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

  1. L37
    specialize mod_eq_add (c)
  2. L38
    apply mod_eq_add
  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_add (p)
  8. L53
    specialize mod_eq_add (a)
  9. L54
    specialize mod_eq_add (a)
  10. L55
    specialize mod_eq_add (b + c)
12Use earlier factsL56–65

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

  1. L56
    specialize mod_eq_add (y)
  2. L57
    apply mod_eq_add
  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 add_assoc (a)
  10. L75
    specialize add_assoc (b)
14Use earlier factsL76–78

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

  1. L76
    specialize add_assoc (c)
  2. L77
    apply add_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_add (p)
  34. 0034specialize mod_eq_add (a + b)
  35. 0035specialize mod_eq_add (x)
  36. 0036specialize mod_eq_add (c)
  37. 0037specialize mod_eq_add (c)
  38. 0038apply mod_eq_add
  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_add (p)
  53. 0053specialize mod_eq_add (a)
  54. 0054specialize mod_eq_add (a)
  55. 0055specialize mod_eq_add (b + c)
  56. 0056specialize mod_eq_add (y)
  57. 0057apply mod_eq_add
  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 add_assoc (a)
  75. 0075specialize add_assoc (b)
  76. 0076specialize add_assoc (c)
  77. 0077apply add_assoc
  78. 0078exact hr