PQ0016

prime_field_polynomial_subtract_zero_left

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

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

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 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))))))))))))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 2 declared prerequisites and contains 30 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PQ0013 prime_field_polynomial_subtract_from_add PQ000B prime_field_polynomial_negate_add_zero

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

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.

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 exact 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