PG0022

prime_field_polynomial_shift_scale_aligned_congruent

Formal equivalence of two old prefixes preserves every actual aligned sum of their trailing-zero shifts with a fixed actual scalar multiple of the same source. Both old lengths, all shift/scale encodings, both leading paddings and the sum encodings remain independent; only formal output coefficients are concluded equal.

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. ∀ c. ∀ ab. ∀ ac. ∀ L. ∀ b0. ∀ c0. ∀ N0. ∀ b1. ∀ c1. ∀ N1. ∀ u0b. ∀ u0c. ∀ v0b. ∀ v0c. ∀ UP0b. ∀ UP0c. ∀ VP0b. ∀ VP0c. ∀ z0b. ∀ z0c. ∀ u1b. ∀ u1c. ∀ v1b. ∀ v1c. ∀ UP1b. ∀ UP1c. ∀ VP1b. ∀ VP1c. ∀ z1b. ∀ z1c. Prime(p) → PolynomialEquivalent(b0,c0,N0,b1,c1,N1) → PolynomialShift(b0,c0,N0,u0b,u0c) → FpPolyScale(p,c,ab,ac,v0b,v0c,L) → PolynomialLeftPad(u0b,u0c,S N0,L,UP0b,UP0c) → PolynomialLeftPad(v0b,v0c,L,S N0,VP0b,VP0c) → FpPolyAdd(p,UP0b,UP0c,VP0b,VP0c,z0b,z0c,L + S N0) → PolynomialShift(b1,c1,N1,u1b,u1c) → FpPolyScale(p,c,ab,ac,v1b,v1c,L) → PolynomialLeftPad(u1b,u1c,S N1,L,UP1b,UP1c) → PolynomialLeftPad(v1b,v1c,L,S N1,VP1b,VP1c) → FpPolyAdd(p,UP1b,UP1c,VP1b,VP1c,z1b,z1c,L + S N1) → PolynomialEquivalent(z0b,z0c,L + S N0,z1b,z1c,L + S N1)

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

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 1FpPolyAdd(p,ab,ac,bb,bc,cb,cc,l) · 2FpPolyScale(p,k,ab,ac,bb,bc,l) · 2PolynomialLeftPad(b,c,L,t,d,e) · 4PolynomialEquivalent(b,c,L,d,e,M) · 12PolynomialShift(b,c,L,d,e) · 2Prime(p) · 1

Actual proof prerequisites

