PQ000D

prime_field_polynomial_subtract_exists

Construct the entire actual canonical coefficient output by ordinary induction and beta-prefix extension; no output table is assumed.

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. ∀ l. Prime(p) → BetaPrefixInto(ab,ac,l,p) → BetaPrefixInto(bb,bc,l,p) → ∃ x. ∃ y. FpCoefficientSubtraction(p,ab,ac,bb,bc,x,y,l)

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

Definition DAG

FpAdd(p,a,b,c) · 2BetaPrefixInto(b,c,l,B) · 2FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 2Lt(a,b) · 4Prime(p) · 1BetaAt(b,c,i,x) · 8

Actual proof prerequisites

prime_field_polynomial_subtract_emptyle_succ · checked external prerequisitezero_add · checked external prerequisiteprime_field_subtract_existsbeta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall p ab ac bb bc l. (~((p) = 1) /\ forall pfa_factor_left_subtract_exists_prime pfa_factor_right_subtract_exists_prime. (p) = pfa_factor_left_subtract_exists_prime * pfa_factor_right_subtract_exists_prime -> pfa_factor_left_subtract_exists_prime = 1 \/ pfa_factor_right_subtract_exists_prime = 1) -> (forall fom_index_pfp_subtract_exists_ab. (exists fom_gap_pfp_subtract_exists_ab_index_bound. fom_gap_pfp_subtract_exists_ab_index_bound + S (fom_index_pfp_subtract_exists_ab) = l) -> exists fom_value_pfp_subtract_exists_ab. ((((exists fom_beta_height_pfp_subtract_exists_ab_entry. fom_beta_height_pfp_subtract_exists_ab_entry + S (fom_value_pfp_subtract_exists_ab) = S ((S (fom_index_pfp_subtract_exists_ab)) * ac)) /\ exists fom_beta_quotient_pfp_subtract_exists_ab_entry. ab = fom_beta_quotient_pfp_subtract_exists_ab_entry * S ((S (fom_index_pfp_subtract_exists_ab)) * ac) + (fom_value_pfp_subtract_exists_ab))) /\ (exists fom_gap_pfp_subtract_exists_ab_value_bound. fom_gap_pfp_subtract_exists_ab_value_bound + S (fom_value_pfp_subtract_exists_ab) = p))) -> (forall fom_index_pfp_subtract_exists_bb. (exists fom_gap_pfp_subtract_exists_bb_index_bound. fom_gap_pfp_subtract_exists_bb_index_bound + S (fom_index_pfp_subtract_exists_bb) = l) -> exists fom_value_pfp_subtract_exists_bb. ((((exists fom_beta_height_pfp_subtract_exists_bb_entry. fom_beta_height_pfp_subtract_exists_bb_entry + S (fom_value_pfp_subtract_exists_bb) = S ((S (fom_index_pfp_subtract_exists_bb)) * bc)) /\ exists fom_beta_quotient_pfp_subtract_exists_bb_entry. bb = fom_beta_quotient_pfp_subtract_exists_bb_entry * S ((S (fom_index_pfp_subtract_exists_bb)) * bc) + (fom_value_pfp_subtract_exists_bb))) /\ (exists fom_gap_pfp_subtract_exists_bb_value_bound. fom_gap_pfp_subtract_exists_bb_value_bound + S (fom_value_pfp_subtract_exists_bb) = p))) -> exists rb rc. (forall pfs_index_subtract_exists_result. (exists pfa_gap_subtract_exists_resultindex. pfa_gap_subtract_exists_resultindex + S (pfs_index_subtract_exists_result) = (l)) -> exists pfs_left_subtract_exists_result pfs_right_subtract_exists_result pfs_result_subtract_exists_result. ((((exists ff_h_pfp_subtract_exists_resultleft. ff_h_pfp_subtract_exists_resultleft + S (pfs_left_subtract_exists_result) = S ((S (pfs_index_subtract_exists_result)) * ac)) /\ exists ff_q_pfp_subtract_exists_resultleft. ab = ff_q_pfp_subtract_exists_resultleft * S ((S (pfs_index_subtract_exists_result)) * ac) + (pfs_left_subtract_exists_result))) /\ (((((exists ff_h_pfp_subtract_exists_resultright. ff_h_pfp_subtract_exists_resultright + S (pfs_right_subtract_exists_result) = S ((S (pfs_index_subtract_exists_result)) * bc)) /\ exists ff_q_pfp_subtract_exists_resultright. bb = ff_q_pfp_subtract_exists_resultright * S ((S (pfs_index_subtract_exists_result)) * bc) + (pfs_right_subtract_exists_result))) /\ (((((exists ff_h_pfp_subtract_exists_resultresult. ff_h_pfp_subtract_exists_resultresult + S (pfs_result_subtract_exists_result) = S ((S (pfs_index_subtract_exists_result)) * rc)) /\ exists ff_q_pfp_subtract_exists_resultresult. rb = ff_q_pfp_subtract_exists_resultresult * S ((S (pfs_index_subtract_exists_result)) * rc) + (pfs_result_subtract_exists_result))) /\ ((((exists pfa_gap_subtract_exists_resultoperationleft. pfa_gap_subtract_exists_resultoperationleft + S (pfs_right_subtract_exists_result) = (p)) /\ (((exists pfa_gap_subtract_exists_resultoperationright. pfa_gap_subtract_exists_resultoperationright + S (pfs_result_subtract_exists_result) = (p)) /\ ((((exists pfa_gap_subtract_exists_resultoperationresultbound. pfa_gap_subtract_exists_resultoperationresultbound + S (pfs_left_subtract_exists_result) = (p)) /\ ((exists pfa_offset_left_subtract_exists_resultoperationresultcongruence pfa_offset_right_subtract_exists_resultoperationresultcongruence. ((pfs_right_subtract_exists_result) + (pfs_result_subtract_exists_result)) + (p) * pfa_offset_left_subtract_exists_resultoperationresultcongruence = (pfs_left_subtract_exists_result) + (p) * pfa_offset_right_subtract_exists_resultoperationresultcongruence))))))))))))))))

