FP0013

prime_field_right_distributive

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Actual right distributivity of multiplication over addition on bounded representatives.

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

Exact expanded first-order arithmetic statement

forall p a b c s x y u v. (((exists pfa_gap_rightdistribution_sumleft. pfa_gap_rightdistribution_sumleft + S (b) = (p)) /\ (((exists pfa_gap_rightdistribution_sumright. pfa_gap_rightdistribution_sumright + S (c) = (p)) /\ ((((exists pfa_gap_rightdistribution_sumresultbound. pfa_gap_rightdistribution_sumresultbound + S (s) = (p)) /\ ((exists pfa_offset_left_rightdistribution_sumresultcongruence pfa_offset_right_rightdistribution_sumresultcongruence. ((b) + (c)) + (p) * pfa_offset_left_rightdistribution_sumresultcongruence = (s) + (p) * pfa_offset_right_rightdistribution_sumresultcongruence))))))))) -> (((exists pfa_gap_rightdistribution_leftleft. pfa_gap_rightdistribution_leftleft + S (s) = (p)) /\ (((exists pfa_gap_rightdistribution_leftright. pfa_gap_rightdistribution_leftright + S (a) = (p)) /\ ((((exists pfa_gap_rightdistribution_leftresultbound. pfa_gap_rightdistribution_leftresultbound + S (u) = (p)) /\ ((exists pfa_offset_left_rightdistribution_leftresultcongruence pfa_offset_right_rightdistribution_leftresultcongruence. ((s) * (a)) + (p) * pfa_offset_left_rightdistribution_leftresultcongruence = (u) + (p) * pfa_offset_right_rightdistribution_leftresultcongruence))))))))) -> (((exists pfa_gap_rightdistribution_firstleft. pfa_gap_rightdistribution_firstleft + S (b) = (p)) /\ (((exists pfa_gap_rightdistribution_firstright. pfa_gap_rightdistribution_firstright + S (a) = (p)) /\ ((((exists pfa_gap_rightdistribution_firstresultbound. pfa_gap_rightdistribution_firstresultbound + S (x) = (p)) /\ ((exists pfa_offset_left_rightdistribution_firstresultcongruence pfa_offset_right_rightdistribution_firstresultcongruence. ((b) * (a)) + (p) * pfa_offset_left_rightdistribution_firstresultcongruence = (x) + (p) * pfa_offset_right_rightdistribution_firstresultcongruence))))))))) -> (((exists pfa_gap_rightdistribution_secondleft. pfa_gap_rightdistribution_secondleft + S (c) = (p)) /\ (((exists pfa_gap_rightdistribution_secondright. pfa_gap_rightdistribution_secondright + S (a) = (p)) /\ ((((exists pfa_gap_rightdistribution_secondresultbound. pfa_gap_rightdistribution_secondresultbound + S (y) = (p)) /\ ((exists pfa_offset_left_rightdistribution_secondresultcongruence pfa_offset_right_rightdistribution_secondresultcongruence. ((c) * (a)) + (p) * pfa_offset_left_rightdistribution_secondresultcongruence = (y) + (p) * pfa_offset_right_rightdistribution_secondresultcongruence))))))))) -> (((exists pfa_gap_rightdistribution_rightleft. pfa_gap_rightdistribution_rightleft + S (x) = (p)) /\ (((exists pfa_gap_rightdistribution_rightright. pfa_gap_rightdistribution_rightright + S (y) = (p)) /\ ((((exists pfa_gap_rightdistribution_rightresultbound. pfa_gap_rightdistribution_rightresultbound + S (v) = (p)) /\ ((exists pfa_offset_left_rightdistribution_rightresultcongruence pfa_offset_right_rightdistribution_rightresultcongruence. ((x) + (y)) + (p) * pfa_offset_left_rightdistribution_rightresultcongruence = (v) + (p) * pfa_offset_right_rightdistribution_rightresultcongruence))))))))) -> u = v

Constructive proof overview

Generated structural guide

Actual right distributivity of multiplication over addition on bounded representatives.

The unchanged tactic script uses 6 declared prerequisites and contains 77 exact native proof lines.

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

Proof neighborhood

Direct dependencies

