FP0012

prime_field_left_distributive

Actual left distributivity of multiplication over addition on bounded representatives.

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. ∀ s. ∀ x. ∀ y. ∀ u. ∀ v. FpAdd(p,b,c,s) → FpMul(p,a,s,u) → FpMul(p,a,b,x) → FpMul(p,a,c,y) → FpAdd(p,x,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) · 2FpMul(p,a,b,c) · 3

Actual proof prerequisites

mod_eq_mul_left · checked external prerequisitemod_eq_trans · checked external prerequisitemod_eq_add · checked external prerequisitemul_add · checked external prerequisitebinary_canonical_residue_functional · checked external prerequisiteprime_field_residue_input_equal
Original expanded first-order statement 
forall p a b c s x y u v. (((exists pfa_gap_leftdistribution_sumleft. pfa_gap_leftdistribution_sumleft + S (b) = (p)) /\ (((exists pfa_gap_leftdistribution_sumright. pfa_gap_leftdistribution_sumright + S (c) = (p)) /\ ((((exists pfa_gap_leftdistribution_sumresultbound. pfa_gap_leftdistribution_sumresultbound + S (s) = (p)) /\ ((exists pfa_offset_left_leftdistribution_sumresultcongruence pfa_offset_right_leftdistribution_sumresultcongruence. ((b) + (c)) + (p) * pfa_offset_left_leftdistribution_sumresultcongruence = (s) + (p) * pfa_offset_right_leftdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_leftdistribution_leftleft. pfa_gap_leftdistribution_leftleft + S (a) = (p)) /\ (((exists pfa_gap_leftdistribution_leftright. pfa_gap_leftdistribution_leftright + S (s) = (p)) /\ ((((exists pfa_gap_leftdistribution_leftresultbound. pfa_gap_leftdistribution_leftresultbound + S (u) = (p)) /\ ((exists pfa_offset_left_leftdistribution_leftresultcongruence pfa_offset_right_leftdistribution_leftresultcongruence. ((a) * (s)) + (p) * pfa_offset_left_leftdistribution_leftresultcongruence = (u) + (p) * pfa_offset_right_leftdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_leftdistribution_firstleft. pfa_gap_leftdistribution_firstleft + S (a) = (p)) /\ (((exists pfa_gap_leftdistribution_firstright. pfa_gap_leftdistribution_firstright + S (b) = (p)) /\ ((((exists pfa_gap_leftdistribution_firstresultbound. pfa_gap_leftdistribution_firstresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_leftdistribution_firstresultcongruence pfa_offset_right_leftdistribution_firstresultcongruence. ((a) * (b)) + (p) * pfa_offset_left_leftdistribution_firstresultcongruence = (x) + (p) * pfa_offset_right_leftdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_leftdistribution_secondleft. pfa_gap_leftdistribution_secondleft + S (a) = (p)) /\ (((exists pfa_gap_leftdistribution_secondright. pfa_gap_leftdistribution_secondright + S (c) = (p)) /\ ((((exists pfa_gap_leftdistribution_secondresultbound. pfa_gap_leftdistribution_secondresultbound + S (y) = (p)) /\ ((exists pfa_offset_left_leftdistribution_secondresultcongruence pfa_offset_right_leftdistribution_secondresultcongruence. ((a) * (c)) + (p) * pfa_offset_left_leftdistribution_secondresultcongruence = (y) + (p) * pfa_offset_right_leftdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_leftdistribution_rightleft. pfa_gap_leftdistribution_rightleft + S (x) = (p)) /\ (((exists pfa_gap_leftdistribution_rightright. pfa_gap_leftdistribution_rightright + S (y) = (p)) /\ ((((exists pfa_gap_leftdistribution_rightresultbound. pfa_gap_leftdistribution_rightresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_leftdistribution_rightresultcongruence pfa_offset_right_leftdistribution_rightresultcongruence. ((x) + (y)) + (p) * pfa_offset_left_leftdistribution_rightresultcongruence = (v) + (p) * pfa_offset_right_leftdistribution_rightresultcongruence))))))))) -> u = v

Complete tactic proof in conservative notation

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

77 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 s
  6. L6
    intro x
  7. L7
    intro y
  8. L8
    intro u
  9. L9
    intro v
  10. L10
    intro hsum
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hleft
  2. L12
    intro hfirst
  3. L13
    intro hsecond
  4. L14
    intro hright
03Separate the logical casesL15–24

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

  1. L15
    cases hsum
  2. L16
    cases hsum_right
  3. L17
    cases hsum_right_right
  4. L18
    cases hleft
  5. L19
    cases hleft_right
  6. L20
    cases hleft_right_right
  7. L21
    cases hfirst
  8. L22
    cases hfirst_right
  9. L23
    cases hfirst_right_right
  10. L24
    cases hsecond
04Separate the logical casesL25–29

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

  1. L25
    cases hsecond_right
  2. L26
    cases hsecond_right_right
  3. L27
    cases hright
  4. L28
    cases hright_right
  5. L29
    cases hright_right_right
05Establish hlL30–30

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

  1. L30
    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 casesL31–31

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

  1. L31
    split
07Use earlier factsL32–41

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

  1. L32
    exact hleft_right_right_left
  2. L33
    specialize mod_eq_trans (p)
  3. L34
    specialize mod_eq_trans (a * (b + c))
  4. L35
    specialize mod_eq_trans (a * s)
  5. L36
    specialize mod_eq_trans (u)
  6. L37
    apply mod_eq_trans
  7. L38
    specialize mod_eq_mul_left (p)
  8. L39
    specialize mod_eq_mul_left (b + c)
  9. L40
    specialize mod_eq_mul_left (s)
  10. L41
    specialize mod_eq_mul_left (a)
08Use earlier factsL42–44

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

  1. L42
    apply mod_eq_mul_left
  2. L43
    exact hsum_right_right_right
  3. L44
    exact hleft_right_right_right
09Establish hrL45–45

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

  1. L45
    have hr : CanonicalModularResidue(p,a · b + a · c,v)Definitions: CanonicalModularResidue(p,a · b + a · c,v)Original native command in the exact edition
10Separate the logical casesL46–46

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

  1. L46
    split
11Use earlier factsL47–56

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

  1. L47
    exact hright_right_right_left
  2. L48
    specialize mod_eq_trans (p)
  3. L49
    specialize mod_eq_trans (a * b + a * c)
  4. L50
    specialize mod_eq_trans (x + y)
  5. L51
    specialize mod_eq_trans (v)
  6. L52
    apply mod_eq_trans
  7. L53
    specialize mod_eq_add (p)
  8. L54
    specialize mod_eq_add (a * b)
  9. L55
    specialize mod_eq_add (x)
  10. L56
    specialize mod_eq_add (a * c)
12Use earlier factsL57–66

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

  1. L57
    specialize mod_eq_add (y)
  2. L58
    apply mod_eq_add
  3. L59
    exact hfirst_right_right_right
  4. L60
    exact hsecond_right_right_right
  5. L61
    exact hright_right_right_right
  6. L62
    specialize binary_canonical_residue_functional (p)
  7. L63
    specialize binary_canonical_residue_functional (a * (b + c))
  8. L64
    specialize binary_canonical_residue_functional (u)
  9. L65
    specialize binary_canonical_residue_functional (v)
  10. L66
    apply binary_canonical_residue_functional
13Use earlier factsL67–76

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

  1. L67
    exact hl
  2. L68
    specialize prime_field_residue_input_equal (p)
  3. L69
    specialize prime_field_residue_input_equal (a * (b + c))
  4. L70
    specialize prime_field_residue_input_equal (a * b + a * c)
  5. L71
    specialize prime_field_residue_input_equal (v)
  6. L72
    apply prime_field_residue_input_equal
  7. L73
    specialize mul_add (a)
  8. L74
    specialize mul_add (b)
  9. L75
    specialize mul_add (c)
  10. L76
    apply mul_add
14Use earlier factsL77–77

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

  1. L77
    exact hr

Library-wide reading audit

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