Complete tactic proof in conservative notation

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

124 script commands · 44 reading checkpoints · 7 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 (2)
prime field polynomial subtract emptyprime field subtract exists
01Fix variables and assumptionsL1–7

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 l
  7. L7
    intro hp
02Induction on lL8–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L8
    induction l
  2. L9
    intro ha
  3. L10
    intro hb
03Construct an explicit witnessL11–12

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

  1. L11
    exists 0
  2. L12
    exists 0
04Use earlier factsL13–20

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

  1. L13
    specialize prime_field_polynomial_subtract_empty (p)
  2. L14
    specialize prime_field_polynomial_subtract_empty (ab)
  3. L15
    specialize prime_field_polynomial_subtract_empty (ac)
  4. L16
    specialize prime_field_polynomial_subtract_empty (bb)
  5. L17
    specialize prime_field_polynomial_subtract_empty (bc)
  6. L18
    specialize prime_field_polynomial_subtract_empty (0)
  7. L19
    specialize prime_field_polynomial_subtract_empty (0)
  8. L20
    apply prime_field_polynomial_subtract_empty
05Fix variables and assumptionsL21–22

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

  1. L21
    intro ha
  2. L22
    intro hb
06Establish holdL23–32

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

  1. L23
    have hold : ∃ rb. ∃ rc. FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,l)Definitions: FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,l)Original native command in the exact edition
  2. L24
    apply IH
  3. L25
    intro j
  4. L26
    intro hj
  5. L27
    specialize ha (j)
  6. L28
    apply ha
  7. L29
    specialize le_succ (S j)
  8. L30
    specialize le_succ (l)
  9. L31
    apply le_succ
  10. L32
    exact hj
07Fix variables and assumptionsL33–34

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

  1. L33
    intro j
  2. L34
    intro hj
