PQ0010

prime_field_polynomial_subtract_functional

The result is unique by existing decoded-prefix equality, never by equality of beta code numbers.

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. ∀ db. ∀ dc. ∀ l. FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,l) → FpCoefficientSubtraction(p,ab,ac,bb,bc,db,dc,l) → ∀ x. ∀ y. Lt(x,l) → BetaAt(rb,rc,x,y) → BetaAt(db,dc,x,y)

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

Definition DAG

FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 5

Actual proof prerequisites

beta_at_exists · checked external prerequisiteprime_field_add_cancel_left · checked external prerequisiteprime_field_polynomial_subtract_entry
Original expanded first-order statement 
forall p ab ac bb bc rb rc db dc l. (forall pfs_index_subtract_functional_first. (exists pfa_gap_subtract_functional_firstindex. pfa_gap_subtract_functional_firstindex + S (pfs_index_subtract_functional_first) = (l)) -> exists pfs_left_subtract_functional_first pfs_right_subtract_functional_first pfs_result_subtract_functional_first. ((((exists ff_h_pfp_subtract_functional_firstleft. ff_h_pfp_subtract_functional_firstleft + S (pfs_left_subtract_functional_first) = S ((S (pfs_index_subtract_functional_first)) * ac)) /\ exists ff_q_pfp_subtract_functional_firstleft. ab = ff_q_pfp_subtract_functional_firstleft * S ((S (pfs_index_subtract_functional_first)) * ac) + (pfs_left_subtract_functional_first))) /\ (((((exists ff_h_pfp_subtract_functional_firstright. ff_h_pfp_subtract_functional_firstright + S (pfs_right_subtract_functional_first) = S ((S (pfs_index_subtract_functional_first)) * bc)) /\ exists ff_q_pfp_subtract_functional_firstright. bb = ff_q_pfp_subtract_functional_firstright * S ((S (pfs_index_subtract_functional_first)) * bc) + (pfs_right_subtract_functional_first))) /\ (((((exists ff_h_pfp_subtract_functional_firstresult. ff_h_pfp_subtract_functional_firstresult + S (pfs_result_subtract_functional_first) = S ((S (pfs_index_subtract_functional_first)) * rc)) /\ exists ff_q_pfp_subtract_functional_firstresult. rb = ff_q_pfp_subtract_functional_firstresult * S ((S (pfs_index_subtract_functional_first)) * rc) + (pfs_result_subtract_functional_first))) /\ ((((exists pfa_gap_subtract_functional_firstoperationleft. pfa_gap_subtract_functional_firstoperationleft + S (pfs_right_subtract_functional_first) = (p)) /\ (((exists pfa_gap_subtract_functional_firstoperationright. pfa_gap_subtract_functional_firstoperationright + S (pfs_result_subtract_functional_first) = (p)) /\ ((((exists pfa_gap_subtract_functional_firstoperationresultbound. pfa_gap_subtract_functional_firstoperationresultbound + S (pfs_left_subtract_functional_first) = (p)) /\ ((exists pfa_offset_left_subtract_functional_firstoperationresultcongruence pfa_offset_right_subtract_functional_firstoperationresultcongruence. ((pfs_right_subtract_functional_first) + (pfs_result_subtract_functional_first)) + (p) * pfa_offset_left_subtract_functional_firstoperationresultcongruence = (pfs_left_subtract_functional_first) + (p) * pfa_offset_right_subtract_functional_firstoperationresultcongruence)))))))))))))))) -> (forall pfs_index_subtract_functional_second. (exists pfa_gap_subtract_functional_secondindex. pfa_gap_subtract_functional_secondindex + S (pfs_index_subtract_functional_second) = (l)) -> exists pfs_left_subtract_functional_second pfs_right_subtract_functional_second pfs_result_subtract_functional_second. ((((exists ff_h_pfp_subtract_functional_secondleft. ff_h_pfp_subtract_functional_secondleft + S (pfs_left_subtract_functional_second) = S ((S (pfs_index_subtract_functional_second)) * ac)) /\ exists ff_q_pfp_subtract_functional_secondleft. ab = ff_q_pfp_subtract_functional_secondleft * S ((S (pfs_index_subtract_functional_second)) * ac) + (pfs_left_subtract_functional_second))) /\ (((((exists ff_h_pfp_subtract_functional_secondright. ff_h_pfp_subtract_functional_secondright + S (pfs_right_subtract_functional_second) = S ((S (pfs_index_subtract_functional_second)) * bc)) /\ exists ff_q_pfp_subtract_functional_secondright. bb = ff_q_pfp_subtract_functional_secondright * S ((S (pfs_index_subtract_functional_second)) * bc) + (pfs_right_subtract_functional_second))) /\ (((((exists ff_h_pfp_subtract_functional_secondresult. ff_h_pfp_subtract_functional_secondresult + S (pfs_result_subtract_functional_second) = S ((S (pfs_index_subtract_functional_second)) * dc)) /\ exists ff_q_pfp_subtract_functional_secondresult. db = ff_q_pfp_subtract_functional_secondresult * S ((S (pfs_index_subtract_functional_second)) * dc) + (pfs_result_subtract_functional_second))) /\ ((((exists pfa_gap_subtract_functional_secondoperationleft. pfa_gap_subtract_functional_secondoperationleft + S (pfs_right_subtract_functional_second) = (p)) /\ (((exists pfa_gap_subtract_functional_secondoperationright. pfa_gap_subtract_functional_secondoperationright + S (pfs_result_subtract_functional_second) = (p)) /\ ((((exists pfa_gap_subtract_functional_secondoperationresultbound. pfa_gap_subtract_functional_secondoperationresultbound + S (pfs_left_subtract_functional_second) = (p)) /\ ((exists pfa_offset_left_subtract_functional_secondoperationresultcongruence pfa_offset_right_subtract_functional_secondoperationresultcongruence. ((pfs_right_subtract_functional_second) + (pfs_result_subtract_functional_second)) + (p) * pfa_offset_left_subtract_functional_secondoperationresultcongruence = (pfs_left_subtract_functional_second) + (p) * pfa_offset_right_subtract_functional_secondoperationresultcongruence)))))))))))))))) -> (forall mdr_i_pfp_subtract_functional_result mdr_a_pfp_subtract_functional_result. (exists mdr_gap_pfp_subtract_functional_resultb. mdr_gap_pfp_subtract_functional_resultb + S (mdr_i_pfp_subtract_functional_result) = (l)) -> (((exists ff_h_mdr_pfp_subtract_functional_resulto. ff_h_mdr_pfp_subtract_functional_resulto + S (mdr_a_pfp_subtract_functional_result) = S ((S (mdr_i_pfp_subtract_functional_result)) * rc)) /\ exists ff_q_mdr_pfp_subtract_functional_resulto. rb = ff_q_mdr_pfp_subtract_functional_resulto * S ((S (mdr_i_pfp_subtract_functional_result)) * rc) + (mdr_a_pfp_subtract_functional_result))) -> (((exists ff_h_mdr_pfp_subtract_functional_resultn. ff_h_mdr_pfp_subtract_functional_resultn + S (mdr_a_pfp_subtract_functional_result) = S ((S (mdr_i_pfp_subtract_functional_result)) * dc)) /\ exists ff_q_mdr_pfp_subtract_functional_resultn. db = ff_q_mdr_pfp_subtract_functional_resultn * S ((S (mdr_i_pfp_subtract_functional_result)) * dc) + (mdr_a_pfp_subtract_functional_result))))

