PQ0006

prime_field_polynomial_negate_bounded

The actual operation graph itself forces every source and result coefficient to be canonical.

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

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

Definition DAG

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

Actual proof prerequisites

none
Original expanded first-order statement 
forall p ab ac rb rc l. (forall pfs_index_negate_bounded_graph. (exists pfa_gap_negate_bounded_graphindex. pfa_gap_negate_bounded_graphindex + S (pfs_index_negate_bounded_graph) = (l)) -> exists pfs_source_negate_bounded_graph pfs_result_negate_bounded_graph. ((((exists ff_h_pfp_negate_bounded_graphsource. ff_h_pfp_negate_bounded_graphsource + S (pfs_source_negate_bounded_graph) = S ((S (pfs_index_negate_bounded_graph)) * ac)) /\ exists ff_q_pfp_negate_bounded_graphsource. ab = ff_q_pfp_negate_bounded_graphsource * S ((S (pfs_index_negate_bounded_graph)) * ac) + (pfs_source_negate_bounded_graph))) /\ (((((exists ff_h_pfp_negate_bounded_graphresult. ff_h_pfp_negate_bounded_graphresult + S (pfs_result_negate_bounded_graph) = S ((S (pfs_index_negate_bounded_graph)) * rc)) /\ exists ff_q_pfp_negate_bounded_graphresult. rb = ff_q_pfp_negate_bounded_graphresult * S ((S (pfs_index_negate_bounded_graph)) * rc) + (pfs_result_negate_bounded_graph))) /\ ((((exists pfa_gap_negate_bounded_graphoperationadditionleft. pfa_gap_negate_bounded_graphoperationadditionleft + S (pfs_source_negate_bounded_graph) = (p)) /\ (((exists pfa_gap_negate_bounded_graphoperationadditionright. pfa_gap_negate_bounded_graphoperationadditionright + S (pfs_result_negate_bounded_graph) = (p)) /\ ((((exists pfa_gap_negate_bounded_graphoperationadditionresultbound. pfa_gap_negate_bounded_graphoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_negate_bounded_graphoperationadditionresultcongruence pfa_offset_right_negate_bounded_graphoperationadditionresultcongruence. ((pfs_source_negate_bounded_graph) + (pfs_result_negate_bounded_graph)) + (p) * pfa_offset_left_negate_bounded_graphoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_negate_bounded_graphoperationadditionresultcongruence)))))))))))))) -> ((forall fom_index_pfp_negate_bounded_ab. (exists fom_gap_pfp_negate_bounded_ab_index_bound. fom_gap_pfp_negate_bounded_ab_index_bound + S (fom_index_pfp_negate_bounded_ab) = l) -> exists fom_value_pfp_negate_bounded_ab. ((((exists fom_beta_height_pfp_negate_bounded_ab_entry. fom_beta_height_pfp_negate_bounded_ab_entry + S (fom_value_pfp_negate_bounded_ab) = S ((S (fom_index_pfp_negate_bounded_ab)) * ac)) /\ exists fom_beta_quotient_pfp_negate_bounded_ab_entry. ab = fom_beta_quotient_pfp_negate_bounded_ab_entry * S ((S (fom_index_pfp_negate_bounded_ab)) * ac) + (fom_value_pfp_negate_bounded_ab))) /\ (exists fom_gap_pfp_negate_bounded_ab_value_bound. fom_gap_pfp_negate_bounded_ab_value_bound + S (fom_value_pfp_negate_bounded_ab) = p))) /\ ((forall fom_index_pfp_negate_bounded_rb. (exists fom_gap_pfp_negate_bounded_rb_index_bound. fom_gap_pfp_negate_bounded_rb_index_bound + S (fom_index_pfp_negate_bounded_rb) = l) -> exists fom_value_pfp_negate_bounded_rb. ((((exists fom_beta_height_pfp_negate_bounded_rb_entry. fom_beta_height_pfp_negate_bounded_rb_entry + S (fom_value_pfp_negate_bounded_rb) = S ((S (fom_index_pfp_negate_bounded_rb)) * rc)) /\ exists fom_beta_quotient_pfp_negate_bounded_rb_entry. rb = fom_beta_quotient_pfp_negate_bounded_rb_entry * S ((S (fom_index_pfp_negate_bounded_rb)) * rc) + (fom_value_pfp_negate_bounded_rb))) /\ (exists fom_gap_pfp_negate_bounded_rb_value_bound. fom_gap_pfp_negate_bounded_rb_value_bound + S (fom_value_pfp_negate_bounded_rb) = p)))))

