PQ001A

prime_field_polynomial_subtract_common_right_cancel

Two actual differences with the same subtrahend and result have equal represented minuend coefficients.

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. ∀ cb. ∀ cc. ∀ rb. ∀ rc. ∀ l. FpCoefficientSubtraction(p,ab,ac,cb,cc,rb,rc,l) → FpCoefficientSubtraction(p,bb,bc,cb,cc,rb,rc,l) → ∀ x. ∀ y. Lt(x,l) → BetaAt(ab,ac,x,y) → BetaAt(bb,bc,x,y)

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

Definition DAG

FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 2Lt(a,b) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

prime_field_polynomial_add_functional · checked external prerequisiteprime_field_polynomial_subtract_recover_add
Original expanded first-order statement 
forall p ab ac bb bc cb cc rb rc l. (forall pfs_index_sub_cancel_right_first. (exists pfa_gap_sub_cancel_right_firstindex. pfa_gap_sub_cancel_right_firstindex + S (pfs_index_sub_cancel_right_first) = (l)) -> exists pfs_left_sub_cancel_right_first pfs_right_sub_cancel_right_first pfs_result_sub_cancel_right_first. ((((exists ff_h_pfp_sub_cancel_right_firstleft. ff_h_pfp_sub_cancel_right_firstleft + S (pfs_left_sub_cancel_right_first) = S ((S (pfs_index_sub_cancel_right_first)) * ac)) /\ exists ff_q_pfp_sub_cancel_right_firstleft. ab = ff_q_pfp_sub_cancel_right_firstleft * S ((S (pfs_index_sub_cancel_right_first)) * ac) + (pfs_left_sub_cancel_right_first))) /\ (((((exists ff_h_pfp_sub_cancel_right_firstright. ff_h_pfp_sub_cancel_right_firstright + S (pfs_right_sub_cancel_right_first) = S ((S (pfs_index_sub_cancel_right_first)) * cc)) /\ exists ff_q_pfp_sub_cancel_right_firstright. cb = ff_q_pfp_sub_cancel_right_firstright * S ((S (pfs_index_sub_cancel_right_first)) * cc) + (pfs_right_sub_cancel_right_first))) /\ (((((exists ff_h_pfp_sub_cancel_right_firstresult. ff_h_pfp_sub_cancel_right_firstresult + S (pfs_result_sub_cancel_right_first) = S ((S (pfs_index_sub_cancel_right_first)) * rc)) /\ exists ff_q_pfp_sub_cancel_right_firstresult. rb = ff_q_pfp_sub_cancel_right_firstresult * S ((S (pfs_index_sub_cancel_right_first)) * rc) + (pfs_result_sub_cancel_right_first))) /\ ((((exists pfa_gap_sub_cancel_right_firstoperationleft. pfa_gap_sub_cancel_right_firstoperationleft + S (pfs_right_sub_cancel_right_first) = (p)) /\ (((exists pfa_gap_sub_cancel_right_firstoperationright. pfa_gap_sub_cancel_right_firstoperationright + S (pfs_result_sub_cancel_right_first) = (p)) /\ ((((exists pfa_gap_sub_cancel_right_firstoperationresultbound. pfa_gap_sub_cancel_right_firstoperationresultbound + S (pfs_left_sub_cancel_right_first) = (p)) /\ ((exists pfa_offset_left_sub_cancel_right_firstoperationresultcongruence pfa_offset_right_sub_cancel_right_firstoperationresultcongruence. ((pfs_right_sub_cancel_right_first) + (pfs_result_sub_cancel_right_first)) + (p) * pfa_offset_left_sub_cancel_right_firstoperationresultcongruence = (pfs_left_sub_cancel_right_first) + (p) * pfa_offset_right_sub_cancel_right_firstoperationresultcongruence)))))))))))))))) -> (forall pfs_index_sub_cancel_right_second. (exists pfa_gap_sub_cancel_right_secondindex. pfa_gap_sub_cancel_right_secondindex + S (pfs_index_sub_cancel_right_second) = (l)) -> exists pfs_left_sub_cancel_right_second pfs_right_sub_cancel_right_second pfs_result_sub_cancel_right_second. ((((exists ff_h_pfp_sub_cancel_right_secondleft. ff_h_pfp_sub_cancel_right_secondleft + S (pfs_left_sub_cancel_right_second) = S ((S (pfs_index_sub_cancel_right_second)) * bc)) /\ exists ff_q_pfp_sub_cancel_right_secondleft. bb = ff_q_pfp_sub_cancel_right_secondleft * S ((S (pfs_index_sub_cancel_right_second)) * bc) + (pfs_left_sub_cancel_right_second))) /\ (((((exists ff_h_pfp_sub_cancel_right_secondright. ff_h_pfp_sub_cancel_right_secondright + S (pfs_right_sub_cancel_right_second) = S ((S (pfs_index_sub_cancel_right_second)) * cc)) /\ exists ff_q_pfp_sub_cancel_right_secondright. cb = ff_q_pfp_sub_cancel_right_secondright * S ((S (pfs_index_sub_cancel_right_second)) * cc) + (pfs_right_sub_cancel_right_second))) /\ (((((exists ff_h_pfp_sub_cancel_right_secondresult. ff_h_pfp_sub_cancel_right_secondresult + S (pfs_result_sub_cancel_right_second) = S ((S (pfs_index_sub_cancel_right_second)) * rc)) /\ exists ff_q_pfp_sub_cancel_right_secondresult. rb = ff_q_pfp_sub_cancel_right_secondresult * S ((S (pfs_index_sub_cancel_right_second)) * rc) + (pfs_result_sub_cancel_right_second))) /\ ((((exists pfa_gap_sub_cancel_right_secondoperationleft. pfa_gap_sub_cancel_right_secondoperationleft + S (pfs_right_sub_cancel_right_second) = (p)) /\ (((exists pfa_gap_sub_cancel_right_secondoperationright. pfa_gap_sub_cancel_right_secondoperationright + S (pfs_result_sub_cancel_right_second) = (p)) /\ ((((exists pfa_gap_sub_cancel_right_secondoperationresultbound. pfa_gap_sub_cancel_right_secondoperationresultbound + S (pfs_left_sub_cancel_right_second) = (p)) /\ ((exists pfa_offset_left_sub_cancel_right_secondoperationresultcongruence pfa_offset_right_sub_cancel_right_secondoperationresultcongruence. ((pfs_right_sub_cancel_right_second) + (pfs_result_sub_cancel_right_second)) + (p) * pfa_offset_left_sub_cancel_right_secondoperationresultcongruence = (pfs_left_sub_cancel_right_second) + (p) * pfa_offset_right_sub_cancel_right_secondoperationresultcongruence)))))))))))))))) -> (forall mdr_i_pfp_sub_cancel_right_result mdr_a_pfp_sub_cancel_right_result. (exists mdr_gap_pfp_sub_cancel_right_resultb. mdr_gap_pfp_sub_cancel_right_resultb + S (mdr_i_pfp_sub_cancel_right_result) = (l)) -> (((exists ff_h_mdr_pfp_sub_cancel_right_resulto. ff_h_mdr_pfp_sub_cancel_right_resulto + S (mdr_a_pfp_sub_cancel_right_result) = S ((S (mdr_i_pfp_sub_cancel_right_result)) * ac)) /\ exists ff_q_mdr_pfp_sub_cancel_right_resulto. ab = ff_q_mdr_pfp_sub_cancel_right_resulto * S ((S (mdr_i_pfp_sub_cancel_right_result)) * ac) + (mdr_a_pfp_sub_cancel_right_result))) -> (((exists ff_h_mdr_pfp_sub_cancel_right_resultn. ff_h_mdr_pfp_sub_cancel_right_resultn + S (mdr_a_pfp_sub_cancel_right_result) = S ((S (mdr_i_pfp_sub_cancel_right_result)) * bc)) /\ exists ff_q_mdr_pfp_sub_cancel_right_resultn. bb = ff_q_mdr_pfp_sub_cancel_right_resultn * S ((S (mdr_i_pfp_sub_cancel_right_result)) * bc) + (mdr_a_pfp_sub_cancel_right_result))))

