PX006E

prime_field_polynomial_convolution_left_padding_equivalent_left

Genuine leading-zero padding of the left factor preserves the formal polynomial product, including empty factors whose proper product lengths need not differ by the padding count.

Alpha v34 checked-use · first admitted v33 · 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.

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. ∀ cb. ∀ cc. ∀ N. ∀ AB. ∀ AC. ∀ t. ∀ CB. ∀ CC. ∀ K. ¬p = 0 → PolynomialLeftPad(ab,ac,L,t,AB,AC) → FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) → FpPolyProduct(p,AB,AC,t + L,bb,bc,M,CB,CC,K) → PolynomialEquivalent(cb,cc,N,CB,CC,K)

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

Definition DAG

FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) · 2PolynomialLeftPad(b,c,L,t,d,e) · 2PolynomialEquivalent(b,c,L,d,e,M) · 5Repeat(b,c,a,l) · 6

Actual proof prerequisites

eq_decidable · checked external prerequisitematrix_rank_no_index_below_zero · checked external prerequisiteprime_field_polynomial_convolution_zero_left · checked external prerequisiteprime_field_polynomial_convolution_zero_right · checked external prerequisitepolynomial_left_pad_zero_prefixprime_field_polynomial_zero_prefix_equivalent_emptyprime_field_polynomial_equivalent_transitiveprime_field_polynomial_equivalent_symmetricprime_field_polynomial_convolution_left_padding_nonempty_leftprime_field_polynomial_left_pad_equivalent
Original expanded first-order statement 
forall p ab ac L bb bc M cb cc N AB AC t CB CC K. (~(p=0)) -> (((forall pfp_repeat_index_product_factor_padding_leftzeros. (exists pfa_gap_product_factor_padding_leftzerosindex. pfa_gap_product_factor_padding_leftzerosindex + S (pfp_repeat_index_product_factor_padding_leftzeros) = (t)) -> (((exists ff_h_pfp_product_factor_padding_leftzerosentry. ff_h_pfp_product_factor_padding_leftzerosentry + S (0) = S ((S (pfp_repeat_index_product_factor_padding_leftzeros)) * AC)) /\ exists ff_q_pfp_product_factor_padding_leftzerosentry. AB = ff_q_pfp_product_factor_padding_leftzerosentry * S ((S (pfp_repeat_index_product_factor_padding_leftzeros)) * AC) + (0)))) /\ ((forall pfrep_index_product_factor_padding_left pfrep_value_product_factor_padding_left. (exists pfa_gap_product_factor_padding_leftbound. pfa_gap_product_factor_padding_leftbound + S (pfrep_index_product_factor_padding_left) = (L)) -> (((exists ff_h_pfp_product_factor_padding_leftinput. ff_h_pfp_product_factor_padding_leftinput + S (pfrep_value_product_factor_padding_left) = S ((S (pfrep_index_product_factor_padding_left)) * ac)) /\ exists ff_q_pfp_product_factor_padding_leftinput. ab = ff_q_pfp_product_factor_padding_leftinput * S ((S (pfrep_index_product_factor_padding_left)) * ac) + (pfrep_value_product_factor_padding_left))) -> (((exists ff_h_pfp_product_factor_padding_leftoutput. ff_h_pfp_product_factor_padding_leftoutput + S (pfrep_value_product_factor_padding_left) = S ((S ((t)+pfrep_index_product_factor_padding_left)) * AC)) /\ exists ff_q_pfp_product_factor_padding_leftoutput. AB = ff_q_pfp_product_factor_padding_leftoutput * S ((S ((t)+pfrep_index_product_factor_padding_left)) * AC) + (pfrep_value_product_factor_padding_left))))))) -> (((forall fom_index_pfp_product_original_leftleft. (exists fom_gap_pfp_product_original_leftleft_index_bound. fom_gap_pfp_product_original_leftleft_index_bound + S (fom_index_pfp_product_original_leftleft) = L) -> exists fom_value_pfp_product_original_leftleft. ((((exists fom_beta_height_pfp_product_original_leftleft_entry. fom_beta_height_pfp_product_original_leftleft_entry + S (fom_value_pfp_product_original_leftleft) = S ((S (fom_index_pfp_product_original_leftleft)) * ac)) /\ exists fom_beta_quotient_pfp_product_original_leftleft_entry. ab = fom_beta_quotient_pfp_product_original_leftleft_entry * S ((S (fom_index_pfp_product_original_leftleft)) * ac) + (fom_value_pfp_product_original_leftleft))) /\ (exists fom_gap_pfp_product_original_leftleft_value_bound. fom_gap_pfp_product_original_leftleft_value_bound + S (fom_value_pfp_product_original_leftleft) = p))) /\ (((forall fom_index_pfp_product_original_leftright. (exists fom_gap_pfp_product_original_leftright_index_bound. fom_gap_pfp_product_original_leftright_index_bound + S (fom_index_pfp_product_original_leftright) = M) -> exists fom_value_pfp_product_original_leftright. ((((exists fom_beta_height_pfp_product_original_leftright_entry. fom_beta_height_pfp_product_original_leftright_entry + S (fom_value_pfp_product_original_leftright) = S ((S (fom_index_pfp_product_original_leftright)) * bc)) /\ exists fom_beta_quotient_pfp_product_original_leftright_entry. bb = fom_beta_quotient_pfp_product_original_leftright_entry * S ((S (fom_index_pfp_product_original_leftright)) * bc) + (fom_value_pfp_product_original_leftright))) /\ (exists fom_gap_pfp_product_original_leftright_value_bound. fom_gap_pfp_product_original_leftright_value_bound + S (fom_value_pfp_product_original_leftright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_product_original_leftcoefficients. (exists pfa_gap_product_original_leftcoefficientsbound. pfa_gap_product_original_leftcoefficientsbound + S (pfc_index_product_original_leftcoefficients) = (N)) -> exists pfc_value_product_original_leftcoefficients. ((((exists ff_h_pfp_product_original_leftcoefficientsentry. ff_h_pfp_product_original_leftcoefficientsentry + S (pfc_value_product_original_leftcoefficients) = S ((S (pfc_index_product_original_leftcoefficients)) * cc)) /\ exists ff_q_pfp_product_original_leftcoefficientsentry. cb = ff_q_pfp_product_original_leftcoefficientsentry * S ((S (pfc_index_product_original_leftcoefficients)) * cc) + (pfc_value_product_original_leftcoefficients))) /\ ((exists pfc_terms_code_product_original_leftcoefficientscoefficient pfc_terms_scale_product_original_leftcoefficientscoefficient pfc_natural_sum_product_original_leftcoefficientscoefficient. ((forall pfc_index_product_original_leftcoefficientscoefficientdiagonal. (exists pfa_gap_product_original_leftcoefficientscoefficientdiagonalbound. pfa_gap_product_original_leftcoefficientscoefficientdiagonalbound + S (pfc_index_product_original_leftcoefficientscoefficientdiagonal) = (S (pfc_index_product_original_leftcoefficients))) -> exists pfc_value_product_original_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_product_original_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_product_original_leftcoefficientscoefficientdiagonalentry + S (pfc_value_product_original_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_product_original_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_original_leftcoefficientscoefficient)) /\ exists ff_q_pfp_product_original_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_product_original_leftcoefficientscoefficient = ff_q_pfp_product_original_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_product_original_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_original_leftcoefficientscoefficient) + (pfc_value_product_original_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_product_original_leftcoefficientscoefficientdiagonalterm pfc_left_product_original_leftcoefficientscoefficientdiagonalterm pfc_right_product_original_leftcoefficientscoefficientdiagonalterm. (((pfc_index_product_original_leftcoefficientscoefficientdiagonal)+pfc_complement_product_original_leftcoefficientscoefficientdiagonalterm=(pfc_index_product_original_leftcoefficients)) /\ ((((((exists pfa_gap_product_original_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_product_original_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_product_original_leftcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_product_original_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_product_original_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_product_original_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_product_original_leftcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_product_original_leftcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_product_original_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_product_original_leftcoefficientscoefficientdiagonal)) * ac) + (pfc_left_product_original_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_original_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_product_original_leftcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_product_original_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_product_original_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_product_original_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_product_original_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_product_original_leftcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_product_original_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_product_original_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_product_original_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_product_original_leftcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_product_original_leftcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_product_original_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_product_original_leftcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_product_original_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_original_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_product_original_leftcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_product_original_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_product_original_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_product_original_leftcoefficientscoefficientdiagonal)=pfc_left_product_original_leftcoefficientscoefficientdiagonalterm*pfc_right_product_original_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_product_original_leftcoefficientscoefficientsum fs_v_pfc_product_original_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_product_original_leftcoefficientscoefficientsum_body_start. fs_h_pfc_product_original_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_product_original_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_leftcoefficientscoefficientsum_body_start. fs_u_pfc_product_original_leftcoefficientscoefficientsum = fs_q_pfc_product_original_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_product_original_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_product_original_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_product_original_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_product_original_leftcoefficientscoefficient) = S ((S (S (pfc_index_product_original_leftcoefficients))) * fs_v_pfc_product_original_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_product_original_leftcoefficientscoefficientsum = fs_q_pfc_product_original_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_product_original_leftcoefficients))) * fs_v_pfc_product_original_leftcoefficientscoefficientsum) + (pfc_natural_sum_product_original_leftcoefficientscoefficient))) /\ forall fs_i_pfc_product_original_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_product_original_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_product_original_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_product_original_leftcoefficientscoefficientsum_body_steps = S (pfc_index_product_original_leftcoefficients)) -> exists fs_a_pfc_product_original_leftcoefficientscoefficientsum_body_steps fs_r_pfc_product_original_leftcoefficientscoefficientsum_body_steps fs_s_pfc_product_original_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_product_original_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_product_original_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_product_original_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_original_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_original_leftcoefficientscoefficient)) /\ exists fs_q_pfc_product_original_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_product_original_leftcoefficientscoefficient = fs_q_pfc_product_original_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_product_original_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_original_leftcoefficientscoefficient) + (fs_a_pfc_product_original_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_original_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_product_original_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_product_original_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_original_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_product_original_leftcoefficientscoefficientsum = fs_q_pfc_product_original_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_product_original_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_leftcoefficientscoefficientsum) + (fs_r_pfc_product_original_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_original_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_product_original_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_product_original_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_product_original_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_product_original_leftcoefficientscoefficientsum = fs_q_pfc_product_original_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_product_original_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_leftcoefficientscoefficientsum) + (fs_s_pfc_product_original_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_product_original_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_product_original_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_product_original_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_product_original_leftcoefficientscoefficientresiduebound. pfa_gap_product_original_leftcoefficientscoefficientresiduebound + S (pfc_value_product_original_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_product_original_leftcoefficientscoefficientresiduecongruence pfa_offset_right_product_original_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_product_original_leftcoefficientscoefficient) + (p) * pfa_offset_left_product_original_leftcoefficientscoefficientresiduecongruence = (pfc_value_product_original_leftcoefficients) + (p) * pfa_offset_right_product_original_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_product_padded_leftleft. (exists fom_gap_pfp_product_padded_leftleft_index_bound. fom_gap_pfp_product_padded_leftleft_index_bound + S (fom_index_pfp_product_padded_leftleft) = t+L) -> exists fom_value_pfp_product_padded_leftleft. ((((exists fom_beta_height_pfp_product_padded_leftleft_entry. fom_beta_height_pfp_product_padded_leftleft_entry + S (fom_value_pfp_product_padded_leftleft) = S ((S (fom_index_pfp_product_padded_leftleft)) * AC)) /\ exists fom_beta_quotient_pfp_product_padded_leftleft_entry. AB = fom_beta_quotient_pfp_product_padded_leftleft_entry * S ((S (fom_index_pfp_product_padded_leftleft)) * AC) + (fom_value_pfp_product_padded_leftleft))) /\ (exists fom_gap_pfp_product_padded_leftleft_value_bound. fom_gap_pfp_product_padded_leftleft_value_bound + S (fom_value_pfp_product_padded_leftleft) = p))) /\ (((forall fom_index_pfp_product_padded_leftright. (exists fom_gap_pfp_product_padded_leftright_index_bound. fom_gap_pfp_product_padded_leftright_index_bound + S (fom_index_pfp_product_padded_leftright) = M) -> exists fom_value_pfp_product_padded_leftright. ((((exists fom_beta_height_pfp_product_padded_leftright_entry. fom_beta_height_pfp_product_padded_leftright_entry + S (fom_value_pfp_product_padded_leftright) = S ((S (fom_index_pfp_product_padded_leftright)) * bc)) /\ exists fom_beta_quotient_pfp_product_padded_leftright_entry. bb = fom_beta_quotient_pfp_product_padded_leftright_entry * S ((S (fom_index_pfp_product_padded_leftright)) * bc) + (fom_value_pfp_product_padded_leftright))) /\ (exists fom_gap_pfp_product_padded_leftright_value_bound. fom_gap_pfp_product_padded_leftright_value_bound + S (fom_value_pfp_product_padded_leftright) = p))) /\ (((((((t+L)=0 \/ (M)=0) /\ (((K)=0)))) \/ (((~((t+L)=0)) /\ (((~((M)=0)) /\ (((t+L)+(M)=S (K)))))))) /\ ((forall pfc_index_product_padded_leftcoefficients. (exists pfa_gap_product_padded_leftcoefficientsbound. pfa_gap_product_padded_leftcoefficientsbound + S (pfc_index_product_padded_leftcoefficients) = (K)) -> exists pfc_value_product_padded_leftcoefficients. ((((exists ff_h_pfp_product_padded_leftcoefficientsentry. ff_h_pfp_product_padded_leftcoefficientsentry + S (pfc_value_product_padded_leftcoefficients) = S ((S (pfc_index_product_padded_leftcoefficients)) * CC)) /\ exists ff_q_pfp_product_padded_leftcoefficientsentry. CB = ff_q_pfp_product_padded_leftcoefficientsentry * S ((S (pfc_index_product_padded_leftcoefficients)) * CC) + (pfc_value_product_padded_leftcoefficients))) /\ ((exists pfc_terms_code_product_padded_leftcoefficientscoefficient pfc_terms_scale_product_padded_leftcoefficientscoefficient pfc_natural_sum_product_padded_leftcoefficientscoefficient. ((forall pfc_index_product_padded_leftcoefficientscoefficientdiagonal. (exists pfa_gap_product_padded_leftcoefficientscoefficientdiagonalbound. pfa_gap_product_padded_leftcoefficientscoefficientdiagonalbound + S (pfc_index_product_padded_leftcoefficientscoefficientdiagonal) = (S (pfc_index_product_padded_leftcoefficients))) -> exists pfc_value_product_padded_leftcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_product_padded_leftcoefficientscoefficientdiagonalentry. ff_h_pfp_product_padded_leftcoefficientscoefficientdiagonalentry + S (pfc_value_product_padded_leftcoefficientscoefficientdiagonal) = S ((S (pfc_index_product_padded_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_padded_leftcoefficientscoefficient)) /\ exists ff_q_pfp_product_padded_leftcoefficientscoefficientdiagonalentry. pfc_terms_code_product_padded_leftcoefficientscoefficient = ff_q_pfp_product_padded_leftcoefficientscoefficientdiagonalentry * S ((S (pfc_index_product_padded_leftcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_padded_leftcoefficientscoefficient) + (pfc_value_product_padded_leftcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_product_padded_leftcoefficientscoefficientdiagonalterm pfc_left_product_padded_leftcoefficientscoefficientdiagonalterm pfc_right_product_padded_leftcoefficientscoefficientdiagonalterm. (((pfc_index_product_padded_leftcoefficientscoefficientdiagonal)+pfc_complement_product_padded_leftcoefficientscoefficientdiagonalterm=(pfc_index_product_padded_leftcoefficients)) /\ ((((((exists pfa_gap_product_padded_leftcoefficientscoefficientdiagonaltermleftinside. pfa_gap_product_padded_leftcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_product_padded_leftcoefficientscoefficientdiagonal) = (t+L)) /\ ((((exists ff_h_pfp_product_padded_leftcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_product_padded_leftcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_product_padded_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_product_padded_leftcoefficientscoefficientdiagonal)) * AC)) /\ exists ff_q_pfp_product_padded_leftcoefficientscoefficientdiagonaltermleftentry. AB = ff_q_pfp_product_padded_leftcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_product_padded_leftcoefficientscoefficientdiagonal)) * AC) + (pfc_left_product_padded_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_padded_leftcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_product_padded_leftcoefficientscoefficientdiagonaltermleftoutside+(t+L)=(pfc_index_product_padded_leftcoefficientscoefficientdiagonal)) /\ (((pfc_left_product_padded_leftcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_product_padded_leftcoefficientscoefficientdiagonaltermrightinside. pfa_gap_product_padded_leftcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_product_padded_leftcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_product_padded_leftcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_product_padded_leftcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_product_padded_leftcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_product_padded_leftcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_product_padded_leftcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_product_padded_leftcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_product_padded_leftcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_product_padded_leftcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_padded_leftcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_product_padded_leftcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_product_padded_leftcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_product_padded_leftcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_product_padded_leftcoefficientscoefficientdiagonal)=pfc_left_product_padded_leftcoefficientscoefficientdiagonalterm*pfc_right_product_padded_leftcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_product_padded_leftcoefficientscoefficientsum fs_v_pfc_product_padded_leftcoefficientscoefficientsum. ((((exists fs_h_pfc_product_padded_leftcoefficientscoefficientsum_body_start. fs_h_pfc_product_padded_leftcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_product_padded_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_leftcoefficientscoefficientsum_body_start. fs_u_pfc_product_padded_leftcoefficientscoefficientsum = fs_q_pfc_product_padded_leftcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_product_padded_leftcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_product_padded_leftcoefficientscoefficientsum_body_terminal. fs_h_pfc_product_padded_leftcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_product_padded_leftcoefficientscoefficient) = S ((S (S (pfc_index_product_padded_leftcoefficients))) * fs_v_pfc_product_padded_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_leftcoefficientscoefficientsum_body_terminal. fs_u_pfc_product_padded_leftcoefficientscoefficientsum = fs_q_pfc_product_padded_leftcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_product_padded_leftcoefficients))) * fs_v_pfc_product_padded_leftcoefficientscoefficientsum) + (pfc_natural_sum_product_padded_leftcoefficientscoefficient))) /\ forall fs_i_pfc_product_padded_leftcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_product_padded_leftcoefficientscoefficientsum_body_steps = S (pfc_index_product_padded_leftcoefficients)) -> exists fs_a_pfc_product_padded_leftcoefficientscoefficientsum_body_steps fs_r_pfc_product_padded_leftcoefficientscoefficientsum_body_steps fs_s_pfc_product_padded_leftcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_product_padded_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_padded_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_padded_leftcoefficientscoefficient)) /\ exists fs_q_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_product_padded_leftcoefficientscoefficient = fs_q_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_product_padded_leftcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_padded_leftcoefficientscoefficient) + (fs_a_pfc_product_padded_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_product_padded_leftcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_padded_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_product_padded_leftcoefficientscoefficientsum = fs_q_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_product_padded_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_leftcoefficientscoefficientsum) + (fs_r_pfc_product_padded_leftcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_product_padded_leftcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_product_padded_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_leftcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_product_padded_leftcoefficientscoefficientsum = fs_q_pfc_product_padded_leftcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_product_padded_leftcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_leftcoefficientscoefficientsum) + (fs_s_pfc_product_padded_leftcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_product_padded_leftcoefficientscoefficientsum_body_steps = fs_r_pfc_product_padded_leftcoefficientscoefficientsum_body_steps + fs_a_pfc_product_padded_leftcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_product_padded_leftcoefficientscoefficientresiduebound. pfa_gap_product_padded_leftcoefficientscoefficientresiduebound + S (pfc_value_product_padded_leftcoefficients) = (p)) /\ ((exists pfa_offset_left_product_padded_leftcoefficientscoefficientresiduecongruence pfa_offset_right_product_padded_leftcoefficientscoefficientresiduecongruence. (pfc_natural_sum_product_padded_leftcoefficientscoefficient) + (p) * pfa_offset_left_product_padded_leftcoefficientscoefficientresiduecongruence = (pfc_value_product_padded_leftcoefficients) + (p) * pfa_offset_right_product_padded_leftcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_product_equivalent_left pfrep_left_product_equivalent_left pfrep_right_product_equivalent_left. ((exists pfrep_position_product_equivalent_leftfirst. ((pfrep_position_product_equivalent_leftfirst+S (pfrep_power_product_equivalent_left)=(N)) /\ ((((exists ff_h_pfp_product_equivalent_leftfirstentry. ff_h_pfp_product_equivalent_leftfirstentry + S (pfrep_left_product_equivalent_left) = S ((S (pfrep_position_product_equivalent_leftfirst)) * cc)) /\ exists ff_q_pfp_product_equivalent_leftfirstentry. cb = ff_q_pfp_product_equivalent_leftfirstentry * S ((S (pfrep_position_product_equivalent_leftfirst)) * cc) + (pfrep_left_product_equivalent_left)))))) \/ (((exists pfrep_gap_product_equivalent_leftfirstoutside. pfrep_gap_product_equivalent_leftfirstoutside+(N)=(pfrep_power_product_equivalent_left)) /\ (((pfrep_left_product_equivalent_left)=0))))) -> ((exists pfrep_position_product_equivalent_leftsecond. ((pfrep_position_product_equivalent_leftsecond+S (pfrep_power_product_equivalent_left)=(K)) /\ ((((exists ff_h_pfp_product_equivalent_leftsecondentry. ff_h_pfp_product_equivalent_leftsecondentry + S (pfrep_right_product_equivalent_left) = S ((S (pfrep_position_product_equivalent_leftsecond)) * CC)) /\ exists ff_q_pfp_product_equivalent_leftsecondentry. CB = ff_q_pfp_product_equivalent_leftsecondentry * S ((S (pfrep_position_product_equivalent_leftsecond)) * CC) + (pfrep_right_product_equivalent_left)))))) \/ (((exists pfrep_gap_product_equivalent_leftsecondoutside. pfrep_gap_product_equivalent_leftsecondoutside+(K)=(pfrep_power_product_equivalent_left)) /\ (((pfrep_right_product_equivalent_left)=0))))) -> pfrep_left_product_equivalent_left=pfrep_right_product_equivalent_left)

Complete tactic proof in conservative notation

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

211 script commands · 35 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 (6)
polynomial left pad zero prefixprime field polynomial zero prefix equivalent emptyprime field polynomial equivalent transitiveprime field polynomial equivalent symmetricprime field polynomial convolution left padding nonempty leftprime field polynomial left pad equivalent
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 cb
  9. L9
    intro cc
  10. L10
    intro N
02Fix variables and assumptionsL11–20

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

  1. L11
    intro AB
  2. L12
    intro AC
  3. L13
    intro t
  4. L14
    intro CB
  5. L15
    intro CC
  6. L16
    intro K
  7. L17
    intro hp
  8. L18
    intro hpad
  9. L19
    intro hc
  10. L20
    intro hn
03Establish hLL21–24

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

  1. L21
    have hL : L=0 \/ ~(L=0)
  2. L22
    specialize eq_decidable (L)
  3. L23
    specialize eq_decidable (0)
  4. L24
    apply eq_decidable
04Separate the logical casesL25–25

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

  1. L25
    cases hL
05Establish hzL26–29

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

  1. L26
  2. L27
    intro j
  3. L28
    intro hj
  4. L29
    rewrite hL_left at hj
06Separate the logical casesL30–30

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

  1. L30
    exfalso
07Use earlier factsL31–33

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

  1. L31
    specialize matrix_rank_no_index_below_zero (j)
  2. L32
    apply matrix_rank_no_index_below_zero
  3. L33
    exact hj
08Establish hc0L34–43

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

  1. L34
    have hc0 : Repeat(cb,cc,0,N)Definitions: Repeat(cb,cc,0,N)Original native command in the exact edition
  2. L35
    specialize prime_field_polynomial_convolution_zero_left (p)
  3. L36
    specialize prime_field_polynomial_convolution_zero_left (ab)
  4. L37
    specialize prime_field_polynomial_convolution_zero_left (ac)
  5. L38
    specialize prime_field_polynomial_convolution_zero_left (L)
  6. L39
    specialize prime_field_polynomial_convolution_zero_left (bb)
  7. L40
    specialize prime_field_polynomial_convolution_zero_left (bc)
  8. L41
    specialize prime_field_polynomial_convolution_zero_left (M)
  9. L42
    specialize prime_field_polynomial_convolution_zero_left (cb)
  10. L43
    specialize prime_field_polynomial_convolution_zero_left (cc)
09Use earlier factsL44–48

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

  1. L44
    specialize prime_field_polynomial_convolution_zero_left (N)
  2. L45
    apply prime_field_polynomial_convolution_zero_left
  3. L46
    exact hp
  4. L47
    exact hz
  5. L48
    exact hc
10Establish hn0L49–58

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

  1. L49
    have hn0 : Repeat(CB,CC,0,K)Definitions: Repeat(CB,CC,0,K)Original native command in the exact edition
  2. L50
    specialize prime_field_polynomial_convolution_zero_left (p)
  3. L51
    specialize prime_field_polynomial_convolution_zero_left (AB)
  4. L52
    specialize prime_field_polynomial_convolution_zero_left (AC)
  5. L53
    specialize prime_field_polynomial_convolution_zero_left (t+L)
  6. L54
    specialize prime_field_polynomial_convolution_zero_left (bb)
  7. L55
    specialize prime_field_polynomial_convolution_zero_left (bc)
  8. L56
    specialize prime_field_polynomial_convolution_zero_left (M)
  9. L57
    specialize prime_field_polynomial_convolution_zero_left (CB)
  10. L58
    specialize prime_field_polynomial_convolution_zero_left (CC)
11Use earlier factsL59–68

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

  1. L59
    specialize prime_field_polynomial_convolution_zero_left (K)
  2. L60
    apply prime_field_polynomial_convolution_zero_left
  3. L61
    exact hp
  4. L62
    specialize polynomial_left_pad_zero_prefix (ab)
  5. L63
    specialize polynomial_left_pad_zero_prefix (ac)
  6. L64
    specialize polynomial_left_pad_zero_prefix (L)
  7. L65
    specialize polynomial_left_pad_zero_prefix (t)
  8. L66
    specialize polynomial_left_pad_zero_prefix (AB)
  9. L67
    specialize polynomial_left_pad_zero_prefix (AC)
  10. L68
    apply polynomial_left_pad_zero_prefix
12Use earlier factsL69–71

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

  1. L69
    exact hz
  2. L70
    exact hpad
  3. L71
    exact hn
13Establish hecL72–77

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

  1. L72
    have hec : PolynomialEquivalent(cb,cc,N,0,0,0)Definitions: PolynomialEquivalent(cb,cc,N,0,0,0)Original native command in the exact edition
  2. L73
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (cb)
  3. L74
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (cc)
  4. L75
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (N)
  5. L76
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L77
    exact hc0
14Establish henL78–87

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

  1. L78
    have hen : PolynomialEquivalent(CB,CC,K,0,0,0)Definitions: PolynomialEquivalent(CB,CC,K,0,0,0)Original native command in the exact edition
  2. L79
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (CB)
  3. L80
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (CC)
  4. L81
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  5. L82
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L83
    exact hn0
  7. L84
    specialize prime_field_polynomial_equivalent_transitive (cb)
  8. L85
    specialize prime_field_polynomial_equivalent_transitive (cc)
  9. L86
    specialize prime_field_polynomial_equivalent_transitive (N)
  10. L87
    specialize prime_field_polynomial_equivalent_transitive (0)
15Use earlier factsL88–97

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

  1. L88
    specialize prime_field_polynomial_equivalent_transitive (0)
  2. L89
    specialize prime_field_polynomial_equivalent_transitive (0)
  3. L90
    specialize prime_field_polynomial_equivalent_transitive (CB)
  4. L91
    specialize prime_field_polynomial_equivalent_transitive (CC)
  5. L92
    specialize prime_field_polynomial_equivalent_transitive (K)
  6. L93
    apply prime_field_polynomial_equivalent_transitive
  7. L94
    exact hec
  8. L95
    specialize prime_field_polynomial_equivalent_symmetric (CB)
  9. L96
    specialize prime_field_polynomial_equivalent_symmetric (CC)
  10. L97
    specialize prime_field_polynomial_equivalent_symmetric (K)
16Use earlier factsL98–102

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

  1. L98
    specialize prime_field_polynomial_equivalent_symmetric (0)
  2. L99
    specialize prime_field_polynomial_equivalent_symmetric (0)
  3. L100
    specialize prime_field_polynomial_equivalent_symmetric (0)
  4. L101
    apply prime_field_polynomial_equivalent_symmetric
  5. L102
    exact hen
17Establish hML103–106

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

  1. L103
    have hM : M=0 \/ ~(M=0)
  2. L104
    specialize eq_decidable (M)
  3. L105
    specialize eq_decidable (0)
  4. L106
    apply eq_decidable
18Separate the logical casesL107–107

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

  1. L107
    cases hM
19Establish hzL108–111

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

  1. L108
  2. L109
    intro j
  3. L110
    intro hj
  4. L111
    rewrite hM_left at hj
20Separate the logical casesL112–112

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

  1. L112
    exfalso
21Use earlier factsL113–115

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

  1. L113
    specialize matrix_rank_no_index_below_zero (j)
  2. L114
    apply matrix_rank_no_index_below_zero
  3. L115
    exact hj
22Establish hc0L116–125

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

  1. L116
    have hc0 : Repeat(cb,cc,0,N)Definitions: Repeat(cb,cc,0,N)Original native command in the exact edition
  2. L117
    specialize prime_field_polynomial_convolution_zero_right (p)
  3. L118
    specialize prime_field_polynomial_convolution_zero_right (ab)
  4. L119
    specialize prime_field_polynomial_convolution_zero_right (ac)
  5. L120
    specialize prime_field_polynomial_convolution_zero_right (L)
  6. L121
    specialize prime_field_polynomial_convolution_zero_right (bb)
  7. L122
    specialize prime_field_polynomial_convolution_zero_right (bc)
  8. L123
    specialize prime_field_polynomial_convolution_zero_right (M)
  9. L124
    specialize prime_field_polynomial_convolution_zero_right (cb)
  10. L125
    specialize prime_field_polynomial_convolution_zero_right (cc)
23Use earlier factsL126–130

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

  1. L126
    specialize prime_field_polynomial_convolution_zero_right (N)
  2. L127
    apply prime_field_polynomial_convolution_zero_right
  3. L128
    exact hp
  4. L129
    exact hz
  5. L130
    exact hc
24Establish hn0L131–140

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

  1. L131
    have hn0 : Repeat(CB,CC,0,K)Definitions: Repeat(CB,CC,0,K)Original native command in the exact edition
  2. L132
    specialize prime_field_polynomial_convolution_zero_right (p)
  3. L133
    specialize prime_field_polynomial_convolution_zero_right (AB)
  4. L134
    specialize prime_field_polynomial_convolution_zero_right (AC)
  5. L135
    specialize prime_field_polynomial_convolution_zero_right (t+L)
  6. L136
    specialize prime_field_polynomial_convolution_zero_right (bb)
  7. L137
    specialize prime_field_polynomial_convolution_zero_right (bc)
  8. L138
    specialize prime_field_polynomial_convolution_zero_right (M)
  9. L139
    specialize prime_field_polynomial_convolution_zero_right (CB)
  10. L140
    specialize prime_field_polynomial_convolution_zero_right (CC)
25Use earlier factsL141–145

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

  1. L141
    specialize prime_field_polynomial_convolution_zero_right (K)
  2. L142
    apply prime_field_polynomial_convolution_zero_right
  3. L143
    exact hp
  4. L144
    exact hz
  5. L145
    exact hn
26Establish hecL146–151

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

  1. L146
    have hec : PolynomialEquivalent(cb,cc,N,0,0,0)Definitions: PolynomialEquivalent(cb,cc,N,0,0,0)Original native command in the exact edition
  2. L147
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (cb)
  3. L148
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (cc)
  4. L149
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (N)
  5. L150
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L151
    exact hc0
27Establish henL152–161

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

  1. L152
    have hen : PolynomialEquivalent(CB,CC,K,0,0,0)Definitions: PolynomialEquivalent(CB,CC,K,0,0,0)Original native command in the exact edition
  2. L153
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (CB)
  3. L154
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (CC)
  4. L155
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  5. L156
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L157
    exact hn0
  7. L158
    specialize prime_field_polynomial_equivalent_transitive (cb)
  8. L159
    specialize prime_field_polynomial_equivalent_transitive (cc)
  9. L160
    specialize prime_field_polynomial_equivalent_transitive (N)
  10. L161
    specialize prime_field_polynomial_equivalent_transitive (0)
28Use earlier factsL162–171

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

  1. L162
    specialize prime_field_polynomial_equivalent_transitive (0)
  2. L163
    specialize prime_field_polynomial_equivalent_transitive (0)
  3. L164
    specialize prime_field_polynomial_equivalent_transitive (CB)
  4. L165
    specialize prime_field_polynomial_equivalent_transitive (CC)
  5. L166
    specialize prime_field_polynomial_equivalent_transitive (K)
  6. L167
    apply prime_field_polynomial_equivalent_transitive
  7. L168
    exact hec
  8. L169
    specialize prime_field_polynomial_equivalent_symmetric (CB)
  9. L170
    specialize prime_field_polynomial_equivalent_symmetric (CC)
  10. L171
    specialize prime_field_polynomial_equivalent_symmetric (K)
29Use earlier factsL172–176

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

  1. L172
    specialize prime_field_polynomial_equivalent_symmetric (0)
  2. L173
    specialize prime_field_polynomial_equivalent_symmetric (0)
  3. L174
    specialize prime_field_polynomial_equivalent_symmetric (0)
  4. L175
    apply prime_field_polynomial_equivalent_symmetric
  5. L176
    exact hen
30Establish hdL177–186

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

  1. L177
    have hd : K = t + N ∧ PolynomialLeftPad(cb,cc,N,t,CB,CC)Definitions: PolynomialLeftPad(cb,cc,N,t,CB,CC)Original native command in the exact edition
  2. L178
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (p)
  3. L179
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (ab)
  4. L180
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (ac)
  5. L181
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (L)
  6. L182
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (bb)
  7. L183
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (bc)
  8. L184
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (M)
  9. L185
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (cb)
  10. L186
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (cc)
31Use earlier factsL187–196

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

  1. L187
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (N)
  2. L188
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (AB)
  3. L189
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (AC)
  4. L190
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (t)
  5. L191
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (CB)
  6. L192
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (CC)
  7. L193
    specialize prime_field_polynomial_convolution_left_padding_nonempty_left (K)
  8. L194
    apply prime_field_polynomial_convolution_left_padding_nonempty_left
  9. L195
    exact hp
  10. L196
    exact hL_right
32Use earlier factsL197–200

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

  1. L197
    exact hM_right
  2. L198
    exact hpad
  3. L199
    exact hc
  4. L200
    exact hn
33Separate the logical casesL201–201

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

  1. L201
    cases hd
34Calculate and transport equalitiesL202–203

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L202
    rewrite hd_left
  2. L203
    rewrite hd_left
35Use earlier factsL204–211

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

  1. L204
    specialize prime_field_polynomial_left_pad_equivalent (cb)
  2. L205
    specialize prime_field_polynomial_left_pad_equivalent (cc)
  3. L206
    specialize prime_field_polynomial_left_pad_equivalent (N)
  4. L207
    specialize prime_field_polynomial_left_pad_equivalent (t)
  5. L208
    specialize prime_field_polynomial_left_pad_equivalent (CB)
  6. L209
    specialize prime_field_polynomial_left_pad_equivalent (CC)
  7. L210
    apply prime_field_polynomial_left_pad_equivalent
  8. L211
    exact hd_right

Library-wide reading audit

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