PG0044

prime_field_polynomial_aligned_subtract_from_fixed

A genuine fixed-length subtraction is an aligned subtraction because its actual coefficient graph supplies B+R=A.

Alpha v34 checked-use · first admitted v34 · 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 products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ rb. ∀ rc. ∀ K. FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,K) → FpPolynomialAlignedAdd(p,bb,bc,K,rb,rc,K,ab,ac,K)

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

Definition DAG

FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 1FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N) · 1

Actual proof prerequisites

prime_field_polynomial_aligned_add_from_fixedprime_field_polynomial_subtract_recover_add · checked external prerequisite
Original expanded first-order statement 
forall p ab ac bb bc rb rc K. (forall pfs_index_sub_fixed_input. (exists pfa_gap_sub_fixed_inputindex. pfa_gap_sub_fixed_inputindex + S (pfs_index_sub_fixed_input) = (K)) -> exists pfs_left_sub_fixed_input pfs_right_sub_fixed_input pfs_result_sub_fixed_input. ((((exists ff_h_pfp_sub_fixed_inputleft. ff_h_pfp_sub_fixed_inputleft + S (pfs_left_sub_fixed_input) = S ((S (pfs_index_sub_fixed_input)) * ac)) /\ exists ff_q_pfp_sub_fixed_inputleft. ab = ff_q_pfp_sub_fixed_inputleft * S ((S (pfs_index_sub_fixed_input)) * ac) + (pfs_left_sub_fixed_input))) /\ (((((exists ff_h_pfp_sub_fixed_inputright. ff_h_pfp_sub_fixed_inputright + S (pfs_right_sub_fixed_input) = S ((S (pfs_index_sub_fixed_input)) * bc)) /\ exists ff_q_pfp_sub_fixed_inputright. bb = ff_q_pfp_sub_fixed_inputright * S ((S (pfs_index_sub_fixed_input)) * bc) + (pfs_right_sub_fixed_input))) /\ (((((exists ff_h_pfp_sub_fixed_inputresult. ff_h_pfp_sub_fixed_inputresult + S (pfs_result_sub_fixed_input) = S ((S (pfs_index_sub_fixed_input)) * rc)) /\ exists ff_q_pfp_sub_fixed_inputresult. rb = ff_q_pfp_sub_fixed_inputresult * S ((S (pfs_index_sub_fixed_input)) * rc) + (pfs_result_sub_fixed_input))) /\ ((((exists pfa_gap_sub_fixed_inputoperationleft. pfa_gap_sub_fixed_inputoperationleft + S (pfs_right_sub_fixed_input) = (p)) /\ (((exists pfa_gap_sub_fixed_inputoperationright. pfa_gap_sub_fixed_inputoperationright + S (pfs_result_sub_fixed_input) = (p)) /\ ((((exists pfa_gap_sub_fixed_inputoperationresultbound. pfa_gap_sub_fixed_inputoperationresultbound + S (pfs_left_sub_fixed_input) = (p)) /\ ((exists pfa_offset_left_sub_fixed_inputoperationresultcongruence pfa_offset_right_sub_fixed_inputoperationresultcongruence. ((pfs_right_sub_fixed_input) + (pfs_result_sub_fixed_input)) + (p) * pfa_offset_left_sub_fixed_inputoperationresultcongruence = (pfs_left_sub_fixed_input) + (p) * pfa_offset_right_sub_fixed_inputoperationresultcongruence)))))))))))))))) -> (((forall fom_index_pfp_sub_fixed_result_left_bounded. (exists fom_gap_pfp_sub_fixed_result_left_bounded_index_bound. fom_gap_pfp_sub_fixed_result_left_bounded_index_bound + S (fom_index_pfp_sub_fixed_result_left_bounded) = K) -> exists fom_value_pfp_sub_fixed_result_left_bounded. ((((exists fom_beta_height_pfp_sub_fixed_result_left_bounded_entry. fom_beta_height_pfp_sub_fixed_result_left_bounded_entry + S (fom_value_pfp_sub_fixed_result_left_bounded) = S ((S (fom_index_pfp_sub_fixed_result_left_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_sub_fixed_result_left_bounded_entry. bb = fom_beta_quotient_pfp_sub_fixed_result_left_bounded_entry * S ((S (fom_index_pfp_sub_fixed_result_left_bounded)) * bc) + (fom_value_pfp_sub_fixed_result_left_bounded))) /\ (exists fom_gap_pfp_sub_fixed_result_left_bounded_value_bound. fom_gap_pfp_sub_fixed_result_left_bounded_value_bound + S (fom_value_pfp_sub_fixed_result_left_bounded) = p))) /\ (((forall fom_index_pfp_sub_fixed_result_right_bounded. (exists fom_gap_pfp_sub_fixed_result_right_bounded_index_bound. fom_gap_pfp_sub_fixed_result_right_bounded_index_bound + S (fom_index_pfp_sub_fixed_result_right_bounded) = K) -> exists fom_value_pfp_sub_fixed_result_right_bounded. ((((exists fom_beta_height_pfp_sub_fixed_result_right_bounded_entry. fom_beta_height_pfp_sub_fixed_result_right_bounded_entry + S (fom_value_pfp_sub_fixed_result_right_bounded) = S ((S (fom_index_pfp_sub_fixed_result_right_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_sub_fixed_result_right_bounded_entry. rb = fom_beta_quotient_pfp_sub_fixed_result_right_bounded_entry * S ((S (fom_index_pfp_sub_fixed_result_right_bounded)) * rc) + (fom_value_pfp_sub_fixed_result_right_bounded))) /\ (exists fom_gap_pfp_sub_fixed_result_right_bounded_value_bound. fom_gap_pfp_sub_fixed_result_right_bounded_value_bound + S (fom_value_pfp_sub_fixed_result_right_bounded) = p))) /\ (((forall fom_index_pfp_sub_fixed_result_result_bounded. (exists fom_gap_pfp_sub_fixed_result_result_bounded_index_bound. fom_gap_pfp_sub_fixed_result_result_bounded_index_bound + S (fom_index_pfp_sub_fixed_result_result_bounded) = K) -> exists fom_value_pfp_sub_fixed_result_result_bounded. ((((exists fom_beta_height_pfp_sub_fixed_result_result_bounded_entry. fom_beta_height_pfp_sub_fixed_result_result_bounded_entry + S (fom_value_pfp_sub_fixed_result_result_bounded) = S ((S (fom_index_pfp_sub_fixed_result_result_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_sub_fixed_result_result_bounded_entry. ab = fom_beta_quotient_pfp_sub_fixed_result_result_bounded_entry * S ((S (fom_index_pfp_sub_fixed_result_result_bounded)) * ac) + (fom_value_pfp_sub_fixed_result_result_bounded))) /\ (exists fom_gap_pfp_sub_fixed_result_result_bounded_value_bound. fom_gap_pfp_sub_fixed_result_result_bounded_value_bound + S (fom_value_pfp_sub_fixed_result_result_bounded) = p))) /\ ((exists pfaa_left_b_sub_fixed_result pfaa_left_c_sub_fixed_result pfaa_right_b_sub_fixed_result pfaa_right_c_sub_fixed_result pfaa_sum_b_sub_fixed_result pfaa_sum_c_sub_fixed_result pfaa_length_sub_fixed_result. ((((forall pfrep_power_sub_fixed_result_witness_common_left pfrep_left_sub_fixed_result_witness_common_left pfrep_right_sub_fixed_result_witness_common_left. ((exists pfrep_position_sub_fixed_result_witness_common_leftfirst. ((pfrep_position_sub_fixed_result_witness_common_leftfirst+S (pfrep_power_sub_fixed_result_witness_common_left)=(K)) /\ ((((exists ff_h_pfp_sub_fixed_result_witness_common_leftfirstentry. ff_h_pfp_sub_fixed_result_witness_common_leftfirstentry + S (pfrep_left_sub_fixed_result_witness_common_left) = S ((S (pfrep_position_sub_fixed_result_witness_common_leftfirst)) * bc)) /\ exists ff_q_pfp_sub_fixed_result_witness_common_leftfirstentry. bb = ff_q_pfp_sub_fixed_result_witness_common_leftfirstentry * S ((S (pfrep_position_sub_fixed_result_witness_common_leftfirst)) * bc) + (pfrep_left_sub_fixed_result_witness_common_left)))))) \/ (((exists pfrep_gap_sub_fixed_result_witness_common_leftfirstoutside. pfrep_gap_sub_fixed_result_witness_common_leftfirstoutside+(K)=(pfrep_power_sub_fixed_result_witness_common_left)) /\ (((pfrep_left_sub_fixed_result_witness_common_left)=0))))) -> ((exists pfrep_position_sub_fixed_result_witness_common_leftsecond. ((pfrep_position_sub_fixed_result_witness_common_leftsecond+S (pfrep_power_sub_fixed_result_witness_common_left)=(pfaa_length_sub_fixed_result)) /\ ((((exists ff_h_pfp_sub_fixed_result_witness_common_leftsecondentry. ff_h_pfp_sub_fixed_result_witness_common_leftsecondentry + S (pfrep_right_sub_fixed_result_witness_common_left) = S ((S (pfrep_position_sub_fixed_result_witness_common_leftsecond)) * pfaa_left_c_sub_fixed_result)) /\ exists ff_q_pfp_sub_fixed_result_witness_common_leftsecondentry. pfaa_left_b_sub_fixed_result = ff_q_pfp_sub_fixed_result_witness_common_leftsecondentry * S ((S (pfrep_position_sub_fixed_result_witness_common_leftsecond)) * pfaa_left_c_sub_fixed_result) + (pfrep_right_sub_fixed_result_witness_common_left)))))) \/ (((exists pfrep_gap_sub_fixed_result_witness_common_leftsecondoutside. pfrep_gap_sub_fixed_result_witness_common_leftsecondoutside+(pfaa_length_sub_fixed_result)=(pfrep_power_sub_fixed_result_witness_common_left)) /\ (((pfrep_right_sub_fixed_result_witness_common_left)=0))))) -> pfrep_left_sub_fixed_result_witness_common_left=pfrep_right_sub_fixed_result_witness_common_left) /\ ((forall pfrep_power_sub_fixed_result_witness_common_right pfrep_left_sub_fixed_result_witness_common_right pfrep_right_sub_fixed_result_witness_common_right. ((exists pfrep_position_sub_fixed_result_witness_common_rightfirst. ((pfrep_position_sub_fixed_result_witness_common_rightfirst+S (pfrep_power_sub_fixed_result_witness_common_right)=(K)) /\ ((((exists ff_h_pfp_sub_fixed_result_witness_common_rightfirstentry. ff_h_pfp_sub_fixed_result_witness_common_rightfirstentry + S (pfrep_left_sub_fixed_result_witness_common_right) = S ((S (pfrep_position_sub_fixed_result_witness_common_rightfirst)) * rc)) /\ exists ff_q_pfp_sub_fixed_result_witness_common_rightfirstentry. rb = ff_q_pfp_sub_fixed_result_witness_common_rightfirstentry * S ((S (pfrep_position_sub_fixed_result_witness_common_rightfirst)) * rc) + (pfrep_left_sub_fixed_result_witness_common_right)))))) \/ (((exists pfrep_gap_sub_fixed_result_witness_common_rightfirstoutside. pfrep_gap_sub_fixed_result_witness_common_rightfirstoutside+(K)=(pfrep_power_sub_fixed_result_witness_common_right)) /\ (((pfrep_left_sub_fixed_result_witness_common_right)=0))))) -> ((exists pfrep_position_sub_fixed_result_witness_common_rightsecond. ((pfrep_position_sub_fixed_result_witness_common_rightsecond+S (pfrep_power_sub_fixed_result_witness_common_right)=(pfaa_length_sub_fixed_result)) /\ ((((exists ff_h_pfp_sub_fixed_result_witness_common_rightsecondentry. ff_h_pfp_sub_fixed_result_witness_common_rightsecondentry + S (pfrep_right_sub_fixed_result_witness_common_right) = S ((S (pfrep_position_sub_fixed_result_witness_common_rightsecond)) * pfaa_right_c_sub_fixed_result)) /\ exists ff_q_pfp_sub_fixed_result_witness_common_rightsecondentry. pfaa_right_b_sub_fixed_result = ff_q_pfp_sub_fixed_result_witness_common_rightsecondentry * S ((S (pfrep_position_sub_fixed_result_witness_common_rightsecond)) * pfaa_right_c_sub_fixed_result) + (pfrep_right_sub_fixed_result_witness_common_right)))))) \/ (((exists pfrep_gap_sub_fixed_result_witness_common_rightsecondoutside. pfrep_gap_sub_fixed_result_witness_common_rightsecondoutside+(pfaa_length_sub_fixed_result)=(pfrep_power_sub_fixed_result_witness_common_right)) /\ (((pfrep_right_sub_fixed_result_witness_common_right)=0))))) -> pfrep_left_sub_fixed_result_witness_common_right=pfrep_right_sub_fixed_result_witness_common_right)))) /\ (((forall pfp_index_sub_fixed_result_witness_operation. (exists pfa_gap_sub_fixed_result_witness_operationindex. pfa_gap_sub_fixed_result_witness_operationindex + S (pfp_index_sub_fixed_result_witness_operation) = (pfaa_length_sub_fixed_result)) -> exists pfp_left_sub_fixed_result_witness_operation pfp_right_sub_fixed_result_witness_operation pfp_value_sub_fixed_result_witness_operation. ((((exists ff_h_pfp_sub_fixed_result_witness_operationleft. ff_h_pfp_sub_fixed_result_witness_operationleft + S (pfp_left_sub_fixed_result_witness_operation) = S ((S (pfp_index_sub_fixed_result_witness_operation)) * pfaa_left_c_sub_fixed_result)) /\ exists ff_q_pfp_sub_fixed_result_witness_operationleft. pfaa_left_b_sub_fixed_result = ff_q_pfp_sub_fixed_result_witness_operationleft * S ((S (pfp_index_sub_fixed_result_witness_operation)) * pfaa_left_c_sub_fixed_result) + (pfp_left_sub_fixed_result_witness_operation))) /\ (((((exists ff_h_pfp_sub_fixed_result_witness_operationright. ff_h_pfp_sub_fixed_result_witness_operationright + S (pfp_right_sub_fixed_result_witness_operation) = S ((S (pfp_index_sub_fixed_result_witness_operation)) * pfaa_right_c_sub_fixed_result)) /\ exists ff_q_pfp_sub_fixed_result_witness_operationright. pfaa_right_b_sub_fixed_result = ff_q_pfp_sub_fixed_result_witness_operationright * S ((S (pfp_index_sub_fixed_result_witness_operation)) * pfaa_right_c_sub_fixed_result) + (pfp_right_sub_fixed_result_witness_operation))) /\ (((((exists ff_h_pfp_sub_fixed_result_witness_operationtarget. ff_h_pfp_sub_fixed_result_witness_operationtarget + S (pfp_value_sub_fixed_result_witness_operation) = S ((S (pfp_index_sub_fixed_result_witness_operation)) * pfaa_sum_c_sub_fixed_result)) /\ exists ff_q_pfp_sub_fixed_result_witness_operationtarget. pfaa_sum_b_sub_fixed_result = ff_q_pfp_sub_fixed_result_witness_operationtarget * S ((S (pfp_index_sub_fixed_result_witness_operation)) * pfaa_sum_c_sub_fixed_result) + (pfp_value_sub_fixed_result_witness_operation))) /\ ((((exists pfa_gap_sub_fixed_result_witness_operationoperationleft. pfa_gap_sub_fixed_result_witness_operationoperationleft + S (pfp_left_sub_fixed_result_witness_operation) = (p)) /\ (((exists pfa_gap_sub_fixed_result_witness_operationoperationright. pfa_gap_sub_fixed_result_witness_operationoperationright + S (pfp_right_sub_fixed_result_witness_operation) = (p)) /\ ((((exists pfa_gap_sub_fixed_result_witness_operationoperationresultbound. pfa_gap_sub_fixed_result_witness_operationoperationresultbound + S (pfp_value_sub_fixed_result_witness_operation) = (p)) /\ ((exists pfa_offset_left_sub_fixed_result_witness_operationoperationresultcongruence pfa_offset_right_sub_fixed_result_witness_operationoperationresultcongruence. ((pfp_left_sub_fixed_result_witness_operation) + (pfp_right_sub_fixed_result_witness_operation)) + (p) * pfa_offset_left_sub_fixed_result_witness_operationoperationresultcongruence = (pfp_value_sub_fixed_result_witness_operation) + (p) * pfa_offset_right_sub_fixed_result_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_sub_fixed_result_witness_output pfrep_left_sub_fixed_result_witness_output pfrep_right_sub_fixed_result_witness_output. ((exists pfrep_position_sub_fixed_result_witness_outputfirst. ((pfrep_position_sub_fixed_result_witness_outputfirst+S (pfrep_power_sub_fixed_result_witness_output)=(pfaa_length_sub_fixed_result)) /\ ((((exists ff_h_pfp_sub_fixed_result_witness_outputfirstentry. ff_h_pfp_sub_fixed_result_witness_outputfirstentry + S (pfrep_left_sub_fixed_result_witness_output) = S ((S (pfrep_position_sub_fixed_result_witness_outputfirst)) * pfaa_sum_c_sub_fixed_result)) /\ exists ff_q_pfp_sub_fixed_result_witness_outputfirstentry. pfaa_sum_b_sub_fixed_result = ff_q_pfp_sub_fixed_result_witness_outputfirstentry * S ((S (pfrep_position_sub_fixed_result_witness_outputfirst)) * pfaa_sum_c_sub_fixed_result) + (pfrep_left_sub_fixed_result_witness_output)))))) \/ (((exists pfrep_gap_sub_fixed_result_witness_outputfirstoutside. pfrep_gap_sub_fixed_result_witness_outputfirstoutside+(pfaa_length_sub_fixed_result)=(pfrep_power_sub_fixed_result_witness_output)) /\ (((pfrep_left_sub_fixed_result_witness_output)=0))))) -> ((exists pfrep_position_sub_fixed_result_witness_outputsecond. ((pfrep_position_sub_fixed_result_witness_outputsecond+S (pfrep_power_sub_fixed_result_witness_output)=(K)) /\ ((((exists ff_h_pfp_sub_fixed_result_witness_outputsecondentry. ff_h_pfp_sub_fixed_result_witness_outputsecondentry + S (pfrep_right_sub_fixed_result_witness_output) = S ((S (pfrep_position_sub_fixed_result_witness_outputsecond)) * ac)) /\ exists ff_q_pfp_sub_fixed_result_witness_outputsecondentry. ab = ff_q_pfp_sub_fixed_result_witness_outputsecondentry * S ((S (pfrep_position_sub_fixed_result_witness_outputsecond)) * ac) + (pfrep_right_sub_fixed_result_witness_output)))))) \/ (((exists pfrep_gap_sub_fixed_result_witness_outputsecondoutside. pfrep_gap_sub_fixed_result_witness_outputsecondoutside+(K)=(pfrep_power_sub_fixed_result_witness_output)) /\ (((pfrep_right_sub_fixed_result_witness_output)=0))))) -> pfrep_left_sub_fixed_result_witness_output=pfrep_right_sub_fixed_result_witness_output)))))))))))))

Complete tactic proof in conservative notation

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

28 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 (1)
prime field polynomial aligned add from fixed
01Fix variables and assumptionsL1–9

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 rb
  7. L7
    intro rc
  8. L8
    intro K
  9. L9
    intro h
02Use earlier factsL10–19

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

  1. L10
    specialize prime_field_polynomial_aligned_add_from_fixed (p)
  2. L11
    specialize prime_field_polynomial_aligned_add_from_fixed (bb)
  3. L12
    specialize prime_field_polynomial_aligned_add_from_fixed (bc)
  4. L13
    specialize prime_field_polynomial_aligned_add_from_fixed (rb)
  5. L14
    specialize prime_field_polynomial_aligned_add_from_fixed (rc)
  6. L15
    specialize prime_field_polynomial_aligned_add_from_fixed (ab)
  7. L16
    specialize prime_field_polynomial_aligned_add_from_fixed (ac)
  8. L17
    specialize prime_field_polynomial_aligned_add_from_fixed (K)
  9. L18
    apply prime_field_polynomial_aligned_add_from_fixed
  10. L19
    specialize prime_field_polynomial_subtract_recover_add (p)
03Use earlier factsL20–28

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

  1. L20
    specialize prime_field_polynomial_subtract_recover_add (ab)
  2. L21
    specialize prime_field_polynomial_subtract_recover_add (ac)
  3. L22
    specialize prime_field_polynomial_subtract_recover_add (bb)
  4. L23
    specialize prime_field_polynomial_subtract_recover_add (bc)
  5. L24
    specialize prime_field_polynomial_subtract_recover_add (rb)
  6. L25
    specialize prime_field_polynomial_subtract_recover_add (rc)
  7. L26
    specialize prime_field_polynomial_subtract_recover_add (K)
  8. L27
    apply prime_field_polynomial_subtract_recover_add
  9. L28
    exact h

Library-wide reading audit

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