PQ0001

prime_field_subtract_exists

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

Alpha v34 checked-use · first admitted v32 · 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.

All coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.

Exact theorem in conservative defined notation

∀ p. ∀ a. ∀ b. Prime(p) → Lt(a,p) → Lt(b,p) → ∃ x. FpAdd(p,b,x,a)

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

Definition DAG

FpAdd(p,a,b,c) · 4Lt(a,b) · 4Prime(p) · 1

Actual proof prerequisites

prime_field_negate_exists · checked external prerequisiteprime_field_add_exists · checked external prerequisiteprime_field_add_associative · checked external prerequisiteprime_field_add_zero_left · checked external prerequisite
Original expanded first-order 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)))))))))

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ∃ n. FpAdd(p,b,n,0)Definitions: FpAdd(p,b,n,0)Original native command in the exact edition
  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
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 : ∃ r. FpAdd(p,x,a,r)Definitions: FpAdd(p,x,a,r)Original native command in the exact edition
  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
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 : ∃ t. FpAdd(p,b,x1,t)Definitions: FpAdd(p,b,x1,t)Original native command in the exact edition
  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 defined 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 : ∃ n. FpAdd(p,b,n,0)
  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 : Lt(x,p)
  15. 0015cases hn_witness
  16. 0016cases hn_witness_right
  17. 0017exact hn_witness_right_left
  18. 0018have hr : ∃ r. FpAdd(p,x,a,r)
  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 : Lt(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 : ∃ t. FpAdd(p,b,x1,t)
  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