PQ0001

prime_field_subtract_exists

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

Construct a genuine bounded solution of b+r=a using actual additive inverse and addition witnesses.

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. (~((p) = 1) /\ forall pfa_factor_left_scalar_prime pfa_factor_right_scalar_prime. (p) = pfa_factor_left_scalar_prime * pfa_factor_right_scalar_prime -> pfa_factor_left_scalar_prime = 1 \/ pfa_factor_right_scalar_prime = 1) -> (exists pfa_gap_scalar_left. pfa_gap_scalar_left + S (a) = (p)) -> (exists pfa_gap_scalar_right. pfa_gap_scalar_right + S (b) = (p)) -> exists r. (((exists pfa_gap_scalar_subtractleft. pfa_gap_scalar_subtractleft + S (b) = (p)) /\ (((exists pfa_gap_scalar_subtractright. pfa_gap_scalar_subtractright + S (r) = (p)) /\ ((((exists pfa_gap_scalar_subtractresultbound. pfa_gap_scalar_subtractresultbound + S (a) = (p)) /\ ((exists pfa_offset_left_scalar_subtractresultcongruence pfa_offset_right_scalar_subtractresultcongruence. ((b) + (r)) + (p) * pfa_offset_left_scalar_subtractresultcongruence = (a) + (p) * pfa_offset_right_scalar_subtractresultcongruence)))))))))

Constructive proof overview

Generated structural guide

Construct a genuine bounded solution of b+r=a using actual additive inverse and addition witnesses.

The unchanged tactic script uses 4 declared prerequisites and contains 62 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_field_negate_exists Alpha theorem; checked-use authorized prime_field_add_exists Alpha theorem; checked-use authorized prime_field_add_associative Alpha theorem; checked-use authorized prime_field_add_zero_left Alpha theorem; checked-use authorized

Direct dependents

PQ000D prime_field_polynomial_subtract_exists

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

62 script commands · 18 reading checkpoints · 6 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.

01Fix variables and assumptionsL1–6

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 hp
  5. L5
    intro ha
  6. L6
    intro hb
02Establish hnL7–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field negate exists.

  1. L7
    have hn : exists n. (((exists pfa_gap_scalar_negadditionleft. pfa_gap_scalar_negadditionleft + S (b) = (p)) /\ (((exists pfa_gap_scalar_negadditionright. pfa_gap_scalar_negadditionright + S (n) = (p)) /\ ((((exists pfa_gap_scalar_negadditionresultbound. pfa_gap_scalar_negadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_scalar_negadditionresultcongruence pfa_offset_right_scalar_negadditionresultcongruence. ((b) + (n)) + (p) * pfa_offset_left_scalar_negadditionresultcongruence = (0) + (p) * pfa_offset_right_scalar_negadditionresultcongruence)))))))))
  2. L8
    specialize prime_field_negate_exists (p)
  3. L9
    specialize prime_field_negate_exists (b)
  4. L10
    apply prime_field_negate_exists
  5. L11
    exact hp
  6. L12
    exact hb
03Separate the logical casesL13–13

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

  1. L13
    cases hn
04Establish hnbL14–14

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

  1. L14
    have hnb : exists pfa_gap_scalar_neg_bound. pfa_gap_scalar_neg_bound + S (x) = (p)
05Separate the logical casesL15–16

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

  1. L15
    cases hn_witness
  2. L16
    cases hn_witness_right
06Use earlier factsL17–17

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

  1. L17
    exact hn_witness_right_left
07Establish hrL18–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field add exists.

  1. L18
    have hr : exists r. (((exists pfa_gap_scalar_resultleft. pfa_gap_scalar_resultleft + S (x) = (p)) /\ (((exists pfa_gap_scalar_resultright. pfa_gap_scalar_resultright + S (a) = (p)) /\ ((((exists pfa_gap_scalar_resultresultbound. pfa_gap_scalar_resultresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_scalar_resultresultcongruence pfa_offset_right_scalar_resultresultcongruence. ((x) + (a)) + (p) * pfa_offset_left_scalar_resultresultcongruence = (r) + (p) * pfa_offset_right_scalar_resultresultcongruence)))))))))
  2. L19
    specialize prime_field_add_exists (p)
  3. L20
    specialize prime_field_add_exists (x)
  4. L21
    specialize prime_field_add_exists (a)
  5. L22
    apply prime_field_add_exists
  6. L23
    exact hp
  7. L24
    exact hnb
  8. L25
    exact ha