Complete tactic proof in conservative notation

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

80 script commands · 15 reading checkpoints · 4 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.

Named ingredients (1)
prime field polynomial subtract entry
01Fix variables and assumptionsL1–10

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 db
  9. L9
    intro dc
  10. L10
    intro l
02Fix variables and assumptionsL11–16

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

  1. L11
    intro hfirst
  2. L12
    intro hsecond
  3. L13
    intro i
  4. L14
    intro r
  5. L15
    intro hi
  6. L16
    intro hr
03Establish hchosen0L17–21

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

  1. L17
    have hchosen0 : ∃ v. BetaAt(ab,ac,i,v)Definitions: BetaAt(ab,ac,i,v)Original native command in the exact edition
  2. L18
    specialize beta_at_exists (ab)
  3. L19
    specialize beta_at_exists (ac)
  4. L20
    specialize beta_at_exists (i)
  5. L21
    apply beta_at_exists
04Separate the logical casesL22–22

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

  1. L22
    cases hchosen0
05Establish hchosen1L23–27

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

  1. L23
    have hchosen1 : ∃ v. BetaAt(bb,bc,i,v)Definitions: BetaAt(bb,bc,i,v)Original native command in the exact edition
  2. L24
    specialize beta_at_exists (bb)
  3. L25
    specialize beta_at_exists (bc)
  4. L26
    specialize beta_at_exists (i)
  5. L27
    apply beta_at_exists