Complete tactic proof in conservative notation

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

42 script commands · 14 reading checkpoints · 2 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.

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 rb
  5. L5
    intro rc
  6. L6
    intro l
  7. L7
    intro h
02Separate the logical casesL8–8

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

  1. L8
    split
03Fix variables and assumptionsL9–10

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

  1. L9
    intro i
  2. L10
    intro hi
04Establish hvL11–14

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

  1. L11
    have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,a,r,0))Definitions: BetaAt(ab,ac,i,a)BetaAt(rb,rc,i,r)FpAdd(p,a,r,0)Original native command in the exact edition
  2. L12
    specialize h (i)
  3. L13
    apply h
  4. L14
    exact hi
05Separate the logical casesL15–21

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

  1. L15
    cases hv
  2. L16
    cases hv_witness
  3. L17
    cases hv_witness_witness
  4. L18
    cases hv_witness_witness_right
  5. L19
    cases hv_witness_witness_right_right
  6. L20
    cases hv_witness_witness_right_right_right
  7. L21
    cases hv_witness_witness_right_right_right_right
06Construct an explicit witnessL22–22

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

  1. L22
    exists x
07Separate the logical casesL23–23

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

  1. L23
    split
08Use earlier factsL24–25

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

  1. L24
    exact hv_witness_witness_left
  2. L25
    exact hv_witness_witness_right_right_left
09Fix variables and assumptionsL26–27

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

  1. L26
    intro i
  2. L27
    intro hi
10Establish hvL28–31

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

  1. L28
    have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,a,r,0))Definitions: BetaAt(ab,ac,i,a)BetaAt(rb,rc,i,r)FpAdd(p,a,r,0)Original native command in the exact edition
  2. L29
    specialize h (i)
  3. L30
    apply h
  4. L31
    exact hi
11Separate the logical casesL32–38

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

  1. L32
    cases hv
  2. L33
    cases hv_witness
  3. L34
    cases hv_witness_witness
  4. L35
    cases hv_witness_witness_right
  5. L36
    cases hv_witness_witness_right_right
  6. L37
    cases hv_witness_witness_right_right_right
  7. L38
    cases hv_witness_witness_right_right_right_right
12Construct an explicit witnessL39–39

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

  1. L39
    exists x1
13Separate the logical casesL40–40

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

  1. L40
    split
14Use earlier factsL41–42

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

  1. L41
    exact hv_witness_witness_right_left
  2. L42
    exact hv_witness_witness_right_right_right_left

Library-wide reading audit

Original defined command ledger · 42 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro l
  7. 0007intro h
  8. 0008split
  9. 0009intro i
  10. 0010intro hi
  11. 0011have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,a,r,0))
  12. 0012specialize h (i)
  13. 0013apply h
  14. 0014exact hi
  15. 0015cases hv
  16. 0016cases hv_witness
  17. 0017cases hv_witness_witness
  18. 0018cases hv_witness_witness_right
  19. 0019cases hv_witness_witness_right_right
  20. 0020cases hv_witness_witness_right_right_right
  21. 0021cases hv_witness_witness_right_right_right_right
  22. 0022exists x
  23. 0023split
  24. 0024exact hv_witness_witness_left
  25. 0025exact hv_witness_witness_right_right_left
  26. 0026intro i
  27. 0027intro hi
  28. 0028have hv : ∃ a. ∃ r. BetaAt(ab,ac,i,a) ∧ (BetaAt(rb,rc,i,r) ∧ FpAdd(p,a,r,0))
  29. 0029specialize h (i)
  30. 0030apply h
  31. 0031exact hi
  32. 0032cases hv
  33. 0033cases hv_witness
  34. 0034cases hv_witness_witness
  35. 0035cases hv_witness_witness_right
  36. 0036cases hv_witness_witness_right_right
  37. 0037cases hv_witness_witness_right_right_right
  38. 0038cases hv_witness_witness_right_right_right_right
  39. 0039exists x1
  40. 0040split
  41. 0041exact hv_witness_witness_right_left
  42. 0042exact hv_witness_witness_right_right_right_left