PX002F

prime_field_polynomial_quotient_prefix_convolution_entry

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every actual convolution coefficient below the constructed quotient length equals the corresponding input coefficient, proved from the execution rather than assumed.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall p k ab ac bb bc d qb qc N b i r. (~((p) = 1) /\ forall pfa_factor_left_division_match_prime pfa_factor_right_division_match_prime. (p) = pfa_factor_left_division_match_prime * pfa_factor_right_division_match_prime -> pfa_factor_left_division_match_prime = 1 \/ pfa_factor_right_division_match_prime = 1) -> (((exists ff_h_pfp_division_match_head. ff_h_pfp_division_match_head + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_match_head. bb = ff_q_pfp_division_match_head * S ((S (0)) * bc) + (b))) -> (((~((b) = 0)) /\ ((((exists pfa_gap_division_match_inversemultiplicationleft. pfa_gap_division_match_inversemultiplicationleft + S (b) = (p)) /\ (((exists pfa_gap_division_match_inversemultiplicationright. pfa_gap_division_match_inversemultiplicationright + S (k) = (p)) /\ ((((exists pfa_gap_division_match_inversemultiplicationresultbound. pfa_gap_division_match_inversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_match_inversemultiplicationresultcongruence pfa_offset_right_division_match_inversemultiplicationresultcongruence. ((b) * (k)) + (p) * pfa_offset_left_division_match_inversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_match_inversemultiplicationresultcongruence)))))))))))) -> (forall pfd_index_division_match_execution. (exists pfa_gap_division_match_executionbound. pfa_gap_division_match_executionbound + S (pfd_index_division_match_execution) = (N)) -> exists pfd_value_division_match_execution. ((((exists ff_h_pfp_division_match_executionentry. ff_h_pfp_division_match_executionentry + S (pfd_value_division_match_execution) = S ((S (pfd_index_division_match_execution)) * qc)) /\ exists ff_q_pfp_division_match_executionentry. qb = ff_q_pfp_division_match_executionentry * S ((S (pfd_index_division_match_execution)) * qc) + (pfd_value_division_match_execution))) /\ ((exists pfd_input_division_match_executionstep pfd_previous_division_match_executionstep pfd_difference_division_match_executionstep. ((((exists ff_h_pfp_division_match_executionstepinput. ff_h_pfp_division_match_executionstepinput + S (pfd_input_division_match_executionstep) = S ((S (pfd_index_division_match_execution)) * ac)) /\ exists ff_q_pfp_division_match_executionstepinput. ab = ff_q_pfp_division_match_executionstepinput * S ((S (pfd_index_division_match_execution)) * ac) + (pfd_input_division_match_executionstep))) /\ (((exists pfc_terms_code_division_match_executionstepprevious pfc_terms_scale_division_match_executionstepprevious pfc_natural_sum_division_match_executionstepprevious. ((forall pfc_index_division_match_executionsteppreviousdiagonal. (exists pfa_gap_division_match_executionsteppreviousdiagonalbound. pfa_gap_division_match_executionsteppreviousdiagonalbound + S (pfc_index_division_match_executionsteppreviousdiagonal) = (S (pfd_index_division_match_execution))) -> exists pfc_value_division_match_executionsteppreviousdiagonal. ((((exists ff_h_pfp_division_match_executionsteppreviousdiagonalentry. ff_h_pfp_division_match_executionsteppreviousdiagonalentry + S (pfc_value_division_match_executionsteppreviousdiagonal) = S ((S (pfc_index_division_match_executionsteppreviousdiagonal)) * pfc_terms_scale_division_match_executionstepprevious)) /\ exists ff_q_pfp_division_match_executionsteppreviousdiagonalentry. pfc_terms_code_division_match_executionstepprevious = ff_q_pfp_division_match_executionsteppreviousdiagonalentry * S ((S (pfc_index_division_match_executionsteppreviousdiagonal)) * pfc_terms_scale_division_match_executionstepprevious) + (pfc_value_division_match_executionsteppreviousdiagonal))) /\ ((exists pfc_complement_division_match_executionsteppreviousdiagonalterm pfc_left_division_match_executionsteppreviousdiagonalterm pfc_right_division_match_executionsteppreviousdiagonalterm. (((pfc_index_division_match_executionsteppreviousdiagonal)+pfc_complement_division_match_executionsteppreviousdiagonalterm=(pfd_index_division_match_execution)) /\ ((((((exists pfa_gap_division_match_executionsteppreviousdiagonaltermleftinside. pfa_gap_division_match_executionsteppreviousdiagonaltermleftinside + S (pfc_index_division_match_executionsteppreviousdiagonal) = (pfd_index_division_match_execution)) /\ ((((exists ff_h_pfp_division_match_executionsteppreviousdiagonaltermleftentry. ff_h_pfp_division_match_executionsteppreviousdiagonaltermleftentry + S (pfc_left_division_match_executionsteppreviousdiagonalterm) = S ((S (pfc_index_division_match_executionsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_match_executionsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_match_executionsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_match_executionsteppreviousdiagonal)) * qc) + (pfc_left_division_match_executionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_match_executionsteppreviousdiagonaltermleftoutside. pfc_gap_division_match_executionsteppreviousdiagonaltermleftoutside+(pfd_index_division_match_execution)=(pfc_index_division_match_executionsteppreviousdiagonal)) /\ (((pfc_left_division_match_executionsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_match_executionsteppreviousdiagonaltermrightinside. pfa_gap_division_match_executionsteppreviousdiagonaltermrightinside + S (pfc_complement_division_match_executionsteppreviousdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_match_executionsteppreviousdiagonaltermrightentry. ff_h_pfp_division_match_executionsteppreviousdiagonaltermrightentry + S (pfc_right_division_match_executionsteppreviousdiagonalterm) = S ((S (pfc_complement_division_match_executionsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_match_executionsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_match_executionsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_match_executionsteppreviousdiagonalterm)) * bc) + (pfc_right_division_match_executionsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_match_executionsteppreviousdiagonaltermrightoutside. pfc_gap_division_match_executionsteppreviousdiagonaltermrightoutside+(S d)=(pfc_complement_division_match_executionsteppreviousdiagonalterm)) /\ (((pfc_right_division_match_executionsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_match_executionsteppreviousdiagonal)=pfc_left_division_match_executionsteppreviousdiagonalterm*pfc_right_division_match_executionsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_match_executionstepprevioussum fs_v_pfc_division_match_executionstepprevioussum. ((((exists fs_h_pfc_division_match_executionstepprevioussum_body_start. fs_h_pfc_division_match_executionstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_match_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_executionstepprevioussum_body_start. fs_u_pfc_division_match_executionstepprevioussum = fs_q_pfc_division_match_executionstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_match_executionstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_match_executionstepprevioussum_body_terminal. fs_h_pfc_division_match_executionstepprevioussum_body_terminal + S (pfc_natural_sum_division_match_executionstepprevious) = S ((S (S (pfd_index_division_match_execution))) * fs_v_pfc_division_match_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_executionstepprevioussum_body_terminal. fs_u_pfc_division_match_executionstepprevioussum = fs_q_pfc_division_match_executionstepprevioussum_body_terminal * S ((S (S (pfd_index_division_match_execution))) * fs_v_pfc_division_match_executionstepprevioussum) + (pfc_natural_sum_division_match_executionstepprevious))) /\ forall fs_i_pfc_division_match_executionstepprevioussum_body_steps. (exists fs_lt_pfc_division_match_executionstepprevioussum_body_steps_bound. fs_lt_pfc_division_match_executionstepprevioussum_body_steps_bound + S fs_i_pfc_division_match_executionstepprevioussum_body_steps = S (pfd_index_division_match_execution)) -> exists fs_a_pfc_division_match_executionstepprevioussum_body_steps fs_r_pfc_division_match_executionstepprevioussum_body_steps fs_s_pfc_division_match_executionstepprevioussum_body_steps. ((((exists fs_h_pfc_division_match_executionstepprevioussum_body_steps_summand. fs_h_pfc_division_match_executionstepprevioussum_body_steps_summand + S (fs_a_pfc_division_match_executionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * pfc_terms_scale_division_match_executionstepprevious)) /\ exists fs_q_pfc_division_match_executionstepprevioussum_body_steps_summand. pfc_terms_code_division_match_executionstepprevious = fs_q_pfc_division_match_executionstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * pfc_terms_scale_division_match_executionstepprevious) + (fs_a_pfc_division_match_executionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_match_executionstepprevioussum_body_steps_partial. fs_h_pfc_division_match_executionstepprevioussum_body_steps_partial + S (fs_r_pfc_division_match_executionstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_executionstepprevioussum_body_steps_partial. fs_u_pfc_division_match_executionstepprevioussum = fs_q_pfc_division_match_executionstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_executionstepprevioussum) + (fs_r_pfc_division_match_executionstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_match_executionstepprevioussum_body_steps_successor. fs_h_pfc_division_match_executionstepprevioussum_body_steps_successor + S (fs_s_pfc_division_match_executionstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_executionstepprevioussum)) /\ exists fs_q_pfc_division_match_executionstepprevioussum_body_steps_successor. fs_u_pfc_division_match_executionstepprevioussum = fs_q_pfc_division_match_executionstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_match_executionstepprevioussum_body_steps)) * fs_v_pfc_division_match_executionstepprevioussum) + (fs_s_pfc_division_match_executionstepprevioussum_body_steps))) /\ fs_s_pfc_division_match_executionstepprevioussum_body_steps = fs_r_pfc_division_match_executionstepprevioussum_body_steps + fs_a_pfc_division_match_executionstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_match_executionsteppreviousresiduebound. pfa_gap_division_match_executionsteppreviousresiduebound + S (pfd_previous_division_match_executionstep) = (p)) /\ ((exists pfa_offset_left_division_match_executionsteppreviousresiduecongruence pfa_offset_right_division_match_executionsteppreviousresiduecongruence. (pfc_natural_sum_division_match_executionstepprevious) + (p) * pfa_offset_left_division_match_executionsteppreviousresiduecongruence = (pfd_previous_division_match_executionstep) + (p) * pfa_offset_right_division_match_executionsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_match_executionstepsubtractleft. pfa_gap_division_match_executionstepsubtractleft + S (pfd_previous_division_match_executionstep) = (p)) /\ (((exists pfa_gap_division_match_executionstepsubtractright. pfa_gap_division_match_executionstepsubtractright + S (pfd_difference_division_match_executionstep) = (p)) /\ ((((exists pfa_gap_division_match_executionstepsubtractresultbound. pfa_gap_division_match_executionstepsubtractresultbound + S (pfd_input_division_match_executionstep) = (p)) /\ ((exists pfa_offset_left_division_match_executionstepsubtractresultcongruence pfa_offset_right_division_match_executionstepsubtractresultcongruence. ((pfd_previous_division_match_executionstep) + (pfd_difference_division_match_executionstep)) + (p) * pfa_offset_left_division_match_executionstepsubtractresultcongruence = (pfd_input_division_match_executionstep) + (p) * pfa_offset_right_division_match_executionstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_match_executionstepmultiplyleft. pfa_gap_division_match_executionstepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_match_executionstepmultiplyright. pfa_gap_division_match_executionstepmultiplyright + S (pfd_difference_division_match_executionstep) = (p)) /\ ((((exists pfa_gap_division_match_executionstepmultiplyresultbound. pfa_gap_division_match_executionstepmultiplyresultbound + S (pfd_value_division_match_execution) = (p)) /\ ((exists pfa_offset_left_division_match_executionstepmultiplyresultcongruence pfa_offset_right_division_match_executionstepmultiplyresultcongruence. ((k) * (pfd_difference_division_match_executionstep)) + (p) * pfa_offset_left_division_match_executionstepmultiplyresultcongruence = (pfd_value_division_match_execution) + (p) * pfa_offset_right_division_match_executionstepmultiplyresultcongruence))))))))))))))))))) -> (exists pfa_gap_division_match_index. pfa_gap_division_match_index + S (i) = (N)) -> (exists pfc_terms_code_division_match_actual_coefficient pfc_terms_scale_division_match_actual_coefficient pfc_natural_sum_division_match_actual_coefficient. ((forall pfc_index_division_match_actual_coefficientdiagonal. (exists pfa_gap_division_match_actual_coefficientdiagonalbound. pfa_gap_division_match_actual_coefficientdiagonalbound + S (pfc_index_division_match_actual_coefficientdiagonal) = (S (i))) -> exists pfc_value_division_match_actual_coefficientdiagonal. ((((exists ff_h_pfp_division_match_actual_coefficientdiagonalentry. ff_h_pfp_division_match_actual_coefficientdiagonalentry + S (pfc_value_division_match_actual_coefficientdiagonal) = S ((S (pfc_index_division_match_actual_coefficientdiagonal)) * pfc_terms_scale_division_match_actual_coefficient)) /\ exists ff_q_pfp_division_match_actual_coefficientdiagonalentry. pfc_terms_code_division_match_actual_coefficient = ff_q_pfp_division_match_actual_coefficientdiagonalentry * S ((S (pfc_index_division_match_actual_coefficientdiagonal)) * pfc_terms_scale_division_match_actual_coefficient) + (pfc_value_division_match_actual_coefficientdiagonal))) /\ ((exists pfc_complement_division_match_actual_coefficientdiagonalterm pfc_left_division_match_actual_coefficientdiagonalterm pfc_right_division_match_actual_coefficientdiagonalterm. (((pfc_index_division_match_actual_coefficientdiagonal)+pfc_complement_division_match_actual_coefficientdiagonalterm=(i)) /\ ((((((exists pfa_gap_division_match_actual_coefficientdiagonaltermleftinside. pfa_gap_division_match_actual_coefficientdiagonaltermleftinside + S (pfc_index_division_match_actual_coefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_division_match_actual_coefficientdiagonaltermleftentry. ff_h_pfp_division_match_actual_coefficientdiagonaltermleftentry + S (pfc_left_division_match_actual_coefficientdiagonalterm) = S ((S (pfc_index_division_match_actual_coefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_match_actual_coefficientdiagonaltermleftentry. qb = ff_q_pfp_division_match_actual_coefficientdiagonaltermleftentry * S ((S (pfc_index_division_match_actual_coefficientdiagonal)) * qc) + (pfc_left_division_match_actual_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_match_actual_coefficientdiagonaltermleftoutside. pfc_gap_division_match_actual_coefficientdiagonaltermleftoutside+(N)=(pfc_index_division_match_actual_coefficientdiagonal)) /\ (((pfc_left_division_match_actual_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_match_actual_coefficientdiagonaltermrightinside. pfa_gap_division_match_actual_coefficientdiagonaltermrightinside + S (pfc_complement_division_match_actual_coefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_match_actual_coefficientdiagonaltermrightentry. ff_h_pfp_division_match_actual_coefficientdiagonaltermrightentry + S (pfc_right_division_match_actual_coefficientdiagonalterm) = S ((S (pfc_complement_division_match_actual_coefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_match_actual_coefficientdiagonaltermrightentry. bb = ff_q_pfp_division_match_actual_coefficientdiagonaltermrightentry * S ((S (pfc_complement_division_match_actual_coefficientdiagonalterm)) * bc) + (pfc_right_division_match_actual_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_match_actual_coefficientdiagonaltermrightoutside. pfc_gap_division_match_actual_coefficientdiagonaltermrightoutside+(S d)=(pfc_complement_division_match_actual_coefficientdiagonalterm)) /\ (((pfc_right_division_match_actual_coefficientdiagonalterm)=0))))) /\ (((pfc_value_division_match_actual_coefficientdiagonal)=pfc_left_division_match_actual_coefficientdiagonalterm*pfc_right_division_match_actual_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_match_actual_coefficientsum fs_v_pfc_division_match_actual_coefficientsum. ((((exists fs_h_pfc_division_match_actual_coefficientsum_body_start. fs_h_pfc_division_match_actual_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_match_actual_coefficientsum)) /\ exists fs_q_pfc_division_match_actual_coefficientsum_body_start. fs_u_pfc_division_match_actual_coefficientsum = fs_q_pfc_division_match_actual_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_match_actual_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_match_actual_coefficientsum_body_terminal. fs_h_pfc_division_match_actual_coefficientsum_body_terminal + S (pfc_natural_sum_division_match_actual_coefficient) = S ((S (S (i))) * fs_v_pfc_division_match_actual_coefficientsum)) /\ exists fs_q_pfc_division_match_actual_coefficientsum_body_terminal. fs_u_pfc_division_match_actual_coefficientsum = fs_q_pfc_division_match_actual_coefficientsum_body_terminal * S ((S (S (i))) * fs_v_pfc_division_match_actual_coefficientsum) + (pfc_natural_sum_division_match_actual_coefficient))) /\ forall fs_i_pfc_division_match_actual_coefficientsum_body_steps. (exists fs_lt_pfc_division_match_actual_coefficientsum_body_steps_bound. fs_lt_pfc_division_match_actual_coefficientsum_body_steps_bound + S fs_i_pfc_division_match_actual_coefficientsum_body_steps = S (i)) -> exists fs_a_pfc_division_match_actual_coefficientsum_body_steps fs_r_pfc_division_match_actual_coefficientsum_body_steps fs_s_pfc_division_match_actual_coefficientsum_body_steps. ((((exists fs_h_pfc_division_match_actual_coefficientsum_body_steps_summand. fs_h_pfc_division_match_actual_coefficientsum_body_steps_summand + S (fs_a_pfc_division_match_actual_coefficientsum_body_steps) = S ((S (fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * pfc_terms_scale_division_match_actual_coefficient)) /\ exists fs_q_pfc_division_match_actual_coefficientsum_body_steps_summand. pfc_terms_code_division_match_actual_coefficient = fs_q_pfc_division_match_actual_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * pfc_terms_scale_division_match_actual_coefficient) + (fs_a_pfc_division_match_actual_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_match_actual_coefficientsum_body_steps_partial. fs_h_pfc_division_match_actual_coefficientsum_body_steps_partial + S (fs_r_pfc_division_match_actual_coefficientsum_body_steps) = S ((S (fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * fs_v_pfc_division_match_actual_coefficientsum)) /\ exists fs_q_pfc_division_match_actual_coefficientsum_body_steps_partial. fs_u_pfc_division_match_actual_coefficientsum = fs_q_pfc_division_match_actual_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * fs_v_pfc_division_match_actual_coefficientsum) + (fs_r_pfc_division_match_actual_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_match_actual_coefficientsum_body_steps_successor. fs_h_pfc_division_match_actual_coefficientsum_body_steps_successor + S (fs_s_pfc_division_match_actual_coefficientsum_body_steps) = S ((S (S fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * fs_v_pfc_division_match_actual_coefficientsum)) /\ exists fs_q_pfc_division_match_actual_coefficientsum_body_steps_successor. fs_u_pfc_division_match_actual_coefficientsum = fs_q_pfc_division_match_actual_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_match_actual_coefficientsum_body_steps)) * fs_v_pfc_division_match_actual_coefficientsum) + (fs_s_pfc_division_match_actual_coefficientsum_body_steps))) /\ fs_s_pfc_division_match_actual_coefficientsum_body_steps = fs_r_pfc_division_match_actual_coefficientsum_body_steps + fs_a_pfc_division_match_actual_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_match_actual_coefficientresiduebound. pfa_gap_division_match_actual_coefficientresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_division_match_actual_coefficientresiduecongruence pfa_offset_right_division_match_actual_coefficientresiduecongruence. (pfc_natural_sum_division_match_actual_coefficient) + (p) * pfa_offset_left_division_match_actual_coefficientresiduecongruence = (r) + (p) * pfa_offset_right_division_match_actual_coefficientresiduecongruence))))))))) -> (((exists ff_h_pfp_division_match_input. ff_h_pfp_division_match_input + S (r) = S ((S (i)) * ac)) /\ exists ff_q_pfp_division_match_input. ab = ff_q_pfp_division_match_input * S ((S (i)) * ac) + (r)))

Constructive proof overview

Generated structural guide

Every actual convolution coefficient below the constructed quotient length equals the corresponding input coefficient, proved from the execution rather than assumed.

The unchanged tactic script uses 5 declared prerequisites and contains 121 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_field_multiply_exists Alpha theorem; checked-use authorized PX0003 prime_field_convolution_coefficient_prefix_transport le_refl Alpha theorem; checked-use authorized PX0008 prime_field_convolution_coefficient_append PX0027 prime_field_polynomial_quotient_scalar_cancellation

Direct dependents

PX0030 prime_field_polynomial_quotient_prefix_product_matches

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

121 script commands · 24 reading checkpoints · 7 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (3)
prime field convolution coefficient prefix transportprime field convolution coefficient appendprime field polynomial quotient scalar cancellation

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro d
  8. L8
    intro qb
  9. L9
    intro qc
  10. L10
    intro N
02Fix variables and assumptionsL11–19

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

  1. L11
    intro b
  2. L12
    intro i
  3. L13
    intro r
  4. L14
    intro hp
  5. L15
    intro hb
  6. L16
    intro hk
  7. L17
    intro hq
  8. L18
    intro hi
  9. L19
    intro hr
03Establish hpointL20–23

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

  1. L20
    have hpoint : ∃ q. BetaAt(qb,qc,i,q) ∧ FpPolynomialQuotientStep(p,k,ab,ac,bb,bc,S d,qb,qc,i,q)Definitions: FpPolynomialQuotientStepBetaAt
  2. L21
    specialize hq (i)
  3. L22
    apply hq
  4. L23
    exact hi
04Separate the logical casesL24–31

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

  1. L24
    cases hpoint
  2. L25
    cases hpoint_witness
  3. L26
    cases hpoint_witness_right
  4. L27
    cases hpoint_witness_right_witness
  5. L28
    cases hpoint_witness_right_witness_witness
  6. L29
    cases hpoint_witness_right_witness_witness_witness
  7. L30
    cases hpoint_witness_right_witness_witness_witness_right
  8. L31
    cases hpoint_witness_right_witness_witness_witness_right_right
05Establish hqboundL32–32

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

  1. L32
    have hqbound : exists pfa_gap_division_match_value_bound. pfa_gap_division_match_value_bound + S (x) = (p)
06Separate the logical casesL33–35

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

  1. L33
    cases hpoint_witness_right_witness_witness_witness_right_right_right
  2. L34
    cases hpoint_witness_right_witness_witness_witness_right_right_right_right
  3. L35
    cases hpoint_witness_right_witness_witness_witness_right_right_right_right_right
07Use earlier factsL36–36

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

  1. L36
    exact hpoint_witness_right_witness_witness_witness_right_right_right_right_right_left
08Establish hbndL37–37

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

  1. L37
    have hbnd : exists pfa_gap_division_match_head_bound. pfa_gap_division_match_head_bound + S (b) = (p)
09Separate the logical casesL38–39

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

  1. L38
    cases hk
  2. L39
    cases hk_right
10Use earlier factsL40–40

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

  1. L40
    exact hk_right_left
11Establish hproductL41–48

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

  1. L41
    have hproduct : ∃ t. FpMul(p,x,b,t)Definitions: FpMul
  2. L42
    specialize prime_field_multiply_exists (p)
  3. L43
    specialize prime_field_multiply_exists (x)
  4. L44
    specialize prime_field_multiply_exists (b)
  5. L45
    apply prime_field_multiply_exists
  6. L46
    exact hp
  7. L47
    exact hqbound
  8. L48
    exact hbnd
12Separate the logical casesL49–49

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

  1. L49
    cases hproduct
13Establish hshortL50–59

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

  1. L50
    have hshort : FpConvolutionCoefficient(p,qb,qc,S i,bb,bc,S d,i,r)Definitions: FpConvolutionCoefficient
  2. L51
    specialize prime_field_convolution_coefficient_prefix_transport (p)
  3. L52
    specialize prime_field_convolution_coefficient_prefix_transport (qb)
  4. L53
    specialize prime_field_convolution_coefficient_prefix_transport (qc)
  5. L54
    specialize prime_field_convolution_coefficient_prefix_transport (N)
  6. L55
    specialize prime_field_convolution_coefficient_prefix_transport (qb)
  7. L56
    specialize prime_field_convolution_coefficient_prefix_transport (qc)
  8. L57
    specialize prime_field_convolution_coefficient_prefix_transport (S i)
  9. L58
    specialize prime_field_convolution_coefficient_prefix_transport (bb)
  10. L59
    specialize prime_field_convolution_coefficient_prefix_transport (bc)
14Use earlier factsL60–67

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

  1. L60
    specialize prime_field_convolution_coefficient_prefix_transport (S d)
  2. L61
    specialize prime_field_convolution_coefficient_prefix_transport (S i)
  3. L62
    specialize prime_field_convolution_coefficient_prefix_transport (i)
  4. L63
    specialize prime_field_convolution_coefficient_prefix_transport (r)
  5. L64
    apply prime_field_convolution_coefficient_prefix_transport
  6. L65
    exact hi
  7. L66
    specialize le_refl (S i)
  8. L67
    apply le_refl
15Fix variables and assumptionsL68–71

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

  1. L68
    intro j
  2. L69
    intro v
  3. L70
    intro hj
  4. L71
    intro hv
16Use earlier factsL72–75

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

  1. L72
    exact hv
  2. L73
    specialize le_refl (S i)
  3. L74
    apply le_refl
  4. L75
    exact hr
17Establish hsumL76–85

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

  1. L76
    have hsum : ((exists pfa_gap_division_match_sumleft. pfa_gap_division_match_sumleft + S (x2) = (p)) /\ (((exists pfa_gap_division_match_sumright. pfa_gap_division_match_sumright + S (x4) = (p)) /\ ((((exists pfa_gap_division_match_sumresultbound. pfa_gap_division_match_sumresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_division_match_sumresultcongruence pfa_offset_right_division_match_sumresultcongruence. ((x2) + (x4)) + (p) * pfa_offset_left_division_match_sumresultcongruence = (r) + (p) * pfa_offset_right_division_match_sumresultcongruence))))))))
  2. L77
    specialize prime_field_convolution_coefficient_append (p)
  3. L78
    specialize prime_field_convolution_coefficient_append (qb)
  4. L79
    specialize prime_field_convolution_coefficient_append (qc)
  5. L80
    specialize prime_field_convolution_coefficient_append (qb)
  6. L81
    specialize prime_field_convolution_coefficient_append (qc)
  7. L82
    specialize prime_field_convolution_coefficient_append (bb)
  8. L83
    specialize prime_field_convolution_coefficient_append (bc)
  9. L84
    specialize prime_field_convolution_coefficient_append (d)
  10. L85
    specialize prime_field_convolution_coefficient_append (i)
18Use earlier factsL86–91

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

  1. L86
    specialize prime_field_convolution_coefficient_append (x)
  2. L87
    specialize prime_field_convolution_coefficient_append (b)
  3. L88
    specialize prime_field_convolution_coefficient_append (x2)
  4. L89
    specialize prime_field_convolution_coefficient_append (x4)
  5. L90
    specialize prime_field_convolution_coefficient_append (r)
  6. L91
    apply prime_field_convolution_coefficient_append
19Fix variables and assumptionsL92–95

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

  1. L92
    intro j
  2. L93
    intro v
  3. L94
    intro hj
  4. L95
    intro hv
20Use earlier factsL96–101

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

  1. L96
    exact hv
  2. L97
    exact hpoint_witness_left
  3. L98
    exact hb
  4. L99
    exact hpoint_witness_right_witness_witness_witness_right_left
  5. L100
    exact hshort
  6. L101
    exact hproduct_witness
21Establish heqL102–111

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

  1. L102
    have heq : r=x1
  2. L103
    specialize prime_field_polynomial_quotient_scalar_cancellation (p)
  3. L104
    specialize prime_field_polynomial_quotient_scalar_cancellation (b)
  4. L105
    specialize prime_field_polynomial_quotient_scalar_cancellation (k)
  5. L106
    specialize prime_field_polynomial_quotient_scalar_cancellation (x2)
  6. L107
    specialize prime_field_polynomial_quotient_scalar_cancellation (x3)
  7. L108
    specialize prime_field_polynomial_quotient_scalar_cancellation (x1)
  8. L109
    specialize prime_field_polynomial_quotient_scalar_cancellation (x)
  9. L110
    specialize prime_field_polynomial_quotient_scalar_cancellation (x4)
  10. L111
    specialize prime_field_polynomial_quotient_scalar_cancellation (r)
22Use earlier factsL112–118

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

  1. L112
    apply prime_field_polynomial_quotient_scalar_cancellation
  2. L113
    exact hp
  3. L114
    exact hk
  4. L115
    exact hpoint_witness_right_witness_witness_witness_right_right_left
  5. L116
    exact hpoint_witness_right_witness_witness_witness_right_right_right
  6. L117
    exact hproduct_witness
  7. L118
    exact hsum
23Calculate and transport equalitiesL119–120

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

  1. L119
    rewrite heq
  2. L120
    rewrite heq
24Use earlier factsL121–121

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

  1. L121
    exact hpoint_witness_right_witness_witness_witness_left

Library-wide reading audit

Original exact command ledger · 121 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro d
  8. 0008intro qb
  9. 0009intro qc
  10. 0010intro N
  11. 0011intro b
  12. 0012intro i
  13. 0013intro r
  14. 0014intro hp
  15. 0015intro hb
  16. 0016intro hk
  17. 0017intro hq
  18. 0018intro hi
  19. 0019intro hr
  20. 0020have hpoint : exists q. ((((exists ff_h_pfp_division_match_quotient_entry. ff_h_pfp_division_match_quotient_entry + S (q) = S ((S (i)) * qc)) /\ exists ff_q_pfp_division_match_quotient_entry. qb = ff_q_pfp_division_match_quotient_entry * S ((S (i)) * qc) + (q))) /\ ((exists pfd_input_division_match_step pfd_previous_division_match_step pfd_difference_division_match_step. ((((exists ff_h_pfp_division_match_stepinput. ff_h_pfp_division_match_stepinput + S (pfd_input_division_match_step) = S ((S (i)) * ac)) /\ exists ff_q_pfp_division_match_stepinput. ab = ff_q_pfp_division_match_stepinput * S ((S (i)) * ac) + (pfd_input_division_match_step))) /\ (((exists pfc_terms_code_division_match_stepprevious pfc_terms_scale_division_match_stepprevious pfc_natural_sum_division_match_stepprevious. ((forall pfc_index_division_match_steppreviousdiagonal. (exists pfa_gap_division_match_steppreviousdiagonalbound. pfa_gap_division_match_steppreviousdiagonalbound + S (pfc_index_division_match_steppreviousdiagonal) = (S (i))) -> exists pfc_value_division_match_steppreviousdiagonal. ((((exists ff_h_pfp_division_match_steppreviousdiagonalentry. ff_h_pfp_division_match_steppreviousdiagonalentry + S (pfc_value_division_match_steppreviousdiagonal) = S ((S (pfc_index_division_match_steppreviousdiagonal)) * pfc_terms_scale_division_match_stepprevious)) /\ exists ff_q_pfp_division_match_steppreviousdiagonalentry. pfc_terms_code_division_match_stepprevious = ff_q_pfp_division_match_steppreviousdiagonalentry * S ((S (pfc_index_division_match_steppreviousdiagonal)) * pfc_terms_scale_division_match_stepprevious) + (pfc_value_division_match_steppreviousdiagonal))) /\ ((exists pfc_complement_division_match_steppreviousdiagonalterm pfc_left_division_match_steppreviousdiagonalterm pfc_right_division_match_steppreviousdiagonalterm. (((pfc_index_division_match_steppreviousdiagonal)+pfc_complement_division_match_steppreviousdiagonalterm=(i)) /\ ((((((exists pfa_gap_division_match_steppreviousdiagonaltermleftinside. pfa_gap_division_match_steppreviousdiagonaltermleftinside + S (pfc_index_division_match_steppreviousdiagonal) = (i)) /\ ((((exists ff_h_pfp_division_match_steppreviousdiagonaltermleftentry. ff_h_pfp_division_match_steppreviousdiagonaltermleftentry + S (pfc_left_division_match_steppreviousdiagonalterm) = S ((S (pfc_index_division_match_steppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_match_steppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_match_steppreviousdiagonaltermleftentry * S ((S (pfc_index_division_match_steppreviousdiagonal)) * qc) + (pfc_left_division_match_steppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_match_steppreviousdiagonaltermleftoutside. pfc_gap_division_match_steppreviousdiagonaltermleftoutside+(i)=(pfc_index_division_match_steppreviousdiagonal)) /\ (((pfc_left_division_match_steppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_match_steppreviousdiagonaltermrightinside. pfa_gap_division_match_steppreviousdiagonaltermrightinside + S (pfc_complement_division_match_steppreviousdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_match_steppreviousdiagonaltermrightentry. ff_h_pfp_division_match_steppreviousdiagonaltermrightentry + S (pfc_right_division_match_steppreviousdiagonalterm) = S ((S (pfc_complement_division_match_steppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_match_steppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_match_steppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_match_steppreviousdiagonalterm)) * bc) + (pfc_right_division_match_steppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_match_steppreviousdiagonaltermrightoutside. pfc_gap_division_match_steppreviousdiagonaltermrightoutside+(S d)=(pfc_complement_division_match_steppreviousdiagonalterm)) /\ (((pfc_right_division_match_steppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_match_steppreviousdiagonal)=pfc_left_division_match_steppreviousdiagonalterm*pfc_right_division_match_steppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_match_stepprevioussum fs_v_pfc_division_match_stepprevioussum. ((((exists fs_h_pfc_division_match_stepprevioussum_body_start. fs_h_pfc_division_match_stepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_match_stepprevioussum)) /\ exists fs_q_pfc_division_match_stepprevioussum_body_start. fs_u_pfc_division_match_stepprevioussum = fs_q_pfc_division_match_stepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_match_stepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_match_stepprevioussum_body_terminal. fs_h_pfc_division_match_stepprevioussum_body_terminal + S (pfc_natural_sum_division_match_stepprevious) = S ((S (S (i))) * fs_v_pfc_division_match_stepprevioussum)) /\ exists fs_q_pfc_division_match_stepprevioussum_body_terminal. fs_u_pfc_division_match_stepprevioussum = fs_q_pfc_division_match_stepprevioussum_body_terminal * S ((S (S (i))) * fs_v_pfc_division_match_stepprevioussum) + (pfc_natural_sum_division_match_stepprevious))) /\ forall fs_i_pfc_division_match_stepprevioussum_body_steps. (exists fs_lt_pfc_division_match_stepprevioussum_body_steps_bound. fs_lt_pfc_division_match_stepprevioussum_body_steps_bound + S fs_i_pfc_division_match_stepprevioussum_body_steps = S (i)) -> exists fs_a_pfc_division_match_stepprevioussum_body_steps fs_r_pfc_division_match_stepprevioussum_body_steps fs_s_pfc_division_match_stepprevioussum_body_steps. ((((exists fs_h_pfc_division_match_stepprevioussum_body_steps_summand. fs_h_pfc_division_match_stepprevioussum_body_steps_summand + S (fs_a_pfc_division_match_stepprevioussum_body_steps) = S ((S (fs_i_pfc_division_match_stepprevioussum_body_steps)) * pfc_terms_scale_division_match_stepprevious)) /\ exists fs_q_pfc_division_match_stepprevioussum_body_steps_summand. pfc_terms_code_division_match_stepprevious = fs_q_pfc_division_match_stepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_match_stepprevioussum_body_steps)) * pfc_terms_scale_division_match_stepprevious) + (fs_a_pfc_division_match_stepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_match_stepprevioussum_body_steps_partial. fs_h_pfc_division_match_stepprevioussum_body_steps_partial + S (fs_r_pfc_division_match_stepprevioussum_body_steps) = S ((S (fs_i_pfc_division_match_stepprevioussum_body_steps)) * fs_v_pfc_division_match_stepprevioussum)) /\ exists fs_q_pfc_division_match_stepprevioussum_body_steps_partial. fs_u_pfc_division_match_stepprevioussum = fs_q_pfc_division_match_stepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_match_stepprevioussum_body_steps)) * fs_v_pfc_division_match_stepprevioussum) + (fs_r_pfc_division_match_stepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_match_stepprevioussum_body_steps_successor. fs_h_pfc_division_match_stepprevioussum_body_steps_successor + S (fs_s_pfc_division_match_stepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_match_stepprevioussum_body_steps)) * fs_v_pfc_division_match_stepprevioussum)) /\ exists fs_q_pfc_division_match_stepprevioussum_body_steps_successor. fs_u_pfc_division_match_stepprevioussum = fs_q_pfc_division_match_stepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_match_stepprevioussum_body_steps)) * fs_v_pfc_division_match_stepprevioussum) + (fs_s_pfc_division_match_stepprevioussum_body_steps))) /\ fs_s_pfc_division_match_stepprevioussum_body_steps = fs_r_pfc_division_match_stepprevioussum_body_steps + fs_a_pfc_division_match_stepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_match_steppreviousresiduebound. pfa_gap_division_match_steppreviousresiduebound + S (pfd_previous_division_match_step) = (p)) /\ ((exists pfa_offset_left_division_match_steppreviousresiduecongruence pfa_offset_right_division_match_steppreviousresiduecongruence. (pfc_natural_sum_division_match_stepprevious) + (p) * pfa_offset_left_division_match_steppreviousresiduecongruence = (pfd_previous_division_match_step) + (p) * pfa_offset_right_division_match_steppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_match_stepsubtractleft. pfa_gap_division_match_stepsubtractleft + S (pfd_previous_division_match_step) = (p)) /\ (((exists pfa_gap_division_match_stepsubtractright. pfa_gap_division_match_stepsubtractright + S (pfd_difference_division_match_step) = (p)) /\ ((((exists pfa_gap_division_match_stepsubtractresultbound. pfa_gap_division_match_stepsubtractresultbound + S (pfd_input_division_match_step) = (p)) /\ ((exists pfa_offset_left_division_match_stepsubtractresultcongruence pfa_offset_right_division_match_stepsubtractresultcongruence. ((pfd_previous_division_match_step) + (pfd_difference_division_match_step)) + (p) * pfa_offset_left_division_match_stepsubtractresultcongruence = (pfd_input_division_match_step) + (p) * pfa_offset_right_division_match_stepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_match_stepmultiplyleft. pfa_gap_division_match_stepmultiplyleft + S (k) = (p)) /\ (((exists pfa_gap_division_match_stepmultiplyright. pfa_gap_division_match_stepmultiplyright + S (pfd_difference_division_match_step) = (p)) /\ ((((exists pfa_gap_division_match_stepmultiplyresultbound. pfa_gap_division_match_stepmultiplyresultbound + S (q) = (p)) /\ ((exists pfa_offset_left_division_match_stepmultiplyresultcongruence pfa_offset_right_division_match_stepmultiplyresultcongruence. ((k) * (pfd_difference_division_match_step)) + (p) * pfa_offset_left_division_match_stepmultiplyresultcongruence = (q) + (p) * pfa_offset_right_division_match_stepmultiplyresultcongruence))))))))))))))))))
  21. 0021specialize hq (i)
  22. 0022apply hq
  23. 0023exact hi
  24. 0024cases hpoint
  25. 0025cases hpoint_witness
  26. 0026cases hpoint_witness_right
  27. 0027cases hpoint_witness_right_witness
  28. 0028cases hpoint_witness_right_witness_witness
  29. 0029cases hpoint_witness_right_witness_witness_witness
  30. 0030cases hpoint_witness_right_witness_witness_witness_right
  31. 0031cases hpoint_witness_right_witness_witness_witness_right_right
  32. 0032have hqbound : exists pfa_gap_division_match_value_bound. pfa_gap_division_match_value_bound + S (x) = (p)
  33. 0033cases hpoint_witness_right_witness_witness_witness_right_right_right
  34. 0034cases hpoint_witness_right_witness_witness_witness_right_right_right_right
  35. 0035cases hpoint_witness_right_witness_witness_witness_right_right_right_right_right
  36. 0036exact hpoint_witness_right_witness_witness_witness_right_right_right_right_right_left
  37. 0037have hbnd : exists pfa_gap_division_match_head_bound. pfa_gap_division_match_head_bound + S (b) = (p)
  38. 0038cases hk
  39. 0039cases hk_right
  40. 0040exact hk_right_left
  41. 0041have hproduct : exists t. (((exists pfa_gap_division_match_productleft. pfa_gap_division_match_productleft + S (x) = (p)) /\ (((exists pfa_gap_division_match_productright. pfa_gap_division_match_productright + S (b) = (p)) /\ ((((exists pfa_gap_division_match_productresultbound. pfa_gap_division_match_productresultbound + S (t) = (p)) /\ ((exists pfa_offset_left_division_match_productresultcongruence pfa_offset_right_division_match_productresultcongruence. ((x) * (b)) + (p) * pfa_offset_left_division_match_productresultcongruence = (t) + (p) * pfa_offset_right_division_match_productresultcongruence)))))))))
  42. 0042specialize prime_field_multiply_exists (p)
  43. 0043specialize prime_field_multiply_exists (x)
  44. 0044specialize prime_field_multiply_exists (b)
  45. 0045apply prime_field_multiply_exists
  46. 0046exact hp
  47. 0047exact hqbound
  48. 0048exact hbnd
  49. 0049cases hproduct
  50. 0050have hshort : exists pfc_terms_code_division_match_shorter pfc_terms_scale_division_match_shorter pfc_natural_sum_division_match_shorter. ((forall pfc_index_division_match_shorterdiagonal. (exists pfa_gap_division_match_shorterdiagonalbound. pfa_gap_division_match_shorterdiagonalbound + S (pfc_index_division_match_shorterdiagonal) = (S (i))) -> exists pfc_value_division_match_shorterdiagonal. ((((exists ff_h_pfp_division_match_shorterdiagonalentry. ff_h_pfp_division_match_shorterdiagonalentry + S (pfc_value_division_match_shorterdiagonal) = S ((S (pfc_index_division_match_shorterdiagonal)) * pfc_terms_scale_division_match_shorter)) /\ exists ff_q_pfp_division_match_shorterdiagonalentry. pfc_terms_code_division_match_shorter = ff_q_pfp_division_match_shorterdiagonalentry * S ((S (pfc_index_division_match_shorterdiagonal)) * pfc_terms_scale_division_match_shorter) + (pfc_value_division_match_shorterdiagonal))) /\ ((exists pfc_complement_division_match_shorterdiagonalterm pfc_left_division_match_shorterdiagonalterm pfc_right_division_match_shorterdiagonalterm. (((pfc_index_division_match_shorterdiagonal)+pfc_complement_division_match_shorterdiagonalterm=(i)) /\ ((((((exists pfa_gap_division_match_shorterdiagonaltermleftinside. pfa_gap_division_match_shorterdiagonaltermleftinside + S (pfc_index_division_match_shorterdiagonal) = (S i)) /\ ((((exists ff_h_pfp_division_match_shorterdiagonaltermleftentry. ff_h_pfp_division_match_shorterdiagonaltermleftentry + S (pfc_left_division_match_shorterdiagonalterm) = S ((S (pfc_index_division_match_shorterdiagonal)) * qc)) /\ exists ff_q_pfp_division_match_shorterdiagonaltermleftentry. qb = ff_q_pfp_division_match_shorterdiagonaltermleftentry * S ((S (pfc_index_division_match_shorterdiagonal)) * qc) + (pfc_left_division_match_shorterdiagonalterm)))))) \/ (((exists pfc_gap_division_match_shorterdiagonaltermleftoutside. pfc_gap_division_match_shorterdiagonaltermleftoutside+(S i)=(pfc_index_division_match_shorterdiagonal)) /\ (((pfc_left_division_match_shorterdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_match_shorterdiagonaltermrightinside. pfa_gap_division_match_shorterdiagonaltermrightinside + S (pfc_complement_division_match_shorterdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_division_match_shorterdiagonaltermrightentry. ff_h_pfp_division_match_shorterdiagonaltermrightentry + S (pfc_right_division_match_shorterdiagonalterm) = S ((S (pfc_complement_division_match_shorterdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_match_shorterdiagonaltermrightentry. bb = ff_q_pfp_division_match_shorterdiagonaltermrightentry * S ((S (pfc_complement_division_match_shorterdiagonalterm)) * bc) + (pfc_right_division_match_shorterdiagonalterm)))))) \/ (((exists pfc_gap_division_match_shorterdiagonaltermrightoutside. pfc_gap_division_match_shorterdiagonaltermrightoutside+(S d)=(pfc_complement_division_match_shorterdiagonalterm)) /\ (((pfc_right_division_match_shorterdiagonalterm)=0))))) /\ (((pfc_value_division_match_shorterdiagonal)=pfc_left_division_match_shorterdiagonalterm*pfc_right_division_match_shorterdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_match_shortersum fs_v_pfc_division_match_shortersum. ((((exists fs_h_pfc_division_match_shortersum_body_start. fs_h_pfc_division_match_shortersum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_match_shortersum)) /\ exists fs_q_pfc_division_match_shortersum_body_start. fs_u_pfc_division_match_shortersum = fs_q_pfc_division_match_shortersum_body_start * S ((S (0)) * fs_v_pfc_division_match_shortersum) + (0))) /\ ((((exists fs_h_pfc_division_match_shortersum_body_terminal. fs_h_pfc_division_match_shortersum_body_terminal + S (pfc_natural_sum_division_match_shorter) = S ((S (S (i))) * fs_v_pfc_division_match_shortersum)) /\ exists fs_q_pfc_division_match_shortersum_body_terminal. fs_u_pfc_division_match_shortersum = fs_q_pfc_division_match_shortersum_body_terminal * S ((S (S (i))) * fs_v_pfc_division_match_shortersum) + (pfc_natural_sum_division_match_shorter))) /\ forall fs_i_pfc_division_match_shortersum_body_steps. (exists fs_lt_pfc_division_match_shortersum_body_steps_bound. fs_lt_pfc_division_match_shortersum_body_steps_bound + S fs_i_pfc_division_match_shortersum_body_steps = S (i)) -> exists fs_a_pfc_division_match_shortersum_body_steps fs_r_pfc_division_match_shortersum_body_steps fs_s_pfc_division_match_shortersum_body_steps. ((((exists fs_h_pfc_division_match_shortersum_body_steps_summand. fs_h_pfc_division_match_shortersum_body_steps_summand + S (fs_a_pfc_division_match_shortersum_body_steps) = S ((S (fs_i_pfc_division_match_shortersum_body_steps)) * pfc_terms_scale_division_match_shorter)) /\ exists fs_q_pfc_division_match_shortersum_body_steps_summand. pfc_terms_code_division_match_shorter = fs_q_pfc_division_match_shortersum_body_steps_summand * S ((S (fs_i_pfc_division_match_shortersum_body_steps)) * pfc_terms_scale_division_match_shorter) + (fs_a_pfc_division_match_shortersum_body_steps))) /\ ((((exists fs_h_pfc_division_match_shortersum_body_steps_partial. fs_h_pfc_division_match_shortersum_body_steps_partial + S (fs_r_pfc_division_match_shortersum_body_steps) = S ((S (fs_i_pfc_division_match_shortersum_body_steps)) * fs_v_pfc_division_match_shortersum)) /\ exists fs_q_pfc_division_match_shortersum_body_steps_partial. fs_u_pfc_division_match_shortersum = fs_q_pfc_division_match_shortersum_body_steps_partial * S ((S (fs_i_pfc_division_match_shortersum_body_steps)) * fs_v_pfc_division_match_shortersum) + (fs_r_pfc_division_match_shortersum_body_steps))) /\ ((((exists fs_h_pfc_division_match_shortersum_body_steps_successor. fs_h_pfc_division_match_shortersum_body_steps_successor + S (fs_s_pfc_division_match_shortersum_body_steps) = S ((S (S fs_i_pfc_division_match_shortersum_body_steps)) * fs_v_pfc_division_match_shortersum)) /\ exists fs_q_pfc_division_match_shortersum_body_steps_successor. fs_u_pfc_division_match_shortersum = fs_q_pfc_division_match_shortersum_body_steps_successor * S ((S (S fs_i_pfc_division_match_shortersum_body_steps)) * fs_v_pfc_division_match_shortersum) + (fs_s_pfc_division_match_shortersum_body_steps))) /\ fs_s_pfc_division_match_shortersum_body_steps = fs_r_pfc_division_match_shortersum_body_steps + fs_a_pfc_division_match_shortersum_body_steps)))))) /\ ((((exists pfa_gap_division_match_shorterresiduebound. pfa_gap_division_match_shorterresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_division_match_shorterresiduecongruence pfa_offset_right_division_match_shorterresiduecongruence. (pfc_natural_sum_division_match_shorter) + (p) * pfa_offset_left_division_match_shorterresiduecongruence = (r) + (p) * pfa_offset_right_division_match_shorterresiduecongruence))))))))
  51. 0051specialize prime_field_convolution_coefficient_prefix_transport (p)
  52. 0052specialize prime_field_convolution_coefficient_prefix_transport (qb)
  53. 0053specialize prime_field_convolution_coefficient_prefix_transport (qc)
  54. 0054specialize prime_field_convolution_coefficient_prefix_transport (N)
  55. 0055specialize prime_field_convolution_coefficient_prefix_transport (qb)
  56. 0056specialize prime_field_convolution_coefficient_prefix_transport (qc)
  57. 0057specialize prime_field_convolution_coefficient_prefix_transport (S i)
  58. 0058specialize prime_field_convolution_coefficient_prefix_transport (bb)
  59. 0059specialize prime_field_convolution_coefficient_prefix_transport (bc)
  60. 0060specialize prime_field_convolution_coefficient_prefix_transport (S d)
  61. 0061specialize prime_field_convolution_coefficient_prefix_transport (S i)
  62. 0062specialize prime_field_convolution_coefficient_prefix_transport (i)
  63. 0063specialize prime_field_convolution_coefficient_prefix_transport (r)
  64. 0064apply prime_field_convolution_coefficient_prefix_transport
  65. 0065exact hi
  66. 0066specialize le_refl (S i)
  67. 0067apply le_refl
  68. 0068intro j
  69. 0069intro v
  70. 0070intro hj
  71. 0071intro hv
  72. 0072exact hv
  73. 0073specialize le_refl (S i)
  74. 0074apply le_refl
  75. 0075exact hr
  76. 0076have hsum : ((exists pfa_gap_division_match_sumleft. pfa_gap_division_match_sumleft + S (x2) = (p)) /\ (((exists pfa_gap_division_match_sumright. pfa_gap_division_match_sumright + S (x4) = (p)) /\ ((((exists pfa_gap_division_match_sumresultbound. pfa_gap_division_match_sumresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_division_match_sumresultcongruence pfa_offset_right_division_match_sumresultcongruence. ((x2) + (x4)) + (p) * pfa_offset_left_division_match_sumresultcongruence = (r) + (p) * pfa_offset_right_division_match_sumresultcongruence))))))))
  77. 0077specialize prime_field_convolution_coefficient_append (p)
  78. 0078specialize prime_field_convolution_coefficient_append (qb)
  79. 0079specialize prime_field_convolution_coefficient_append (qc)
  80. 0080specialize prime_field_convolution_coefficient_append (qb)
  81. 0081specialize prime_field_convolution_coefficient_append (qc)
  82. 0082specialize prime_field_convolution_coefficient_append (bb)
  83. 0083specialize prime_field_convolution_coefficient_append (bc)
  84. 0084specialize prime_field_convolution_coefficient_append (d)
  85. 0085specialize prime_field_convolution_coefficient_append (i)
  86. 0086specialize prime_field_convolution_coefficient_append (x)
  87. 0087specialize prime_field_convolution_coefficient_append (b)
  88. 0088specialize prime_field_convolution_coefficient_append (x2)
  89. 0089specialize prime_field_convolution_coefficient_append (x4)
  90. 0090specialize prime_field_convolution_coefficient_append (r)
  91. 0091apply prime_field_convolution_coefficient_append
  92. 0092intro j
  93. 0093intro v
  94. 0094intro hj
  95. 0095intro hv
  96. 0096exact hv
  97. 0097exact hpoint_witness_left
  98. 0098exact hb
  99. 0099exact hpoint_witness_right_witness_witness_witness_right_left
  100. 0100exact hshort
  101. 0101exact hproduct_witness
  102. 0102have heq : r=x1
  103. 0103specialize prime_field_polynomial_quotient_scalar_cancellation (p)
  104. 0104specialize prime_field_polynomial_quotient_scalar_cancellation (b)
  105. 0105specialize prime_field_polynomial_quotient_scalar_cancellation (k)
  106. 0106specialize prime_field_polynomial_quotient_scalar_cancellation (x2)
  107. 0107specialize prime_field_polynomial_quotient_scalar_cancellation (x3)
  108. 0108specialize prime_field_polynomial_quotient_scalar_cancellation (x1)
  109. 0109specialize prime_field_polynomial_quotient_scalar_cancellation (x)
  110. 0110specialize prime_field_polynomial_quotient_scalar_cancellation (x4)
  111. 0111specialize prime_field_polynomial_quotient_scalar_cancellation (r)
  112. 0112apply prime_field_polynomial_quotient_scalar_cancellation
  113. 0113exact hp
  114. 0114exact hk
  115. 0115exact hpoint_witness_right_witness_witness_witness_right_right_left
  116. 0116exact hpoint_witness_right_witness_witness_witness_right_right_right
  117. 0117exact hproduct_witness
  118. 0118exact hsum
  119. 0119rewrite heq
  120. 0120rewrite heq
  121. 0121exact hpoint_witness_right_witness_witness_witness_left