PQ000F

prime_field_polynomial_subtract_bounded

The actual operation graph itself forces every source and result coefficient to be canonical.

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. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ rb. ∀ rc. ∀ l. FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,l) → BetaPrefixInto(ab,ac,l,p) ∧ (BetaPrefixInto(bb,bc,l,p) ∧ BetaPrefixInto(rb,rc,l,p))

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

Definition DAG

FpAdd(p,a,b,c) · 3BetaPrefixInto(b,c,l,B) · 3FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 1BetaAt(b,c,i,x) · 9

Actual proof prerequisites

none
Original expanded first-order statement 
forall p ab ac bb bc rb rc l. (forall pfs_index_subtract_bounded_graph. (exists pfa_gap_subtract_bounded_graphindex. pfa_gap_subtract_bounded_graphindex + S (pfs_index_subtract_bounded_graph) = (l)) -> exists pfs_left_subtract_bounded_graph pfs_right_subtract_bounded_graph pfs_result_subtract_bounded_graph. ((((exists ff_h_pfp_subtract_bounded_graphleft. ff_h_pfp_subtract_bounded_graphleft + S (pfs_left_subtract_bounded_graph) = S ((S (pfs_index_subtract_bounded_graph)) * ac)) /\ exists ff_q_pfp_subtract_bounded_graphleft. ab = ff_q_pfp_subtract_bounded_graphleft * S ((S (pfs_index_subtract_bounded_graph)) * ac) + (pfs_left_subtract_bounded_graph))) /\ (((((exists ff_h_pfp_subtract_bounded_graphright. ff_h_pfp_subtract_bounded_graphright + S (pfs_right_subtract_bounded_graph) = S ((S (pfs_index_subtract_bounded_graph)) * bc)) /\ exists ff_q_pfp_subtract_bounded_graphright. bb = ff_q_pfp_subtract_bounded_graphright * S ((S (pfs_index_subtract_bounded_graph)) * bc) + (pfs_right_subtract_bounded_graph))) /\ (((((exists ff_h_pfp_subtract_bounded_graphresult. ff_h_pfp_subtract_bounded_graphresult + S (pfs_result_subtract_bounded_graph) = S ((S (pfs_index_subtract_bounded_graph)) * rc)) /\ exists ff_q_pfp_subtract_bounded_graphresult. rb = ff_q_pfp_subtract_bounded_graphresult * S ((S (pfs_index_subtract_bounded_graph)) * rc) + (pfs_result_subtract_bounded_graph))) /\ ((((exists pfa_gap_subtract_bounded_graphoperationleft. pfa_gap_subtract_bounded_graphoperationleft + S (pfs_right_subtract_bounded_graph) = (p)) /\ (((exists pfa_gap_subtract_bounded_graphoperationright. pfa_gap_subtract_bounded_graphoperationright + S (pfs_result_subtract_bounded_graph) = (p)) /\ ((((exists pfa_gap_subtract_bounded_graphoperationresultbound. pfa_gap_subtract_bounded_graphoperationresultbound + S (pfs_left_subtract_bounded_graph) = (p)) /\ ((exists pfa_offset_left_subtract_bounded_graphoperationresultcongruence pfa_offset_right_subtract_bounded_graphoperationresultcongruence. ((pfs_right_subtract_bounded_graph) + (pfs_result_subtract_bounded_graph)) + (p) * pfa_offset_left_subtract_bounded_graphoperationresultcongruence = (pfs_left_subtract_bounded_graph) + (p) * pfa_offset_right_subtract_bounded_graphoperationresultcongruence)))))))))))))))) -> ((forall fom_index_pfp_subtract_bounded_ab. (exists fom_gap_pfp_subtract_bounded_ab_index_bound. fom_gap_pfp_subtract_bounded_ab_index_bound + S (fom_index_pfp_subtract_bounded_ab) = l) -> exists fom_value_pfp_subtract_bounded_ab. ((((exists fom_beta_height_pfp_subtract_bounded_ab_entry. fom_beta_height_pfp_subtract_bounded_ab_entry + S (fom_value_pfp_subtract_bounded_ab) = S ((S (fom_index_pfp_subtract_bounded_ab)) * ac)) /\ exists fom_beta_quotient_pfp_subtract_bounded_ab_entry. ab = fom_beta_quotient_pfp_subtract_bounded_ab_entry * S ((S (fom_index_pfp_subtract_bounded_ab)) * ac) + (fom_value_pfp_subtract_bounded_ab))) /\ (exists fom_gap_pfp_subtract_bounded_ab_value_bound. fom_gap_pfp_subtract_bounded_ab_value_bound + S (fom_value_pfp_subtract_bounded_ab) = p))) /\ (((forall fom_index_pfp_subtract_bounded_bb. (exists fom_gap_pfp_subtract_bounded_bb_index_bound. fom_gap_pfp_subtract_bounded_bb_index_bound + S (fom_index_pfp_subtract_bounded_bb) = l) -> exists fom_value_pfp_subtract_bounded_bb. ((((exists fom_beta_height_pfp_subtract_bounded_bb_entry. fom_beta_height_pfp_subtract_bounded_bb_entry + S (fom_value_pfp_subtract_bounded_bb) = S ((S (fom_index_pfp_subtract_bounded_bb)) * bc)) /\ exists fom_beta_quotient_pfp_subtract_bounded_bb_entry. bb = fom_beta_quotient_pfp_subtract_bounded_bb_entry * S ((S (fom_index_pfp_subtract_bounded_bb)) * bc) + (fom_value_pfp_subtract_bounded_bb))) /\ (exists fom_gap_pfp_subtract_bounded_bb_value_bound. fom_gap_pfp_subtract_bounded_bb_value_bound + S (fom_value_pfp_subtract_bounded_bb) = p))) /\ ((forall fom_index_pfp_subtract_bounded_rb. (exists fom_gap_pfp_subtract_bounded_rb_index_bound. fom_gap_pfp_subtract_bounded_rb_index_bound + S (fom_index_pfp_subtract_bounded_rb) = l) -> exists fom_value_pfp_subtract_bounded_rb. ((((exists fom_beta_height_pfp_subtract_bounded_rb_entry. fom_beta_height_pfp_subtract_bounded_rb_entry + S (fom_value_pfp_subtract_bounded_rb) = S ((S (fom_index_pfp_subtract_bounded_rb)) * rc)) /\ exists fom_beta_quotient_pfp_subtract_bounded_rb_entry. rb = fom_beta_quotient_pfp_subtract_bounded_rb_entry * S ((S (fom_index_pfp_subtract_bounded_rb)) * rc) + (fom_value_pfp_subtract_bounded_rb))) /\ (exists fom_gap_pfp_subtract_bounded_rb_value_bound. fom_gap_pfp_subtract_bounded_rb_value_bound + S (fom_value_pfp_subtract_bounded_rb) = p)))))))