06Separate the logical casesL28–28

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

  1. L28
    cases hchosen1
07Establish hchosen2L29–33

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

  1. L29
    have hchosen2 : ∃ v. BetaAt(db,dc,i,v)Definitions: BetaAt(db,dc,i,v)Original native command in the exact edition
  2. L30
    specialize beta_at_exists (db)
  3. L31
    specialize beta_at_exists (dc)
  4. L32
    specialize beta_at_exists (i)
  5. L33
    apply beta_at_exists
08Separate the logical casesL34–34

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

  1. L34
    cases hchosen2
09Establish heqL35–44

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

  1. L35
    have heq : r=x2
  2. L36
    specialize prime_field_add_cancel_left (p)
  3. L37
    specialize prime_field_add_cancel_left (x1)
  4. L38
    specialize prime_field_add_cancel_left (r)
  5. L39
    specialize prime_field_add_cancel_left (x2)
  6. L40
    specialize prime_field_add_cancel_left (x)
  7. L41
    apply prime_field_add_cancel_left
  8. L42
    specialize prime_field_polynomial_subtract_entry (p)
  9. L43
    specialize prime_field_polynomial_subtract_entry (ab)
  10. L44
    specialize prime_field_polynomial_subtract_entry (ac)
10Use earlier factsL45–54

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

  1. L45
    specialize prime_field_polynomial_subtract_entry (bb)
  2. L46
    specialize prime_field_polynomial_subtract_entry (bc)
  3. L47
    specialize prime_field_polynomial_subtract_entry (rb)
  4. L48
    specialize prime_field_polynomial_subtract_entry (rc)
  5. L49
    specialize prime_field_polynomial_subtract_entry (l)
  6. L50
    specialize prime_field_polynomial_subtract_entry (i)
  7. L51
    specialize prime_field_polynomial_subtract_entry (x)
  8. L52
    specialize prime_field_polynomial_subtract_entry (x1)
  9. L53
    specialize prime_field_polynomial_subtract_entry (r)
  10. L54
    apply prime_field_polynomial_subtract_entry
11Use earlier factsL55–64

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

  1. L55
    exact hfirst
  2. L56
    exact hi
  3. L57
    exact hchosen0_witness
  4. L58
    exact hchosen1_witness
  5. L59
    exact hr
  6. L60
    specialize prime_field_polynomial_subtract_entry (p)
  7. L61
    specialize prime_field_polynomial_subtract_entry (ab)
  8. L62
    specialize prime_field_polynomial_subtract_entry (ac)
  9. L63
    specialize prime_field_polynomial_subtract_entry (bb)
  10. L64
    specialize prime_field_polynomial_subtract_entry (bc)
12Use earlier factsL65–74

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

  1. L65
    specialize prime_field_polynomial_subtract_entry (db)
  2. L66
    specialize prime_field_polynomial_subtract_entry (dc)
  3. L67
    specialize prime_field_polynomial_subtract_entry (l)
  4. L68
    specialize prime_field_polynomial_subtract_entry (i)
  5. L69
    specialize prime_field_polynomial_subtract_entry (x)
  6. L70
    specialize prime_field_polynomial_subtract_entry (x1)
  7. L71
    specialize prime_field_polynomial_subtract_entry (x2)
  8. L72
    apply prime_field_polynomial_subtract_entry
  9. L73
    exact hsecond
  10. L74
    exact hi
13Use earlier factsL75–77

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

  1. L75
    exact hchosen0_witness
  2. L76
    exact hchosen1_witness
  3. L77
    exact hchosen2_witness