Complete tactic proof in conservative notation

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

43 script commands · 6 reading checkpoints · 0 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 subtract recover add
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 bb
  5. L5
    intro bc
  6. L6
    intro cb
  7. L7
    intro cc
  8. L8
    intro rb
  9. L9
    intro rc
  10. L10
    intro l
02Fix variables and assumptionsL11–12

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

  1. L11
    intro ha
  2. L12
    intro hb
03Use earlier factsL13–22

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

  1. L13
    specialize prime_field_polynomial_add_functional (p)
  2. L14
    specialize prime_field_polynomial_add_functional (cb)
  3. L15
    specialize prime_field_polynomial_add_functional (cc)
  4. L16
    specialize prime_field_polynomial_add_functional (rb)
  5. L17
    specialize prime_field_polynomial_add_functional (rc)
  6. L18
    specialize prime_field_polynomial_add_functional (ab)
  7. L19
    specialize prime_field_polynomial_add_functional (ac)
  8. L20
    specialize prime_field_polynomial_add_functional (bb)
  9. L21
    specialize prime_field_polynomial_add_functional (bc)
  10. L22
    specialize prime_field_polynomial_add_functional (l)
04Use earlier factsL23–32

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

  1. L23
    apply prime_field_polynomial_add_functional
  2. L24
    specialize prime_field_polynomial_subtract_recover_add (p)
  3. L25
    specialize prime_field_polynomial_subtract_recover_add (ab)
  4. L26
    specialize prime_field_polynomial_subtract_recover_add (ac)
  5. L27
    specialize prime_field_polynomial_subtract_recover_add (cb)
  6. L28
    specialize prime_field_polynomial_subtract_recover_add (cc)
  7. L29
    specialize prime_field_polynomial_subtract_recover_add (rb)
  8. L30
    specialize prime_field_polynomial_subtract_recover_add (rc)
  9. L31
    specialize prime_field_polynomial_subtract_recover_add (l)
  10. L32
    apply prime_field_polynomial_subtract_recover_add
