PQ0004

prime_field_polynomial_negate_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. ∀ l. Prime(p) → BetaPrefixInto(ab,ac,l,p) → ∃ x. ∃ y. FpCoefficientNegation(p,ab,ac,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) · 1FpCoefficientNegation(p,ab,ac,rb,rc,L) · 2Lt(a,b) · 3Prime(p) · 1BetaAt(b,c,i,x) · 6

Actual proof prerequisites

prime_field_polynomial_negate_emptyle_succ · checked external prerequisitezero_add · checked external prerequisiteprime_field_negate_exists · checked external prerequisitebeta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall p ab ac l. (~((p) = 1) /\ forall pfa_factor_left_negate_exists_prime pfa_factor_right_negate_exists_prime. (p) = pfa_factor_left_negate_exists_prime * pfa_factor_right_negate_exists_prime -> pfa_factor_left_negate_exists_prime = 1 \/ pfa_factor_right_negate_exists_prime = 1) -> (forall fom_index_pfp_negate_exists_ab. (exists fom_gap_pfp_negate_exists_ab_index_bound. fom_gap_pfp_negate_exists_ab_index_bound + S (fom_index_pfp_negate_exists_ab) = l) -> exists fom_value_pfp_negate_exists_ab. ((((exists fom_beta_height_pfp_negate_exists_ab_entry. fom_beta_height_pfp_negate_exists_ab_entry + S (fom_value_pfp_negate_exists_ab) = S ((S (fom_index_pfp_negate_exists_ab)) * ac)) /\ exists fom_beta_quotient_pfp_negate_exists_ab_entry. ab = fom_beta_quotient_pfp_negate_exists_ab_entry * S ((S (fom_index_pfp_negate_exists_ab)) * ac) + (fom_value_pfp_negate_exists_ab))) /\ (exists fom_gap_pfp_negate_exists_ab_value_bound. fom_gap_pfp_negate_exists_ab_value_bound + S (fom_value_pfp_negate_exists_ab) = p))) -> exists rb rc. (forall pfs_index_negate_exists_result. (exists pfa_gap_negate_exists_resultindex. pfa_gap_negate_exists_resultindex + S (pfs_index_negate_exists_result) = (l)) -> exists pfs_source_negate_exists_result pfs_result_negate_exists_result. ((((exists ff_h_pfp_negate_exists_resultsource. ff_h_pfp_negate_exists_resultsource + S (pfs_source_negate_exists_result) = S ((S (pfs_index_negate_exists_result)) * ac)) /\ exists ff_q_pfp_negate_exists_resultsource. ab = ff_q_pfp_negate_exists_resultsource * S ((S (pfs_index_negate_exists_result)) * ac) + (pfs_source_negate_exists_result))) /\ (((((exists ff_h_pfp_negate_exists_resultresult. ff_h_pfp_negate_exists_resultresult + S (pfs_result_negate_exists_result) = S ((S (pfs_index_negate_exists_result)) * rc)) /\ exists ff_q_pfp_negate_exists_resultresult. rb = ff_q_pfp_negate_exists_resultresult * S ((S (pfs_index_negate_exists_result)) * rc) + (pfs_result_negate_exists_result))) /\ ((((exists pfa_gap_negate_exists_resultoperationadditionleft. pfa_gap_negate_exists_resultoperationadditionleft + S (pfs_source_negate_exists_result) = (p)) /\ (((exists pfa_gap_negate_exists_resultoperationadditionright. pfa_gap_negate_exists_resultoperationadditionright + S (pfs_result_negate_exists_result) = (p)) /\ ((((exists pfa_gap_negate_exists_resultoperationadditionresultbound. pfa_gap_negate_exists_resultoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negate_exists_resultoperationadditionresultcongruence pfa_offset_right_negate_exists_resultoperationadditionresultcongruence. ((pfs_source_negate_exists_result) + (pfs_result_negate_exists_result)) + (p) * pfa_offset_left_negate_exists_resultoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_negate_exists_resultoperationadditionresultcongruence))))))))))))))

Complete tactic proof in conservative notation

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

91 script commands · 33 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.

Named ingredients (1)
prime field polynomial negate empty
01Fix variables and assumptionsL1–5

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 l
  5. L5
    intro hp
02Induction on lL6–7

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

  1. L6
    induction l
  2. L7
    intro ha
03Construct an explicit witnessL8–9

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

  1. L8
    exists 0
  2. L9
    exists 0
04Use earlier factsL10–15

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

  1. L10
    specialize prime_field_polynomial_negate_empty (p)
  2. L11
    specialize prime_field_polynomial_negate_empty (ab)
  3. L12
    specialize prime_field_polynomial_negate_empty (ac)
  4. L13
    specialize prime_field_polynomial_negate_empty (0)
  5. L14
    specialize prime_field_polynomial_negate_empty (0)
  6. L15
    apply prime_field_polynomial_negate_empty