mod_eq_mul_right Stable theorem; checked-use authorized mod_eq_trans Stable theorem; checked-use authorized mod_eq_add Stable theorem; checked-use authorized add_mul Stable 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 FP0049 prime_field_right_table_distributive

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 : ((exists pfa_gap_rightdistribution_raw_leftbound. pfa_gap_rightdistribution_raw_leftbound + S (u) = (p)) /\ ((exists pfa_offset_left_rightdistribution_raw_leftcongruence pfa_offset_right_rightdistribution_raw_leftcongruence. ((b + c) * a) + (p) * pfa_offset_left_rightdistribution_raw_leftcongruence = (u) + (p) * pfa_offset_right_rightdistribution_raw_leftcongruence)))
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 ((b + c) * a)
  4. L35
    specialize mod_eq_trans (s * a)
  5. L36
    specialize mod_eq_trans (u)
  6. L37
    apply mod_eq_trans
  7. L38
    specialize mod_eq_mul_right (p)
  8. L39
    specialize mod_eq_mul_right (b + c)
  9. L40
    specialize mod_eq_mul_right (s)
  10. L41
    specialize mod_eq_mul_right (a)
08Use earlier factsL42–44

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

  1. L42
    apply mod_eq_mul_right
  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 : ((exists pfa_gap_rightdistribution_raw_rightbound. pfa_gap_rightdistribution_raw_rightbound + S (v) = (p)) /\ ((exists pfa_offset_left_rightdistribution_raw_rightcongruence pfa_offset_right_rightdistribution_raw_rightcongruence. (b * a + c * a) + (p) * pfa_offset_left_rightdistribution_raw_rightcongruence = (v) + (p) * pfa_offset_right_rightdistribution_raw_rightcongruence)))
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 (b * a + c * a)
  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 (b * a)
  9. L55
    specialize mod_eq_add (x)
  10. L56
    specialize mod_eq_add (c * a)
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 ((b + c) * a)
  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 ((b + c) * a)
  4. L70
    specialize prime_field_residue_input_equal (b * a + c * a)
  5. L71
    specialize prime_field_residue_input_equal (v)
  6. L72
    apply prime_field_residue_input_equal
  7. L73
    specialize add_mul (b)
  8. L74
    specialize add_mul (c)
  9. L75
    specialize add_mul (a)
  10. L76
    apply add_mul
14Use earlier factsL77–77

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

  1. L77
    exact hr

Library-wide reading audit

Original exact 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 : ((exists pfa_gap_rightdistribution_raw_leftbound. pfa_gap_rightdistribution_raw_leftbound + S (u) = (p)) /\ ((exists pfa_offset_left_rightdistribution_raw_leftcongruence pfa_offset_right_rightdistribution_raw_leftcongruence. ((b + c) * a) + (p) * pfa_offset_left_rightdistribution_raw_leftcongruence = (u) + (p) * pfa_offset_right_rightdistribution_raw_leftcongruence)))
  31. 0031split
  32. 0032exact hleft_right_right_left
  33. 0033specialize mod_eq_trans (p)
  34. 0034specialize mod_eq_trans ((b + c) * a)
  35. 0035specialize mod_eq_trans (s * a)
  36. 0036specialize mod_eq_trans (u)
  37. 0037apply mod_eq_trans
  38. 0038specialize mod_eq_mul_right (p)
  39. 0039specialize mod_eq_mul_right (b + c)
  40. 0040specialize mod_eq_mul_right (s)
  41. 0041specialize mod_eq_mul_right (a)
  42. 0042apply mod_eq_mul_right
  43. 0043exact hsum_right_right_right
  44. 0044exact hleft_right_right_right
  45. 0045have hr : ((exists pfa_gap_rightdistribution_raw_rightbound. pfa_gap_rightdistribution_raw_rightbound + S (v) = (p)) /\ ((exists pfa_offset_left_rightdistribution_raw_rightcongruence pfa_offset_right_rightdistribution_raw_rightcongruence. (b * a + c * a) + (p) * pfa_offset_left_rightdistribution_raw_rightcongruence = (v) + (p) * pfa_offset_right_rightdistribution_raw_rightcongruence)))
  46. 0046split
  47. 0047exact hright_right_right_left
  48. 0048specialize mod_eq_trans (p)
  49. 0049specialize mod_eq_trans (b * a + c * a)
  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 (b * a)
  55. 0055specialize mod_eq_add (x)
  56. 0056specialize mod_eq_add (c * a)
  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 ((b + c) * a)
  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 ((b + c) * a)
  70. 0070specialize prime_field_residue_input_equal (b * a + c * a)
  71. 0071specialize prime_field_residue_input_equal (v)
  72. 0072apply prime_field_residue_input_equal
  73. 0073specialize add_mul (b)
  74. 0074specialize add_mul (c)
  75. 0075specialize add_mul (a)
  76. 0076apply add_mul
  77. 0077exact hr