08Use earlier factsL35–40

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

  1. L35
    specialize hb (j)
  2. L36
    apply hb
  3. L37
    specialize le_succ (S j)
  4. L38
    specialize le_succ (l)
  5. L39
    apply le_succ
  6. L40
    exact hj
09Separate the logical casesL41–42

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

  1. L41
    cases hold
  2. L42
    cases hold_witness
10Establish hsource0L43–45

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

  1. L43
    have hsource0 : ∃ a. BetaAt(ab,ac,l,a) ∧ Lt(a,p)Definitions: BetaAt(ab,ac,l,a)Lt(a,p)Original native command in the exact edition
  2. L44
    specialize ha (l)
  3. L45
    apply ha
11Construct an explicit witnessL46–46

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

  1. L46
    exists 0
12Use earlier factsL47–47

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

  1. L47
    apply zero_add
13Separate the logical casesL48–49

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

  1. L48
    cases hsource0
  2. L49
    cases hsource0_witness
14Establish hsource1L50–52

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

  1. L50
    have hsource1 : ∃ a. BetaAt(bb,bc,l,a) ∧ Lt(a,p)Definitions: BetaAt(bb,bc,l,a)Lt(a,p)Original native command in the exact edition
  2. L51
    specialize hb (l)
  3. L52
    apply hb
15Construct an explicit witnessL53–53

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

  1. L53
    exists 0
16Use earlier factsL54–54

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

  1. L54
    apply zero_add
17Separate the logical casesL55–56

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

  1. L55
    cases hsource1
  2. L56
    cases hsource1_witness
18Establish hvalueL57–64

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

  1. L57
    have hvalue : ∃ r. FpAdd(p,x3,r,x2)Definitions: FpAdd(p,x3,r,x2)Original native command in the exact edition
  2. L58
    specialize prime_field_subtract_exists (p)
  3. L59
    specialize prime_field_subtract_exists (x2)
  4. L60
    specialize prime_field_subtract_exists (x3)
  5. L61
    apply prime_field_subtract_exists
  6. L62
    exact hp
  7. L63
    exact hsource0_witness_right
  8. L64
    exact hsource1_witness_right
19Separate the logical casesL65–65

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

  1. L65
    cases hvalue
20Establish hnewL66–71

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

  1. L66
    have hnew : ∃ db. ∃ dc. BetaAt(db,dc,l,x4) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(db,dc,y,z))Definitions: BetaAt(db,dc,l,x4)Lt(y,l)BetaAt(x,x1,y,z)BetaAt(db,dc,y,z)Original native command in the exact edition
  2. L67
    specialize beta_prefix_extend (l)
  3. L68
    specialize beta_prefix_extend (x)
  4. L69
    specialize beta_prefix_extend (x1)
  5. L70
    specialize beta_prefix_extend (x4)
  6. L71
    apply beta_prefix_extend
21Separate the logical casesL72–74

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

  1. L72
    cases hnew
  2. L73
    cases hnew_witness
  3. L74
    cases hnew_witness_witness
22Construct an explicit witnessL75–76

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

  1. L75
    exists x5
  2. L76
    exists x6
23Fix variables and assumptionsL77–78

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

  1. L77
    intro j
  2. L78
    intro hj
24Establish hcaseL79–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L79
    have hcase : j = l ∨ Lt(j,l)Definitions: Lt(j,l)Original native command in the exact edition
  2. L80
    specialize finite_lt_succ_eq_or_lt (l)
  3. L81
    specialize finite_lt_succ_eq_or_lt (j)
  4. L82
    apply finite_lt_succ_eq_or_lt
  5. L83
    exact hj
25Separate the logical casesL84–84

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

  1. L84
    cases hcase
26Construct an explicit witnessL85–87

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

  1. L85
    exists x2
  2. L86
    exists x3
  3. L87
    exists x4
27Separate the logical casesL88–88

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

  1. L88
    split
28Calculate and transport equalitiesL89–90

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

  1. L89
    rewrite hcase_left
  2. L90
    rewrite hcase_left
29Use earlier factsL91–91

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

  1. L91
    exact hsource0_witness_left