05Fix variables and assumptionsL16–16

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

  1. L16
    intro ha
06Establish holdL17–26

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

  1. L17
    have hold : ∃ rb. ∃ rc. FpCoefficientNegation(p,ab,ac,rb,rc,l)Definitions: FpCoefficientNegation(p,ab,ac,rb,rc,l)Original native command in the exact edition
  2. L18
    apply IH
  3. L19
    intro j
  4. L20
    intro hj
  5. L21
    specialize ha (j)
  6. L22
    apply ha
  7. L23
    specialize le_succ (S j)
  8. L24
    specialize le_succ (l)
  9. L25
    apply le_succ
  10. L26
    exact hj
07Separate the logical casesL27–28

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

  1. L27
    cases hold
  2. L28
    cases hold_witness
08Establish hsource0L29–31

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

  1. L29
    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. L30
    specialize ha (l)
  3. L31
    apply ha
09Construct an explicit witnessL32–32

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

  1. L32
    exists 0
10Use earlier factsL33–33

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

  1. L33
    apply zero_add
11Separate the logical casesL34–35

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

  1. L34
    cases hsource0
  2. L35
    cases hsource0_witness
12Establish hvalueL36–41

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

  1. L36
    have hvalue : ∃ r. FpAdd(p,x2,r,0)Definitions: FpAdd(p,x2,r,0)Original native command in the exact edition
  2. L37
    specialize prime_field_negate_exists (p)
  3. L38
    specialize prime_field_negate_exists (x2)
  4. L39
    apply prime_field_negate_exists
  5. L40
    exact hp
  6. L41
    exact hsource0_witness_right
13Separate the logical casesL42–42

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

  1. L42
    cases hvalue
14Establish hnewL43–48

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

  1. L43
    have hnew : ∃ db. ∃ dc. BetaAt(db,dc,l,x3) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(db,dc,y,z))Definitions: BetaAt(db,dc,l,x3)Lt(y,l)BetaAt(x,x1,y,z)BetaAt(db,dc,y,z)Original native command in the exact edition
  2. L44
    specialize beta_prefix_extend (l)
  3. L45
    specialize beta_prefix_extend (x)
  4. L46
    specialize beta_prefix_extend (x1)
  5. L47
    specialize beta_prefix_extend (x3)
  6. L48
    apply beta_prefix_extend
15Separate the logical casesL49–51

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

  1. L49
    cases hnew
  2. L50
    cases hnew_witness
  3. L51
    cases hnew_witness_witness
16Construct an explicit witnessL52–53

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

  1. L52
    exists x4
  2. L53
    exists x5
17Fix variables and assumptionsL54–55

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

  1. L54
    intro j
  2. L55
    intro hj
18Establish hcaseL56–60

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. L56
    have hcase : j = l ∨ Lt(j,l)Definitions: Lt(j,l)Original native command in the exact edition
  2. L57
    specialize finite_lt_succ_eq_or_lt (l)
  3. L58
    specialize finite_lt_succ_eq_or_lt (j)
  4. L59
    apply finite_lt_succ_eq_or_lt
  5. L60
    exact hj
19Separate the logical casesL61–61

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

  1. L61
    cases hcase
20Construct an explicit witnessL62–63

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

  1. L62
    exists x2
  2. L63
    exists x3
21Separate the logical casesL64–64

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

  1. L64
    split
22Calculate and transport equalitiesL65–66

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

  1. L65
    rewrite hcase_left
  2. L66
    rewrite hcase_left
23Use earlier factsL67–67

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

  1. L67
    exact hsource0_witness_left
24Separate the logical casesL68–68

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

  1. L68
    split
25Calculate and transport equalitiesL69–70

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

  1. L69
    rewrite hcase_left
  2. L70
    rewrite hcase_left
26Use earlier factsL71–72

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

  1. L71
    exact hnew_witness_witness_left
  2. L72
    exact hvalue_witness
27Establish hpreviousL73–76

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

  1. L73
    have hprevious : ∃ v0. ∃ v1. BetaAt(ab,ac,j,v0) ∧ (BetaAt(x,x1,j,v1) ∧ FpAdd(p,v0,v1,0))Definitions: BetaAt(ab,ac,j,v0)BetaAt(x,x1,j,v1)FpAdd(p,v0,v1,0)Original native command in the exact edition
  2. L74
    specialize hold_witness_witness (j)
  3. L75
    apply hold_witness_witness
  4. L76
    exact hcase_right
28Separate the logical casesL77–80

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

  1. L77
    cases hprevious
  2. L78
    cases hprevious_witness
  3. L79
    cases hprevious_witness_witness
  4. L80
    cases hprevious_witness_witness_right
