PQ0007

prime_field_polynomial_negate_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. ∀ rb. ∀ rc. ∀ db. ∀ dc. ∀ l. FpCoefficientNegation(p,ab,ac,rb,rc,l) → FpCoefficientNegation(p,ab,ac,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

FpCoefficientNegation(p,ab,ac,rb,rc,L) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 4

Actual proof prerequisites

beta_at_exists · checked external prerequisiteprime_field_negate_functional · checked external prerequisiteprime_field_polynomial_negate_entry
Original expanded first-order statement 
forall p ab ac rb rc db dc l. (forall pfs_index_negate_functional_first. (exists pfa_gap_negate_functional_firstindex. pfa_gap_negate_functional_firstindex + S (pfs_index_negate_functional_first) = (l)) -> exists pfs_source_negate_functional_first pfs_result_negate_functional_first. ((((exists ff_h_pfp_negate_functional_firstsource. ff_h_pfp_negate_functional_firstsource + S (pfs_source_negate_functional_first) = S ((S (pfs_index_negate_functional_first)) * ac)) /\ exists ff_q_pfp_negate_functional_firstsource. ab = ff_q_pfp_negate_functional_firstsource * S ((S (pfs_index_negate_functional_first)) * ac) + (pfs_source_negate_functional_first))) /\ (((((exists ff_h_pfp_negate_functional_firstresult. ff_h_pfp_negate_functional_firstresult + S (pfs_result_negate_functional_first) = S ((S (pfs_index_negate_functional_first)) * rc)) /\ exists ff_q_pfp_negate_functional_firstresult. rb = ff_q_pfp_negate_functional_firstresult * S ((S (pfs_index_negate_functional_first)) * rc) + (pfs_result_negate_functional_first))) /\ ((((exists pfa_gap_negate_functional_firstoperationadditionleft. pfa_gap_negate_functional_firstoperationadditionleft + S (pfs_source_negate_functional_first) = (p)) /\ (((exists pfa_gap_negate_functional_firstoperationadditionright. pfa_gap_negate_functional_firstoperationadditionright + S (pfs_result_negate_functional_first) = (p)) /\ ((((exists pfa_gap_negate_functional_firstoperationadditionresultbound. pfa_gap_negate_functional_firstoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negate_functional_firstoperationadditionresultcongruence pfa_offset_right_negate_functional_firstoperationadditionresultcongruence. ((pfs_source_negate_functional_first) + (pfs_result_negate_functional_first)) + (p) * pfa_offset_left_negate_functional_firstoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_negate_functional_firstoperationadditionresultcongruence)))))))))))))) -> (forall pfs_index_negate_functional_second. (exists pfa_gap_negate_functional_secondindex. pfa_gap_negate_functional_secondindex + S (pfs_index_negate_functional_second) = (l)) -> exists pfs_source_negate_functional_second pfs_result_negate_functional_second. ((((exists ff_h_pfp_negate_functional_secondsource. ff_h_pfp_negate_functional_secondsource + S (pfs_source_negate_functional_second) = S ((S (pfs_index_negate_functional_second)) * ac)) /\ exists ff_q_pfp_negate_functional_secondsource. ab = ff_q_pfp_negate_functional_secondsource * S ((S (pfs_index_negate_functional_second)) * ac) + (pfs_source_negate_functional_second))) /\ (((((exists ff_h_pfp_negate_functional_secondresult. ff_h_pfp_negate_functional_secondresult + S (pfs_result_negate_functional_second) = S ((S (pfs_index_negate_functional_second)) * dc)) /\ exists ff_q_pfp_negate_functional_secondresult. db = ff_q_pfp_negate_functional_secondresult * S ((S (pfs_index_negate_functional_second)) * dc) + (pfs_result_negate_functional_second))) /\ ((((exists pfa_gap_negate_functional_secondoperationadditionleft. pfa_gap_negate_functional_secondoperationadditionleft + S (pfs_source_negate_functional_second) = (p)) /\ (((exists pfa_gap_negate_functional_secondoperationadditionright. pfa_gap_negate_functional_secondoperationadditionright + S (pfs_result_negate_functional_second) = (p)) /\ ((((exists pfa_gap_negate_functional_secondoperationadditionresultbound. pfa_gap_negate_functional_secondoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negate_functional_secondoperationadditionresultcongruence pfa_offset_right_negate_functional_secondoperationadditionresultcongruence. ((pfs_source_negate_functional_second) + (pfs_result_negate_functional_second)) + (p) * pfa_offset_left_negate_functional_secondoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_negate_functional_secondoperationadditionresultcongruence)))))))))))))) -> (forall mdr_i_pfp_negate_functional_result mdr_a_pfp_negate_functional_result. (exists mdr_gap_pfp_negate_functional_resultb. mdr_gap_pfp_negate_functional_resultb + S (mdr_i_pfp_negate_functional_result) = (l)) -> (((exists ff_h_mdr_pfp_negate_functional_resulto. ff_h_mdr_pfp_negate_functional_resulto + S (mdr_a_pfp_negate_functional_result) = S ((S (mdr_i_pfp_negate_functional_result)) * rc)) /\ exists ff_q_mdr_pfp_negate_functional_resulto. rb = ff_q_mdr_pfp_negate_functional_resulto * S ((S (mdr_i_pfp_negate_functional_result)) * rc) + (mdr_a_pfp_negate_functional_result))) -> (((exists ff_h_mdr_pfp_negate_functional_resultn. ff_h_mdr_pfp_negate_functional_resultn + S (mdr_a_pfp_negate_functional_result) = S ((S (mdr_i_pfp_negate_functional_result)) * dc)) /\ exists ff_q_mdr_pfp_negate_functional_resultn. db = ff_q_mdr_pfp_negate_functional_resultn * S ((S (mdr_i_pfp_negate_functional_result)) * dc) + (mdr_a_pfp_negate_functional_result))))