30Separate the logical casesL92–92

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

  1. L92
    split
31Calculate and transport equalitiesL93–94

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

  1. L93
    rewrite hcase_left
  2. L94
    rewrite hcase_left
32Use earlier factsL95–95

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

  1. L95
    exact hsource1_witness_left
33Separate the logical casesL96–96

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

  1. L96
    split
34Calculate and transport equalitiesL97–98

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

  1. L97
    rewrite hcase_left
  2. L98
    rewrite hcase_left
35Use earlier factsL99–100

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

  1. L99
    exact hnew_witness_witness_left
  2. L100
    exact hvalue_witness
36Establish hpreviousL101–104

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

  1. L101
    have hprevious : ∃ v0. ∃ v1. ∃ v2. BetaAt(ab,ac,j,v0) ∧ (BetaAt(bb,bc,j,v1) ∧ (BetaAt(x,x1,j,v2) ∧ FpAdd(p,v1,v2,v0)))Definitions: BetaAt(ab,ac,j,v0)BetaAt(bb,bc,j,v1)BetaAt(x,x1,j,v2)FpAdd(p,v1,v2,v0)Original native command in the exact edition
  2. L102
    specialize hold_witness_witness (j)
  3. L103
    apply hold_witness_witness
  4. L104
    exact hcase_right
37Separate the logical casesL105–110

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

  1. L105
    cases hprevious
  2. L106
    cases hprevious_witness
  3. L107
    cases hprevious_witness_witness
  4. L108
    cases hprevious_witness_witness_witness
  5. L109
    cases hprevious_witness_witness_witness_right
  6. L110
    cases hprevious_witness_witness_witness_right_right
38Construct an explicit witnessL111–113

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

  1. L111
    exists x7
  2. L112
    exists x8
  3. L113
    exists x9
39Separate the logical casesL114–114

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

  1. L114
    split
40Use earlier factsL115–115

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

  1. L115
    exact hprevious_witness_witness_witness_left
41Separate the logical casesL116–116

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

  1. L116
    split
42Use earlier factsL117–117

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

  1. L117
    exact hprevious_witness_witness_witness_right_left
43Separate the logical casesL118–118

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

  1. L118
    split
