FP0012

prime_field_left_distributive

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

Actual left distributivity of multiplication over addition on bounded representatives.

Exact expanded first-order arithmetic 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

Constructive proof overview

Generated structural guide

Actual left distributivity of multiplication over addition on bounded representatives.

The unchanged tactic script uses 6 declared prerequisites and contains 77 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_left Alpha theorem; checked-use authorized mod_eq_trans Alpha theorem; checked-use authorized mod_eq_add Alpha theorem; checked-use authorized mul_add 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 FP0048 prime_field_left_table_distributive

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

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_leftdistribution_raw_leftbound. pfa_gap_leftdistribution_raw_leftbound + S (u) = (p)) /\ ((exists pfa_offset_left_leftdistribution_raw_leftcongruence pfa_offset_right_leftdistribution_raw_leftcongruence. (a * (b + c)) + (p) * pfa_offset_left_leftdistribution_raw_leftcongruence = (u) + (p) * pfa_offset_right_leftdistribution_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 (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 : ((exists pfa_gap_leftdistribution_raw_rightbound. pfa_gap_leftdistribution_raw_rightbound + S (v) = (p)) /\ ((exists pfa_offset_left_leftdistribution_raw_rightcongruence pfa_offset_right_leftdistribution_raw_rightcongruence. (a * b + a * c) + (p) * pfa_offset_left_leftdistribution_raw_rightcongruence = (v) + (p) * pfa_offset_right_leftdistribution_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 (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 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_leftdistribution_raw_leftbound. pfa_gap_leftdistribution_raw_leftbound + S (u) = (p)) /\ ((exists pfa_offset_left_leftdistribution_raw_leftcongruence pfa_offset_right_leftdistribution_raw_leftcongruence. (a * (b + c)) + (p) * pfa_offset_left_leftdistribution_raw_leftcongruence = (u) + (p) * pfa_offset_right_leftdistribution_raw_leftcongruence)))
  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 : ((exists pfa_gap_leftdistribution_raw_rightbound. pfa_gap_leftdistribution_raw_rightbound + S (v) = (p)) /\ ((exists pfa_offset_left_leftdistribution_raw_rightcongruence pfa_offset_right_leftdistribution_raw_rightcongruence. (a * b + a * c) + (p) * pfa_offset_left_leftdistribution_raw_rightcongruence = (v) + (p) * pfa_offset_right_leftdistribution_raw_rightcongruence)))
  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