prime_field_polynomial_shift_equivalent_congruentprime_field_polynomial_scale_functional · checked external prerequisiteprime_field_polynomial_equal_implies_equivalent · checked external prerequisiteprime_field_polynomial_left_pad_equivalent · checked external prerequisiteadd_comm · checked external prerequisiteprime_field_polynomial_equivalent_transitive · checked external prerequisiteprime_field_polynomial_equivalent_symmetric · checked external prerequisiteprime_field_polynomial_add_equivalent_congruent · checked external prerequisite
Original expanded first-order statement 
forall p c ab ac L b0 c0 N0 b1 c1 N1 u0b u0c v0b v0c UP0b UP0c VP0b VP0c z0b z0c u1b u1c v1b v1c UP1b UP1c VP1b VP1c z1b z1c. (~((p) = 1) /\ forall pfa_factor_left_step_alignment_prime pfa_factor_right_step_alignment_prime. (p) = pfa_factor_left_step_alignment_prime * pfa_factor_right_step_alignment_prime -> pfa_factor_left_step_alignment_prime = 1 \/ pfa_factor_right_step_alignment_prime = 1) -> (forall pfrep_power_step_alignment_old_equal pfrep_left_step_alignment_old_equal pfrep_right_step_alignment_old_equal. ((exists pfrep_position_step_alignment_old_equalfirst. ((pfrep_position_step_alignment_old_equalfirst+S (pfrep_power_step_alignment_old_equal)=(N0)) /\ ((((exists ff_h_pfp_step_alignment_old_equalfirstentry. ff_h_pfp_step_alignment_old_equalfirstentry + S (pfrep_left_step_alignment_old_equal) = S ((S (pfrep_position_step_alignment_old_equalfirst)) * c0)) /\ exists ff_q_pfp_step_alignment_old_equalfirstentry. b0 = ff_q_pfp_step_alignment_old_equalfirstentry * S ((S (pfrep_position_step_alignment_old_equalfirst)) * c0) + (pfrep_left_step_alignment_old_equal)))))) \/ (((exists pfrep_gap_step_alignment_old_equalfirstoutside. pfrep_gap_step_alignment_old_equalfirstoutside+(N0)=(pfrep_power_step_alignment_old_equal)) /\ (((pfrep_left_step_alignment_old_equal)=0))))) -> ((exists pfrep_position_step_alignment_old_equalsecond. ((pfrep_position_step_alignment_old_equalsecond+S (pfrep_power_step_alignment_old_equal)=(N1)) /\ ((((exists ff_h_pfp_step_alignment_old_equalsecondentry. ff_h_pfp_step_alignment_old_equalsecondentry + S (pfrep_right_step_alignment_old_equal) = S ((S (pfrep_position_step_alignment_old_equalsecond)) * c1)) /\ exists ff_q_pfp_step_alignment_old_equalsecondentry. b1 = ff_q_pfp_step_alignment_old_equalsecondentry * S ((S (pfrep_position_step_alignment_old_equalsecond)) * c1) + (pfrep_right_step_alignment_old_equal)))))) \/ (((exists pfrep_gap_step_alignment_old_equalsecondoutside. pfrep_gap_step_alignment_old_equalsecondoutside+(N1)=(pfrep_power_step_alignment_old_equal)) /\ (((pfrep_right_step_alignment_old_equal)=0))))) -> pfrep_left_step_alignment_old_equal=pfrep_right_step_alignment_old_equal) -> (((forall mdr_i_pfp_step_alignment_old_shiftprefix mdr_a_pfp_step_alignment_old_shiftprefix. (exists mdr_gap_pfp_step_alignment_old_shiftprefixb. mdr_gap_pfp_step_alignment_old_shiftprefixb + S (mdr_i_pfp_step_alignment_old_shiftprefix) = (N0)) -> (((exists ff_h_mdr_pfp_step_alignment_old_shiftprefixo. ff_h_mdr_pfp_step_alignment_old_shiftprefixo + S (mdr_a_pfp_step_alignment_old_shiftprefix) = S ((S (mdr_i_pfp_step_alignment_old_shiftprefix)) * c0)) /\ exists ff_q_mdr_pfp_step_alignment_old_shiftprefixo. b0 = ff_q_mdr_pfp_step_alignment_old_shiftprefixo * S ((S (mdr_i_pfp_step_alignment_old_shiftprefix)) * c0) + (mdr_a_pfp_step_alignment_old_shiftprefix))) -> (((exists ff_h_mdr_pfp_step_alignment_old_shiftprefixn. ff_h_mdr_pfp_step_alignment_old_shiftprefixn + S (mdr_a_pfp_step_alignment_old_shiftprefix) = S ((S (mdr_i_pfp_step_alignment_old_shiftprefix)) * u0c)) /\ exists ff_q_mdr_pfp_step_alignment_old_shiftprefixn. u0b = ff_q_mdr_pfp_step_alignment_old_shiftprefixn * S ((S (mdr_i_pfp_step_alignment_old_shiftprefix)) * u0c) + (mdr_a_pfp_step_alignment_old_shiftprefix)))) /\ ((((exists ff_h_pfp_step_alignment_old_shiftzero. ff_h_pfp_step_alignment_old_shiftzero + S (0) = S ((S (N0)) * u0c)) /\ exists ff_q_pfp_step_alignment_old_shiftzero. u0b = ff_q_pfp_step_alignment_old_shiftzero * S ((S (N0)) * u0c) + (0)))))) -> (((exists pfa_gap_step_alignment_old_scalescalar. pfa_gap_step_alignment_old_scalescalar + S (c) = (p)) /\ ((forall pfp_index_step_alignment_old_scale. (exists pfa_gap_step_alignment_old_scaleindex. pfa_gap_step_alignment_old_scaleindex + S (pfp_index_step_alignment_old_scale) = (L)) -> exists pfp_source_step_alignment_old_scale pfp_value_step_alignment_old_scale. ((((exists ff_h_pfp_step_alignment_old_scalesource. ff_h_pfp_step_alignment_old_scalesource + S (pfp_source_step_alignment_old_scale) = S ((S (pfp_index_step_alignment_old_scale)) * ac)) /\ exists ff_q_pfp_step_alignment_old_scalesource. ab = ff_q_pfp_step_alignment_old_scalesource * S ((S (pfp_index_step_alignment_old_scale)) * ac) + (pfp_source_step_alignment_old_scale))) /\ (((((exists ff_h_pfp_step_alignment_old_scaletarget. ff_h_pfp_step_alignment_old_scaletarget + S (pfp_value_step_alignment_old_scale) = S ((S (pfp_index_step_alignment_old_scale)) * v0c)) /\ exists ff_q_pfp_step_alignment_old_scaletarget. v0b = ff_q_pfp_step_alignment_old_scaletarget * S ((S (pfp_index_step_alignment_old_scale)) * v0c) + (pfp_value_step_alignment_old_scale))) /\ ((((exists pfa_gap_step_alignment_old_scaleoperationleft. pfa_gap_step_alignment_old_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_step_alignment_old_scaleoperationright. pfa_gap_step_alignment_old_scaleoperationright + S (pfp_source_step_alignment_old_scale) = (p)) /\ ((((exists pfa_gap_step_alignment_old_scaleoperationresultbound. pfa_gap_step_alignment_old_scaleoperationresultbound + S (pfp_value_step_alignment_old_scale) = (p)) /\ ((exists pfa_offset_left_step_alignment_old_scaleoperationresultcongruence pfa_offset_right_step_alignment_old_scaleoperationresultcongruence. ((c) * (pfp_source_step_alignment_old_scale)) + (p) * pfa_offset_left_step_alignment_old_scaleoperationresultcongruence = (pfp_value_step_alignment_old_scale) + (p) * pfa_offset_right_step_alignment_old_scaleoperationresultcongruence))))))))))))))))) -> (((forall pfp_repeat_index_step_alignment_old_leftzeros. (exists pfa_gap_step_alignment_old_leftzerosindex. pfa_gap_step_alignment_old_leftzerosindex + S (pfp_repeat_index_step_alignment_old_leftzeros) = (L)) -> (((exists ff_h_pfp_step_alignment_old_leftzerosentry. ff_h_pfp_step_alignment_old_leftzerosentry + S (0) = S ((S (pfp_repeat_index_step_alignment_old_leftzeros)) * UP0c)) /\ exists ff_q_pfp_step_alignment_old_leftzerosentry. UP0b = ff_q_pfp_step_alignment_old_leftzerosentry * S ((S (pfp_repeat_index_step_alignment_old_leftzeros)) * UP0c) + (0)))) /\ ((forall pfrep_index_step_alignment_old_left pfrep_value_step_alignment_old_left. (exists pfa_gap_step_alignment_old_leftbound. pfa_gap_step_alignment_old_leftbound + S (pfrep_index_step_alignment_old_left) = (S N0)) -> (((exists ff_h_pfp_step_alignment_old_leftinput. ff_h_pfp_step_alignment_old_leftinput + S (pfrep_value_step_alignment_old_left) = S ((S (pfrep_index_step_alignment_old_left)) * u0c)) /\ exists ff_q_pfp_step_alignment_old_leftinput. u0b = ff_q_pfp_step_alignment_old_leftinput * S ((S (pfrep_index_step_alignment_old_left)) * u0c) + (pfrep_value_step_alignment_old_left))) -> (((exists ff_h_pfp_step_alignment_old_leftoutput. ff_h_pfp_step_alignment_old_leftoutput + S (pfrep_value_step_alignment_old_left) = S ((S ((L)+pfrep_index_step_alignment_old_left)) * UP0c)) /\ exists ff_q_pfp_step_alignment_old_leftoutput. UP0b = ff_q_pfp_step_alignment_old_leftoutput * S ((S ((L)+pfrep_index_step_alignment_old_left)) * UP0c) + (pfrep_value_step_alignment_old_left))))))) -> (((forall pfp_repeat_index_step_alignment_old_rightzeros. (exists pfa_gap_step_alignment_old_rightzerosindex. pfa_gap_step_alignment_old_rightzerosindex + S (pfp_repeat_index_step_alignment_old_rightzeros) = (S N0)) -> (((exists ff_h_pfp_step_alignment_old_rightzerosentry. ff_h_pfp_step_alignment_old_rightzerosentry + S (0) = S ((S (pfp_repeat_index_step_alignment_old_rightzeros)) * VP0c)) /\ exists ff_q_pfp_step_alignment_old_rightzerosentry. VP0b = ff_q_pfp_step_alignment_old_rightzerosentry * S ((S (pfp_repeat_index_step_alignment_old_rightzeros)) * VP0c) + (0)))) /\ ((forall pfrep_index_step_alignment_old_right pfrep_value_step_alignment_old_right. (exists pfa_gap_step_alignment_old_rightbound. pfa_gap_step_alignment_old_rightbound + S (pfrep_index_step_alignment_old_right) = (L)) -> (((exists ff_h_pfp_step_alignment_old_rightinput. ff_h_pfp_step_alignment_old_rightinput + S (pfrep_value_step_alignment_old_right) = S ((S (pfrep_index_step_alignment_old_right)) * v0c)) /\ exists ff_q_pfp_step_alignment_old_rightinput. v0b = ff_q_pfp_step_alignment_old_rightinput * S ((S (pfrep_index_step_alignment_old_right)) * v0c) + (pfrep_value_step_alignment_old_right))) -> (((exists ff_h_pfp_step_alignment_old_rightoutput. ff_h_pfp_step_alignment_old_rightoutput + S (pfrep_value_step_alignment_old_right) = S ((S ((S N0)+pfrep_index_step_alignment_old_right)) * VP0c)) /\ exists ff_q_pfp_step_alignment_old_rightoutput. VP0b = ff_q_pfp_step_alignment_old_rightoutput * S ((S ((S N0)+pfrep_index_step_alignment_old_right)) * VP0c) + (pfrep_value_step_alignment_old_right))))))) -> (forall pfp_index_step_alignment_old_sum. (exists pfa_gap_step_alignment_old_sumindex. pfa_gap_step_alignment_old_sumindex + S (pfp_index_step_alignment_old_sum) = (L+S N0)) -> exists pfp_left_step_alignment_old_sum pfp_right_step_alignment_old_sum pfp_value_step_alignment_old_sum. ((((exists ff_h_pfp_step_alignment_old_sumleft. ff_h_pfp_step_alignment_old_sumleft + S (pfp_left_step_alignment_old_sum) = S ((S (pfp_index_step_alignment_old_sum)) * UP0c)) /\ exists ff_q_pfp_step_alignment_old_sumleft. UP0b = ff_q_pfp_step_alignment_old_sumleft * S ((S (pfp_index_step_alignment_old_sum)) * UP0c) + (pfp_left_step_alignment_old_sum))) /\ (((((exists ff_h_pfp_step_alignment_old_sumright. ff_h_pfp_step_alignment_old_sumright + S (pfp_right_step_alignment_old_sum) = S ((S (pfp_index_step_alignment_old_sum)) * VP0c)) /\ exists ff_q_pfp_step_alignment_old_sumright. VP0b = ff_q_pfp_step_alignment_old_sumright * S ((S (pfp_index_step_alignment_old_sum)) * VP0c) + (pfp_right_step_alignment_old_sum))) /\ (((((exists ff_h_pfp_step_alignment_old_sumtarget. ff_h_pfp_step_alignment_old_sumtarget + S (pfp_value_step_alignment_old_sum) = S ((S (pfp_index_step_alignment_old_sum)) * z0c)) /\ exists ff_q_pfp_step_alignment_old_sumtarget. z0b = ff_q_pfp_step_alignment_old_sumtarget * S ((S (pfp_index_step_alignment_old_sum)) * z0c) + (pfp_value_step_alignment_old_sum))) /\ ((((exists pfa_gap_step_alignment_old_sumoperationleft. pfa_gap_step_alignment_old_sumoperationleft + S (pfp_left_step_alignment_old_sum) = (p)) /\ (((exists pfa_gap_step_alignment_old_sumoperationright. pfa_gap_step_alignment_old_sumoperationright + S (pfp_right_step_alignment_old_sum) = (p)) /\ ((((exists pfa_gap_step_alignment_old_sumoperationresultbound. pfa_gap_step_alignment_old_sumoperationresultbound + S (pfp_value_step_alignment_old_sum) = (p)) /\ ((exists pfa_offset_left_step_alignment_old_sumoperationresultcongruence pfa_offset_right_step_alignment_old_sumoperationresultcongruence. ((pfp_left_step_alignment_old_sum) + (pfp_right_step_alignment_old_sum)) + (p) * pfa_offset_left_step_alignment_old_sumoperationresultcongruence = (pfp_value_step_alignment_old_sum) + (p) * pfa_offset_right_step_alignment_old_sumoperationresultcongruence)))))))))))))))) -> (((forall mdr_i_pfp_step_alignment_new_shiftprefix mdr_a_pfp_step_alignment_new_shiftprefix. (exists mdr_gap_pfp_step_alignment_new_shiftprefixb. mdr_gap_pfp_step_alignment_new_shiftprefixb + S (mdr_i_pfp_step_alignment_new_shiftprefix) = (N1)) -> (((exists ff_h_mdr_pfp_step_alignment_new_shiftprefixo. ff_h_mdr_pfp_step_alignment_new_shiftprefixo + S (mdr_a_pfp_step_alignment_new_shiftprefix) = S ((S (mdr_i_pfp_step_alignment_new_shiftprefix)) * c1)) /\ exists ff_q_mdr_pfp_step_alignment_new_shiftprefixo. b1 = ff_q_mdr_pfp_step_alignment_new_shiftprefixo * S ((S (mdr_i_pfp_step_alignment_new_shiftprefix)) * c1) + (mdr_a_pfp_step_alignment_new_shiftprefix))) -> (((exists ff_h_mdr_pfp_step_alignment_new_shiftprefixn. ff_h_mdr_pfp_step_alignment_new_shiftprefixn + S (mdr_a_pfp_step_alignment_new_shiftprefix) = S ((S (mdr_i_pfp_step_alignment_new_shiftprefix)) * u1c)) /\ exists ff_q_mdr_pfp_step_alignment_new_shiftprefixn. u1b = ff_q_mdr_pfp_step_alignment_new_shiftprefixn * S ((S (mdr_i_pfp_step_alignment_new_shiftprefix)) * u1c) + (mdr_a_pfp_step_alignment_new_shiftprefix)))) /\ ((((exists ff_h_pfp_step_alignment_new_shiftzero. ff_h_pfp_step_alignment_new_shiftzero + S (0) = S ((S (N1)) * u1c)) /\ exists ff_q_pfp_step_alignment_new_shiftzero. u1b = ff_q_pfp_step_alignment_new_shiftzero * S ((S (N1)) * u1c) + (0)))))) -> (((exists pfa_gap_step_alignment_new_scalescalar. pfa_gap_step_alignment_new_scalescalar + S (c) = (p)) /\ ((forall pfp_index_step_alignment_new_scale. (exists pfa_gap_step_alignment_new_scaleindex. pfa_gap_step_alignment_new_scaleindex + S (pfp_index_step_alignment_new_scale) = (L)) -> exists pfp_source_step_alignment_new_scale pfp_value_step_alignment_new_scale. ((((exists ff_h_pfp_step_alignment_new_scalesource. ff_h_pfp_step_alignment_new_scalesource + S (pfp_source_step_alignment_new_scale) = S ((S (pfp_index_step_alignment_new_scale)) * ac)) /\ exists ff_q_pfp_step_alignment_new_scalesource. ab = ff_q_pfp_step_alignment_new_scalesource * S ((S (pfp_index_step_alignment_new_scale)) * ac) + (pfp_source_step_alignment_new_scale))) /\ (((((exists ff_h_pfp_step_alignment_new_scaletarget. ff_h_pfp_step_alignment_new_scaletarget + S (pfp_value_step_alignment_new_scale) = S ((S (pfp_index_step_alignment_new_scale)) * v1c)) /\ exists ff_q_pfp_step_alignment_new_scaletarget. v1b = ff_q_pfp_step_alignment_new_scaletarget * S ((S (pfp_index_step_alignment_new_scale)) * v1c) + (pfp_value_step_alignment_new_scale))) /\ ((((exists pfa_gap_step_alignment_new_scaleoperationleft. pfa_gap_step_alignment_new_scaleoperationleft + S (c) = (p)) /\ (((exists pfa_gap_step_alignment_new_scaleoperationright. pfa_gap_step_alignment_new_scaleoperationright + S (pfp_source_step_alignment_new_scale) = (p)) /\ ((((exists pfa_gap_step_alignment_new_scaleoperationresultbound. pfa_gap_step_alignment_new_scaleoperationresultbound + S (pfp_value_step_alignment_new_scale) = (p)) /\ ((exists pfa_offset_left_step_alignment_new_scaleoperationresultcongruence pfa_offset_right_step_alignment_new_scaleoperationresultcongruence. ((c) * (pfp_source_step_alignment_new_scale)) + (p) * pfa_offset_left_step_alignment_new_scaleoperationresultcongruence = (pfp_value_step_alignment_new_scale) + (p) * pfa_offset_right_step_alignment_new_scaleoperationresultcongruence))))))))))))))))) -> (((forall pfp_repeat_index_step_alignment_new_leftzeros. (exists pfa_gap_step_alignment_new_leftzerosindex. pfa_gap_step_alignment_new_leftzerosindex + S (pfp_repeat_index_step_alignment_new_leftzeros) = (L)) -> (((exists ff_h_pfp_step_alignment_new_leftzerosentry. ff_h_pfp_step_alignment_new_leftzerosentry + S (0) = S ((S (pfp_repeat_index_step_alignment_new_leftzeros)) * UP1c)) /\ exists ff_q_pfp_step_alignment_new_leftzerosentry. UP1b = ff_q_pfp_step_alignment_new_leftzerosentry * S ((S (pfp_repeat_index_step_alignment_new_leftzeros)) * UP1c) + (0)))) /\ ((forall pfrep_index_step_alignment_new_left pfrep_value_step_alignment_new_left. (exists pfa_gap_step_alignment_new_leftbound. pfa_gap_step_alignment_new_leftbound + S (pfrep_index_step_alignment_new_left) = (S N1)) -> (((exists ff_h_pfp_step_alignment_new_leftinput. ff_h_pfp_step_alignment_new_leftinput + S (pfrep_value_step_alignment_new_left) = S ((S (pfrep_index_step_alignment_new_left)) * u1c)) /\ exists ff_q_pfp_step_alignment_new_leftinput. u1b = ff_q_pfp_step_alignment_new_leftinput * S ((S (pfrep_index_step_alignment_new_left)) * u1c) + (pfrep_value_step_alignment_new_left))) -> (((exists ff_h_pfp_step_alignment_new_leftoutput. ff_h_pfp_step_alignment_new_leftoutput + S (pfrep_value_step_alignment_new_left) = S ((S ((L)+pfrep_index_step_alignment_new_left)) * UP1c)) /\ exists ff_q_pfp_step_alignment_new_leftoutput. UP1b = ff_q_pfp_step_alignment_new_leftoutput * S ((S ((L)+pfrep_index_step_alignment_new_left)) * UP1c) + (pfrep_value_step_alignment_new_left))))))) -> (((forall pfp_repeat_index_step_alignment_new_rightzeros. (exists pfa_gap_step_alignment_new_rightzerosindex. pfa_gap_step_alignment_new_rightzerosindex + S (pfp_repeat_index_step_alignment_new_rightzeros) = (S N1)) -> (((exists ff_h_pfp_step_alignment_new_rightzerosentry. ff_h_pfp_step_alignment_new_rightzerosentry + S (0) = S ((S (pfp_repeat_index_step_alignment_new_rightzeros)) * VP1c)) /\ exists ff_q_pfp_step_alignment_new_rightzerosentry. VP1b = ff_q_pfp_step_alignment_new_rightzerosentry * S ((S (pfp_repeat_index_step_alignment_new_rightzeros)) * VP1c) + (0)))) /\ ((forall pfrep_index_step_alignment_new_right pfrep_value_step_alignment_new_right. (exists pfa_gap_step_alignment_new_rightbound. pfa_gap_step_alignment_new_rightbound + S (pfrep_index_step_alignment_new_right) = (L)) -> (((exists ff_h_pfp_step_alignment_new_rightinput. ff_h_pfp_step_alignment_new_rightinput + S (pfrep_value_step_alignment_new_right) = S ((S (pfrep_index_step_alignment_new_right)) * v1c)) /\ exists ff_q_pfp_step_alignment_new_rightinput. v1b = ff_q_pfp_step_alignment_new_rightinput * S ((S (pfrep_index_step_alignment_new_right)) * v1c) + (pfrep_value_step_alignment_new_right))) -> (((exists ff_h_pfp_step_alignment_new_rightoutput. ff_h_pfp_step_alignment_new_rightoutput + S (pfrep_value_step_alignment_new_right) = S ((S ((S N1)+pfrep_index_step_alignment_new_right)) * VP1c)) /\ exists ff_q_pfp_step_alignment_new_rightoutput. VP1b = ff_q_pfp_step_alignment_new_rightoutput * S ((S ((S N1)+pfrep_index_step_alignment_new_right)) * VP1c) + (pfrep_value_step_alignment_new_right))))))) -> (forall pfp_index_step_alignment_new_sum. (exists pfa_gap_step_alignment_new_sumindex. pfa_gap_step_alignment_new_sumindex + S (pfp_index_step_alignment_new_sum) = (L+S N1)) -> exists pfp_left_step_alignment_new_sum pfp_right_step_alignment_new_sum pfp_value_step_alignment_new_sum. ((((exists ff_h_pfp_step_alignment_new_sumleft. ff_h_pfp_step_alignment_new_sumleft + S (pfp_left_step_alignment_new_sum) = S ((S (pfp_index_step_alignment_new_sum)) * UP1c)) /\ exists ff_q_pfp_step_alignment_new_sumleft. UP1b = ff_q_pfp_step_alignment_new_sumleft * S ((S (pfp_index_step_alignment_new_sum)) * UP1c) + (pfp_left_step_alignment_new_sum))) /\ (((((exists ff_h_pfp_step_alignment_new_sumright. ff_h_pfp_step_alignment_new_sumright + S (pfp_right_step_alignment_new_sum) = S ((S (pfp_index_step_alignment_new_sum)) * VP1c)) /\ exists ff_q_pfp_step_alignment_new_sumright. VP1b = ff_q_pfp_step_alignment_new_sumright * S ((S (pfp_index_step_alignment_new_sum)) * VP1c) + (pfp_right_step_alignment_new_sum))) /\ (((((exists ff_h_pfp_step_alignment_new_sumtarget. ff_h_pfp_step_alignment_new_sumtarget + S (pfp_value_step_alignment_new_sum) = S ((S (pfp_index_step_alignment_new_sum)) * z1c)) /\ exists ff_q_pfp_step_alignment_new_sumtarget. z1b = ff_q_pfp_step_alignment_new_sumtarget * S ((S (pfp_index_step_alignment_new_sum)) * z1c) + (pfp_value_step_alignment_new_sum))) /\ ((((exists pfa_gap_step_alignment_new_sumoperationleft. pfa_gap_step_alignment_new_sumoperationleft + S (pfp_left_step_alignment_new_sum) = (p)) /\ (((exists pfa_gap_step_alignment_new_sumoperationright. pfa_gap_step_alignment_new_sumoperationright + S (pfp_right_step_alignment_new_sum) = (p)) /\ ((((exists pfa_gap_step_alignment_new_sumoperationresultbound. pfa_gap_step_alignment_new_sumoperationresultbound + S (pfp_value_step_alignment_new_sum) = (p)) /\ ((exists pfa_offset_left_step_alignment_new_sumoperationresultcongruence pfa_offset_right_step_alignment_new_sumoperationresultcongruence. ((pfp_left_step_alignment_new_sum) + (pfp_right_step_alignment_new_sum)) + (p) * pfa_offset_left_step_alignment_new_sumoperationresultcongruence = (pfp_value_step_alignment_new_sum) + (p) * pfa_offset_right_step_alignment_new_sumoperationresultcongruence)))))))))))))))) -> (forall pfrep_power_step_alignment_result pfrep_left_step_alignment_result pfrep_right_step_alignment_result. ((exists pfrep_position_step_alignment_resultfirst. ((pfrep_position_step_alignment_resultfirst+S (pfrep_power_step_alignment_result)=(L+S N0)) /\ ((((exists ff_h_pfp_step_alignment_resultfirstentry. ff_h_pfp_step_alignment_resultfirstentry + S (pfrep_left_step_alignment_result) = S ((S (pfrep_position_step_alignment_resultfirst)) * z0c)) /\ exists ff_q_pfp_step_alignment_resultfirstentry. z0b = ff_q_pfp_step_alignment_resultfirstentry * S ((S (pfrep_position_step_alignment_resultfirst)) * z0c) + (pfrep_left_step_alignment_result)))))) \/ (((exists pfrep_gap_step_alignment_resultfirstoutside. pfrep_gap_step_alignment_resultfirstoutside+(L+S N0)=(pfrep_power_step_alignment_result)) /\ (((pfrep_left_step_alignment_result)=0))))) -> ((exists pfrep_position_step_alignment_resultsecond. ((pfrep_position_step_alignment_resultsecond+S (pfrep_power_step_alignment_result)=(L+S N1)) /\ ((((exists ff_h_pfp_step_alignment_resultsecondentry. ff_h_pfp_step_alignment_resultsecondentry + S (pfrep_right_step_alignment_result) = S ((S (pfrep_position_step_alignment_resultsecond)) * z1c)) /\ exists ff_q_pfp_step_alignment_resultsecondentry. z1b = ff_q_pfp_step_alignment_resultsecondentry * S ((S (pfrep_position_step_alignment_resultsecond)) * z1c) + (pfrep_right_step_alignment_result)))))) \/ (((exists pfrep_gap_step_alignment_resultsecondoutside. pfrep_gap_step_alignment_resultsecondoutside+(L+S N1)=(pfrep_power_step_alignment_result)) /\ (((pfrep_right_step_alignment_result)=0))))) -> pfrep_left_step_alignment_result=pfrep_right_step_alignment_result)