44Use earlier factsL119–124

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

  1. L119
    specialize hnew_witness_witness_right (j)
  2. L120
    specialize hnew_witness_witness_right (x9)
  3. L121
    apply hnew_witness_witness_right
  4. L122
    exact hcase_right
  5. L123
    exact hprevious_witness_witness_witness_right_right_left
  6. L124
    exact hprevious_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 124 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro l
  7. 0007intro hp
  8. 0008induction l
  9. 0009intro ha
  10. 0010intro hb
  11. 0011exists 0
  12. 0012exists 0
  13. 0013specialize prime_field_polynomial_subtract_empty (p)
  14. 0014specialize prime_field_polynomial_subtract_empty (ab)
  15. 0015specialize prime_field_polynomial_subtract_empty (ac)
  16. 0016specialize prime_field_polynomial_subtract_empty (bb)
  17. 0017specialize prime_field_polynomial_subtract_empty (bc)
  18. 0018specialize prime_field_polynomial_subtract_empty (0)
  19. 0019specialize prime_field_polynomial_subtract_empty (0)
  20. 0020apply prime_field_polynomial_subtract_empty
  21. 0021intro ha
  22. 0022intro hb
  23. 0023have hold : ∃ rb. ∃ rc. FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,l)
  24. 0024apply IH
  25. 0025intro j
  26. 0026intro hj
  27. 0027specialize ha (j)
  28. 0028apply ha
  29. 0029specialize le_succ (S j)
  30. 0030specialize le_succ (l)
  31. 0031apply le_succ
  32. 0032exact hj
  33. 0033intro j
  34. 0034intro hj
  35. 0035specialize hb (j)
  36. 0036apply hb
  37. 0037specialize le_succ (S j)
  38. 0038specialize le_succ (l)
  39. 0039apply le_succ
  40. 0040exact hj
  41. 0041cases hold
  42. 0042cases hold_witness
  43. 0043have hsource0 : ∃ a. BetaAt(ab,ac,l,a) ∧ Lt(a,p)
  44. 0044specialize ha (l)
  45. 0045apply ha
  46. 0046exists 0
  47. 0047apply zero_add
  48. 0048cases hsource0
  49. 0049cases hsource0_witness
  50. 0050have hsource1 : ∃ a. BetaAt(bb,bc,l,a) ∧ Lt(a,p)
  51. 0051specialize hb (l)
  52. 0052apply hb
  53. 0053exists 0
  54. 0054apply zero_add
  55. 0055cases hsource1
  56. 0056cases hsource1_witness
  57. 0057have hvalue : ∃ r. FpAdd(p,x3,r,x2)
  58. 0058specialize prime_field_subtract_exists (p)
  59. 0059specialize prime_field_subtract_exists (x2)
  60. 0060specialize prime_field_subtract_exists (x3)
  61. 0061apply prime_field_subtract_exists
  62. 0062exact hp
  63. 0063exact hsource0_witness_right
  64. 0064exact hsource1_witness_right
  65. 0065cases hvalue
  66. 0066have hnew : ∃ db. ∃ dc. BetaAt(db,dc,l,x4) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(db,dc,y,z))
  67. 0067specialize beta_prefix_extend (l)
  68. 0068specialize beta_prefix_extend (x)
  69. 0069specialize beta_prefix_extend (x1)
  70. 0070specialize beta_prefix_extend (x4)
  71. 0071apply beta_prefix_extend
  72. 0072cases hnew
  73. 0073cases hnew_witness
  74. 0074cases hnew_witness_witness
  75. 0075exists x5
  76. 0076exists x6
  77. 0077intro j
  78. 0078intro hj
  79. 0079have hcase : j = l ∨ Lt(j,l)
  80. 0080specialize finite_lt_succ_eq_or_lt (l)
  81. 0081specialize finite_lt_succ_eq_or_lt (j)
  82. 0082apply finite_lt_succ_eq_or_lt
  83. 0083exact hj
  84. 0084cases hcase
  85. 0085exists x2
  86. 0086exists x3
  87. 0087exists x4
  88. 0088split
  89. 0089rewrite hcase_left
  90. 0090rewrite hcase_left
  91. 0091exact hsource0_witness_left
  92. 0092split
  93. 0093rewrite hcase_left
  94. 0094rewrite hcase_left
  95. 0095exact hsource1_witness_left
  96. 0096split
  97. 0097rewrite hcase_left
  98. 0098rewrite hcase_left
  99. 0099exact hnew_witness_witness_left
  100. 0100exact hvalue_witness
  101. 0101have hprevious : ∃ v0. ∃ v1. ∃ v2. BetaAt(ab,ac,j,v0) ∧ (BetaAt(bb,bc,j,v1) ∧ (BetaAt(x,x1,j,v2) ∧ FpAdd(p,v1,v2,v0)))
  102. 0102specialize hold_witness_witness (j)
  103. 0103apply hold_witness_witness
  104. 0104exact hcase_right
  105. 0105cases hprevious
  106. 0106cases hprevious_witness
  107. 0107cases hprevious_witness_witness
  108. 0108cases hprevious_witness_witness_witness
  109. 0109cases hprevious_witness_witness_witness_right
  110. 0110cases hprevious_witness_witness_witness_right_right
  111. 0111exists x7
  112. 0112exists x8
  113. 0113exists x9
  114. 0114split
  115. 0115exact hprevious_witness_witness_witness_left
  116. 0116split
  117. 0117exact hprevious_witness_witness_witness_right_left
  118. 0118split
  119. 0119specialize hnew_witness_witness_right (j)
  120. 0120specialize hnew_witness_witness_right (x9)
  121. 0121apply hnew_witness_witness_right
  122. 0122exact hcase_right
  123. 0123exact hprevious_witness_witness_witness_right_right_left
  124. 0124exact hprevious_witness_witness_witness_right_right_right