PQ0016

prime_field_polynomial_subtract_zero_left

Subtracting an actual canonical prefix from zero yields its actual coefficientwise additive inverse.

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. ∀ bb. ∀ bc. ∀ rb. ∀ rc. ∀ zb. ∀ zc. ∀ l. FpCoefficientNegation(p,bb,bc,rb,rc,l) → Repeat(zb,zc,0,l) → FpCoefficientSubtraction(p,zb,zc,bb,bc,rb,rc,l)

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

Definition DAG

FpCoefficientNegation(p,ab,ac,rb,rc,L) · 1FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 1Repeat(b,c,a,l) · 1

Actual proof prerequisites

prime_field_polynomial_subtract_from_addprime_field_polynomial_negate_add_zero
Original expanded first-order statement 
forall p bb bc rb rc zb zc l. (forall pfs_index_sub_zero_left_neg. (exists pfa_gap_sub_zero_left_negindex. pfa_gap_sub_zero_left_negindex + S (pfs_index_sub_zero_left_neg) = (l)) -> exists pfs_source_sub_zero_left_neg pfs_result_sub_zero_left_neg. ((((exists ff_h_pfp_sub_zero_left_negsource. ff_h_pfp_sub_zero_left_negsource + S (pfs_source_sub_zero_left_neg) = S ((S (pfs_index_sub_zero_left_neg)) * bc)) /\ exists ff_q_pfp_sub_zero_left_negsource. bb = ff_q_pfp_sub_zero_left_negsource * S ((S (pfs_index_sub_zero_left_neg)) * bc) + (pfs_source_sub_zero_left_neg))) /\ (((((exists ff_h_pfp_sub_zero_left_negresult. ff_h_pfp_sub_zero_left_negresult + S (pfs_result_sub_zero_left_neg) = S ((S (pfs_index_sub_zero_left_neg)) * rc)) /\ exists ff_q_pfp_sub_zero_left_negresult. rb = ff_q_pfp_sub_zero_left_negresult * S ((S (pfs_index_sub_zero_left_neg)) * rc) + (pfs_result_sub_zero_left_neg))) /\ ((((exists pfa_gap_sub_zero_left_negoperationadditionleft. pfa_gap_sub_zero_left_negoperationadditionleft + S (pfs_source_sub_zero_left_neg) = (p)) /\ (((exists pfa_gap_sub_zero_left_negoperationadditionright. pfa_gap_sub_zero_left_negoperationadditionright + S (pfs_result_sub_zero_left_neg) = (p)) /\ ((((exists pfa_gap_sub_zero_left_negoperationadditionresultbound. pfa_gap_sub_zero_left_negoperationadditionresultbound + S (0) = (p)) /\ ((exists pfa_offset_left_sub_zero_left_negoperationadditionresultcongruence pfa_offset_right_sub_zero_left_negoperationadditionresultcongruence. ((pfs_source_sub_zero_left_neg) + (pfs_result_sub_zero_left_neg)) + (p) * pfa_offset_left_sub_zero_left_negoperationadditionresultcongruence = (0) + (p) * pfa_offset_right_sub_zero_left_negoperationadditionresultcongruence)))))))))))))) -> (forall pfp_repeat_index_sub_zero_left_zero. (exists pfa_gap_sub_zero_left_zeroindex. pfa_gap_sub_zero_left_zeroindex + S (pfp_repeat_index_sub_zero_left_zero) = (l)) -> (((exists ff_h_pfp_sub_zero_left_zeroentry. ff_h_pfp_sub_zero_left_zeroentry + S (0) = S ((S (pfp_repeat_index_sub_zero_left_zero)) * zc)) /\ exists ff_q_pfp_sub_zero_left_zeroentry. zb = ff_q_pfp_sub_zero_left_zeroentry * S ((S (pfp_repeat_index_sub_zero_left_zero)) * zc) + (0)))) -> (forall pfs_index_sub_zero_left_result. (exists pfa_gap_sub_zero_left_resultindex. pfa_gap_sub_zero_left_resultindex + S (pfs_index_sub_zero_left_result) = (l)) -> exists pfs_left_sub_zero_left_result pfs_right_sub_zero_left_result pfs_result_sub_zero_left_result. ((((exists ff_h_pfp_sub_zero_left_resultleft. ff_h_pfp_sub_zero_left_resultleft + S (pfs_left_sub_zero_left_result) = S ((S (pfs_index_sub_zero_left_result)) * zc)) /\ exists ff_q_pfp_sub_zero_left_resultleft. zb = ff_q_pfp_sub_zero_left_resultleft * S ((S (pfs_index_sub_zero_left_result)) * zc) + (pfs_left_sub_zero_left_result))) /\ (((((exists ff_h_pfp_sub_zero_left_resultright. ff_h_pfp_sub_zero_left_resultright + S (pfs_right_sub_zero_left_result) = S ((S (pfs_index_sub_zero_left_result)) * bc)) /\ exists ff_q_pfp_sub_zero_left_resultright. bb = ff_q_pfp_sub_zero_left_resultright * S ((S (pfs_index_sub_zero_left_result)) * bc) + (pfs_right_sub_zero_left_result))) /\ (((((exists ff_h_pfp_sub_zero_left_resultresult. ff_h_pfp_sub_zero_left_resultresult + S (pfs_result_sub_zero_left_result) = S ((S (pfs_index_sub_zero_left_result)) * rc)) /\ exists ff_q_pfp_sub_zero_left_resultresult. rb = ff_q_pfp_sub_zero_left_resultresult * S ((S (pfs_index_sub_zero_left_result)) * rc) + (pfs_result_sub_zero_left_result))) /\ ((((exists pfa_gap_sub_zero_left_resultoperationleft. pfa_gap_sub_zero_left_resultoperationleft + S (pfs_right_sub_zero_left_result) = (p)) /\ (((exists pfa_gap_sub_zero_left_resultoperationright. pfa_gap_sub_zero_left_resultoperationright + S (pfs_result_sub_zero_left_result) = (p)) /\ ((((exists pfa_gap_sub_zero_left_resultoperationresultbound. pfa_gap_sub_zero_left_resultoperationresultbound + S (pfs_left_sub_zero_left_result) = (p)) /\ ((exists pfa_offset_left_sub_zero_left_resultoperationresultcongruence pfa_offset_right_sub_zero_left_resultoperationresultcongruence. ((pfs_right_sub_zero_left_result) + (pfs_result_sub_zero_left_result)) + (p) * pfa_offset_left_sub_zero_left_resultoperationresultcongruence = (pfs_left_sub_zero_left_result) + (p) * pfa_offset_right_sub_zero_left_resultoperationresultcongruence))))))))))))))))