Complete tactic proof in conservative notation

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

214 script commands · 26 reading checkpoints · 13 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 shift equivalent congruent
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro c
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro L
  6. L6
    intro b0
  7. L7
    intro c0
  8. L8
    intro N0
  9. L9
    intro b1
  10. L10
    intro c1
02Fix variables and assumptionsL11–20

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

  1. L11
    intro N1
  2. L12
    intro u0b
  3. L13
    intro u0c
  4. L14
    intro v0b
  5. L15
    intro v0c
  6. L16
    intro UP0b
  7. L17
    intro UP0c
  8. L18
    intro VP0b
  9. L19
    intro VP0c
  10. L20
    intro z0b
03Fix variables and assumptionsL21–30

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

  1. L21
    intro z0c
  2. L22
    intro u1b
  3. L23
    intro u1c
  4. L24
    intro v1b
  5. L25
    intro v1c
  6. L26
    intro UP1b
  7. L27
    intro UP1c
  8. L28
    intro VP1b
  9. L29
    intro VP1c
  10. L30
    intro z1b
04Fix variables and assumptionsL31–40

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

  1. L31
    intro z1c
  2. L32
    intro hp
  3. L33
    intro he
  4. L34
    intro hU0
  5. L35
    intro hV0
  6. L36
    intro hUP0
  7. L37
    intro hVP0
  8. L38
    intro hZ0
  9. L39
    intro hU1
  10. L40
    intro hV1