Complete tactic proof in conservative notation

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

63 script commands · 12 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.

Named ingredients (1)
prime field polynomial negate 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 rb
  5. L5
    intro rc
  6. L6
    intro db
  7. L7
    intro dc
  8. L8
    intro l
  9. L9
    intro hfirst
  10. L10
    intro hsecond
02Fix variables and assumptionsL11–14

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

  1. L11
    intro i
  2. L12
    intro r
  3. L13
    intro hi
  4. L14
    intro hr
03Establish hchosen0L15–19

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

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

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

  1. L20
    cases hchosen0
05Establish hchosen1L21–25

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

  1. L21
    have hchosen1 : ∃ v. BetaAt(db,dc,i,v)Definitions: BetaAt(db,dc,i,v)Original native command in the exact edition
  2. L22
    specialize beta_at_exists (db)
  3. L23
    specialize beta_at_exists (dc)
  4. L24
    specialize beta_at_exists (i)
  5. L25
    apply beta_at_exists
06Separate the logical casesL26–26

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

  1. L26
    cases hchosen1
07Establish heqL27–36

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

  1. L27
    have heq : r=x1
  2. L28
    specialize prime_field_negate_functional (p)
  3. L29
    specialize prime_field_negate_functional (x)
  4. L30
    specialize prime_field_negate_functional (r)
  5. L31
    specialize prime_field_negate_functional (x1)
  6. L32
    apply prime_field_negate_functional
  7. L33
    specialize prime_field_polynomial_negate_entry (p)
  8. L34
    specialize prime_field_polynomial_negate_entry (ab)
  9. L35
    specialize prime_field_polynomial_negate_entry (ac)
  10. L36
    specialize prime_field_polynomial_negate_entry (rb)
08Use earlier factsL37–46

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

  1. L37
    specialize prime_field_polynomial_negate_entry (rc)
  2. L38
    specialize prime_field_polynomial_negate_entry (l)
  3. L39
    specialize prime_field_polynomial_negate_entry (i)
  4. L40
    specialize prime_field_polynomial_negate_entry (x)
  5. L41
    specialize prime_field_polynomial_negate_entry (r)
  6. L42
    apply prime_field_polynomial_negate_entry
  7. L43
    exact hfirst
  8. L44
    exact hi
  9. L45
    exact hchosen0_witness
  10. L46
    exact hr