14Calculate and transport equalitiesL78–79

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

  1. L78
    rewrite heq
  2. L79
    rewrite heq
15Use earlier factsL80–80

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

  1. L80
    exact hchosen2_witness

Library-wide reading audit

Original defined command ledger · 80 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro db
  9. 0009intro dc
  10. 0010intro l
  11. 0011intro hfirst
  12. 0012intro hsecond
  13. 0013intro i
  14. 0014intro r
  15. 0015intro hi
  16. 0016intro hr
  17. 0017have hchosen0 : ∃ v. BetaAt(ab,ac,i,v)
  18. 0018specialize beta_at_exists (ab)
  19. 0019specialize beta_at_exists (ac)
  20. 0020specialize beta_at_exists (i)
  21. 0021apply beta_at_exists
  22. 0022cases hchosen0
  23. 0023have hchosen1 : ∃ v. BetaAt(bb,bc,i,v)
  24. 0024specialize beta_at_exists (bb)
  25. 0025specialize beta_at_exists (bc)
  26. 0026specialize beta_at_exists (i)
  27. 0027apply beta_at_exists
  28. 0028cases hchosen1
  29. 0029have hchosen2 : ∃ v. BetaAt(db,dc,i,v)
  30. 0030specialize beta_at_exists (db)
  31. 0031specialize beta_at_exists (dc)
  32. 0032specialize beta_at_exists (i)
  33. 0033apply beta_at_exists
  34. 0034cases hchosen2
  35. 0035have heq : r=x2
  36. 0036specialize prime_field_add_cancel_left (p)
  37. 0037specialize prime_field_add_cancel_left (x1)
  38. 0038specialize prime_field_add_cancel_left (r)
  39. 0039specialize prime_field_add_cancel_left (x2)
  40. 0040specialize prime_field_add_cancel_left (x)
  41. 0041apply prime_field_add_cancel_left
  42. 0042specialize prime_field_polynomial_subtract_entry (p)
  43. 0043specialize prime_field_polynomial_subtract_entry (ab)
  44. 0044specialize prime_field_polynomial_subtract_entry (ac)
  45. 0045specialize prime_field_polynomial_subtract_entry (bb)
  46. 0046specialize prime_field_polynomial_subtract_entry (bc)
  47. 0047specialize prime_field_polynomial_subtract_entry (rb)
  48. 0048specialize prime_field_polynomial_subtract_entry (rc)
  49. 0049specialize prime_field_polynomial_subtract_entry (l)
  50. 0050specialize prime_field_polynomial_subtract_entry (i)
  51. 0051specialize prime_field_polynomial_subtract_entry (x)
  52. 0052specialize prime_field_polynomial_subtract_entry (x1)
  53. 0053specialize prime_field_polynomial_subtract_entry (r)
  54. 0054apply prime_field_polynomial_subtract_entry
  55. 0055exact hfirst
  56. 0056exact hi
  57. 0057exact hchosen0_witness
  58. 0058exact hchosen1_witness
  59. 0059exact hr
  60. 0060specialize prime_field_polynomial_subtract_entry (p)
  61. 0061specialize prime_field_polynomial_subtract_entry (ab)
  62. 0062specialize prime_field_polynomial_subtract_entry (ac)
  63. 0063specialize prime_field_polynomial_subtract_entry (bb)
  64. 0064specialize prime_field_polynomial_subtract_entry (bc)
  65. 0065specialize prime_field_polynomial_subtract_entry (db)
  66. 0066specialize prime_field_polynomial_subtract_entry (dc)
  67. 0067specialize prime_field_polynomial_subtract_entry (l)
  68. 0068specialize prime_field_polynomial_subtract_entry (i)
  69. 0069specialize prime_field_polynomial_subtract_entry (x)
  70. 0070specialize prime_field_polynomial_subtract_entry (x1)
  71. 0071specialize prime_field_polynomial_subtract_entry (x2)
  72. 0072apply prime_field_polynomial_subtract_entry
  73. 0073exact hsecond
  74. 0074exact hi
  75. 0075exact hchosen0_witness
  76. 0076exact hchosen1_witness
  77. 0077exact hchosen2_witness
  78. 0078rewrite heq
  79. 0079rewrite heq
  80. 0080exact hchosen2_witness