05Use earlier factsL33–42

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

  1. L33
    exact ha
  2. L34
    specialize prime_field_polynomial_subtract_recover_add (p)
  3. L35
    specialize prime_field_polynomial_subtract_recover_add (bb)
  4. L36
    specialize prime_field_polynomial_subtract_recover_add (bc)
  5. L37
    specialize prime_field_polynomial_subtract_recover_add (cb)
  6. L38
    specialize prime_field_polynomial_subtract_recover_add (cc)
  7. L39
    specialize prime_field_polynomial_subtract_recover_add (rb)
  8. L40
    specialize prime_field_polynomial_subtract_recover_add (rc)
  9. L41
    specialize prime_field_polynomial_subtract_recover_add (l)
  10. L42
    apply prime_field_polynomial_subtract_recover_add
06Use earlier factsL43–43

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

  1. L43
    exact hb

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro cb
  7. 0007intro cc
  8. 0008intro rb
  9. 0009intro rc
  10. 0010intro l
  11. 0011intro ha
  12. 0012intro hb
  13. 0013specialize prime_field_polynomial_add_functional (p)
  14. 0014specialize prime_field_polynomial_add_functional (cb)
  15. 0015specialize prime_field_polynomial_add_functional (cc)
  16. 0016specialize prime_field_polynomial_add_functional (rb)
  17. 0017specialize prime_field_polynomial_add_functional (rc)
  18. 0018specialize prime_field_polynomial_add_functional (ab)
  19. 0019specialize prime_field_polynomial_add_functional (ac)
  20. 0020specialize prime_field_polynomial_add_functional (bb)
  21. 0021specialize prime_field_polynomial_add_functional (bc)
  22. 0022specialize prime_field_polynomial_add_functional (l)
  23. 0023apply prime_field_polynomial_add_functional
  24. 0024specialize prime_field_polynomial_subtract_recover_add (p)
  25. 0025specialize prime_field_polynomial_subtract_recover_add (ab)
  26. 0026specialize prime_field_polynomial_subtract_recover_add (ac)
  27. 0027specialize prime_field_polynomial_subtract_recover_add (cb)
  28. 0028specialize prime_field_polynomial_subtract_recover_add (cc)
  29. 0029specialize prime_field_polynomial_subtract_recover_add (rb)
  30. 0030specialize prime_field_polynomial_subtract_recover_add (rc)
  31. 0031specialize prime_field_polynomial_subtract_recover_add (l)
  32. 0032apply prime_field_polynomial_subtract_recover_add
  33. 0033exact ha
  34. 0034specialize prime_field_polynomial_subtract_recover_add (p)
  35. 0035specialize prime_field_polynomial_subtract_recover_add (bb)
  36. 0036specialize prime_field_polynomial_subtract_recover_add (bc)
  37. 0037specialize prime_field_polynomial_subtract_recover_add (cb)
  38. 0038specialize prime_field_polynomial_subtract_recover_add (cc)
  39. 0039specialize prime_field_polynomial_subtract_recover_add (rb)
  40. 0040specialize prime_field_polynomial_subtract_recover_add (rc)
  41. 0041specialize prime_field_polynomial_subtract_recover_add (l)
  42. 0042apply prime_field_polynomial_subtract_recover_add
  43. 0043exact hb