09Use earlier factsL47–56

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

  1. L47
    specialize prime_field_polynomial_negate_entry (p)
  2. L48
    specialize prime_field_polynomial_negate_entry (ab)
  3. L49
    specialize prime_field_polynomial_negate_entry (ac)
  4. L50
    specialize prime_field_polynomial_negate_entry (db)
  5. L51
    specialize prime_field_polynomial_negate_entry (dc)
  6. L52
    specialize prime_field_polynomial_negate_entry (l)
  7. L53
    specialize prime_field_polynomial_negate_entry (i)
  8. L54
    specialize prime_field_polynomial_negate_entry (x)
  9. L55
    specialize prime_field_polynomial_negate_entry (x1)
  10. L56
    apply prime_field_polynomial_negate_entry
10Use earlier factsL57–60

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

  1. L57
    exact hsecond
  2. L58
    exact hi
  3. L59
    exact hchosen0_witness
  4. L60
    exact hchosen1_witness
11Calculate and transport equalitiesL61–62

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

  1. L61
    rewrite heq
  2. L62
    rewrite heq
12Use earlier factsL63–63

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

  1. L63
    exact hchosen1_witness

Library-wide reading audit

Original defined command ledger · 63 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro db
  7. 0007intro dc
  8. 0008intro l
  9. 0009intro hfirst
  10. 0010intro hsecond
  11. 0011intro i
  12. 0012intro r
  13. 0013intro hi
  14. 0014intro hr
  15. 0015have hchosen0 : ∃ v. BetaAt(ab,ac,i,v)
  16. 0016specialize beta_at_exists (ab)
  17. 0017specialize beta_at_exists (ac)
  18. 0018specialize beta_at_exists (i)
  19. 0019apply beta_at_exists
  20. 0020cases hchosen0
  21. 0021have hchosen1 : ∃ v. BetaAt(db,dc,i,v)
  22. 0022specialize beta_at_exists (db)
  23. 0023specialize beta_at_exists (dc)
  24. 0024specialize beta_at_exists (i)
  25. 0025apply beta_at_exists
  26. 0026cases hchosen1
  27. 0027have heq : r=x1
  28. 0028specialize prime_field_negate_functional (p)
  29. 0029specialize prime_field_negate_functional (x)
  30. 0030specialize prime_field_negate_functional (r)
  31. 0031specialize prime_field_negate_functional (x1)
  32. 0032apply prime_field_negate_functional
  33. 0033specialize prime_field_polynomial_negate_entry (p)
  34. 0034specialize prime_field_polynomial_negate_entry (ab)
  35. 0035specialize prime_field_polynomial_negate_entry (ac)
  36. 0036specialize prime_field_polynomial_negate_entry (rb)
  37. 0037specialize prime_field_polynomial_negate_entry (rc)
  38. 0038specialize prime_field_polynomial_negate_entry (l)
  39. 0039specialize prime_field_polynomial_negate_entry (i)
  40. 0040specialize prime_field_polynomial_negate_entry (x)
  41. 0041specialize prime_field_polynomial_negate_entry (r)
  42. 0042apply prime_field_polynomial_negate_entry
  43. 0043exact hfirst
  44. 0044exact hi
  45. 0045exact hchosen0_witness
  46. 0046exact hr
  47. 0047specialize prime_field_polynomial_negate_entry (p)
  48. 0048specialize prime_field_polynomial_negate_entry (ab)
  49. 0049specialize prime_field_polynomial_negate_entry (ac)
  50. 0050specialize prime_field_polynomial_negate_entry (db)
  51. 0051specialize prime_field_polynomial_negate_entry (dc)
  52. 0052specialize prime_field_polynomial_negate_entry (l)
  53. 0053specialize prime_field_polynomial_negate_entry (i)
  54. 0054specialize prime_field_polynomial_negate_entry (x)
  55. 0055specialize prime_field_polynomial_negate_entry (x1)
  56. 0056apply prime_field_polynomial_negate_entry
  57. 0057exact hsecond
  58. 0058exact hi
  59. 0059exact hchosen0_witness
  60. 0060exact hchosen1_witness
  61. 0061rewrite heq
  62. 0062rewrite heq
  63. 0063exact hchosen1_witness