PQ0004

prime_field_polynomial_negate_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic 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))))))))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 6 declared prerequisites and contains 91 exact native proof lines.

Alpha v34 checked-use · first admitted v32 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

PQ0003 prime_field_polynomial_negate_empty le_succ Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized prime_field_negate_exists Alpha theorem; checked-use authorized beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (1)
prime field polynomial negate empty

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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 : exists a. ((((exists ff_h_pfp_negate_last_source0. ff_h_pfp_negate_last_source0 + S (a) = S ((S (l)) * ac)) /\ exists ff_q_pfp_negate_last_source0. ab = ff_q_pfp_negate_last_source0 * S ((S (l)) * ac) + (a))) /\ ((exists pfa_gap_negate_last_bound0. pfa_gap_negate_last_bound0 + S (a) = (p))))
  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
  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: LtBetaAt
  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 \/ (exists pfa_gap_negate_index_case. pfa_gap_negate_index_case + S (j) = (l))
  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: FpAddBetaAt
  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 exact 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 : exists rb rc. (forall pfs_index_negate_old. (exists pfa_gap_negate_oldindex. pfa_gap_negate_oldindex + S (pfs_index_negate_old) = (l)) -> exists pfs_source_negate_old pfs_result_negate_old. ((((exists ff_h_pfp_negate_oldsource. ff_h_pfp_negate_oldsource + S (pfs_source_negate_old) = S ((S (pfs_index_negate_old)) * ac)) /\ exists ff_q_pfp_negate_oldsource. ab = ff_q_pfp_negate_oldsource * S ((S (pfs_index_negate_old)) * ac) + (pfs_source_negate_old))) /\ (((((exists ff_h_pfp_negate_oldresult. ff_h_pfp_negate_oldresult + S (pfs_result_negate_old) = S ((S (pfs_index_negate_old)) * rc)) /\ exists ff_q_pfp_negate_oldresult. rb = ff_q_pfp_negate_oldresult * S ((S (pfs_index_negate_old)) * rc) + (pfs_result_negate_old))) /\ ((((exists pfa_gap_negate_oldoperationadditionleft. pfa_gap_negate_oldoperationadditionleft + S (pfs_source_negate_old) = (p)) /\ (((exists pfa_gap_negate_oldoperationadditionright. pfa_gap_negate_oldoperationadditionright + S (pfs_result_negate_old) = (p)) /\ ((((exists pfa_gap_negate_oldoperationadditionresultbound. pfa_gap_negate_oldoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negate_oldoperationadditionresultcongruence pfa_offset_right_negate_oldoperationadditionresultcongruence. ((pfs_source_negate_old) + (pfs_result_negate_old)) + (p) * pfa_offset_left_negate_oldoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_negate_oldoperationadditionresultcongruence))))))))))))))
  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 : exists a. ((((exists ff_h_pfp_negate_last_source0. ff_h_pfp_negate_last_source0 + S (a) = S ((S (l)) * ac)) /\ exists ff_q_pfp_negate_last_source0. ab = ff_q_pfp_negate_last_source0 * S ((S (l)) * ac) + (a))) /\ ((exists pfa_gap_negate_last_bound0. pfa_gap_negate_last_bound0 + S (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 : exists r. (((exists pfa_gap_negate_last_valueadditionleft. pfa_gap_negate_last_valueadditionleft + S (x2) = (p)) /\ (((exists pfa_gap_negate_last_valueadditionright. pfa_gap_negate_last_valueadditionright + S (r) = (p)) /\ ((((exists pfa_gap_negate_last_valueadditionresultbound. pfa_gap_negate_last_valueadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negate_last_valueadditionresultcongruence pfa_offset_right_negate_last_valueadditionresultcongruence. ((x2) + (r)) + (p) * pfa_offset_left_negate_last_valueadditionresultcongruence = (0) + (p) * pfa_offset_right_negate_last_valueadditionresultcongruence)))))))))
  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 : exists db dc. (((((exists ff_h_pfp_negate_append. ff_h_pfp_negate_append + S (x3) = S ((S (l)) * dc)) /\ exists ff_q_pfp_negate_append. db = ff_q_pfp_negate_append * S ((S (l)) * dc) + (x3))) /\ ((forall mdr_i_pfp_negate_preserve mdr_a_pfp_negate_preserve. (exists mdr_gap_pfp_negate_preserveb. mdr_gap_pfp_negate_preserveb + S (mdr_i_pfp_negate_preserve) = (l)) -> (((exists ff_h_mdr_pfp_negate_preserveo. ff_h_mdr_pfp_negate_preserveo + S (mdr_a_pfp_negate_preserve) = S ((S (mdr_i_pfp_negate_preserve)) * x1)) /\ exists ff_q_mdr_pfp_negate_preserveo. x = ff_q_mdr_pfp_negate_preserveo * S ((S (mdr_i_pfp_negate_preserve)) * x1) + (mdr_a_pfp_negate_preserve))) -> (((exists ff_h_mdr_pfp_negate_preserven. ff_h_mdr_pfp_negate_preserven + S (mdr_a_pfp_negate_preserve) = S ((S (mdr_i_pfp_negate_preserve)) * dc)) /\ exists ff_q_mdr_pfp_negate_preserven. db = ff_q_mdr_pfp_negate_preserven * S ((S (mdr_i_pfp_negate_preserve)) * dc) + (mdr_a_pfp_negate_preserve)))))))
  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 \/ (exists pfa_gap_negate_index_case. pfa_gap_negate_index_case + S (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 : exists v0 v1. (((((exists ff_h_pfp_negate_previous0. ff_h_pfp_negate_previous0 + S (v0) = S ((S (j)) * ac)) /\ exists ff_q_pfp_negate_previous0. ab = ff_q_pfp_negate_previous0 * S ((S (j)) * ac) + (v0))) /\ (((((exists ff_h_pfp_negate_previous1. ff_h_pfp_negate_previous1 + S (v1) = S ((S (j)) * x1)) /\ exists ff_q_pfp_negate_previous1. x = ff_q_pfp_negate_previous1 * S ((S (j)) * x1) + (v1))) /\ ((((exists pfa_gap_negate_previousoperationadditionleft. pfa_gap_negate_previousoperationadditionleft + S (v0) = (p)) /\ (((exists pfa_gap_negate_previousoperationadditionright. pfa_gap_negate_previousoperationadditionright + S (v1) = (p)) /\ ((((exists pfa_gap_negate_previousoperationadditionresultbound. pfa_gap_negate_previousoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negate_previousoperationadditionresultcongruence pfa_offset_right_negate_previousoperationadditionresultcongruence. ((v0) + (v1)) + (p) * pfa_offset_left_negate_previousoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_negate_previousoperationadditionresultcongruence))))))))))))))
  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