08Separate the logical casesL26–26

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

  1. L26
    cases hr
09Establish hrbL27–27

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

  1. L27
    have hrb : exists pfa_gap_scalar_result_bound. pfa_gap_scalar_result_bound + S (x1) = (p)
10Separate the logical casesL28–30

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

  1. L28
    cases hr_witness
  2. L29
    cases hr_witness_right
  3. L30
    cases hr_witness_right_right
11Use earlier factsL31–31

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

  1. L31
    exact hr_witness_right_right_left
12Establish htL32–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field add exists.

  1. L32
    have ht : exists t. (((exists pfa_gap_scalar_check_sumleft. pfa_gap_scalar_check_sumleft + S (b) = (p)) /\ (((exists pfa_gap_scalar_check_sumright. pfa_gap_scalar_check_sumright + S (x1) = (p)) /\ ((((exists pfa_gap_scalar_check_sumresultbound. pfa_gap_scalar_check_sumresultbound + S (t) = (p)) /\ ((exists pfa_offset_left_scalar_check_sumresultcongruence pfa_offset_right_scalar_check_sumresultcongruence. ((b) + (x1)) + (p) * pfa_offset_left_scalar_check_sumresultcongruence = (t) + (p) * pfa_offset_right_scalar_check_sumresultcongruence)))))))))
  2. L33
    specialize prime_field_add_exists (p)
  3. L34
    specialize prime_field_add_exists (b)
  4. L35
    specialize prime_field_add_exists (x1)
  5. L36
    apply prime_field_add_exists
  6. L37
    exact hp
  7. L38
    exact hb
  8. L39
    exact hrb
13Separate the logical casesL40–40

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

  1. L40
    cases ht
14Establish heqL41–50

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field add associative.

  1. L41
    have heq : a=x2
  2. L42
    specialize prime_field_add_associative (p)
  3. L43
    specialize prime_field_add_associative (b)
  4. L44
    specialize prime_field_add_associative (x)
  5. L45
    specialize prime_field_add_associative (a)
  6. L46
    specialize prime_field_add_associative (0)
  7. L47
    specialize prime_field_add_associative (x1)
  8. L48
    specialize prime_field_add_associative (a)
  9. L49
    specialize prime_field_add_associative (x2)
  10. L50
    apply prime_field_add_associative
15Use earlier factsL51–58

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

  1. L51
    exact hn_witness
  2. L52
    specialize prime_field_add_zero_left (p)
  3. L53
    specialize prime_field_add_zero_left (a)
  4. L54
    apply prime_field_add_zero_left
  5. L55
    exact hp
  6. L56
    exact ha
  7. L57
    exact hr_witness
  8. L58
    exact ht_witness
16Construct an explicit witnessL59–59

Supply the displayed value, then prove that it has the required property.

  1. L59
    exists x1
17Calculate and transport equalitiesL60–61

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L60
    rewrite heq
  2. L61
    rewrite heq
18Use earlier factsL62–62

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

  1. L62
    exact ht_witness

Library-wide reading audit