Complete tactic proof in conservative notation

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

68 script commands · 21 reading checkpoints · 3 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–9

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

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro rb
  7. L7
    intro rc
  8. L8
    intro l
  9. L9
    intro h
02Separate the logical casesL10–10

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

  1. L10
    split
03Fix variables and assumptionsL11–12

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

  1. L11
    intro i
  2. L12
    intro hi
04Establish hvL13–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply h.

  1. L13
    have hv : ∃ a. ∃ b. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,b) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,b,r,a)))Definitions: BetaAt(ab,ac,i,a)BetaAt(bb,bc,i,b)BetaAt(rb,rc,i,r)FpAdd(p,b,r,a)Original native command in the exact edition
  2. L14
    specialize h (i)
  3. L15
    apply h
  4. L16
    exact hi
05Separate the logical casesL17–25

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

  1. L17
    cases hv
  2. L18
    cases hv_witness
  3. L19
    cases hv_witness_witness
  4. L20
    cases hv_witness_witness_witness
  5. L21
    cases hv_witness_witness_witness_right
  6. L22
    cases hv_witness_witness_witness_right_right
  7. L23
    cases hv_witness_witness_witness_right_right_right
  8. L24
    cases hv_witness_witness_witness_right_right_right_right
  9. L25
    cases hv_witness_witness_witness_right_right_right_right_right
06Construct an explicit witnessL26–26

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

  1. L26
    exists x
07Separate the logical casesL27–27

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

  1. L27
    split
08Use earlier factsL28–29

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

  1. L28
    exact hv_witness_witness_witness_left
  2. L29
    exact hv_witness_witness_witness_right_right_right_right_right_left
09Separate the logical casesL30–30

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

  1. L30
    split
10Fix variables and assumptionsL31–32

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

  1. L31
    intro i
  2. L32
    intro hi
11Establish hvL33–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply h.

  1. L33
    have hv : ∃ a. ∃ b. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,b) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,b,r,a)))Definitions: BetaAt(ab,ac,i,a)BetaAt(bb,bc,i,b)BetaAt(rb,rc,i,r)FpAdd(p,b,r,a)Original native command in the exact edition
  2. L34
    specialize h (i)
  3. L35
    apply h
  4. L36
    exact hi
12Separate the logical casesL37–45

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

  1. L37
    cases hv
  2. L38
    cases hv_witness
  3. L39
    cases hv_witness_witness
  4. L40
    cases hv_witness_witness_witness
  5. L41
    cases hv_witness_witness_witness_right
  6. L42
    cases hv_witness_witness_witness_right_right
  7. L43
    cases hv_witness_witness_witness_right_right_right
  8. L44
    cases hv_witness_witness_witness_right_right_right_right
  9. L45
    cases hv_witness_witness_witness_right_right_right_right_right