05Fix variables and assumptionsL41–43

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

  1. L41
    intro hUP1
  2. L42
    intro hVP1
  3. L43
    intro hZ1
06Establish hshiftedL44–53

Establish this local claim before using it. It is not an additional assumption.

  1. L44
    have hshifted : PolynomialEquivalent(u0b,u0c,S N0,u1b,u1c,S N1)Definitions: PolynomialEquivalent(u0b,u0c,S N0,u1b,u1c,S N1)Original native command in the exact edition
  2. L45
    specialize prime_field_polynomial_shift_equivalent_congruent (b0)
  3. L46
    specialize prime_field_polynomial_shift_equivalent_congruent (c0)
  4. L47
    specialize prime_field_polynomial_shift_equivalent_congruent (N0)
  5. L48
    specialize prime_field_polynomial_shift_equivalent_congruent (b1)
  6. L49
    specialize prime_field_polynomial_shift_equivalent_congruent (c1)
  7. L50
    specialize prime_field_polynomial_shift_equivalent_congruent (N1)
  8. L51
    specialize prime_field_polynomial_shift_equivalent_congruent (u0b)
  9. L52
    specialize prime_field_polynomial_shift_equivalent_congruent (u0c)
  10. L53
    specialize prime_field_polynomial_shift_equivalent_congruent (u1b)