Original exact command ledger · 62 lines
  1. 0001intro p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hp
  5. 0005intro ha
  6. 0006intro hb
  7. 0007have hn : exists n. (((exists pfa_gap_scalar_negadditionleft. pfa_gap_scalar_negadditionleft + S (b) = (p)) /\ (((exists pfa_gap_scalar_negadditionright. pfa_gap_scalar_negadditionright + S (n) = (p)) /\ ((((exists pfa_gap_scalar_negadditionresultbound. pfa_gap_scalar_negadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_scalar_negadditionresultcongruence pfa_offset_right_scalar_negadditionresultcongruence. ((b) + (n)) + (p) * pfa_offset_left_scalar_negadditionresultcongruence = (0) + (p) * pfa_offset_right_scalar_negadditionresultcongruence)))))))))
  8. 0008specialize prime_field_negate_exists (p)
  9. 0009specialize prime_field_negate_exists (b)
  10. 0010apply prime_field_negate_exists
  11. 0011exact hp
  12. 0012exact hb
  13. 0013cases hn
  14. 0014have hnb : exists pfa_gap_scalar_neg_bound. pfa_gap_scalar_neg_bound + S (x) = (p)
  15. 0015cases hn_witness
  16. 0016cases hn_witness_right
  17. 0017exact hn_witness_right_left
  18. 0018have hr : exists r. (((exists pfa_gap_scalar_resultleft. pfa_gap_scalar_resultleft + S (x) = (p)) /\ (((exists pfa_gap_scalar_resultright. pfa_gap_scalar_resultright + S (a) = (p)) /\ ((((exists pfa_gap_scalar_resultresultbound. pfa_gap_scalar_resultresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_scalar_resultresultcongruence pfa_offset_right_scalar_resultresultcongruence. ((x) + (a)) + (p) * pfa_offset_left_scalar_resultresultcongruence = (r) + (p) * pfa_offset_right_scalar_resultresultcongruence)))))))))
  19. 0019specialize prime_field_add_exists (p)
  20. 0020specialize prime_field_add_exists (x)
  21. 0021specialize prime_field_add_exists (a)
  22. 0022apply prime_field_add_exists
  23. 0023exact hp
  24. 0024exact hnb
  25. 0025exact ha
  26. 0026cases hr
  27. 0027have hrb : exists pfa_gap_scalar_result_bound. pfa_gap_scalar_result_bound + S (x1) = (p)
  28. 0028cases hr_witness
  29. 0029cases hr_witness_right
  30. 0030cases hr_witness_right_right
  31. 0031exact hr_witness_right_right_left
  32. 0032have ht : exists t. (((exists pfa_gap_scalar_check_sumleft. pfa_gap_scalar_check_sumleft + S (b) = (p)) /\ (((exists pfa_gap_scalar_check_sumright. pfa_gap_scalar_check_sumright + S (x1) = (p)) /\ ((((exists pfa_gap_scalar_check_sumresultbound. pfa_gap_scalar_check_sumresultbound + S (t) = (p)) /\ ((exists pfa_offset_left_scalar_check_sumresultcongruence pfa_offset_right_scalar_check_sumresultcongruence. ((b) + (x1)) + (p) * pfa_offset_left_scalar_check_sumresultcongruence = (t) + (p) * pfa_offset_right_scalar_check_sumresultcongruence)))))))))
  33. 0033specialize prime_field_add_exists (p)
  34. 0034specialize prime_field_add_exists (b)
  35. 0035specialize prime_field_add_exists (x1)
  36. 0036apply prime_field_add_exists
  37. 0037exact hp
  38. 0038exact hb
  39. 0039exact hrb
  40. 0040cases ht
  41. 0041have heq : a=x2
  42. 0042specialize prime_field_add_associative (p)
  43. 0043specialize prime_field_add_associative (b)
  44. 0044specialize prime_field_add_associative (x)
  45. 0045specialize prime_field_add_associative (a)
  46. 0046specialize prime_field_add_associative (0)
  47. 0047specialize prime_field_add_associative (x1)
  48. 0048specialize prime_field_add_associative (a)
  49. 0049specialize prime_field_add_associative (x2)
  50. 0050apply prime_field_add_associative
  51. 0051exact hn_witness
  52. 0052specialize prime_field_add_zero_left (p)
  53. 0053specialize prime_field_add_zero_left (a)
  54. 0054apply prime_field_add_zero_left
  55. 0055exact hp
  56. 0056exact ha
  57. 0057exact hr_witness
  58. 0058exact ht_witness
  59. 0059exists x1
  60. 0060rewrite heq
  61. 0061rewrite heq
  62. 0062exact ht_witness