29Construct an explicit witnessL81–82

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

  1. L81
    exists x6
  2. L82
    exists x7
30Separate the logical casesL83–83

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

  1. L83
    split
31Use earlier factsL84–84

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

  1. L84
    exact hprevious_witness_witness_left
32Separate the logical casesL85–85

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

  1. L85
    split
33Use earlier factsL86–91

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

  1. L86
    specialize hnew_witness_witness_right (j)
  2. L87
    specialize hnew_witness_witness_right (x7)
  3. L88
    apply hnew_witness_witness_right
  4. L89
    exact hcase_right
  5. L90
    exact hprevious_witness_witness_right_left
  6. L91
    exact hprevious_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 91 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro l
  5. 0005intro hp
  6. 0006induction l
  7. 0007intro ha
  8. 0008exists 0
  9. 0009exists 0
  10. 0010specialize prime_field_polynomial_negate_empty (p)
  11. 0011specialize prime_field_polynomial_negate_empty (ab)
  12. 0012specialize prime_field_polynomial_negate_empty (ac)
  13. 0013specialize prime_field_polynomial_negate_empty (0)
  14. 0014specialize prime_field_polynomial_negate_empty (0)
  15. 0015apply prime_field_polynomial_negate_empty
  16. 0016intro ha
  17. 0017have hold : ∃ rb. ∃ rc. FpCoefficientNegation(p,ab,ac,rb,rc,l)
  18. 0018apply IH
  19. 0019intro j
  20. 0020intro hj
  21. 0021specialize ha (j)
  22. 0022apply ha
  23. 0023specialize le_succ (S j)
  24. 0024specialize le_succ (l)
  25. 0025apply le_succ
  26. 0026exact hj
  27. 0027cases hold
  28. 0028cases hold_witness
  29. 0029have hsource0 : ∃ a. BetaAt(ab,ac,l,a) ∧ Lt(a,p)
  30. 0030specialize ha (l)
  31. 0031apply ha
  32. 0032exists 0
  33. 0033apply zero_add
  34. 0034cases hsource0
  35. 0035cases hsource0_witness
  36. 0036have hvalue : ∃ r. FpAdd(p,x2,r,0)
  37. 0037specialize prime_field_negate_exists (p)
  38. 0038specialize prime_field_negate_exists (x2)
  39. 0039apply prime_field_negate_exists
  40. 0040exact hp
  41. 0041exact hsource0_witness_right
  42. 0042cases hvalue
  43. 0043have hnew : ∃ db. ∃ dc. BetaAt(db,dc,l,x3) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(db,dc,y,z))
  44. 0044specialize beta_prefix_extend (l)
  45. 0045specialize beta_prefix_extend (x)
  46. 0046specialize beta_prefix_extend (x1)
  47. 0047specialize beta_prefix_extend (x3)
  48. 0048apply beta_prefix_extend
  49. 0049cases hnew
  50. 0050cases hnew_witness
  51. 0051cases hnew_witness_witness
  52. 0052exists x4
  53. 0053exists x5
  54. 0054intro j
  55. 0055intro hj
  56. 0056have hcase : j = l ∨ Lt(j,l)
  57. 0057specialize finite_lt_succ_eq_or_lt (l)
  58. 0058specialize finite_lt_succ_eq_or_lt (j)
  59. 0059apply finite_lt_succ_eq_or_lt
  60. 0060exact hj
  61. 0061cases hcase
  62. 0062exists x2
  63. 0063exists x3
  64. 0064split
  65. 0065rewrite hcase_left
  66. 0066rewrite hcase_left
  67. 0067exact hsource0_witness_left
  68. 0068split
  69. 0069rewrite hcase_left
  70. 0070rewrite hcase_left
  71. 0071exact hnew_witness_witness_left
  72. 0072exact hvalue_witness
  73. 0073have hprevious : ∃ v0. ∃ v1. BetaAt(ab,ac,j,v0) ∧ (BetaAt(x,x1,j,v1) ∧ FpAdd(p,v0,v1,0))
  74. 0074specialize hold_witness_witness (j)
  75. 0075apply hold_witness_witness
  76. 0076exact hcase_right
  77. 0077cases hprevious
  78. 0078cases hprevious_witness
  79. 0079cases hprevious_witness_witness
  80. 0080cases hprevious_witness_witness_right
  81. 0081exists x6
  82. 0082exists x7
  83. 0083split
  84. 0084exact hprevious_witness_witness_left
  85. 0085split
  86. 0086specialize hnew_witness_witness_right (j)
  87. 0087specialize hnew_witness_witness_right (x7)
  88. 0088apply hnew_witness_witness_right
  89. 0089exact hcase_right
  90. 0090exact hprevious_witness_witness_right_left
  91. 0091exact hprevious_witness_witness_right_right