07Use earlier factsL54–58

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

  1. L54
    specialize prime_field_polynomial_shift_equivalent_congruent (u1c)
  2. L55
    apply prime_field_polynomial_shift_equivalent_congruent
  3. L56
    exact he
  4. L57
    exact hU0
  5. L58
    exact hU1
08Establish hscaledL59–68

Establish this local claim before using it. It is not an additional assumption.

  1. L59
    have hscaled : BetaPrefixEqual(v0b,v0c,v1b,v1c,L)Definitions: BetaPrefixEqual(v0b,v0c,v1b,v1c,L)Original native command in the exact edition
  2. L60
    specialize prime_field_polynomial_scale_functional (p)
  3. L61
    specialize prime_field_polynomial_scale_functional (c)
  4. L62
    specialize prime_field_polynomial_scale_functional (ab)
  5. L63
    specialize prime_field_polynomial_scale_functional (ac)
  6. L64
    specialize prime_field_polynomial_scale_functional (v0b)
  7. L65
    specialize prime_field_polynomial_scale_functional (v0c)
  8. L66
    specialize prime_field_polynomial_scale_functional (v1b)
  9. L67
    specialize prime_field_polynomial_scale_functional (v1c)
  10. L68
    specialize prime_field_polynomial_scale_functional (L)
09Use earlier factsL69–71

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

  1. L69
    apply prime_field_polynomial_scale_functional
  2. L70
    exact hV0
  3. L71
    exact hV1
10Establish hscalar_equalL72–79

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial equal implies equivalent.

  1. L72
    have hscalar_equal : PolynomialEquivalent(v0b,v0c,L,v1b,v1c,L)Definitions: PolynomialEquivalent(v0b,v0c,L,v1b,v1c,L)Original native command in the exact edition
  2. L73
    specialize prime_field_polynomial_equal_implies_equivalent (v0b)
  3. L74
    specialize prime_field_polynomial_equal_implies_equivalent (v0c)
  4. L75
    specialize prime_field_polynomial_equal_implies_equivalent (v1b)
  5. L76
    specialize prime_field_polynomial_equal_implies_equivalent (v1c)
  6. L77
    specialize prime_field_polynomial_equal_implies_equivalent (L)
  7. L78
    apply prime_field_polynomial_equal_implies_equivalent
  8. L79
    exact hscaled
11Establish hpad_left0L80–88

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial left pad equivalent.

  1. L80
    have hpad_left0 : PolynomialEquivalent(u0b,u0c,S N0,UP0b,UP0c,L + S N0)Definitions: PolynomialEquivalent(u0b,u0c,S N0,UP0b,UP0c,L + S N0)Original native command in the exact edition
  2. L81
    specialize prime_field_polynomial_left_pad_equivalent (u0b)
  3. L82
    specialize prime_field_polynomial_left_pad_equivalent (u0c)
  4. L83
    specialize prime_field_polynomial_left_pad_equivalent (S N0)
  5. L84
    specialize prime_field_polynomial_left_pad_equivalent (L)
  6. L85
    specialize prime_field_polynomial_left_pad_equivalent (UP0b)
  7. L86
    specialize prime_field_polynomial_left_pad_equivalent (UP0c)
  8. L87
    apply prime_field_polynomial_left_pad_equivalent
  9. L88
    exact hUP0
12Establish hpad_left1L89–97

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial left pad equivalent.

  1. L89
    have hpad_left1 : PolynomialEquivalent(u1b,u1c,S N1,UP1b,UP1c,L + S N1)Definitions: PolynomialEquivalent(u1b,u1c,S N1,UP1b,UP1c,L + S N1)Original native command in the exact edition
  2. L90
    specialize prime_field_polynomial_left_pad_equivalent (u1b)
  3. L91
    specialize prime_field_polynomial_left_pad_equivalent (u1c)
  4. L92
    specialize prime_field_polynomial_left_pad_equivalent (S N1)
  5. L93
    specialize prime_field_polynomial_left_pad_equivalent (L)
  6. L94
    specialize prime_field_polynomial_left_pad_equivalent (UP1b)
  7. L95
    specialize prime_field_polynomial_left_pad_equivalent (UP1c)
  8. L96
    apply prime_field_polynomial_left_pad_equivalent
  9. L97
    exact hUP1
13Establish hpad_right0L98–106

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial left pad equivalent.

  1. L98
    have hpad_right0 : PolynomialEquivalent(v0b,v0c,L,VP0b,VP0c,S N0 + L)Definitions: PolynomialEquivalent(v0b,v0c,L,VP0b,VP0c,S N0 + L)Original native command in the exact edition
  2. L99
    specialize prime_field_polynomial_left_pad_equivalent (v0b)
  3. L100
    specialize prime_field_polynomial_left_pad_equivalent (v0c)
  4. L101
    specialize prime_field_polynomial_left_pad_equivalent (L)
  5. L102
    specialize prime_field_polynomial_left_pad_equivalent (S N0)
  6. L103
    specialize prime_field_polynomial_left_pad_equivalent (VP0b)
  7. L104
    specialize prime_field_polynomial_left_pad_equivalent (VP0c)
  8. L105
    apply prime_field_polynomial_left_pad_equivalent
  9. L106
    exact hVP0
14Establish hcomm_right0L107–112

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add comm.

  1. L107
    have hcomm_right0 : S N0+L=L+S N0
  2. L108
    specialize add_comm (S N0)
  3. L109
    specialize add_comm (L)
  4. L110
    apply add_comm
  5. L111
    rewrite hcomm_right0 at hpad_right0
  6. L112
    rewrite hcomm_right0 at hpad_right0