Complete tactic proof in conservative notation

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

30 script commands · 3 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 (2)
prime field polynomial subtract from addprime field polynomial negate add zero
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro bb
  3. L3
    intro bc
  4. L4
    intro rb
  5. L5
    intro rc
  6. L6
    intro zb
  7. L7
    intro zc
  8. L8
    intro l
  9. L9
    intro hn
  10. L10
    intro hz
02Use earlier factsL11–20

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

  1. L11
    specialize prime_field_polynomial_subtract_from_add (p)
  2. L12
    specialize prime_field_polynomial_subtract_from_add (zb)
  3. L13
    specialize prime_field_polynomial_subtract_from_add (zc)
  4. L14
    specialize prime_field_polynomial_subtract_from_add (bb)
  5. L15
    specialize prime_field_polynomial_subtract_from_add (bc)
  6. L16
    specialize prime_field_polynomial_subtract_from_add (rb)
  7. L17
    specialize prime_field_polynomial_subtract_from_add (rc)
  8. L18
    specialize prime_field_polynomial_subtract_from_add (l)
  9. L19
    apply prime_field_polynomial_subtract_from_add
  10. L20
    specialize prime_field_polynomial_negate_add_zero (p)
03Use earlier factsL21–30

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

  1. L21
    specialize prime_field_polynomial_negate_add_zero (bb)
  2. L22
    specialize prime_field_polynomial_negate_add_zero (bc)
  3. L23
    specialize prime_field_polynomial_negate_add_zero (rb)
  4. L24
    specialize prime_field_polynomial_negate_add_zero (rc)
  5. L25
    specialize prime_field_polynomial_negate_add_zero (zb)
  6. L26
    specialize prime_field_polynomial_negate_add_zero (zc)
  7. L27
    specialize prime_field_polynomial_negate_add_zero (l)
  8. L28
    apply prime_field_polynomial_negate_add_zero
  9. L29
    exact hn
  10. L30
    exact hz

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro p
  2. 0002intro bb
  3. 0003intro bc
  4. 0004intro rb
  5. 0005intro rc
  6. 0006intro zb
  7. 0007intro zc
  8. 0008intro l
  9. 0009intro hn
  10. 0010intro hz
  11. 0011specialize prime_field_polynomial_subtract_from_add (p)
  12. 0012specialize prime_field_polynomial_subtract_from_add (zb)
  13. 0013specialize prime_field_polynomial_subtract_from_add (zc)
  14. 0014specialize prime_field_polynomial_subtract_from_add (bb)
  15. 0015specialize prime_field_polynomial_subtract_from_add (bc)
  16. 0016specialize prime_field_polynomial_subtract_from_add (rb)
  17. 0017specialize prime_field_polynomial_subtract_from_add (rc)
  18. 0018specialize prime_field_polynomial_subtract_from_add (l)
  19. 0019apply prime_field_polynomial_subtract_from_add
  20. 0020specialize prime_field_polynomial_negate_add_zero (p)
  21. 0021specialize prime_field_polynomial_negate_add_zero (bb)
  22. 0022specialize prime_field_polynomial_negate_add_zero (bc)
  23. 0023specialize prime_field_polynomial_negate_add_zero (rb)
  24. 0024specialize prime_field_polynomial_negate_add_zero (rc)
  25. 0025specialize prime_field_polynomial_negate_add_zero (zb)
  26. 0026specialize prime_field_polynomial_negate_add_zero (zc)
  27. 0027specialize prime_field_polynomial_negate_add_zero (l)
  28. 0028apply prime_field_polynomial_negate_add_zero
  29. 0029exact hn
  30. 0030exact hz