PG0060 — prime_field_polynomial_aligned_add_empty_right

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 ab ac A. (~((p) = 1) /\ forall pfa_factor_left_empty_add_prime pfa_factor_right_empty_add_prime. (p) = pfa_factor_left_empty_add_prime * pfa_factor_right_empty_add_prime -> pfa_factor_left_empty_add_prime = 1 \/ pfa_factor_right_empty_add_prime = 1) -> (forall fom_index_pfp_empty_add_bound. (exists fom_gap_pfp_empty_add_bound_index_bound. fom_gap_pfp_empty_add_bound_index_bound + S (fom_index_pfp_empty_add_bound) = A) -> exists fom_value_pfp_empty_add_bound. ((((exists fom_beta_height_pfp_empty_add_bound_entry. fom_beta_height_pfp_empty_add_bound_entry + S (fom_value_pfp_empty_add_bound) = S ((S (fom_index_pfp_empty_add_bound)) * ac)) /\ exists fom_beta_quotient_pfp_empty_add_bound_entry. ab = fom_beta_quotient_pfp_empty_add_bound_entry * S ((S (fom_index_pfp_empty_add_bound)) * ac) + (fom_value_pfp_empty_add_bound))) /\ (exists fom_gap_pfp_empty_add_bound_value_bound. fom_gap_pfp_empty_add_bound_value_bound + S (fom_value_pfp_empty_add_bound) = p))) -> (((forall fom_index_pfp_empty_add_result_left_bounded. (exists fom_gap_pfp_empty_add_result_left_bounded_index_bound. fom_gap_pfp_empty_add_result_left_bounded_index_bound + S (fom_index_pfp_empty_add_result_left_bounded) = A) -> exists fom_value_pfp_empty_add_result_left_bounded. ((((exists fom_beta_height_pfp_empty_add_result_left_bounded_entry. fom_beta_height_pfp_empty_add_result_left_bounded_entry + S (fom_value_pfp_empty_add_result_left_bounded) = S ((S (fom_index_pfp_empty_add_result_left_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_empty_add_result_left_bounded_entry. ab = fom_beta_quotient_pfp_empty_add_result_left_bounded_entry * S ((S (fom_index_pfp_empty_add_result_left_bounded)) * ac) + (fom_value_pfp_empty_add_result_left_bounded))) /\ (exists fom_gap_pfp_empty_add_result_left_bounded_value_bound. fom_gap_pfp_empty_add_result_left_bounded_value_bound + S (fom_value_pfp_empty_add_result_left_bounded) = p))) /\ (((forall fom_index_pfp_empty_add_result_right_bounded. (exists fom_gap_pfp_empty_add_result_right_bounded_index_bound. fom_gap_pfp_empty_add_result_right_bounded_index_bound + S (fom_index_pfp_empty_add_result_right_bounded) = 0) -> exists fom_value_pfp_empty_add_result_right_bounded. ((((exists fom_beta_height_pfp_empty_add_result_right_bounded_entry. fom_beta_height_pfp_empty_add_result_right_bounded_entry + S (fom_value_pfp_empty_add_result_right_bounded) = S ((S (fom_index_pfp_empty_add_result_right_bounded)) * 0)) /\ exists fom_beta_quotient_pfp_empty_add_result_right_bounded_entry. 0 = fom_beta_quotient_pfp_empty_add_result_right_bounded_entry * S ((S (fom_index_pfp_empty_add_result_right_bounded)) * 0) + (fom_value_pfp_empty_add_result_right_bounded))) /\ (exists fom_gap_pfp_empty_add_result_right_bounded_value_bound. fom_gap_pfp_empty_add_result_right_bounded_value_bound + S (fom_value_pfp_empty_add_result_right_bounded) = p))) /\ (((forall fom_index_pfp_empty_add_result_result_bounded. (exists fom_gap_pfp_empty_add_result_result_bounded_index_bound. fom_gap_pfp_empty_add_result_result_bounded_index_bound + S (fom_index_pfp_empty_add_result_result_bounded) = A) -> exists fom_value_pfp_empty_add_result_result_bounded. ((((exists fom_beta_height_pfp_empty_add_result_result_bounded_entry. fom_beta_height_pfp_empty_add_result_result_bounded_entry + S (fom_value_pfp_empty_add_result_result_bounded) = S ((S (fom_index_pfp_empty_add_result_result_bounded)) * ac)) /\ exists fom_beta_quotient_pfp_empty_add_result_result_bounded_entry. ab = fom_beta_quotient_pfp_empty_add_result_result_bounded_entry * S ((S (fom_index_pfp_empty_add_result_result_bounded)) * ac) + (fom_value_pfp_empty_add_result_result_bounded))) /\ (exists fom_gap_pfp_empty_add_result_result_bounded_value_bound. fom_gap_pfp_empty_add_result_result_bounded_value_bound + S (fom_value_pfp_empty_add_result_result_bounded) = p))) /\ ((exists pfaa_left_b_empty_add_result pfaa_left_c_empty_add_result pfaa_right_b_empty_add_result pfaa_right_c_empty_add_result pfaa_sum_b_empty_add_result pfaa_sum_c_empty_add_result pfaa_length_empty_add_result. ((((forall pfrep_power_empty_add_result_witness_common_left pfrep_left_empty_add_result_witness_common_left pfrep_right_empty_add_result_witness_common_left. ((exists pfrep_position_empty_add_result_witness_common_leftfirst. ((pfrep_position_empty_add_result_witness_common_leftfirst+S (pfrep_power_empty_add_result_witness_common_left)=(A)) /\ ((((exists ff_h_pfp_empty_add_result_witness_common_leftfirstentry. ff_h_pfp_empty_add_result_witness_common_leftfirstentry + S (pfrep_left_empty_add_result_witness_common_left) = S ((S (pfrep_position_empty_add_result_witness_common_leftfirst)) * ac)) /\ exists ff_q_pfp_empty_add_result_witness_common_leftfirstentry. ab = ff_q_pfp_empty_add_result_witness_common_leftfirstentry * S ((S (pfrep_position_empty_add_result_witness_common_leftfirst)) * ac) + (pfrep_left_empty_add_result_witness_common_left)))))) \/ (((exists pfrep_gap_empty_add_result_witness_common_leftfirstoutside. pfrep_gap_empty_add_result_witness_common_leftfirstoutside+(A)=(pfrep_power_empty_add_result_witness_common_left)) /\ (((pfrep_left_empty_add_result_witness_common_left)=0))))) -> ((exists pfrep_position_empty_add_result_witness_common_leftsecond. ((pfrep_position_empty_add_result_witness_common_leftsecond+S (pfrep_power_empty_add_result_witness_common_left)=(pfaa_length_empty_add_result)) /\ ((((exists ff_h_pfp_empty_add_result_witness_common_leftsecondentry. ff_h_pfp_empty_add_result_witness_common_leftsecondentry + S (pfrep_right_empty_add_result_witness_common_left) = S ((S (pfrep_position_empty_add_result_witness_common_leftsecond)) * pfaa_left_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_common_leftsecondentry. pfaa_left_b_empty_add_result = ff_q_pfp_empty_add_result_witness_common_leftsecondentry * S ((S (pfrep_position_empty_add_result_witness_common_leftsecond)) * pfaa_left_c_empty_add_result) + (pfrep_right_empty_add_result_witness_common_left)))))) \/ (((exists pfrep_gap_empty_add_result_witness_common_leftsecondoutside. pfrep_gap_empty_add_result_witness_common_leftsecondoutside+(pfaa_length_empty_add_result)=(pfrep_power_empty_add_result_witness_common_left)) /\ (((pfrep_right_empty_add_result_witness_common_left)=0))))) -> pfrep_left_empty_add_result_witness_common_left=pfrep_right_empty_add_result_witness_common_left) /\ ((forall pfrep_power_empty_add_result_witness_common_right pfrep_left_empty_add_result_witness_common_right pfrep_right_empty_add_result_witness_common_right. ((exists pfrep_position_empty_add_result_witness_common_rightfirst. ((pfrep_position_empty_add_result_witness_common_rightfirst+S (pfrep_power_empty_add_result_witness_common_right)=(0)) /\ ((((exists ff_h_pfp_empty_add_result_witness_common_rightfirstentry. ff_h_pfp_empty_add_result_witness_common_rightfirstentry + S (pfrep_left_empty_add_result_witness_common_right) = S ((S (pfrep_position_empty_add_result_witness_common_rightfirst)) * 0)) /\ exists ff_q_pfp_empty_add_result_witness_common_rightfirstentry. 0 = ff_q_pfp_empty_add_result_witness_common_rightfirstentry * S ((S (pfrep_position_empty_add_result_witness_common_rightfirst)) * 0) + (pfrep_left_empty_add_result_witness_common_right)))))) \/ (((exists pfrep_gap_empty_add_result_witness_common_rightfirstoutside. pfrep_gap_empty_add_result_witness_common_rightfirstoutside+(0)=(pfrep_power_empty_add_result_witness_common_right)) /\ (((pfrep_left_empty_add_result_witness_common_right)=0))))) -> ((exists pfrep_position_empty_add_result_witness_common_rightsecond. ((pfrep_position_empty_add_result_witness_common_rightsecond+S (pfrep_power_empty_add_result_witness_common_right)=(pfaa_length_empty_add_result)) /\ ((((exists ff_h_pfp_empty_add_result_witness_common_rightsecondentry. ff_h_pfp_empty_add_result_witness_common_rightsecondentry + S (pfrep_right_empty_add_result_witness_common_right) = S ((S (pfrep_position_empty_add_result_witness_common_rightsecond)) * pfaa_right_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_common_rightsecondentry. pfaa_right_b_empty_add_result = ff_q_pfp_empty_add_result_witness_common_rightsecondentry * S ((S (pfrep_position_empty_add_result_witness_common_rightsecond)) * pfaa_right_c_empty_add_result) + (pfrep_right_empty_add_result_witness_common_right)))))) \/ (((exists pfrep_gap_empty_add_result_witness_common_rightsecondoutside. pfrep_gap_empty_add_result_witness_common_rightsecondoutside+(pfaa_length_empty_add_result)=(pfrep_power_empty_add_result_witness_common_right)) /\ (((pfrep_right_empty_add_result_witness_common_right)=0))))) -> pfrep_left_empty_add_result_witness_common_right=pfrep_right_empty_add_result_witness_common_right)))) /\ (((forall pfp_index_empty_add_result_witness_operation. (exists pfa_gap_empty_add_result_witness_operationindex. pfa_gap_empty_add_result_witness_operationindex + S (pfp_index_empty_add_result_witness_operation) = (pfaa_length_empty_add_result)) -> exists pfp_left_empty_add_result_witness_operation pfp_right_empty_add_result_witness_operation pfp_value_empty_add_result_witness_operation. ((((exists ff_h_pfp_empty_add_result_witness_operationleft. ff_h_pfp_empty_add_result_witness_operationleft + S (pfp_left_empty_add_result_witness_operation) = S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_left_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_operationleft. pfaa_left_b_empty_add_result = ff_q_pfp_empty_add_result_witness_operationleft * S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_left_c_empty_add_result) + (pfp_left_empty_add_result_witness_operation))) /\ (((((exists ff_h_pfp_empty_add_result_witness_operationright. ff_h_pfp_empty_add_result_witness_operationright + S (pfp_right_empty_add_result_witness_operation) = S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_right_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_operationright. pfaa_right_b_empty_add_result = ff_q_pfp_empty_add_result_witness_operationright * S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_right_c_empty_add_result) + (pfp_right_empty_add_result_witness_operation))) /\ (((((exists ff_h_pfp_empty_add_result_witness_operationtarget. ff_h_pfp_empty_add_result_witness_operationtarget + S (pfp_value_empty_add_result_witness_operation) = S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_sum_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_operationtarget. pfaa_sum_b_empty_add_result = ff_q_pfp_empty_add_result_witness_operationtarget * S ((S (pfp_index_empty_add_result_witness_operation)) * pfaa_sum_c_empty_add_result) + (pfp_value_empty_add_result_witness_operation))) /\ ((((exists pfa_gap_empty_add_result_witness_operationoperationleft. pfa_gap_empty_add_result_witness_operationoperationleft + S (pfp_left_empty_add_result_witness_operation) = (p)) /\ (((exists pfa_gap_empty_add_result_witness_operationoperationright. pfa_gap_empty_add_result_witness_operationoperationright + S (pfp_right_empty_add_result_witness_operation) = (p)) /\ ((((exists pfa_gap_empty_add_result_witness_operationoperationresultbound. pfa_gap_empty_add_result_witness_operationoperationresultbound + S (pfp_value_empty_add_result_witness_operation) = (p)) /\ ((exists pfa_offset_left_empty_add_result_witness_operationoperationresultcongruence pfa_offset_right_empty_add_result_witness_operationoperationresultcongruence. ((pfp_left_empty_add_result_witness_operation) + (pfp_right_empty_add_result_witness_operation)) + (p) * pfa_offset_left_empty_add_result_witness_operationoperationresultcongruence = (pfp_value_empty_add_result_witness_operation) + (p) * pfa_offset_right_empty_add_result_witness_operationoperationresultcongruence)))))))))))))))) /\ ((forall pfrep_power_empty_add_result_witness_output pfrep_left_empty_add_result_witness_output pfrep_right_empty_add_result_witness_output. ((exists pfrep_position_empty_add_result_witness_outputfirst. ((pfrep_position_empty_add_result_witness_outputfirst+S (pfrep_power_empty_add_result_witness_output)=(pfaa_length_empty_add_result)) /\ ((((exists ff_h_pfp_empty_add_result_witness_outputfirstentry. ff_h_pfp_empty_add_result_witness_outputfirstentry + S (pfrep_left_empty_add_result_witness_output) = S ((S (pfrep_position_empty_add_result_witness_outputfirst)) * pfaa_sum_c_empty_add_result)) /\ exists ff_q_pfp_empty_add_result_witness_outputfirstentry. pfaa_sum_b_empty_add_result = ff_q_pfp_empty_add_result_witness_outputfirstentry * S ((S (pfrep_position_empty_add_result_witness_outputfirst)) * pfaa_sum_c_empty_add_result) + (pfrep_left_empty_add_result_witness_output)))))) \/ (((exists pfrep_gap_empty_add_result_witness_outputfirstoutside. pfrep_gap_empty_add_result_witness_outputfirstoutside+(pfaa_length_empty_add_result)=(pfrep_power_empty_add_result_witness_output)) /\ (((pfrep_left_empty_add_result_witness_output)=0))))) -> ((exists pfrep_position_empty_add_result_witness_outputsecond. ((pfrep_position_empty_add_result_witness_outputsecond+S (pfrep_power_empty_add_result_witness_output)=(A)) /\ ((((exists ff_h_pfp_empty_add_result_witness_outputsecondentry. ff_h_pfp_empty_add_result_witness_outputsecondentry + S (pfrep_right_empty_add_result_witness_output) = S ((S (pfrep_position_empty_add_result_witness_outputsecond)) * ac)) /\ exists ff_q_pfp_empty_add_result_witness_outputsecondentry. ab = ff_q_pfp_empty_add_result_witness_outputsecondentry * S ((S (pfrep_position_empty_add_result_witness_outputsecond)) * ac) + (pfrep_right_empty_add_result_witness_output)))))) \/ (((exists pfrep_gap_empty_add_result_witness_outputsecondoutside. pfrep_gap_empty_add_result_witness_outputsecondoutside+(A)=(pfrep_power_empty_add_result_witness_output)) /\ (((pfrep_right_empty_add_result_witness_output)=0))))) -> pfrep_left_empty_add_result_witness_output=pfrep_right_empty_add_result_witness_output)))))))))))))

Constructive proof overview

Generated structural guide

Construct a real zero prefix at the input length and its formal equivalence to the empty polynomial, giving an actual aligned right-zero sum for every canonical input.

The unchanged tactic script uses 7 declared prerequisites and contains 67 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_repeat_exists Alpha theorem; checked-use authorized PG003C prime_field_polynomial_aligned_add_from_common matrix_rank_bounded_prefix_empty Alpha theorem; checked-use authorized prime_field_polynomial_power_coefficient_functional Alpha theorem; checked-use authorized prime_field_polynomial_equivalent_symmetric Alpha theorem; checked-use authorized prime_field_polynomial_zero_prefix_equivalent_empty Alpha theorem; checked-use authorized prime_field_polynomial_add_zero_right Alpha theorem; checked-use authorized

Direct dependents

PG0061 prime_field_polynomial_bezout_from_right_multiple

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

67 script commands · 10 reading checkpoints · 1 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 (1)

prime field polynomial aligned add from common

01Fix variables and assumptionsL1–6

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

L1
intro p
L2
intro ab
L3
intro ac
L4
intro A
L5
intro hp
L6
intro ha

02Establish hzL7–10

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta repeat exists.

L7
have hz : exists zb zc. forall pfp_repeat_index_empty_add_zeros. (exists pfa_gap_empty_add_zerosindex. pfa_gap_empty_add_zerosindex + S (pfp_repeat_index_empty_add_zeros) = (A)) -> (((exists ff_h_pfp_empty_add_zerosentry. ff_h_pfp_empty_add_zerosentry + S (0) = S ((S (pfp_repeat_index_empty_add_zeros)) * zc)) /\ exists ff_q_pfp_empty_add_zerosentry. zb = ff_q_pfp_empty_add_zerosentry * S ((S (pfp_repeat_index_empty_add_zeros)) * zc) + (0)))
L8
specialize beta_repeat_exists (0)
L9
specialize beta_repeat_exists (A)
L10
apply beta_repeat_exists

03Separate the logical casesL11–12

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

L11
cases hz
L12
cases hz_witness

04Use earlier factsL13–22