15Establish hpad_right1L113–121

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial left pad equivalent.

  1. L113
    have hpad_right1 : PolynomialEquivalent(v1b,v1c,L,VP1b,VP1c,S N1 + L)Definitions: PolynomialEquivalent(v1b,v1c,L,VP1b,VP1c,S N1 + L)Original native command in the exact edition
  2. L114
    specialize prime_field_polynomial_left_pad_equivalent (v1b)
  3. L115
    specialize prime_field_polynomial_left_pad_equivalent (v1c)
  4. L116
    specialize prime_field_polynomial_left_pad_equivalent (L)
  5. L117
    specialize prime_field_polynomial_left_pad_equivalent (S N1)
  6. L118
    specialize prime_field_polynomial_left_pad_equivalent (VP1b)
  7. L119
    specialize prime_field_polynomial_left_pad_equivalent (VP1c)
  8. L120
    apply prime_field_polynomial_left_pad_equivalent
  9. L121
    exact hVP1
16Establish hcomm_right1L122–127

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add comm.

  1. L122
    have hcomm_right1 : S N1+L=L+S N1
  2. L123
    specialize add_comm (S N1)
  3. L124
    specialize add_comm (L)
  4. L125
    apply add_comm
  5. L126
    rewrite hcomm_right1 at hpad_right1
  6. L127
    rewrite hcomm_right1 at hpad_right1
17Establish hmiddle_leftL128–137

Establish this local claim before using it. It is not an additional assumption.

  1. L128
    have hmiddle_left : PolynomialEquivalent(UP0b,UP0c,L + S N0,u1b,u1c,S N1)Definitions: PolynomialEquivalent(UP0b,UP0c,L + S N0,u1b,u1c,S N1)Original native command in the exact edition
  2. L129
    specialize prime_field_polynomial_equivalent_transitive (UP0b)
  3. L130
    specialize prime_field_polynomial_equivalent_transitive (UP0c)
  4. L131
    specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  5. L132
    specialize prime_field_polynomial_equivalent_transitive (u0b)
  6. L133
    specialize prime_field_polynomial_equivalent_transitive (u0c)
  7. L134
    specialize prime_field_polynomial_equivalent_transitive (S N0)
  8. L135
    specialize prime_field_polynomial_equivalent_transitive (u1b)
  9. L136
    specialize prime_field_polynomial_equivalent_transitive (u1c)
  10. L137
    specialize prime_field_polynomial_equivalent_transitive (S N1)
18Use earlier factsL138–147

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

  1. L138
    apply prime_field_polynomial_equivalent_transitive
  2. L139
    specialize prime_field_polynomial_equivalent_symmetric (u0b)
  3. L140
    specialize prime_field_polynomial_equivalent_symmetric (u0c)
  4. L141
    specialize prime_field_polynomial_equivalent_symmetric (S N0)
  5. L142
    specialize prime_field_polynomial_equivalent_symmetric (UP0b)
  6. L143
    specialize prime_field_polynomial_equivalent_symmetric (UP0c)
  7. L144
    specialize prime_field_polynomial_equivalent_symmetric (L+S N0)
  8. L145
    apply prime_field_polynomial_equivalent_symmetric
  9. L146
    exact hpad_left0
  10. L147
    exact hshifted
19Establish hequal_leftL148–157

Establish this local claim before using it. It is not an additional assumption.

  1. L148
    have hequal_left : PolynomialEquivalent(UP0b,UP0c,L + S N0,UP1b,UP1c,L + S N1)Definitions: PolynomialEquivalent(UP0b,UP0c,L + S N0,UP1b,UP1c,L + S N1)Original native command in the exact edition
  2. L149
    specialize prime_field_polynomial_equivalent_transitive (UP0b)
  3. L150
    specialize prime_field_polynomial_equivalent_transitive (UP0c)
  4. L151
    specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  5. L152
    specialize prime_field_polynomial_equivalent_transitive (u1b)
  6. L153
    specialize prime_field_polynomial_equivalent_transitive (u1c)
  7. L154
    specialize prime_field_polynomial_equivalent_transitive (S N1)
  8. L155
    specialize prime_field_polynomial_equivalent_transitive (UP1b)
  9. L156
    specialize prime_field_polynomial_equivalent_transitive (UP1c)
  10. L157
    specialize prime_field_polynomial_equivalent_transitive (L+S N1)
20Use earlier factsL158–160

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

  1. L158
    apply prime_field_polynomial_equivalent_transitive
  2. L159
    exact hmiddle_left
  3. L160
    exact hpad_left1
21Establish hmiddle_rightL161–170

Establish this local claim before using it. It is not an additional assumption.

  1. L161
    have hmiddle_right : PolynomialEquivalent(VP0b,VP0c,L + S N0,v1b,v1c,L)Definitions: PolynomialEquivalent(VP0b,VP0c,L + S N0,v1b,v1c,L)Original native command in the exact edition
  2. L162
    specialize prime_field_polynomial_equivalent_transitive (VP0b)
  3. L163
    specialize prime_field_polynomial_equivalent_transitive (VP0c)
  4. L164
    specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  5. L165
    specialize prime_field_polynomial_equivalent_transitive (v0b)
  6. L166
    specialize prime_field_polynomial_equivalent_transitive (v0c)
  7. L167
    specialize prime_field_polynomial_equivalent_transitive (L)
  8. L168
    specialize prime_field_polynomial_equivalent_transitive (v1b)
  9. L169
    specialize prime_field_polynomial_equivalent_transitive (v1c)
  10. L170
    specialize prime_field_polynomial_equivalent_transitive (L)
22Use earlier factsL171–180

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

  1. L171
    apply prime_field_polynomial_equivalent_transitive
  2. L172
    specialize prime_field_polynomial_equivalent_symmetric (v0b)
  3. L173
    specialize prime_field_polynomial_equivalent_symmetric (v0c)
  4. L174
    specialize prime_field_polynomial_equivalent_symmetric (L)
  5. L175
    specialize prime_field_polynomial_equivalent_symmetric (VP0b)
  6. L176
    specialize prime_field_polynomial_equivalent_symmetric (VP0c)
  7. L177
    specialize prime_field_polynomial_equivalent_symmetric (L+S N0)
  8. L178
    apply prime_field_polynomial_equivalent_symmetric
  9. L179
    exact hpad_right0
  10. L180
    exact hscalar_equal
23Establish hequal_rightL181–190

Establish this local claim before using it. It is not an additional assumption.

  1. L181
    have hequal_right : PolynomialEquivalent(VP0b,VP0c,L + S N0,VP1b,VP1c,L + S N1)Definitions: PolynomialEquivalent(VP0b,VP0c,L + S N0,VP1b,VP1c,L + S N1)Original native command in the exact edition
  2. L182
    specialize prime_field_polynomial_equivalent_transitive (VP0b)
  3. L183
    specialize prime_field_polynomial_equivalent_transitive (VP0c)
  4. L184
    specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  5. L185
    specialize prime_field_polynomial_equivalent_transitive (v1b)
  6. L186
    specialize prime_field_polynomial_equivalent_transitive (v1c)
  7. L187
    specialize prime_field_polynomial_equivalent_transitive (L)
  8. L188
    specialize prime_field_polynomial_equivalent_transitive (VP1b)
  9. L189
    specialize prime_field_polynomial_equivalent_transitive (VP1c)
  10. L190
    specialize prime_field_polynomial_equivalent_transitive (L+S N1)
