PG003D

prime_field_polynomial_aligned_add_bounded

Aligned addition includes canonical coefficients for the actual originals and output, not merely for equivalent witnesses.

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. ∀ L. ∀ bb. ∀ bc. ∀ M. ∀ rb. ∀ rc. ∀ N. FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N) → BetaPrefixInto(ab,ac,L,p) ∧ (BetaPrefixInto(bb,bc,M,p) ∧ BetaPrefixInto(rb,rc,N,p))

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

Definition DAG

BetaPrefixInto(b,c,l,B) · 3FpPolynomialAlignedAdd(p,ab,ac,L,bb,bc,M,rb,rc,N) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall p ab ac L bb bc M rb rc N. (((forall fom_index_pfp_aligned_bound_input_left_bounded. (exists fom_gap_pfp_aligned_bound_input_left_bounded_index_bound. fom_gap_pfp_aligned_bound_input_left_bounded_index_bound + S (fom_index_pfp_aligned_bound_input_left_bounded) = L) -> exists fom_value_pfp_aligned_bound_input_left_bounded. ((((exists fom_beta_height_pfp_aligned_bound_input_left_bounded_entry. fom_beta_height_pfp_aligned_bound_input_left_bounded_entry + S (fom_value_pfp_aligned_bound_input_left_bounded) = S ((S (fom_index_pfp_aligned_bound_input_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_aligned_bound_input_left_bounded_entry. ab = fom_beta_quotient_pfp_aligned_bound_input_left_bounded_entry * S ((S (fom_index_pfp_aligned_bound_input_left_bounded)) * ac) + (fom_value_pfp_aligned_bound_input_left_bounded))) /\ (exists fom_gap_pfp_aligned_bound_input_left_bounded_value_bound. fom_gap_pfp_aligned_bound_input_left_bounded_value_bound + S (fom_value_pfp_aligned_bound_input_left_bounded) = p))) /\ (((forall fom_index_pfp_aligned_bound_input_right_bounded. (exists fom_gap_pfp_aligned_bound_input_right_bounded_index_bound. fom_gap_pfp_aligned_bound_input_right_bounded_index_bound + S (fom_index_pfp_aligned_bound_input_right_bounded) = M) -> exists fom_value_pfp_aligned_bound_input_right_bounded. ((((exists fom_beta_height_pfp_aligned_bound_input_right_bounded_entry. fom_beta_height_pfp_aligned_bound_input_right_bounded_entry + S (fom_value_pfp_aligned_bound_input_right_bounded) = S ((S (fom_index_pfp_aligned_bound_input_right_bounded)) * bc)) /\ exists fom_beta_quotient_pfp_aligned_bound_input_right_bounded_entry. bb = fom_beta_quotient_pfp_aligned_bound_input_right_bounded_entry * S ((S (fom_index_pfp_aligned_bound_input_right_bounded)) * bc) + (fom_value_pfp_aligned_bound_input_right_bounded))) /\ (exists fom_gap_pfp_aligned_bound_input_right_bounded_value_bound. fom_gap_pfp_aligned_bound_input_right_bounded_value_bound + S (fom_value_pfp_aligned_bound_input_right_bounded) = p))) /\ (((forall fom_index_pfp_aligned_bound_input_result_bounded. (exists fom_gap_pfp_aligned_bound_input_result_bounded_index_bound. fom_gap_pfp_aligned_bound_input_result_bounded_index_bound + S (fom_index_pfp_aligned_bound_input_result_bounded) = N) -> exists fom_value_pfp_aligned_bound_input_result_bounded. ((((exists fom_beta_height_pfp_aligned_bound_input_result_bounded_entry. fom_beta_height_pfp_aligned_bound_input_result_bounded_entry + S (fom_value_pfp_aligned_bound_input_result_bounded) = S ((S (fom_index_pfp_aligned_bound_input_result_bounded)) * rc)) /\ exists fom_beta_quotient_pfp_aligned_bound_input_result_bounded_entry. rb = fom_beta_quotient_pfp_aligned_bound_input_result_bounded_entry * S ((S (fom_index_pfp_aligned_bound_input_result_bounded)) * rc) + (fom_value_pfp_aligned_bound_input_result_bounded))) /\ (exists fom_gap_pfp_aligned_bound_input_result_bounded_value_bound. fom_gap_pfp_aligned_bound_input_result_bounded_value_bound + S (fom_value_pfp_aligned_bound_input_result_bounded) = p))) /\ ((exists pfaa_left_b_aligned_bound_input pfaa_left_c_aligned_bound_input pfaa_right_b_aligned_bound_input pfaa_right_c_aligned_bound_input pfaa_sum_b_aligned_bound_input pfaa_sum_c_aligned_bound_input pfaa_length_aligned_bound_input. ((((forall pfrep_power_aligned_bound_input_witness_common_left pfrep_left_aligned_bound_input_witness_common_left pfrep_right_aligned_bound_input_witness_common_left. ((exists pfrep_position_aligned_bound_input_witness_common_leftfirst. ((pfrep_position_aligned_bound_input_witness_common_leftfirst+S (pfrep_power_aligned_bound_input_witness_common_left)=(L)) /\ ((((exists ff_h_pfp_aligned_bound_input_witness_common_leftfirstentry. ff_h_pfp_aligned_bound_input_witness_common_leftfirstentry + S (pfrep_left_aligned_bound_input_witness_common_left) = S ((S (pfrep_position_aligned_bound_input_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_aligned_bound_input_witness_common_leftfirstentry. ab = ff_q_pfp_aligned_bound_input_witness_common_leftfirstentry * S ((S (pfrep_position_aligned_bound_input_witness_common_leftfirst)) * ac) + (pfrep_left_aligned_bound_input_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_bound_input_witness_common_leftfirstoutside. pfrep_gap_aligned_bound_input_witness_common_leftfirstoutside+(L)=(pfrep_power_aligned_bound_input_witness_common_left)) /\ (((pfrep_left_aligned_bound_input_witness_common_left)=0))))) -> ((exists pfrep_position_aligned_bound_input_witness_common_leftsecond. ((pfrep_position_aligned_bound_input_witness_common_leftsecond+S (pfrep_power_aligned_bound_input_witness_common_left)=(pfaa_length_aligned_bound_input)) /\ ((((exists ff_h_pfp_aligned_bound_input_witness_common_leftsecondentry. ff_h_pfp_aligned_bound_input_witness_common_leftsecondentry + S (pfrep_right_aligned_bound_input_witness_common_left) = S ((S (pfrep_position_aligned_bound_input_witness_common_leftsecond)) * pfaa_left_c_aligned_bound_input)) /\ exists ff_q_pfp_aligned_bound_input_witness_common_leftsecondentry. pfaa_left_b_aligned_bound_input = ff_q_pfp_aligned_bound_input_witness_common_leftsecondentry * S ((S (pfrep_position_aligned_bound_input_witness_common_leftsecond)) * pfaa_left_c_aligned_bound_input) + (pfrep_right_aligned_bound_input_witness_common_left)))))) \/ (((exists pfrep_gap_aligned_bound_input_witness_common_leftsecondoutside. pfrep_gap_aligned_bound_input_witness_common_leftsecondoutside+(pfaa_length_aligned_bound_input)=(pfrep_power_aligned_bound_input_witness_common_left)) /\ (((pfrep_right_aligned_bound_input_witness_common_left)=0))))) -> pfrep_left_aligned_bound_input_witness_common_left=pfrep_right_aligned_bound_input_witness_common_left) /\ ((forall pfrep_power_aligned_bound_input_witness_common_right pfrep_left_aligned_bound_input_witness_common_right pfrep_right_aligned_bound_input_witness_common_right. ((exists pfrep_position_aligned_bound_input_witness_common_rightfirst. ((pfrep_position_aligned_bound_input_witness_common_rightfirst+S (pfrep_power_aligned_bound_input_witness_common_right)=(M)) /\ ((((exists ff_h_pfp_aligned_bound_input_witness_common_rightfirstentry. ff_h_pfp_aligned_bound_input_witness_common_rightfirstentry + S (pfrep_left_aligned_bound_input_witness_common_right) = S ((S (pfrep_position_aligned_bound_input_witness_common_rightfirst)) * bc)) /\ exists ff_q_pfp_aligned_bound_input_witness_common_rightfirstentry. bb = ff_q_pfp_aligned_bound_input_witness_common_rightfirstentry * S ((S (pfrep_position_aligned_bound_input_witness_common_rightfirst)) * bc) + (pfrep_left_aligned_bound_input_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_bound_input_witness_common_rightfirstoutside. pfrep_gap_aligned_bound_input_witness_common_rightfirstoutside+(M)=(pfrep_power_aligned_bound_input_witness_common_right)) /\ (((pfrep_left_aligned_bound_input_witness_common_right)=0))))) -> ((exists pfrep_position_aligned_bound_input_witness_common_rightsecond. ((pfrep_position_aligned_bound_input_witness_common_rightsecond+S (pfrep_power_aligned_bound_input_witness_common_right)=(pfaa_length_aligned_bound_input)) /\ ((((exists ff_h_pfp_aligned_bound_input_witness_common_rightsecondentry. ff_h_pfp_aligned_bound_input_witness_common_rightsecondentry + S (pfrep_right_aligned_bound_input_witness_common_right) = S ((S (pfrep_position_aligned_bound_input_witness_common_rightsecond)) * pfaa_right_c_aligned_bound_input)) /\ exists ff_q_pfp_aligned_bound_input_witness_common_rightsecondentry. pfaa_right_b_aligned_bound_input = ff_q_pfp_aligned_bound_input_witness_common_rightsecondentry * S ((S (pfrep_position_aligned_bound_input_witness_common_rightsecond)) * pfaa_right_c_aligned_bound_input) + (pfrep_right_aligned_bound_input_witness_common_right)))))) \/ (((exists pfrep_gap_aligned_bound_input_witness_common_rightsecondoutside. pfrep_gap_aligned_bound_input_witness_common_rightsecondoutside+(pfaa_length_aligned_bound_input)=(pfrep_power_aligned_bound_input_witness_common_right)) /\ (((pfrep_right_aligned_bound_input_witness_common_right)=0))))) -> pfrep_left_aligned_bound_input_witness_common_right=pfrep_right_aligned_bound_input_witness_common_right)))) /\ (((forall pfp_index_aligned_bound_input_witness_operation. (exists pfa_gap_aligned_bound_input_witness_operationindex. pfa_gap_aligned_bound_input_witness_operationindex + S (pfp_index_aligned_bound_input_witness_operation) = (pfaa_length_aligned_bound_input)) -> exists pfp_left_aligned_bound_input_witness_operation pfp_right_aligned_bound_input_witness_operation pfp_value_aligned_bound_input_witness_operation. ((((exists ff_h_pfp_aligned_bound_input_witness_operationleft. ff_h_pfp_aligned_bound_input_witness_operationleft + S (pfp_left_aligned_bound_input_witness_operation) = S ((S (pfp_index_aligned_bound_input_witness_operation)) * pfaa_left_c_aligned_bound_input)) /\ exists ff_q_pfp_aligned_bound_input_witness_operationleft. pfaa_left_b_aligned_bound_input = ff_q_pfp_aligned_bound_input_witness_operationleft * S ((S (pfp_index_aligned_bound_input_witness_operation)) * pfaa_left_c_aligned_bound_input) + (pfp_left_aligned_bound_input_witness_operation))) /\ (((((exists ff_h_pfp_aligned_bound_input_witness_operationright. ff_h_pfp_aligned_bound_input_witness_operationright + S (pfp_right_aligned_bound_input_witness_operation) = S ((S (pfp_index_aligned_bound_input_witness_operation)) * pfaa_right_c_aligned_bound_input)) /\ exists ff_q_pfp_aligned_bound_input_witness_operationright. pfaa_right_b_aligned_bound_input = ff_q_pfp_aligned_bound_input_witness_operationright * S ((S (pfp_index_aligned_bound_input_witness_operation)) * pfaa_right_c_aligned_bound_input) + (pfp_right_aligned_bound_input_witness_operation))) /\ (((((exists ff_h_pfp_aligned_bound_input_witness_operationtarget. ff_h_pfp_aligned_bound_input_witness_operationtarget + S (pfp_value_aligned_bound_input_witness_operation) = S ((S (pfp_index_aligned_bound_input_witness_operation)) * pfaa_sum_c_aligned_bound_input)) /\ exists ff_q_pfp_aligned_bound_input_witness_operationtarget. pfaa_sum_b_aligned_bound_input = ff_q_pfp_aligned_bound_input_witness_operationtarget * S ((S (pfp_index_aligned_bound_input_witness_operation)) * pfaa_sum_c_aligned_bound_input) + (pfp_value_aligned_bound_input_witness_operation))) /\ ((((exists pfa_gap_aligned_bound_input_witness_operationoperationleft. pfa_gap_aligned_bound_input_witness_operationoperationleft + S (pfp_left_aligned_bound_input_witness_operation) = (p)) /\ (((exists pfa_gap_aligned_bound_input_witness_operationoperationright. pfa_gap_aligned_bound_input_witness_operationoperationright + S (pfp_right_aligned_bound_input_witness_operation) = (p)) /\ ((((exists pfa_gap_aligned_bound_input_witness_operationoperationresultbound. pfa_gap_aligned_bound_input_witness_operationoperationresultbound + S (pfp_value_aligned_bound_input_witness_operation) = (p)) /\ ((exists pfa_offset_left_aligned_bound_input_witness_operationoperationresultcongruence pfa_offset_right_aligned_bound_input_witness_operationoperationresultcongruence. ((pfp_left_aligned_bound_input_witness_operation) + (pfp_right_aligned_bound_input_witness_operation)) + (p) * pfa_offset_left_aligned_bound_input_witness_operationoperationresultcongruence = (pfp_value_aligned_bound_input_witness_operation) + (p) * pfa_offset_right_aligned_bound_input_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_aligned_bound_input_witness_output pfrep_left_aligned_bound_input_witness_output pfrep_right_aligned_bound_input_witness_output. ((exists pfrep_position_aligned_bound_input_witness_outputfirst. ((pfrep_position_aligned_bound_input_witness_outputfirst+S (pfrep_power_aligned_bound_input_witness_output)=(pfaa_length_aligned_bound_input)) /\ ((((exists ff_h_pfp_aligned_bound_input_witness_outputfirstentry. ff_h_pfp_aligned_bound_input_witness_outputfirstentry + S (pfrep_left_aligned_bound_input_witness_output) = S ((S (pfrep_position_aligned_bound_input_witness_outputfirst)) * pfaa_sum_c_aligned_bound_input)) /\ exists ff_q_pfp_aligned_bound_input_witness_outputfirstentry. pfaa_sum_b_aligned_bound_input = ff_q_pfp_aligned_bound_input_witness_outputfirstentry * S ((S (pfrep_position_aligned_bound_input_witness_outputfirst)) * pfaa_sum_c_aligned_bound_input) + (pfrep_left_aligned_bound_input_witness_output)))))) \/ (((exists pfrep_gap_aligned_bound_input_witness_outputfirstoutside. pfrep_gap_aligned_bound_input_witness_outputfirstoutside+(pfaa_length_aligned_bound_input)=(pfrep_power_aligned_bound_input_witness_output)) /\ (((pfrep_left_aligned_bound_input_witness_output)=0))))) -> ((exists pfrep_position_aligned_bound_input_witness_outputsecond. ((pfrep_position_aligned_bound_input_witness_outputsecond+S (pfrep_power_aligned_bound_input_witness_output)=(N)) /\ ((((exists ff_h_pfp_aligned_bound_input_witness_outputsecondentry. ff_h_pfp_aligned_bound_input_witness_outputsecondentry + S (pfrep_right_aligned_bound_input_witness_output) = S ((S (pfrep_position_aligned_bound_input_witness_outputsecond)) * rc)) /\ exists ff_q_pfp_aligned_bound_input_witness_outputsecondentry. rb = ff_q_pfp_aligned_bound_input_witness_outputsecondentry * S ((S (pfrep_position_aligned_bound_input_witness_outputsecond)) * rc) + (pfrep_right_aligned_bound_input_witness_output)))))) \/ (((exists pfrep_gap_aligned_bound_input_witness_outputsecondoutside. pfrep_gap_aligned_bound_input_witness_outputsecondoutside+(N)=(pfrep_power_aligned_bound_input_witness_output)) /\ (((pfrep_right_aligned_bound_input_witness_output)=0))))) -> pfrep_left_aligned_bound_input_witness_output=pfrep_right_aligned_bound_input_witness_output))))))))))))) -> (((forall fom_index_pfp_aligned_bound_0. (exists fom_gap_pfp_aligned_bound_0_index_bound. fom_gap_pfp_aligned_bound_0_index_bound + S (fom_index_pfp_aligned_bound_0) = L) -> exists fom_value_pfp_aligned_bound_0. ((((exists fom_beta_height_pfp_aligned_bound_0_entry. fom_beta_height_pfp_aligned_bound_0_entry + S (fom_value_pfp_aligned_bound_0) = S ((S (fom_index_pfp_aligned_bound_0)) * ac)) /\ exists fom_beta_quotient_pfp_aligned_bound_0_entry. ab = fom_beta_quotient_pfp_aligned_bound_0_entry * S ((S (fom_index_pfp_aligned_bound_0)) * ac) + (fom_value_pfp_aligned_bound_0))) /\ (exists fom_gap_pfp_aligned_bound_0_value_bound. fom_gap_pfp_aligned_bound_0_value_bound + S (fom_value_pfp_aligned_bound_0) = p))) /\ (((forall fom_index_pfp_aligned_bound_1. (exists fom_gap_pfp_aligned_bound_1_index_bound. fom_gap_pfp_aligned_bound_1_index_bound + S (fom_index_pfp_aligned_bound_1) = M) -> exists fom_value_pfp_aligned_bound_1. ((((exists fom_beta_height_pfp_aligned_bound_1_entry. fom_beta_height_pfp_aligned_bound_1_entry + S (fom_value_pfp_aligned_bound_1) = S ((S (fom_index_pfp_aligned_bound_1)) * bc)) /\ exists fom_beta_quotient_pfp_aligned_bound_1_entry. bb = fom_beta_quotient_pfp_aligned_bound_1_entry * S ((S (fom_index_pfp_aligned_bound_1)) * bc) + (fom_value_pfp_aligned_bound_1))) /\ (exists fom_gap_pfp_aligned_bound_1_value_bound. fom_gap_pfp_aligned_bound_1_value_bound + S (fom_value_pfp_aligned_bound_1) = p))) /\ ((forall fom_index_pfp_aligned_bound_2. (exists fom_gap_pfp_aligned_bound_2_index_bound. fom_gap_pfp_aligned_bound_2_index_bound + S (fom_index_pfp_aligned_bound_2) = N) -> exists fom_value_pfp_aligned_bound_2. ((((exists fom_beta_height_pfp_aligned_bound_2_entry. fom_beta_height_pfp_aligned_bound_2_entry + S (fom_value_pfp_aligned_bound_2) = S ((S (fom_index_pfp_aligned_bound_2)) * rc)) /\ exists fom_beta_quotient_pfp_aligned_bound_2_entry. rb = fom_beta_quotient_pfp_aligned_bound_2_entry * S ((S (fom_index_pfp_aligned_bound_2)) * rc) + (fom_value_pfp_aligned_bound_2))) /\ (exists fom_gap_pfp_aligned_bound_2_value_bound. fom_gap_pfp_aligned_bound_2_value_bound + S (fom_value_pfp_aligned_bound_2) = p))))))))

Complete tactic proof in conservative notation

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

19 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.

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 L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro rb
  9. L9
    intro rc
  10. L10
    intro N
02Fix variables and assumptionsL11–11

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

  1. L11
    intro h
03Separate the logical casesL12–15

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

  1. L12
    cases h
  2. L13
    cases h_right
  3. L14
    cases h_right_right
  4. L15
    split
04Use earlier factsL16–16

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

  1. L16
    exact h_left
05Separate the logical casesL17–17

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

  1. L17
    split
06Use earlier factsL18–19

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

  1. L18
    exact h_right_left
  2. L19
    exact h_right_right_left

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro rb
  9. 0009intro rc
  10. 0010intro N
  11. 0011intro h
  12. 0012cases h
  13. 0013cases h_right
  14. 0014cases h_right_right
  15. 0015split
  16. 0016exact h_left
  17. 0017split
  18. 0018exact h_right_left
  19. 0019exact h_right_right_left