Unconditionally construct an actual general division execution and derive its strict remainder-degree alternative; no theorem claims degree for zero.
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.
forall p ab ac L bb bc d. (~((p) = 1) /\ forall pfa_factor_left_division_bounded_prime pfa_factor_right_division_bounded_prime. (p) = pfa_factor_left_division_bounded_prime * pfa_factor_right_division_bounded_prime -> pfa_factor_left_division_bounded_prime = 1 \/ pfa_factor_right_division_bounded_prime = 1) -> (forall fom_index_pfp_division_bounded_input. (exists fom_gap_pfp_division_bounded_input_index_bound. fom_gap_pfp_division_bounded_input_index_bound + S (fom_index_pfp_division_bounded_input) = L) -> exists fom_value_pfp_division_bounded_input. ((((exists fom_beta_height_pfp_division_bounded_input_entry. fom_beta_height_pfp_division_bounded_input_entry + S (fom_value_pfp_division_bounded_input) = S ((S (fom_index_pfp_division_bounded_input)) * ac)) /\ exists fom_beta_quotient_pfp_division_bounded_input_entry. ab = fom_beta_quotient_pfp_division_bounded_input_entry * S ((S (fom_index_pfp_division_bounded_input)) * ac) + (fom_value_pfp_division_bounded_input))) /\ (exists fom_gap_pfp_division_bounded_input_value_bound. fom_gap_pfp_division_bounded_input_value_bound + S (fom_value_pfp_division_bounded_input) = p))) -> ((((S d)=S (d)) /\ (((forall fom_index_pfp_division_bounded_divisorcoefficients. (exists fom_gap_pfp_division_bounded_divisorcoefficients_index_bound. fom_gap_pfp_division_bounded_divisorcoefficients_index_bound + S (fom_index_pfp_division_bounded_divisorcoefficients) = S d) -> exists fom_value_pfp_division_bounded_divisorcoefficients. ((((exists fom_beta_height_pfp_division_bounded_divisorcoefficients_entry. fom_beta_height_pfp_division_bounded_divisorcoefficients_entry + S (fom_value_pfp_division_bounded_divisorcoefficients) = S ((S (fom_index_pfp_division_bounded_divisorcoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_division_bounded_divisorcoefficients_entry. bb = fom_beta_quotient_pfp_division_bounded_divisorcoefficients_entry * S ((S (fom_index_pfp_division_bounded_divisorcoefficients)) * bc) + (fom_value_pfp_division_bounded_divisorcoefficients))) /\ (exists fom_gap_pfp_division_bounded_divisorcoefficients_value_bound. fom_gap_pfp_division_bounded_divisorcoefficients_value_bound + S (fom_value_pfp_division_bounded_divisorcoefficients) = p))) /\ ((exists pfd_leading_division_bounded_divisor. ((((exists ff_h_pfp_division_bounded_divisorentry. ff_h_pfp_division_bounded_divisorentry + S (pfd_leading_division_bounded_divisor) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_bounded_divisorentry. bb = ff_q_pfp_division_bounded_divisorentry * S ((S (0)) * bc) + (pfd_leading_division_bounded_divisor))) /\ ((~(pfd_leading_division_bounded_divisor=0)))))))))) -> exists qb qc q rb rc R. ((((forall fom_index_pfp_division_bounded_executioninput. (exists fom_gap_pfp_division_bounded_executioninput_index_bound. fom_gap_pfp_division_bounded_executioninput_index_bound + S (fom_index_pfp_division_bounded_executioninput) = L) -> exists fom_value_pfp_division_bounded_executioninput. ((((exists fom_beta_height_pfp_division_bounded_executioninput_entry. fom_beta_height_pfp_division_bounded_executioninput_entry + S (fom_value_pfp_division_bounded_executioninput) = S ((S (fom_index_pfp_division_bounded_executioninput)) * ac)) /\ exists fom_beta_quotient_pfp_division_bounded_executioninput_entry. ab = fom_beta_quotient_pfp_division_bounded_executioninput_entry * S ((S (fom_index_pfp_division_bounded_executioninput)) * ac) + (fom_value_pfp_division_bounded_executioninput))) /\ (exists fom_gap_pfp_division_bounded_executioninput_value_bound. fom_gap_pfp_division_bounded_executioninput_value_bound + S (fom_value_pfp_division_bounded_executioninput) = p))) /\ (((forall fom_index_pfp_division_bounded_executiondivisor. (exists fom_gap_pfp_division_bounded_executiondivisor_index_bound. fom_gap_pfp_division_bounded_executiondivisor_index_bound + S (fom_index_pfp_division_bounded_executiondivisor) = S (d)) -> exists fom_value_pfp_division_bounded_executiondivisor. ((((exists fom_beta_height_pfp_division_bounded_executiondivisor_entry. fom_beta_height_pfp_division_bounded_executiondivisor_entry + S (fom_value_pfp_division_bounded_executiondivisor) = S ((S (fom_index_pfp_division_bounded_executiondivisor)) * bc)) /\ exists fom_beta_quotient_pfp_division_bounded_executiondivisor_entry. bb = fom_beta_quotient_pfp_division_bounded_executiondivisor_entry * S ((S (fom_index_pfp_division_bounded_executiondivisor)) * bc) + (fom_value_pfp_division_bounded_executiondivisor))) /\ (exists fom_gap_pfp_division_bounded_executiondivisor_value_bound. fom_gap_pfp_division_bounded_executiondivisor_value_bound + S (fom_value_pfp_division_bounded_executiondivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_division_bounded_executionlengthshort. pfc_gap_division_bounded_executionlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_division_bounded_execution pfd_inverse_division_bounded_execution pfd_product_code_division_bounded_execution pfd_product_scale_division_bounded_execution pfd_residual_code_division_bounded_execution pfd_residual_scale_division_bounded_execution pfd_cut_division_bounded_execution. ((((exists ff_h_pfp_division_bounded_executionhead. ff_h_pfp_division_bounded_executionhead + S (pfd_head_division_bounded_execution) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_bounded_executionhead. bb = ff_q_pfp_division_bounded_executionhead * S ((S (0)) * bc) + (pfd_head_division_bounded_execution))) /\ (((((~((pfd_head_division_bounded_execution) = 0)) /\ ((((exists pfa_gap_division_bounded_executioninversemultiplicationleft. pfa_gap_division_bounded_executioninversemultiplicationleft + S (pfd_head_division_bounded_execution) = (p)) /\ (((exists pfa_gap_division_bounded_executioninversemultiplicationright. pfa_gap_division_bounded_executioninversemultiplicationright + S (pfd_inverse_division_bounded_execution) = (p)) /\ ((((exists pfa_gap_division_bounded_executioninversemultiplicationresultbound. pfa_gap_division_bounded_executioninversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_bounded_executioninversemultiplicationresultcongruence pfa_offset_right_division_bounded_executioninversemultiplicationresultcongruence. ((pfd_head_division_bounded_execution) * (pfd_inverse_division_bounded_execution)) + (p) * pfa_offset_left_division_bounded_executioninversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_bounded_executioninversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_division_bounded_executionquotient. (exists pfa_gap_division_bounded_executionquotientbound. pfa_gap_division_bounded_executionquotientbound + S (pfd_index_division_bounded_executionquotient) = (q)) -> exists pfd_value_division_bounded_executionquotient. ((((exists ff_h_pfp_division_bounded_executionquotiententry. ff_h_pfp_division_bounded_executionquotiententry + S (pfd_value_division_bounded_executionquotient) = S ((S (pfd_index_division_bounded_executionquotient)) * qc)) /\ exists ff_q_pfp_division_bounded_executionquotiententry. qb = ff_q_pfp_division_bounded_executionquotiententry * S ((S (pfd_index_division_bounded_executionquotient)) * qc) + (pfd_value_division_bounded_executionquotient))) /\ ((exists pfd_input_division_bounded_executionquotientstep pfd_previous_division_bounded_executionquotientstep pfd_difference_division_bounded_executionquotientstep. ((((exists ff_h_pfp_division_bounded_executionquotientstepinput. ff_h_pfp_division_bounded_executionquotientstepinput + S (pfd_input_division_bounded_executionquotientstep) = S ((S (pfd_index_division_bounded_executionquotient)) * ac)) /\ exists ff_q_pfp_division_bounded_executionquotientstepinput. ab = ff_q_pfp_division_bounded_executionquotientstepinput * S ((S (pfd_index_division_bounded_executionquotient)) * ac) + (pfd_input_division_bounded_executionquotientstep))) /\ (((exists pfc_terms_code_division_bounded_executionquotientstepprevious pfc_terms_scale_division_bounded_executionquotientstepprevious pfc_natural_sum_division_bounded_executionquotientstepprevious. ((forall pfc_index_division_bounded_executionquotientsteppreviousdiagonal. (exists pfa_gap_division_bounded_executionquotientsteppreviousdiagonalbound. pfa_gap_division_bounded_executionquotientsteppreviousdiagonalbound + S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal) = (S (pfd_index_division_bounded_executionquotient))) -> exists pfc_value_division_bounded_executionquotientsteppreviousdiagonal. ((((exists ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonalentry. ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonalentry + S (pfc_value_division_bounded_executionquotientsteppreviousdiagonal) = S ((S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_division_bounded_executionquotientstepprevious)) /\ exists ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonalentry. pfc_terms_code_division_bounded_executionquotientstepprevious = ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonalentry * S ((S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal)) * pfc_terms_scale_division_bounded_executionquotientstepprevious) + (pfc_value_division_bounded_executionquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm pfc_left_division_bounded_executionquotientsteppreviousdiagonalterm pfc_right_division_bounded_executionquotientsteppreviousdiagonalterm. (((pfc_index_division_bounded_executionquotientsteppreviousdiagonal)+pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm=(pfd_index_division_bounded_executionquotient)) /\ ((((((exists pfa_gap_division_bounded_executionquotientsteppreviousdiagonaltermleftinside. pfa_gap_division_bounded_executionquotientsteppreviousdiagonaltermleftinside + S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal) = (pfd_index_division_bounded_executionquotient)) /\ ((((exists ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonaltermleftentry + S (pfc_left_division_bounded_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_bounded_executionquotientsteppreviousdiagonal)) * qc) + (pfc_left_division_bounded_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_executionquotientsteppreviousdiagonaltermleftoutside. pfc_gap_division_bounded_executionquotientsteppreviousdiagonaltermleftoutside+(pfd_index_division_bounded_executionquotient)=(pfc_index_division_bounded_executionquotientsteppreviousdiagonal)) /\ (((pfc_left_division_bounded_executionquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_bounded_executionquotientsteppreviousdiagonaltermrightinside. pfa_gap_division_bounded_executionquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_division_bounded_executionquotientsteppreviousdiagonaltermrightentry + S (pfc_right_division_bounded_executionquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_bounded_executionquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_division_bounded_executionquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_executionquotientsteppreviousdiagonaltermrightoutside. pfc_gap_division_bounded_executionquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_division_bounded_executionquotientsteppreviousdiagonalterm)) /\ (((pfc_right_division_bounded_executionquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_bounded_executionquotientsteppreviousdiagonal)=pfc_left_division_bounded_executionquotientsteppreviousdiagonalterm*pfc_right_division_bounded_executionquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_bounded_executionquotientstepprevioussum fs_v_pfc_division_bounded_executionquotientstepprevioussum. ((((exists fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_start. fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_start. fs_u_pfc_division_bounded_executionquotientstepprevioussum = fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_terminal. fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_terminal + S (pfc_natural_sum_division_bounded_executionquotientstepprevious) = S ((S (S (pfd_index_division_bounded_executionquotient))) * fs_v_pfc_division_bounded_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_terminal. fs_u_pfc_division_bounded_executionquotientstepprevioussum = fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_division_bounded_executionquotient))) * fs_v_pfc_division_bounded_executionquotientstepprevioussum) + (pfc_natural_sum_division_bounded_executionquotientstepprevious))) /\ forall fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps. (exists fs_lt_pfc_division_bounded_executionquotientstepprevioussum_body_steps_bound. fs_lt_pfc_division_bounded_executionquotientstepprevioussum_body_steps_bound + S fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps = S (pfd_index_division_bounded_executionquotient)) -> exists fs_a_pfc_division_bounded_executionquotientstepprevioussum_body_steps fs_r_pfc_division_bounded_executionquotientstepprevioussum_body_steps fs_s_pfc_division_bounded_executionquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_summand. fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_division_bounded_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_bounded_executionquotientstepprevious)) /\ exists fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_summand. pfc_terms_code_division_bounded_executionquotientstepprevious = fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_bounded_executionquotientstepprevious) + (fs_a_pfc_division_bounded_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_partial. fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_division_bounded_executionquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_partial. fs_u_pfc_division_bounded_executionquotientstepprevioussum = fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum) + (fs_r_pfc_division_bounded_executionquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_successor. fs_h_pfc_division_bounded_executionquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_division_bounded_executionquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum)) /\ exists fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_successor. fs_u_pfc_division_bounded_executionquotientstepprevioussum = fs_q_pfc_division_bounded_executionquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_bounded_executionquotientstepprevioussum_body_steps)) * fs_v_pfc_division_bounded_executionquotientstepprevioussum) + (fs_s_pfc_division_bounded_executionquotientstepprevioussum_body_steps))) /\ fs_s_pfc_division_bounded_executionquotientstepprevioussum_body_steps = fs_r_pfc_division_bounded_executionquotientstepprevioussum_body_steps + fs_a_pfc_division_bounded_executionquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_bounded_executionquotientsteppreviousresiduebound. pfa_gap_division_bounded_executionquotientsteppreviousresiduebound + S (pfd_previous_division_bounded_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_division_bounded_executionquotientsteppreviousresiduecongruence pfa_offset_right_division_bounded_executionquotientsteppreviousresiduecongruence. (pfc_natural_sum_division_bounded_executionquotientstepprevious) + (p) * pfa_offset_left_division_bounded_executionquotientsteppreviousresiduecongruence = (pfd_previous_division_bounded_executionquotientstep) + (p) * pfa_offset_right_division_bounded_executionquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_bounded_executionquotientstepsubtractleft. pfa_gap_division_bounded_executionquotientstepsubtractleft + S (pfd_previous_division_bounded_executionquotientstep) = (p)) /\ (((exists pfa_gap_division_bounded_executionquotientstepsubtractright. pfa_gap_division_bounded_executionquotientstepsubtractright + S (pfd_difference_division_bounded_executionquotientstep) = (p)) /\ ((((exists pfa_gap_division_bounded_executionquotientstepsubtractresultbound. pfa_gap_division_bounded_executionquotientstepsubtractresultbound + S (pfd_input_division_bounded_executionquotientstep) = (p)) /\ ((exists pfa_offset_left_division_bounded_executionquotientstepsubtractresultcongruence pfa_offset_right_division_bounded_executionquotientstepsubtractresultcongruence. ((pfd_previous_division_bounded_executionquotientstep) + (pfd_difference_division_bounded_executionquotientstep)) + (p) * pfa_offset_left_division_bounded_executionquotientstepsubtractresultcongruence = (pfd_input_division_bounded_executionquotientstep) + (p) * pfa_offset_right_division_bounded_executionquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_bounded_executionquotientstepmultiplyleft. pfa_gap_division_bounded_executionquotientstepmultiplyleft + S (pfd_inverse_division_bounded_execution) = (p)) /\ (((exists pfa_gap_division_bounded_executionquotientstepmultiplyright. pfa_gap_division_bounded_executionquotientstepmultiplyright + S (pfd_difference_division_bounded_executionquotientstep) = (p)) /\ ((((exists pfa_gap_division_bounded_executionquotientstepmultiplyresultbound. pfa_gap_division_bounded_executionquotientstepmultiplyresultbound + S (pfd_value_division_bounded_executionquotient) = (p)) /\ ((exists pfa_offset_left_division_bounded_executionquotientstepmultiplyresultcongruence pfa_offset_right_division_bounded_executionquotientstepmultiplyresultcongruence. ((pfd_inverse_division_bounded_execution) * (pfd_difference_division_bounded_executionquotientstep)) + (p) * pfa_offset_left_division_bounded_executionquotientstepmultiplyresultcongruence = (pfd_value_division_bounded_executionquotient) + (p) * pfa_offset_right_division_bounded_executionquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_division_bounded_executionproduct. (exists pfa_gap_division_bounded_executionproductbound. pfa_gap_division_bounded_executionproductbound + S (pfc_index_division_bounded_executionproduct) = (L)) -> exists pfc_value_division_bounded_executionproduct. ((((exists ff_h_pfp_division_bounded_executionproductentry. ff_h_pfp_division_bounded_executionproductentry + S (pfc_value_division_bounded_executionproduct) = S ((S (pfc_index_division_bounded_executionproduct)) * pfd_product_scale_division_bounded_execution)) /\ exists ff_q_pfp_division_bounded_executionproductentry. pfd_product_code_division_bounded_execution = ff_q_pfp_division_bounded_executionproductentry * S ((S (pfc_index_division_bounded_executionproduct)) * pfd_product_scale_division_bounded_execution) + (pfc_value_division_bounded_executionproduct))) /\ ((exists pfc_terms_code_division_bounded_executionproductcoefficient pfc_terms_scale_division_bounded_executionproductcoefficient pfc_natural_sum_division_bounded_executionproductcoefficient. ((forall pfc_index_division_bounded_executionproductcoefficientdiagonal. (exists pfa_gap_division_bounded_executionproductcoefficientdiagonalbound. pfa_gap_division_bounded_executionproductcoefficientdiagonalbound + S (pfc_index_division_bounded_executionproductcoefficientdiagonal) = (S (pfc_index_division_bounded_executionproduct))) -> exists pfc_value_division_bounded_executionproductcoefficientdiagonal. ((((exists ff_h_pfp_division_bounded_executionproductcoefficientdiagonalentry. ff_h_pfp_division_bounded_executionproductcoefficientdiagonalentry + S (pfc_value_division_bounded_executionproductcoefficientdiagonal) = S ((S (pfc_index_division_bounded_executionproductcoefficientdiagonal)) * pfc_terms_scale_division_bounded_executionproductcoefficient)) /\ exists ff_q_pfp_division_bounded_executionproductcoefficientdiagonalentry. pfc_terms_code_division_bounded_executionproductcoefficient = ff_q_pfp_division_bounded_executionproductcoefficientdiagonalentry * S ((S (pfc_index_division_bounded_executionproductcoefficientdiagonal)) * pfc_terms_scale_division_bounded_executionproductcoefficient) + (pfc_value_division_bounded_executionproductcoefficientdiagonal))) /\ ((exists pfc_complement_division_bounded_executionproductcoefficientdiagonalterm pfc_left_division_bounded_executionproductcoefficientdiagonalterm pfc_right_division_bounded_executionproductcoefficientdiagonalterm. (((pfc_index_division_bounded_executionproductcoefficientdiagonal)+pfc_complement_division_bounded_executionproductcoefficientdiagonalterm=(pfc_index_division_bounded_executionproduct)) /\ ((((((exists pfa_gap_division_bounded_executionproductcoefficientdiagonaltermleftinside. pfa_gap_division_bounded_executionproductcoefficientdiagonaltermleftinside + S (pfc_index_division_bounded_executionproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_bounded_executionproductcoefficientdiagonaltermleftentry. ff_h_pfp_division_bounded_executionproductcoefficientdiagonaltermleftentry + S (pfc_left_division_bounded_executionproductcoefficientdiagonalterm) = S ((S (pfc_index_division_bounded_executionproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_bounded_executionproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_bounded_executionproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_bounded_executionproductcoefficientdiagonal)) * qc) + (pfc_left_division_bounded_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_executionproductcoefficientdiagonaltermleftoutside. pfc_gap_division_bounded_executionproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_bounded_executionproductcoefficientdiagonal)) /\ (((pfc_left_division_bounded_executionproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_bounded_executionproductcoefficientdiagonaltermrightinside. pfa_gap_division_bounded_executionproductcoefficientdiagonaltermrightinside + S (pfc_complement_division_bounded_executionproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_bounded_executionproductcoefficientdiagonaltermrightentry. ff_h_pfp_division_bounded_executionproductcoefficientdiagonaltermrightentry + S (pfc_right_division_bounded_executionproductcoefficientdiagonalterm) = S ((S (pfc_complement_division_bounded_executionproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_bounded_executionproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_bounded_executionproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_bounded_executionproductcoefficientdiagonalterm)) * bc) + (pfc_right_division_bounded_executionproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_bounded_executionproductcoefficientdiagonaltermrightoutside. pfc_gap_division_bounded_executionproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_division_bounded_executionproductcoefficientdiagonalterm)) /\ (((pfc_right_division_bounded_executionproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_bounded_executionproductcoefficientdiagonal)=pfc_left_division_bounded_executionproductcoefficientdiagonalterm*pfc_right_division_bounded_executionproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_bounded_executionproductcoefficientsum fs_v_pfc_division_bounded_executionproductcoefficientsum. ((((exists fs_h_pfc_division_bounded_executionproductcoefficientsum_body_start. fs_h_pfc_division_bounded_executionproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_bounded_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_executionproductcoefficientsum_body_start. fs_u_pfc_division_bounded_executionproductcoefficientsum = fs_q_pfc_division_bounded_executionproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_bounded_executionproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_bounded_executionproductcoefficientsum_body_terminal. fs_h_pfc_division_bounded_executionproductcoefficientsum_body_terminal + S (pfc_natural_sum_division_bounded_executionproductcoefficient) = S ((S (S (pfc_index_division_bounded_executionproduct))) * fs_v_pfc_division_bounded_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_executionproductcoefficientsum_body_terminal. fs_u_pfc_division_bounded_executionproductcoefficientsum = fs_q_pfc_division_bounded_executionproductcoefficientsum_body_terminal * S ((S (S (pfc_index_division_bounded_executionproduct))) * fs_v_pfc_division_bounded_executionproductcoefficientsum) + (pfc_natural_sum_division_bounded_executionproductcoefficient))) /\ forall fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps. (exists fs_lt_pfc_division_bounded_executionproductcoefficientsum_body_steps_bound. fs_lt_pfc_division_bounded_executionproductcoefficientsum_body_steps_bound + S fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps = S (pfc_index_division_bounded_executionproduct)) -> exists fs_a_pfc_division_bounded_executionproductcoefficientsum_body_steps fs_r_pfc_division_bounded_executionproductcoefficientsum_body_steps fs_s_pfc_division_bounded_executionproductcoefficientsum_body_steps. ((((exists fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_summand. fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_summand + S (fs_a_pfc_division_bounded_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_division_bounded_executionproductcoefficient)) /\ exists fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_summand. pfc_terms_code_division_bounded_executionproductcoefficient = fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * pfc_terms_scale_division_bounded_executionproductcoefficient) + (fs_a_pfc_division_bounded_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_partial. fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_partial + S (fs_r_pfc_division_bounded_executionproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_partial. fs_u_pfc_division_bounded_executionproductcoefficientsum = fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_executionproductcoefficientsum) + (fs_r_pfc_division_bounded_executionproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_successor. fs_h_pfc_division_bounded_executionproductcoefficientsum_body_steps_successor + S (fs_s_pfc_division_bounded_executionproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_executionproductcoefficientsum)) /\ exists fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_successor. fs_u_pfc_division_bounded_executionproductcoefficientsum = fs_q_pfc_division_bounded_executionproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_bounded_executionproductcoefficientsum_body_steps)) * fs_v_pfc_division_bounded_executionproductcoefficientsum) + (fs_s_pfc_division_bounded_executionproductcoefficientsum_body_steps))) /\ fs_s_pfc_division_bounded_executionproductcoefficientsum_body_steps = fs_r_pfc_division_bounded_executionproductcoefficientsum_body_steps + fs_a_pfc_division_bounded_executionproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_bounded_executionproductcoefficientresiduebound. pfa_gap_division_bounded_executionproductcoefficientresiduebound + S (pfc_value_division_bounded_executionproduct) = (p)) /\ ((exists pfa_offset_left_division_bounded_executionproductcoefficientresiduecongruence pfa_offset_right_division_bounded_executionproductcoefficientresiduecongruence. (pfc_natural_sum_division_bounded_executionproductcoefficient) + (p) * pfa_offset_left_division_bounded_executionproductcoefficientresiduecongruence = (pfc_value_division_bounded_executionproduct) + (p) * pfa_offset_right_division_bounded_executionproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_division_bounded_executiondifference. (exists pfa_gap_division_bounded_executiondifferenceindex. pfa_gap_division_bounded_executiondifferenceindex + S (pfs_index_division_bounded_executiondifference) = (L)) -> exists pfs_left_division_bounded_executiondifference pfs_right_division_bounded_executiondifference pfs_result_division_bounded_executiondifference. ((((exists ff_h_pfp_division_bounded_executiondifferenceleft. ff_h_pfp_division_bounded_executiondifferenceleft + S (pfs_left_division_bounded_executiondifference) = S ((S (pfs_index_division_bounded_executiondifference)) * ac)) /\ exists ff_q_pfp_division_bounded_executiondifferenceleft. ab = ff_q_pfp_division_bounded_executiondifferenceleft * S ((S (pfs_index_division_bounded_executiondifference)) * ac) + (pfs_left_division_bounded_executiondifference))) /\ (((((exists ff_h_pfp_division_bounded_executiondifferenceright. ff_h_pfp_division_bounded_executiondifferenceright + S (pfs_right_division_bounded_executiondifference) = S ((S (pfs_index_division_bounded_executiondifference)) * pfd_product_scale_division_bounded_execution)) /\ exists ff_q_pfp_division_bounded_executiondifferenceright. pfd_product_code_division_bounded_execution = ff_q_pfp_division_bounded_executiondifferenceright * S ((S (pfs_index_division_bounded_executiondifference)) * pfd_product_scale_division_bounded_execution) + (pfs_right_division_bounded_executiondifference))) /\ (((((exists ff_h_pfp_division_bounded_executiondifferenceresult. ff_h_pfp_division_bounded_executiondifferenceresult + S (pfs_result_division_bounded_executiondifference) = S ((S (pfs_index_division_bounded_executiondifference)) * pfd_residual_scale_division_bounded_execution)) /\ exists ff_q_pfp_division_bounded_executiondifferenceresult. pfd_residual_code_division_bounded_execution = ff_q_pfp_division_bounded_executiondifferenceresult * S ((S (pfs_index_division_bounded_executiondifference)) * pfd_residual_scale_division_bounded_execution) + (pfs_result_division_bounded_executiondifference))) /\ ((((exists pfa_gap_division_bounded_executiondifferenceoperationleft. pfa_gap_division_bounded_executiondifferenceoperationleft + S (pfs_right_division_bounded_executiondifference) = (p)) /\ (((exists pfa_gap_division_bounded_executiondifferenceoperationright. pfa_gap_division_bounded_executiondifferenceoperationright + S (pfs_result_division_bounded_executiondifference) = (p)) /\ ((((exists pfa_gap_division_bounded_executiondifferenceoperationresultbound. pfa_gap_division_bounded_executiondifferenceoperationresultbound + S (pfs_left_division_bounded_executiondifference) = (p)) /\ ((exists pfa_offset_left_division_bounded_executiondifferenceoperationresultcongruence pfa_offset_right_division_bounded_executiondifferenceoperationresultcongruence. ((pfs_right_division_bounded_executiondifference) + (pfs_result_division_bounded_executiondifference)) + (p) * pfa_offset_left_division_bounded_executiondifferenceoperationresultcongruence = (pfs_left_division_bounded_executiondifference) + (p) * pfa_offset_right_division_bounded_executiondifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_division_bounded_execution)+(R)) /\ (((forall fom_index_pfp_division_bounded_executiontriminput. (exists fom_gap_pfp_division_bounded_executiontriminput_index_bound. fom_gap_pfp_division_bounded_executiontriminput_index_bound + S (fom_index_pfp_division_bounded_executiontriminput) = L) -> exists fom_value_pfp_division_bounded_executiontriminput. ((((exists fom_beta_height_pfp_division_bounded_executiontriminput_entry. fom_beta_height_pfp_division_bounded_executiontriminput_entry + S (fom_value_pfp_division_bounded_executiontriminput) = S ((S (fom_index_pfp_division_bounded_executiontriminput)) * pfd_residual_scale_division_bounded_execution)) /\ exists fom_beta_quotient_pfp_division_bounded_executiontriminput_entry. pfd_residual_code_division_bounded_execution = fom_beta_quotient_pfp_division_bounded_executiontriminput_entry * S ((S (fom_index_pfp_division_bounded_executiontriminput)) * pfd_residual_scale_division_bounded_execution) + (fom_value_pfp_division_bounded_executiontriminput))) /\ (exists fom_gap_pfp_division_bounded_executiontriminput_value_bound. fom_gap_pfp_division_bounded_executiontriminput_value_bound + S (fom_value_pfp_division_bounded_executiontriminput) = p))) /\ (((forall pfp_repeat_index_division_bounded_executiontrimremoved. (exists pfa_gap_division_bounded_executiontrimremovedindex. pfa_gap_division_bounded_executiontrimremovedindex + S (pfp_repeat_index_division_bounded_executiontrimremoved) = (pfd_cut_division_bounded_execution)) -> (((exists ff_h_pfp_division_bounded_executiontrimremovedentry. ff_h_pfp_division_bounded_executiontrimremovedentry + S (0) = S ((S (pfp_repeat_index_division_bounded_executiontrimremoved)) * pfd_residual_scale_division_bounded_execution)) /\ exists ff_q_pfp_division_bounded_executiontrimremovedentry. pfd_residual_code_division_bounded_execution = ff_q_pfp_division_bounded_executiontrimremovedentry * S ((S (pfp_repeat_index_division_bounded_executiontrimremoved)) * pfd_residual_scale_division_bounded_execution) + (0)))) /\ (((forall pftrim_index_division_bounded_executiontrimsuffix pftrim_value_division_bounded_executiontrimsuffix. (exists pfa_gap_division_bounded_executiontrimsuffixbound. pfa_gap_division_bounded_executiontrimsuffixbound + S (pftrim_index_division_bounded_executiontrimsuffix) = (R)) -> (((exists ff_h_pfp_division_bounded_executiontrimsuffixsource. ff_h_pfp_division_bounded_executiontrimsuffixsource + S (pftrim_value_division_bounded_executiontrimsuffix) = S ((S ((pfd_cut_division_bounded_execution)+pftrim_index_division_bounded_executiontrimsuffix)) * pfd_residual_scale_division_bounded_execution)) /\ exists ff_q_pfp_division_bounded_executiontrimsuffixsource. pfd_residual_code_division_bounded_execution = ff_q_pfp_division_bounded_executiontrimsuffixsource * S ((S ((pfd_cut_division_bounded_execution)+pftrim_index_division_bounded_executiontrimsuffix)) * pfd_residual_scale_division_bounded_execution) + (pftrim_value_division_bounded_executiontrimsuffix))) -> (((exists ff_h_pfp_division_bounded_executiontrimsuffixoutput. ff_h_pfp_division_bounded_executiontrimsuffixoutput + S (pftrim_value_division_bounded_executiontrimsuffix) = S ((S (pftrim_index_division_bounded_executiontrimsuffix)) * rc)) /\ exists ff_q_pfp_division_bounded_executiontrimsuffixoutput. rb = ff_q_pfp_division_bounded_executiontrimsuffixoutput * S ((S (pftrim_index_division_bounded_executiontrimsuffix)) * rc) + (pftrim_value_division_bounded_executiontrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_bounded_executiontrimnormal. ((((exists ff_h_pfp_division_bounded_executiontrimnormalentry. ff_h_pfp_division_bounded_executiontrimnormalentry + S (pftrim_leading_division_bounded_executiontrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_bounded_executiontrimnormalentry. rb = ff_q_pfp_division_bounded_executiontrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_bounded_executiontrimnormal))) /\ ((~(pftrim_leading_division_bounded_executiontrimnormal=0))))))))))))))))))))))))))))))))) /\ (((R)=0 \/ (exists pfd_remainder_degree_division_bounded_degree. (((((R)=S (pfd_remainder_degree_division_bounded_degree)) /\ (((forall fom_index_pfp_division_bounded_degreerepresentedcoefficients. (exists fom_gap_pfp_division_bounded_degreerepresentedcoefficients_index_bound. fom_gap_pfp_division_bounded_degreerepresentedcoefficients_index_bound + S (fom_index_pfp_division_bounded_degreerepresentedcoefficients) = R) -> exists fom_value_pfp_division_bounded_degreerepresentedcoefficients. ((((exists fom_beta_height_pfp_division_bounded_degreerepresentedcoefficients_entry. fom_beta_height_pfp_division_bounded_degreerepresentedcoefficients_entry + S (fom_value_pfp_division_bounded_degreerepresentedcoefficients) = S ((S (fom_index_pfp_division_bounded_degreerepresentedcoefficients)) * rc)) /\ exists fom_beta_quotient_pfp_division_bounded_degreerepresentedcoefficients_entry. rb = fom_beta_quotient_pfp_division_bounded_degreerepresentedcoefficients_entry * S ((S (fom_index_pfp_division_bounded_degreerepresentedcoefficients)) * rc) + (fom_value_pfp_division_bounded_degreerepresentedcoefficients))) /\ (exists fom_gap_pfp_division_bounded_degreerepresentedcoefficients_value_bound. fom_gap_pfp_division_bounded_degreerepresentedcoefficients_value_bound + S (fom_value_pfp_division_bounded_degreerepresentedcoefficients) = p))) /\ ((exists pfd_leading_division_bounded_degreerepresented. ((((exists ff_h_pfp_division_bounded_degreerepresentedentry. ff_h_pfp_division_bounded_degreerepresentedentry + S (pfd_leading_division_bounded_degreerepresented) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_bounded_degreerepresentedentry. rb = ff_q_pfp_division_bounded_degreerepresentedentry * S ((S (0)) * rc) + (pfd_leading_division_bounded_degreerepresented))) /\ ((~(pfd_leading_division_bounded_degreerepresented=0)))))))))) /\ ((exists pfa_gap_division_bounded_degreestrict. pfa_gap_division_bounded_degreestrict + S (pfd_remainder_degree_division_bounded_degree) = (d))))))))
Complete tactic proof in conservative notation
All 52 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.
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.
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime field polynomial division execution exists.