24Use earlier factsL191–200

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

  1. L191
    apply prime_field_polynomial_equivalent_transitive
  2. L192
    exact hmiddle_right
  3. L193
    exact hpad_right1
  4. L194
    specialize prime_field_polynomial_add_equivalent_congruent (p)
  5. L195
    specialize prime_field_polynomial_add_equivalent_congruent (UP0b)
  6. L196
    specialize prime_field_polynomial_add_equivalent_congruent (UP0c)
  7. L197
    specialize prime_field_polynomial_add_equivalent_congruent (VP0b)
  8. L198
    specialize prime_field_polynomial_add_equivalent_congruent (VP0c)
  9. L199
    specialize prime_field_polynomial_add_equivalent_congruent (z0b)
  10. L200
    specialize prime_field_polynomial_add_equivalent_congruent (z0c)
25Use earlier factsL201–210

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

  1. L201
    specialize prime_field_polynomial_add_equivalent_congruent (L+S N0)
  2. L202
    specialize prime_field_polynomial_add_equivalent_congruent (UP1b)
  3. L203
    specialize prime_field_polynomial_add_equivalent_congruent (UP1c)
  4. L204
    specialize prime_field_polynomial_add_equivalent_congruent (VP1b)
  5. L205
    specialize prime_field_polynomial_add_equivalent_congruent (VP1c)
  6. L206
    specialize prime_field_polynomial_add_equivalent_congruent (z1b)
  7. L207
    specialize prime_field_polynomial_add_equivalent_congruent (z1c)
  8. L208
    specialize prime_field_polynomial_add_equivalent_congruent (L+S N1)
  9. L209
    apply prime_field_polynomial_add_equivalent_congruent
  10. L210
    exact hp
26Use earlier factsL211–214

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

  1. L211
    exact hequal_left
  2. L212
    exact hequal_right
  3. L213
    exact hZ0
  4. L214
    exact hZ1

Library-wide reading audit

