PX006F

prime_field_polynomial_convolution_left_padding_equivalent_right

Genuine leading-zero padding of the right 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. ∀ BB. ∀ BC. ∀ t. ∀ CB. ∀ CC. ∀ K. ¬p = 0 → PolynomialLeftPad(bb,bc,M,t,BB,BC) → FpPolyProduct(p,ab,ac,L,bb,bc,M,cb,cc,N) → FpPolyProduct(p,ab,ac,L,BB,BC,t + 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_rightprime_field_polynomial_left_pad_equivalent
Original expanded first-order statement 
forall p ab ac L bb bc M cb cc N BB BC t CB CC K. (~(p=0)) -> (((forall pfp_repeat_index_product_factor_padding_rightzeros. (exists pfa_gap_product_factor_padding_rightzerosindex. pfa_gap_product_factor_padding_rightzerosindex + S (pfp_repeat_index_product_factor_padding_rightzeros) = (t)) -> (((exists ff_h_pfp_product_factor_padding_rightzerosentry. ff_h_pfp_product_factor_padding_rightzerosentry + S (0) = S ((S (pfp_repeat_index_product_factor_padding_rightzeros)) * BC)) /\ exists ff_q_pfp_product_factor_padding_rightzerosentry. BB = ff_q_pfp_product_factor_padding_rightzerosentry * S ((S (pfp_repeat_index_product_factor_padding_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_product_factor_padding_right pfrep_value_product_factor_padding_right. (exists pfa_gap_product_factor_padding_rightbound. pfa_gap_product_factor_padding_rightbound + S (pfrep_index_product_factor_padding_right) = (M)) -> (((exists ff_h_pfp_product_factor_padding_rightinput. ff_h_pfp_product_factor_padding_rightinput + S (pfrep_value_product_factor_padding_right) = S ((S (pfrep_index_product_factor_padding_right)) * bc)) /\ exists ff_q_pfp_product_factor_padding_rightinput. bb = ff_q_pfp_product_factor_padding_rightinput * S ((S (pfrep_index_product_factor_padding_right)) * bc) + (pfrep_value_product_factor_padding_right))) -> (((exists ff_h_pfp_product_factor_padding_rightoutput. ff_h_pfp_product_factor_padding_rightoutput + S (pfrep_value_product_factor_padding_right) = S ((S ((t)+pfrep_index_product_factor_padding_right)) * BC)) /\ exists ff_q_pfp_product_factor_padding_rightoutput. BB = ff_q_pfp_product_factor_padding_rightoutput * S ((S ((t)+pfrep_index_product_factor_padding_right)) * BC) + (pfrep_value_product_factor_padding_right))))))) -> (((forall fom_index_pfp_product_original_rightleft. (exists fom_gap_pfp_product_original_rightleft_index_bound. fom_gap_pfp_product_original_rightleft_index_bound + S (fom_index_pfp_product_original_rightleft) = L) -> exists fom_value_pfp_product_original_rightleft. ((((exists fom_beta_height_pfp_product_original_rightleft_entry. fom_beta_height_pfp_product_original_rightleft_entry + S (fom_value_pfp_product_original_rightleft) = S ((S (fom_index_pfp_product_original_rightleft)) * ac)) /\ exists fom_beta_quotient_pfp_product_original_rightleft_entry. ab = fom_beta_quotient_pfp_product_original_rightleft_entry * S ((S (fom_index_pfp_product_original_rightleft)) * ac) + (fom_value_pfp_product_original_rightleft))) /\ (exists fom_gap_pfp_product_original_rightleft_value_bound. fom_gap_pfp_product_original_rightleft_value_bound + S (fom_value_pfp_product_original_rightleft) = p))) /\ (((forall fom_index_pfp_product_original_rightright. (exists fom_gap_pfp_product_original_rightright_index_bound. fom_gap_pfp_product_original_rightright_index_bound + S (fom_index_pfp_product_original_rightright) = M) -> exists fom_value_pfp_product_original_rightright. ((((exists fom_beta_height_pfp_product_original_rightright_entry. fom_beta_height_pfp_product_original_rightright_entry + S (fom_value_pfp_product_original_rightright) = S ((S (fom_index_pfp_product_original_rightright)) * bc)) /\ exists fom_beta_quotient_pfp_product_original_rightright_entry. bb = fom_beta_quotient_pfp_product_original_rightright_entry * S ((S (fom_index_pfp_product_original_rightright)) * bc) + (fom_value_pfp_product_original_rightright))) /\ (exists fom_gap_pfp_product_original_rightright_value_bound. fom_gap_pfp_product_original_rightright_value_bound + S (fom_value_pfp_product_original_rightright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_product_original_rightcoefficients. (exists pfa_gap_product_original_rightcoefficientsbound. pfa_gap_product_original_rightcoefficientsbound + S (pfc_index_product_original_rightcoefficients) = (N)) -> exists pfc_value_product_original_rightcoefficients. ((((exists ff_h_pfp_product_original_rightcoefficientsentry. ff_h_pfp_product_original_rightcoefficientsentry + S (pfc_value_product_original_rightcoefficients) = S ((S (pfc_index_product_original_rightcoefficients)) * cc)) /\ exists ff_q_pfp_product_original_rightcoefficientsentry. cb = ff_q_pfp_product_original_rightcoefficientsentry * S ((S (pfc_index_product_original_rightcoefficients)) * cc) + (pfc_value_product_original_rightcoefficients))) /\ ((exists pfc_terms_code_product_original_rightcoefficientscoefficient pfc_terms_scale_product_original_rightcoefficientscoefficient pfc_natural_sum_product_original_rightcoefficientscoefficient. ((forall pfc_index_product_original_rightcoefficientscoefficientdiagonal. (exists pfa_gap_product_original_rightcoefficientscoefficientdiagonalbound. pfa_gap_product_original_rightcoefficientscoefficientdiagonalbound + S (pfc_index_product_original_rightcoefficientscoefficientdiagonal) = (S (pfc_index_product_original_rightcoefficients))) -> exists pfc_value_product_original_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_product_original_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_product_original_rightcoefficientscoefficientdiagonalentry + S (pfc_value_product_original_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_product_original_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_original_rightcoefficientscoefficient)) /\ exists ff_q_pfp_product_original_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_product_original_rightcoefficientscoefficient = ff_q_pfp_product_original_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_product_original_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_original_rightcoefficientscoefficient) + (pfc_value_product_original_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm pfc_left_product_original_rightcoefficientscoefficientdiagonalterm pfc_right_product_original_rightcoefficientscoefficientdiagonalterm. (((pfc_index_product_original_rightcoefficientscoefficientdiagonal)+pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm=(pfc_index_product_original_rightcoefficients)) /\ ((((((exists pfa_gap_product_original_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_product_original_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_product_original_rightcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_product_original_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_product_original_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_product_original_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_product_original_rightcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_product_original_rightcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_product_original_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_product_original_rightcoefficientscoefficientdiagonal)) * ac) + (pfc_left_product_original_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_original_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_product_original_rightcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_product_original_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_product_original_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_product_original_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_product_original_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_product_original_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_product_original_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_product_original_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_product_original_rightcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_product_original_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_product_original_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_original_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_product_original_rightcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_product_original_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_product_original_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_product_original_rightcoefficientscoefficientdiagonal)=pfc_left_product_original_rightcoefficientscoefficientdiagonalterm*pfc_right_product_original_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_product_original_rightcoefficientscoefficientsum fs_v_pfc_product_original_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_start. fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_start. fs_u_pfc_product_original_rightcoefficientscoefficientsum = fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_product_original_rightcoefficientscoefficient) = S ((S (S (pfc_index_product_original_rightcoefficients))) * fs_v_pfc_product_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_product_original_rightcoefficientscoefficientsum = fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_product_original_rightcoefficients))) * fs_v_pfc_product_original_rightcoefficientscoefficientsum) + (pfc_natural_sum_product_original_rightcoefficientscoefficient))) /\ forall fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_product_original_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_product_original_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps = S (pfc_index_product_original_rightcoefficients)) -> exists fs_a_pfc_product_original_rightcoefficientscoefficientsum_body_steps fs_r_pfc_product_original_rightcoefficientscoefficientsum_body_steps fs_s_pfc_product_original_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_product_original_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_original_rightcoefficientscoefficient)) /\ exists fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_product_original_rightcoefficientscoefficient = fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_original_rightcoefficientscoefficient) + (fs_a_pfc_product_original_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_product_original_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_product_original_rightcoefficientscoefficientsum = fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum) + (fs_r_pfc_product_original_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_product_original_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_product_original_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_product_original_rightcoefficientscoefficientsum = fs_q_pfc_product_original_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_product_original_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_original_rightcoefficientscoefficientsum) + (fs_s_pfc_product_original_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_product_original_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_product_original_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_product_original_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_product_original_rightcoefficientscoefficientresiduebound. pfa_gap_product_original_rightcoefficientscoefficientresiduebound + S (pfc_value_product_original_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_product_original_rightcoefficientscoefficientresiduecongruence pfa_offset_right_product_original_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_product_original_rightcoefficientscoefficient) + (p) * pfa_offset_left_product_original_rightcoefficientscoefficientresiduecongruence = (pfc_value_product_original_rightcoefficients) + (p) * pfa_offset_right_product_original_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_product_padded_rightleft. (exists fom_gap_pfp_product_padded_rightleft_index_bound. fom_gap_pfp_product_padded_rightleft_index_bound + S (fom_index_pfp_product_padded_rightleft) = L) -> exists fom_value_pfp_product_padded_rightleft. ((((exists fom_beta_height_pfp_product_padded_rightleft_entry. fom_beta_height_pfp_product_padded_rightleft_entry + S (fom_value_pfp_product_padded_rightleft) = S ((S (fom_index_pfp_product_padded_rightleft)) * ac)) /\ exists fom_beta_quotient_pfp_product_padded_rightleft_entry. ab = fom_beta_quotient_pfp_product_padded_rightleft_entry * S ((S (fom_index_pfp_product_padded_rightleft)) * ac) + (fom_value_pfp_product_padded_rightleft))) /\ (exists fom_gap_pfp_product_padded_rightleft_value_bound. fom_gap_pfp_product_padded_rightleft_value_bound + S (fom_value_pfp_product_padded_rightleft) = p))) /\ (((forall fom_index_pfp_product_padded_rightright. (exists fom_gap_pfp_product_padded_rightright_index_bound. fom_gap_pfp_product_padded_rightright_index_bound + S (fom_index_pfp_product_padded_rightright) = t+M) -> exists fom_value_pfp_product_padded_rightright. ((((exists fom_beta_height_pfp_product_padded_rightright_entry. fom_beta_height_pfp_product_padded_rightright_entry + S (fom_value_pfp_product_padded_rightright) = S ((S (fom_index_pfp_product_padded_rightright)) * BC)) /\ exists fom_beta_quotient_pfp_product_padded_rightright_entry. BB = fom_beta_quotient_pfp_product_padded_rightright_entry * S ((S (fom_index_pfp_product_padded_rightright)) * BC) + (fom_value_pfp_product_padded_rightright))) /\ (exists fom_gap_pfp_product_padded_rightright_value_bound. fom_gap_pfp_product_padded_rightright_value_bound + S (fom_value_pfp_product_padded_rightright) = p))) /\ (((((((L)=0 \/ (t+M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((t+M)=0)) /\ (((L)+(t+M)=S (K)))))))) /\ ((forall pfc_index_product_padded_rightcoefficients. (exists pfa_gap_product_padded_rightcoefficientsbound. pfa_gap_product_padded_rightcoefficientsbound + S (pfc_index_product_padded_rightcoefficients) = (K)) -> exists pfc_value_product_padded_rightcoefficients. ((((exists ff_h_pfp_product_padded_rightcoefficientsentry. ff_h_pfp_product_padded_rightcoefficientsentry + S (pfc_value_product_padded_rightcoefficients) = S ((S (pfc_index_product_padded_rightcoefficients)) * CC)) /\ exists ff_q_pfp_product_padded_rightcoefficientsentry. CB = ff_q_pfp_product_padded_rightcoefficientsentry * S ((S (pfc_index_product_padded_rightcoefficients)) * CC) + (pfc_value_product_padded_rightcoefficients))) /\ ((exists pfc_terms_code_product_padded_rightcoefficientscoefficient pfc_terms_scale_product_padded_rightcoefficientscoefficient pfc_natural_sum_product_padded_rightcoefficientscoefficient. ((forall pfc_index_product_padded_rightcoefficientscoefficientdiagonal. (exists pfa_gap_product_padded_rightcoefficientscoefficientdiagonalbound. pfa_gap_product_padded_rightcoefficientscoefficientdiagonalbound + S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal) = (S (pfc_index_product_padded_rightcoefficients))) -> exists pfc_value_product_padded_rightcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonalentry. ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonalentry + S (pfc_value_product_padded_rightcoefficientscoefficientdiagonal) = S ((S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_padded_rightcoefficientscoefficient)) /\ exists ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonalentry. pfc_terms_code_product_padded_rightcoefficientscoefficient = ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonalentry * S ((S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal)) * pfc_terms_scale_product_padded_rightcoefficientscoefficient) + (pfc_value_product_padded_rightcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm pfc_left_product_padded_rightcoefficientscoefficientdiagonalterm pfc_right_product_padded_rightcoefficientscoefficientdiagonalterm. (((pfc_index_product_padded_rightcoefficientscoefficientdiagonal)+pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm=(pfc_index_product_padded_rightcoefficients)) /\ ((((((exists pfa_gap_product_padded_rightcoefficientscoefficientdiagonaltermleftinside. pfa_gap_product_padded_rightcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_product_padded_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_product_padded_rightcoefficientscoefficientdiagonal)) * ac) + (pfc_left_product_padded_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_padded_rightcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_product_padded_rightcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_product_padded_rightcoefficientscoefficientdiagonal)) /\ (((pfc_left_product_padded_rightcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_product_padded_rightcoefficientscoefficientdiagonaltermrightinside. pfa_gap_product_padded_rightcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm) = (t+M)) /\ ((((exists ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_product_padded_rightcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_product_padded_rightcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm)) * BC)) /\ exists ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonaltermrightentry. BB = ff_q_pfp_product_padded_rightcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm)) * BC) + (pfc_right_product_padded_rightcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_product_padded_rightcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_product_padded_rightcoefficientscoefficientdiagonaltermrightoutside+(t+M)=(pfc_complement_product_padded_rightcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_product_padded_rightcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_product_padded_rightcoefficientscoefficientdiagonal)=pfc_left_product_padded_rightcoefficientscoefficientdiagonalterm*pfc_right_product_padded_rightcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_product_padded_rightcoefficientscoefficientsum fs_v_pfc_product_padded_rightcoefficientscoefficientsum. ((((exists fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_start. fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_start. fs_u_pfc_product_padded_rightcoefficientscoefficientsum = fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_terminal. fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_product_padded_rightcoefficientscoefficient) = S ((S (S (pfc_index_product_padded_rightcoefficients))) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_terminal. fs_u_pfc_product_padded_rightcoefficientscoefficientsum = fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_product_padded_rightcoefficients))) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum) + (pfc_natural_sum_product_padded_rightcoefficientscoefficient))) /\ forall fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps = S (pfc_index_product_padded_rightcoefficients)) -> exists fs_a_pfc_product_padded_rightcoefficientscoefficientsum_body_steps fs_r_pfc_product_padded_rightcoefficientscoefficientsum_body_steps fs_s_pfc_product_padded_rightcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_product_padded_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_padded_rightcoefficientscoefficient)) /\ exists fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_product_padded_rightcoefficientscoefficient = fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_product_padded_rightcoefficientscoefficient) + (fs_a_pfc_product_padded_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_product_padded_rightcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_product_padded_rightcoefficientscoefficientsum = fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum) + (fs_r_pfc_product_padded_rightcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_product_padded_rightcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum)) /\ exists fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_product_padded_rightcoefficientscoefficientsum = fs_q_pfc_product_padded_rightcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)) * fs_v_pfc_product_padded_rightcoefficientscoefficientsum) + (fs_s_pfc_product_padded_rightcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_product_padded_rightcoefficientscoefficientsum_body_steps = fs_r_pfc_product_padded_rightcoefficientscoefficientsum_body_steps + fs_a_pfc_product_padded_rightcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_product_padded_rightcoefficientscoefficientresiduebound. pfa_gap_product_padded_rightcoefficientscoefficientresiduebound + S (pfc_value_product_padded_rightcoefficients) = (p)) /\ ((exists pfa_offset_left_product_padded_rightcoefficientscoefficientresiduecongruence pfa_offset_right_product_padded_rightcoefficientscoefficientresiduecongruence. (pfc_natural_sum_product_padded_rightcoefficientscoefficient) + (p) * pfa_offset_left_product_padded_rightcoefficientscoefficientresiduecongruence = (pfc_value_product_padded_rightcoefficients) + (p) * pfa_offset_right_product_padded_rightcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (forall pfrep_power_product_equivalent_right pfrep_left_product_equivalent_right pfrep_right_product_equivalent_right. ((exists pfrep_position_product_equivalent_rightfirst. ((pfrep_position_product_equivalent_rightfirst+S (pfrep_power_product_equivalent_right)=(N)) /\ ((((exists ff_h_pfp_product_equivalent_rightfirstentry. ff_h_pfp_product_equivalent_rightfirstentry + S (pfrep_left_product_equivalent_right) = S ((S (pfrep_position_product_equivalent_rightfirst)) * cc)) /\ exists ff_q_pfp_product_equivalent_rightfirstentry. cb = ff_q_pfp_product_equivalent_rightfirstentry * S ((S (pfrep_position_product_equivalent_rightfirst)) * cc) + (pfrep_left_product_equivalent_right)))))) \/ (((exists pfrep_gap_product_equivalent_rightfirstoutside. pfrep_gap_product_equivalent_rightfirstoutside+(N)=(pfrep_power_product_equivalent_right)) /\ (((pfrep_left_product_equivalent_right)=0))))) -> ((exists pfrep_position_product_equivalent_rightsecond. ((pfrep_position_product_equivalent_rightsecond+S (pfrep_power_product_equivalent_right)=(K)) /\ ((((exists ff_h_pfp_product_equivalent_rightsecondentry. ff_h_pfp_product_equivalent_rightsecondentry + S (pfrep_right_product_equivalent_right) = S ((S (pfrep_position_product_equivalent_rightsecond)) * CC)) /\ exists ff_q_pfp_product_equivalent_rightsecondentry. CB = ff_q_pfp_product_equivalent_rightsecondentry * S ((S (pfrep_position_product_equivalent_rightsecond)) * CC) + (pfrep_right_product_equivalent_right)))))) \/ (((exists pfrep_gap_product_equivalent_rightsecondoutside. pfrep_gap_product_equivalent_rightsecondoutside+(K)=(pfrep_power_product_equivalent_right)) /\ (((pfrep_right_product_equivalent_right)=0))))) -> pfrep_left_product_equivalent_right=pfrep_right_product_equivalent_right)

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)
prime field polynomial zero prefix equivalent emptyprime field polynomial equivalent transitiveprime field polynomial equivalent symmetricpolynomial left pad zero prefixprime field polynomial convolution left padding nonempty rightprime 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 BB
  2. L12
    intro BC
  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 (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 (t+M)
  9. L57
    specialize prime_field_polynomial_convolution_zero_left (CB)
  10. L58
    specialize prime_field_polynomial_convolution_zero_left (CC)
11Use earlier factsL59–63

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
    exact hz
  5. L63
    exact hn
12Establish hecL64–69

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. L64
    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. L65
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (cb)
  3. L66
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (cc)
  4. L67
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (N)
  5. L68
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L69
    exact hc0
13Establish henL70–79

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. L70
    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. L71
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (CB)
  3. L72
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (CC)
  4. L73
    specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  5. L74
    apply prime_field_polynomial_zero_prefix_equivalent_empty
  6. L75
    exact hn0
  7. L76
    specialize prime_field_polynomial_equivalent_transitive (cb)
  8. L77
    specialize prime_field_polynomial_equivalent_transitive (cc)
  9. L78
    specialize prime_field_polynomial_equivalent_transitive (N)
  10. L79
    specialize prime_field_polynomial_equivalent_transitive (0)
14Use earlier factsL80–89

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

  1. L80
    specialize prime_field_polynomial_equivalent_transitive (0)
  2. L81
    specialize prime_field_polynomial_equivalent_transitive (0)
  3. L82
    specialize prime_field_polynomial_equivalent_transitive (CB)
  4. L83
    specialize prime_field_polynomial_equivalent_transitive (CC)
  5. L84
    specialize prime_field_polynomial_equivalent_transitive (K)
  6. L85
    apply prime_field_polynomial_equivalent_transitive
  7. L86
    exact hec
  8. L87
    specialize prime_field_polynomial_equivalent_symmetric (CB)
  9. L88
    specialize prime_field_polynomial_equivalent_symmetric (CC)
  10. L89
    specialize prime_field_polynomial_equivalent_symmetric (K)
15Use earlier factsL90–94

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

  1. L90
    specialize prime_field_polynomial_equivalent_symmetric (0)
  2. L91
    specialize prime_field_polynomial_equivalent_symmetric (0)
  3. L92
    specialize prime_field_polynomial_equivalent_symmetric (0)
  4. L93
    apply prime_field_polynomial_equivalent_symmetric
  5. L94
    exact hen
16Establish hML95–98

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

  1. L95
    have hM : M=0 \/ ~(M=0)
  2. L96
    specialize eq_decidable (M)
  3. L97
    specialize eq_decidable (0)
  4. L98
    apply eq_decidable
17Separate the logical casesL99–99

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

  1. L99
    cases hM
18Establish hzL100–103

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

  1. L100
  2. L101
    intro j
  3. L102
    intro hj
  4. L103
    rewrite hM_left at hj
19Separate the logical casesL104–104

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

  1. L104
    exfalso
20Use earlier factsL105–107

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

  1. L105
    specialize matrix_rank_no_index_below_zero (j)
  2. L106
    apply matrix_rank_no_index_below_zero
  3. L107
    exact hj
21Establish hc0L108–117

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

  1. L108
    have hc0 : Repeat(cb,cc,0,N)Definitions: Repeat(cb,cc,0,N)Original native command in the exact edition
  2. L109
    specialize prime_field_polynomial_convolution_zero_right (p)
  3. L110
    specialize prime_field_polynomial_convolution_zero_right (ab)
  4. L111
    specialize prime_field_polynomial_convolution_zero_right (ac)
  5. L112
    specialize prime_field_polynomial_convolution_zero_right (L)
  6. L113
    specialize prime_field_polynomial_convolution_zero_right (bb)
  7. L114
    specialize prime_field_polynomial_convolution_zero_right (bc)
  8. L115
    specialize prime_field_polynomial_convolution_zero_right (M)
  9. L116
    specialize prime_field_polynomial_convolution_zero_right (cb)
  10. L117
    specialize prime_field_polynomial_convolution_zero_right (cc)
22Use earlier factsL118–122

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

  1. L118
    specialize prime_field_polynomial_convolution_zero_right (N)
  2. L119
    apply prime_field_polynomial_convolution_zero_right
  3. L120
    exact hp
  4. L121
    exact hz
  5. L122
    exact hc
23Establish hn0L123–132

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

  1. L123
    have hn0 : Repeat(CB,CC,0,K)Definitions: Repeat(CB,CC,0,K)Original native command in the exact edition
  2. L124
    specialize prime_field_polynomial_convolution_zero_right (p)
  3. L125
    specialize prime_field_polynomial_convolution_zero_right (ab)
  4. L126
    specialize prime_field_polynomial_convolution_zero_right (ac)
  5. L127
    specialize prime_field_polynomial_convolution_zero_right (L)
  6. L128
    specialize prime_field_polynomial_convolution_zero_right (BB)
  7. L129
    specialize prime_field_polynomial_convolution_zero_right (BC)
  8. L130
    specialize prime_field_polynomial_convolution_zero_right (t+M)
  9. L131
    specialize prime_field_polynomial_convolution_zero_right (CB)
  10. L132
    specialize prime_field_polynomial_convolution_zero_right (CC)
24Use earlier factsL133–142

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

  1. L133
    specialize prime_field_polynomial_convolution_zero_right (K)
  2. L134
    apply prime_field_polynomial_convolution_zero_right
  3. L135
    exact hp
  4. L136
    specialize polynomial_left_pad_zero_prefix (bb)
  5. L137
    specialize polynomial_left_pad_zero_prefix (bc)
  6. L138
    specialize polynomial_left_pad_zero_prefix (M)
  7. L139
    specialize polynomial_left_pad_zero_prefix (t)
  8. L140
    specialize polynomial_left_pad_zero_prefix (BB)
  9. L141
    specialize polynomial_left_pad_zero_prefix (BC)
  10. L142
    apply polynomial_left_pad_zero_prefix
25Use earlier factsL143–145

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

  1. L143
    exact hz
  2. L144
    exact hpad
  3. 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_right (p)
  3. L179
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (ab)
  4. L180
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (ac)
  5. L181
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (L)
  6. L182
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (bb)
  7. L183
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (bc)
  8. L184
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (M)
  9. L185
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (cb)
  10. L186
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (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_right (N)
  2. L188
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (BB)
  3. L189
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (BC)
  4. L190
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (t)
  5. L191
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (CB)
  6. L192
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (CC)
  7. L193
    specialize prime_field_polynomial_convolution_left_padding_nonempty_right (K)
  8. L194
    apply prime_field_polynomial_convolution_left_padding_nonempty_right
  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 BB
  12. 0012intro BC
  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 (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 (t+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. 0062exact hz
  63. 0063exact hn
  64. 0064have hec : PolynomialEquivalent(cb,cc,N,0,0,0)
  65. 0065specialize prime_field_polynomial_zero_prefix_equivalent_empty (cb)
  66. 0066specialize prime_field_polynomial_zero_prefix_equivalent_empty (cc)
  67. 0067specialize prime_field_polynomial_zero_prefix_equivalent_empty (N)
  68. 0068apply prime_field_polynomial_zero_prefix_equivalent_empty
  69. 0069exact hc0
  70. 0070have hen : PolynomialEquivalent(CB,CC,K,0,0,0)
  71. 0071specialize prime_field_polynomial_zero_prefix_equivalent_empty (CB)
  72. 0072specialize prime_field_polynomial_zero_prefix_equivalent_empty (CC)
  73. 0073specialize prime_field_polynomial_zero_prefix_equivalent_empty (K)
  74. 0074apply prime_field_polynomial_zero_prefix_equivalent_empty
  75. 0075exact hn0
  76. 0076specialize prime_field_polynomial_equivalent_transitive (cb)
  77. 0077specialize prime_field_polynomial_equivalent_transitive (cc)
  78. 0078specialize prime_field_polynomial_equivalent_transitive (N)
  79. 0079specialize prime_field_polynomial_equivalent_transitive (0)
  80. 0080specialize prime_field_polynomial_equivalent_transitive (0)
  81. 0081specialize prime_field_polynomial_equivalent_transitive (0)
  82. 0082specialize prime_field_polynomial_equivalent_transitive (CB)
  83. 0083specialize prime_field_polynomial_equivalent_transitive (CC)
  84. 0084specialize prime_field_polynomial_equivalent_transitive (K)
  85. 0085apply prime_field_polynomial_equivalent_transitive
  86. 0086exact hec
  87. 0087specialize prime_field_polynomial_equivalent_symmetric (CB)
  88. 0088specialize prime_field_polynomial_equivalent_symmetric (CC)
  89. 0089specialize prime_field_polynomial_equivalent_symmetric (K)
  90. 0090specialize prime_field_polynomial_equivalent_symmetric (0)
  91. 0091specialize prime_field_polynomial_equivalent_symmetric (0)
  92. 0092specialize prime_field_polynomial_equivalent_symmetric (0)
  93. 0093apply prime_field_polynomial_equivalent_symmetric
  94. 0094exact hen
  95. 0095have hM : M=0 \/ ~(M=0)
  96. 0096specialize eq_decidable (M)
  97. 0097specialize eq_decidable (0)
  98. 0098apply eq_decidable
  99. 0099cases hM
  100. 0100have hz : Repeat(bb,bc,0,M)
  101. 0101intro j
  102. 0102intro hj
  103. 0103rewrite hM_left at hj
  104. 0104exfalso
  105. 0105specialize matrix_rank_no_index_below_zero (j)
  106. 0106apply matrix_rank_no_index_below_zero
  107. 0107exact hj
  108. 0108have hc0 : Repeat(cb,cc,0,N)
  109. 0109specialize prime_field_polynomial_convolution_zero_right (p)
  110. 0110specialize prime_field_polynomial_convolution_zero_right (ab)
  111. 0111specialize prime_field_polynomial_convolution_zero_right (ac)
  112. 0112specialize prime_field_polynomial_convolution_zero_right (L)
  113. 0113specialize prime_field_polynomial_convolution_zero_right (bb)
  114. 0114specialize prime_field_polynomial_convolution_zero_right (bc)
  115. 0115specialize prime_field_polynomial_convolution_zero_right (M)
  116. 0116specialize prime_field_polynomial_convolution_zero_right (cb)
  117. 0117specialize prime_field_polynomial_convolution_zero_right (cc)
  118. 0118specialize prime_field_polynomial_convolution_zero_right (N)
  119. 0119apply prime_field_polynomial_convolution_zero_right
  120. 0120exact hp
  121. 0121exact hz
  122. 0122exact hc
  123. 0123have hn0 : Repeat(CB,CC,0,K)
  124. 0124specialize prime_field_polynomial_convolution_zero_right (p)
  125. 0125specialize prime_field_polynomial_convolution_zero_right (ab)
  126. 0126specialize prime_field_polynomial_convolution_zero_right (ac)
  127. 0127specialize prime_field_polynomial_convolution_zero_right (L)
  128. 0128specialize prime_field_polynomial_convolution_zero_right (BB)
  129. 0129specialize prime_field_polynomial_convolution_zero_right (BC)
  130. 0130specialize prime_field_polynomial_convolution_zero_right (t+M)
  131. 0131specialize prime_field_polynomial_convolution_zero_right (CB)
  132. 0132specialize prime_field_polynomial_convolution_zero_right (CC)
  133. 0133specialize prime_field_polynomial_convolution_zero_right (K)
  134. 0134apply prime_field_polynomial_convolution_zero_right
  135. 0135exact hp
  136. 0136specialize polynomial_left_pad_zero_prefix (bb)
  137. 0137specialize polynomial_left_pad_zero_prefix (bc)
  138. 0138specialize polynomial_left_pad_zero_prefix (M)
  139. 0139specialize polynomial_left_pad_zero_prefix (t)
  140. 0140specialize polynomial_left_pad_zero_prefix (BB)
  141. 0141specialize polynomial_left_pad_zero_prefix (BC)
  142. 0142apply polynomial_left_pad_zero_prefix
  143. 0143exact hz
  144. 0144exact hpad
  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_right (p)
  179. 0179specialize prime_field_polynomial_convolution_left_padding_nonempty_right (ab)
  180. 0180specialize prime_field_polynomial_convolution_left_padding_nonempty_right (ac)
  181. 0181specialize prime_field_polynomial_convolution_left_padding_nonempty_right (L)
  182. 0182specialize prime_field_polynomial_convolution_left_padding_nonempty_right (bb)
  183. 0183specialize prime_field_polynomial_convolution_left_padding_nonempty_right (bc)
  184. 0184specialize prime_field_polynomial_convolution_left_padding_nonempty_right (M)
  185. 0185specialize prime_field_polynomial_convolution_left_padding_nonempty_right (cb)
  186. 0186specialize prime_field_polynomial_convolution_left_padding_nonempty_right (cc)
  187. 0187specialize prime_field_polynomial_convolution_left_padding_nonempty_right (N)
  188. 0188specialize prime_field_polynomial_convolution_left_padding_nonempty_right (BB)
  189. 0189specialize prime_field_polynomial_convolution_left_padding_nonempty_right (BC)
  190. 0190specialize prime_field_polynomial_convolution_left_padding_nonempty_right (t)
  191. 0191specialize prime_field_polynomial_convolution_left_padding_nonempty_right (CB)
  192. 0192specialize prime_field_polynomial_convolution_left_padding_nonempty_right (CC)
  193. 0193specialize prime_field_polynomial_convolution_left_padding_nonempty_right (K)
  194. 0194apply prime_field_polynomial_convolution_left_padding_nonempty_right
  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