13Construct an explicit witnessL46–46

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

  1. L46
    exists x1
14Separate the logical casesL47–47

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

  1. L47
    split
15Use earlier factsL48–49

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

  1. L48
    exact hv_witness_witness_witness_right_left
  2. L49
    exact hv_witness_witness_witness_right_right_right_left
16Fix variables and assumptionsL50–51

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

  1. L50
    intro i
  2. L51
    intro hi
17Establish hvL52–55

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply h.

  1. L52
    have hv : ∃ a. ∃ b. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,b) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,b,r,a)))Definitions: BetaAt(ab,ac,i,a)BetaAt(bb,bc,i,b)BetaAt(rb,rc,i,r)FpAdd(p,b,r,a)Original native command in the exact edition
  2. L53
    specialize h (i)
  3. L54
    apply h
  4. L55
    exact hi
18Separate the logical casesL56–64

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

  1. L56
    cases hv
  2. L57
    cases hv_witness
  3. L58
    cases hv_witness_witness
  4. L59
    cases hv_witness_witness_witness
  5. L60
    cases hv_witness_witness_witness_right
  6. L61
    cases hv_witness_witness_witness_right_right
  7. L62
    cases hv_witness_witness_witness_right_right_right
  8. L63
    cases hv_witness_witness_witness_right_right_right_right
  9. L64
    cases hv_witness_witness_witness_right_right_right_right_right
19Construct an explicit witnessL65–65

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

  1. L65
    exists x2
20Separate the logical casesL66–66

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

  1. L66
    split
21Use earlier factsL67–68

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

  1. L67
    exact hv_witness_witness_witness_right_right_left
  2. L68
    exact hv_witness_witness_witness_right_right_right_right_left

Library-wide reading audit

Original defined command ledger · 68 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro l
  9. 0009intro h
  10. 0010split
  11. 0011intro i
  12. 0012intro hi
  13. 0013have hv : ∃ a. ∃ b. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,b) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,b,r,a)))
  14. 0014specialize h (i)
  15. 0015apply h
  16. 0016exact hi
  17. 0017cases hv
  18. 0018cases hv_witness
  19. 0019cases hv_witness_witness
  20. 0020cases hv_witness_witness_witness
  21. 0021cases hv_witness_witness_witness_right
  22. 0022cases hv_witness_witness_witness_right_right
  23. 0023cases hv_witness_witness_witness_right_right_right
  24. 0024cases hv_witness_witness_witness_right_right_right_right
  25. 0025cases hv_witness_witness_witness_right_right_right_right_right
  26. 0026exists x
  27. 0027split
  28. 0028exact hv_witness_witness_witness_left
  29. 0029exact hv_witness_witness_witness_right_right_right_right_right_left
  30. 0030split
  31. 0031intro i
  32. 0032intro hi
  33. 0033have hv : ∃ a. ∃ b. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,b) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,b,r,a)))
  34. 0034specialize h (i)
  35. 0035apply h
  36. 0036exact hi
  37. 0037cases hv
  38. 0038cases hv_witness
  39. 0039cases hv_witness_witness
  40. 0040cases hv_witness_witness_witness
  41. 0041cases hv_witness_witness_witness_right
  42. 0042cases hv_witness_witness_witness_right_right
  43. 0043cases hv_witness_witness_witness_right_right_right
  44. 0044cases hv_witness_witness_witness_right_right_right_right
  45. 0045cases hv_witness_witness_witness_right_right_right_right_right
  46. 0046exists x1
  47. 0047split
  48. 0048exact hv_witness_witness_witness_right_left
  49. 0049exact hv_witness_witness_witness_right_right_right_left
  50. 0050intro i
  51. 0051intro hi
  52. 0052have hv : ∃ a. ∃ b. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(bb,bc,i,b) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,b,r,a)))
  53. 0053specialize h (i)
  54. 0054apply h
  55. 0055exact hi
  56. 0056cases hv
  57. 0057cases hv_witness
  58. 0058cases hv_witness_witness
  59. 0059cases hv_witness_witness_witness
  60. 0060cases hv_witness_witness_witness_right
  61. 0061cases hv_witness_witness_witness_right_right
  62. 0062cases hv_witness_witness_witness_right_right_right
  63. 0063cases hv_witness_witness_witness_right_right_right_right
  64. 0064cases hv_witness_witness_witness_right_right_right_right_right
  65. 0065exists x2
  66. 0066split
  67. 0067exact hv_witness_witness_witness_right_right_left
  68. 0068exact hv_witness_witness_witness_right_right_right_right_left