Original defined command ledger · 214 lines
  1. 0001intro p
  2. 0002intro c
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro L
  6. 0006intro b0
  7. 0007intro c0
  8. 0008intro N0
  9. 0009intro b1
  10. 0010intro c1
  11. 0011intro N1
  12. 0012intro u0b
  13. 0013intro u0c
  14. 0014intro v0b
  15. 0015intro v0c
  16. 0016intro UP0b
  17. 0017intro UP0c
  18. 0018intro VP0b
  19. 0019intro VP0c
  20. 0020intro z0b
  21. 0021intro z0c
  22. 0022intro u1b
  23. 0023intro u1c
  24. 0024intro v1b
  25. 0025intro v1c
  26. 0026intro UP1b
  27. 0027intro UP1c
  28. 0028intro VP1b
  29. 0029intro VP1c
  30. 0030intro z1b
  31. 0031intro z1c
  32. 0032intro hp
  33. 0033intro he
  34. 0034intro hU0
  35. 0035intro hV0
  36. 0036intro hUP0
  37. 0037intro hVP0
  38. 0038intro hZ0
  39. 0039intro hU1
  40. 0040intro hV1
  41. 0041intro hUP1
  42. 0042intro hVP1
  43. 0043intro hZ1
  44. 0044have hshifted : PolynomialEquivalent(u0b,u0c,S N0,u1b,u1c,S N1)
  45. 0045specialize prime_field_polynomial_shift_equivalent_congruent (b0)
  46. 0046specialize prime_field_polynomial_shift_equivalent_congruent (c0)
  47. 0047specialize prime_field_polynomial_shift_equivalent_congruent (N0)
  48. 0048specialize prime_field_polynomial_shift_equivalent_congruent (b1)
  49. 0049specialize prime_field_polynomial_shift_equivalent_congruent (c1)
  50. 0050specialize prime_field_polynomial_shift_equivalent_congruent (N1)
  51. 0051specialize prime_field_polynomial_shift_equivalent_congruent (u0b)
  52. 0052specialize prime_field_polynomial_shift_equivalent_congruent (u0c)
  53. 0053specialize prime_field_polynomial_shift_equivalent_congruent (u1b)
  54. 0054specialize prime_field_polynomial_shift_equivalent_congruent (u1c)
  55. 0055apply prime_field_polynomial_shift_equivalent_congruent
  56. 0056exact he
  57. 0057exact hU0
  58. 0058exact hU1
  59. 0059have hscaled : BetaPrefixEqual(v0b,v0c,v1b,v1c,L)
  60. 0060specialize prime_field_polynomial_scale_functional (p)
  61. 0061specialize prime_field_polynomial_scale_functional (c)
  62. 0062specialize prime_field_polynomial_scale_functional (ab)
  63. 0063specialize prime_field_polynomial_scale_functional (ac)
  64. 0064specialize prime_field_polynomial_scale_functional (v0b)
  65. 0065specialize prime_field_polynomial_scale_functional (v0c)
  66. 0066specialize prime_field_polynomial_scale_functional (v1b)
  67. 0067specialize prime_field_polynomial_scale_functional (v1c)
  68. 0068specialize prime_field_polynomial_scale_functional (L)
  69. 0069apply prime_field_polynomial_scale_functional
  70. 0070exact hV0
  71. 0071exact hV1
  72. 0072have hscalar_equal : PolynomialEquivalent(v0b,v0c,L,v1b,v1c,L)
  73. 0073specialize prime_field_polynomial_equal_implies_equivalent (v0b)
  74. 0074specialize prime_field_polynomial_equal_implies_equivalent (v0c)
  75. 0075specialize prime_field_polynomial_equal_implies_equivalent (v1b)
  76. 0076specialize prime_field_polynomial_equal_implies_equivalent (v1c)
  77. 0077specialize prime_field_polynomial_equal_implies_equivalent (L)
  78. 0078apply prime_field_polynomial_equal_implies_equivalent
  79. 0079exact hscaled
  80. 0080have hpad_left0 : PolynomialEquivalent(u0b,u0c,S N0,UP0b,UP0c,L + S N0)
  81. 0081specialize prime_field_polynomial_left_pad_equivalent (u0b)
  82. 0082specialize prime_field_polynomial_left_pad_equivalent (u0c)
  83. 0083specialize prime_field_polynomial_left_pad_equivalent (S N0)
  84. 0084specialize prime_field_polynomial_left_pad_equivalent (L)
  85. 0085specialize prime_field_polynomial_left_pad_equivalent (UP0b)
  86. 0086specialize prime_field_polynomial_left_pad_equivalent (UP0c)
  87. 0087apply prime_field_polynomial_left_pad_equivalent
  88. 0088exact hUP0
  89. 0089have hpad_left1 : PolynomialEquivalent(u1b,u1c,S N1,UP1b,UP1c,L + S N1)
  90. 0090specialize prime_field_polynomial_left_pad_equivalent (u1b)
  91. 0091specialize prime_field_polynomial_left_pad_equivalent (u1c)
  92. 0092specialize prime_field_polynomial_left_pad_equivalent (S N1)
  93. 0093specialize prime_field_polynomial_left_pad_equivalent (L)
  94. 0094specialize prime_field_polynomial_left_pad_equivalent (UP1b)
  95. 0095specialize prime_field_polynomial_left_pad_equivalent (UP1c)
  96. 0096apply prime_field_polynomial_left_pad_equivalent
  97. 0097exact hUP1
  98. 0098have hpad_right0 : PolynomialEquivalent(v0b,v0c,L,VP0b,VP0c,S N0 + L)
  99. 0099specialize prime_field_polynomial_left_pad_equivalent (v0b)
  100. 0100specialize prime_field_polynomial_left_pad_equivalent (v0c)
  101. 0101specialize prime_field_polynomial_left_pad_equivalent (L)
  102. 0102specialize prime_field_polynomial_left_pad_equivalent (S N0)
  103. 0103specialize prime_field_polynomial_left_pad_equivalent (VP0b)
  104. 0104specialize prime_field_polynomial_left_pad_equivalent (VP0c)
  105. 0105apply prime_field_polynomial_left_pad_equivalent
  106. 0106exact hVP0
  107. 0107have hcomm_right0 : S N0+L=L+S N0
  108. 0108specialize add_comm (S N0)
  109. 0109specialize add_comm (L)
  110. 0110apply add_comm
  111. 0111rewrite hcomm_right0 at hpad_right0
  112. 0112rewrite hcomm_right0 at hpad_right0
  113. 0113have hpad_right1 : PolynomialEquivalent(v1b,v1c,L,VP1b,VP1c,S N1 + L)
  114. 0114specialize prime_field_polynomial_left_pad_equivalent (v1b)
  115. 0115specialize prime_field_polynomial_left_pad_equivalent (v1c)
  116. 0116specialize prime_field_polynomial_left_pad_equivalent (L)
  117. 0117specialize prime_field_polynomial_left_pad_equivalent (S N1)
  118. 0118specialize prime_field_polynomial_left_pad_equivalent (VP1b)
  119. 0119specialize prime_field_polynomial_left_pad_equivalent (VP1c)
  120. 0120apply prime_field_polynomial_left_pad_equivalent
  121. 0121exact hVP1
  122. 0122have hcomm_right1 : S N1+L=L+S N1
  123. 0123specialize add_comm (S N1)
  124. 0124specialize add_comm (L)
  125. 0125apply add_comm
  126. 0126rewrite hcomm_right1 at hpad_right1
  127. 0127rewrite hcomm_right1 at hpad_right1
  128. 0128have hmiddle_left : PolynomialEquivalent(UP0b,UP0c,L + S N0,u1b,u1c,S N1)
  129. 0129specialize prime_field_polynomial_equivalent_transitive (UP0b)
  130. 0130specialize prime_field_polynomial_equivalent_transitive (UP0c)
  131. 0131specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  132. 0132specialize prime_field_polynomial_equivalent_transitive (u0b)
  133. 0133specialize prime_field_polynomial_equivalent_transitive (u0c)
  134. 0134specialize prime_field_polynomial_equivalent_transitive (S N0)
  135. 0135specialize prime_field_polynomial_equivalent_transitive (u1b)
  136. 0136specialize prime_field_polynomial_equivalent_transitive (u1c)
  137. 0137specialize prime_field_polynomial_equivalent_transitive (S N1)
  138. 0138apply prime_field_polynomial_equivalent_transitive
  139. 0139specialize prime_field_polynomial_equivalent_symmetric (u0b)
  140. 0140specialize prime_field_polynomial_equivalent_symmetric (u0c)
  141. 0141specialize prime_field_polynomial_equivalent_symmetric (S N0)
  142. 0142specialize prime_field_polynomial_equivalent_symmetric (UP0b)
  143. 0143specialize prime_field_polynomial_equivalent_symmetric (UP0c)
  144. 0144specialize prime_field_polynomial_equivalent_symmetric (L+S N0)
  145. 0145apply prime_field_polynomial_equivalent_symmetric
  146. 0146exact hpad_left0
  147. 0147exact hshifted
  148. 0148have hequal_left : PolynomialEquivalent(UP0b,UP0c,L + S N0,UP1b,UP1c,L + S N1)
  149. 0149specialize prime_field_polynomial_equivalent_transitive (UP0b)
  150. 0150specialize prime_field_polynomial_equivalent_transitive (UP0c)
  151. 0151specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  152. 0152specialize prime_field_polynomial_equivalent_transitive (u1b)
  153. 0153specialize prime_field_polynomial_equivalent_transitive (u1c)
  154. 0154specialize prime_field_polynomial_equivalent_transitive (S N1)
  155. 0155specialize prime_field_polynomial_equivalent_transitive (UP1b)
  156. 0156specialize prime_field_polynomial_equivalent_transitive (UP1c)
  157. 0157specialize prime_field_polynomial_equivalent_transitive (L+S N1)
  158. 0158apply prime_field_polynomial_equivalent_transitive
  159. 0159exact hmiddle_left
  160. 0160exact hpad_left1
  161. 0161have hmiddle_right : PolynomialEquivalent(VP0b,VP0c,L + S N0,v1b,v1c,L)
  162. 0162specialize prime_field_polynomial_equivalent_transitive (VP0b)
  163. 0163specialize prime_field_polynomial_equivalent_transitive (VP0c)
  164. 0164specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  165. 0165specialize prime_field_polynomial_equivalent_transitive (v0b)
  166. 0166specialize prime_field_polynomial_equivalent_transitive (v0c)
  167. 0167specialize prime_field_polynomial_equivalent_transitive (L)
  168. 0168specialize prime_field_polynomial_equivalent_transitive (v1b)
  169. 0169specialize prime_field_polynomial_equivalent_transitive (v1c)
  170. 0170specialize prime_field_polynomial_equivalent_transitive (L)
  171. 0171apply prime_field_polynomial_equivalent_transitive
  172. 0172specialize prime_field_polynomial_equivalent_symmetric (v0b)
  173. 0173specialize prime_field_polynomial_equivalent_symmetric (v0c)
  174. 0174specialize prime_field_polynomial_equivalent_symmetric (L)
  175. 0175specialize prime_field_polynomial_equivalent_symmetric (VP0b)
  176. 0176specialize prime_field_polynomial_equivalent_symmetric (VP0c)
  177. 0177specialize prime_field_polynomial_equivalent_symmetric (L+S N0)
  178. 0178apply prime_field_polynomial_equivalent_symmetric
  179. 0179exact hpad_right0
  180. 0180exact hscalar_equal
  181. 0181have hequal_right : PolynomialEquivalent(VP0b,VP0c,L + S N0,VP1b,VP1c,L + S N1)
  182. 0182specialize prime_field_polynomial_equivalent_transitive (VP0b)
  183. 0183specialize prime_field_polynomial_equivalent_transitive (VP0c)
  184. 0184specialize prime_field_polynomial_equivalent_transitive (L+S N0)
  185. 0185specialize prime_field_polynomial_equivalent_transitive (v1b)
  186. 0186specialize prime_field_polynomial_equivalent_transitive (v1c)
  187. 0187specialize prime_field_polynomial_equivalent_transitive (L)
  188. 0188specialize prime_field_polynomial_equivalent_transitive (VP1b)
  189. 0189specialize prime_field_polynomial_equivalent_transitive (VP1c)
  190. 0190specialize prime_field_polynomial_equivalent_transitive (L+S N1)
  191. 0191apply prime_field_polynomial_equivalent_transitive
  192. 0192exact hmiddle_right
  193. 0193exact hpad_right1
  194. 0194specialize prime_field_polynomial_add_equivalent_congruent (p)
  195. 0195specialize prime_field_polynomial_add_equivalent_congruent (UP0b)
  196. 0196specialize prime_field_polynomial_add_equivalent_congruent (UP0c)
  197. 0197specialize prime_field_polynomial_add_equivalent_congruent (VP0b)
  198. 0198specialize prime_field_polynomial_add_equivalent_congruent (VP0c)
  199. 0199specialize prime_field_polynomial_add_equivalent_congruent (z0b)
  200. 0200specialize prime_field_polynomial_add_equivalent_congruent (z0c)
  201. 0201specialize prime_field_polynomial_add_equivalent_congruent (L+S N0)
  202. 0202specialize prime_field_polynomial_add_equivalent_congruent (UP1b)
  203. 0203specialize prime_field_polynomial_add_equivalent_congruent (UP1c)
  204. 0204specialize prime_field_polynomial_add_equivalent_congruent (VP1b)
  205. 0205specialize prime_field_polynomial_add_equivalent_congruent (VP1c)
  206. 0206specialize prime_field_polynomial_add_equivalent_congruent (z1b)
  207. 0207specialize prime_field_polynomial_add_equivalent_congruent (z1c)
  208. 0208specialize prime_field_polynomial_add_equivalent_congruent (L+S N1)
  209. 0209apply prime_field_polynomial_add_equivalent_congruent
  210. 0210exact hp
  211. 0211exact hequal_left
  212. 0212exact hequal_right
  213. 0213exact hZ0
  214. 0214exact hZ1