PX0039

prime_field_polynomial_division_execution_exists

Construct general quotient and normalized remainder codes from any canonical input and actual nonzero divisor, without assuming any output identity or degree bound.

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

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

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

Exact theorem in conservative defined notation

∀ p. ∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ d. Prime(p) → BetaPrefixInto(ab,ac,L,p) → FpRepresentedDegree(p,bb,bc,S d,d) → ∃ x. ∃ y. ∃ z. ∃ n. ∃ m. ∃ k. FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,x,y,z,n,m,k)

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

Definition DAG

FpInv(p,a,b) · 1BetaPrefixInto(b,c,l,B) · 1FpConvolutionPrefix(p,ab,ac,L,bb,bc,M,cb,cc,l) · 1FpRepresentedDegree(p,b,c,L,d) · 1FpCoefficientSubtraction(p,ab,ac,bb,bc,rb,rc,L) · 1FpPolynomialTrim(p,b,c,L,t,d,e,M) · 1FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,M,qb,qc,N) · 1PolynomialQuotientLength(L,d,q) · 1FpPolynomialDivisionExecution(p,ab,ac,L,bb,bc,d,qb,qc,q,rb,rc,R) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1

Actual proof prerequisites

prime_field_polynomial_division_quotient_data_existsprime_field_polynomial_division_residual_data_exists
Original expanded first-order statement 
forall p ab ac L bb bc d. (~((p) = 1) /\ forall pfa_factor_left_division_total_prime pfa_factor_right_division_total_prime. (p) = pfa_factor_left_division_total_prime * pfa_factor_right_division_total_prime -> pfa_factor_left_division_total_prime = 1 \/ pfa_factor_right_division_total_prime = 1) -> (forall fom_index_pfp_division_total_input. (exists fom_gap_pfp_division_total_input_index_bound. fom_gap_pfp_division_total_input_index_bound + S (fom_index_pfp_division_total_input) = L) -> exists fom_value_pfp_division_total_input. ((((exists fom_beta_height_pfp_division_total_input_entry. fom_beta_height_pfp_division_total_input_entry + S (fom_value_pfp_division_total_input) = S ((S (fom_index_pfp_division_total_input)) * ac)) /\ exists fom_beta_quotient_pfp_division_total_input_entry. ab = fom_beta_quotient_pfp_division_total_input_entry * S ((S (fom_index_pfp_division_total_input)) * ac) + (fom_value_pfp_division_total_input))) /\ (exists fom_gap_pfp_division_total_input_value_bound. fom_gap_pfp_division_total_input_value_bound + S (fom_value_pfp_division_total_input) = p))) -> ((((S d)=S (d)) /\ (((forall fom_index_pfp_division_total_divisorcoefficients. (exists fom_gap_pfp_division_total_divisorcoefficients_index_bound. fom_gap_pfp_division_total_divisorcoefficients_index_bound + S (fom_index_pfp_division_total_divisorcoefficients) = S d) -> exists fom_value_pfp_division_total_divisorcoefficients. ((((exists fom_beta_height_pfp_division_total_divisorcoefficients_entry. fom_beta_height_pfp_division_total_divisorcoefficients_entry + S (fom_value_pfp_division_total_divisorcoefficients) = S ((S (fom_index_pfp_division_total_divisorcoefficients)) * bc)) /\ exists fom_beta_quotient_pfp_division_total_divisorcoefficients_entry. bb = fom_beta_quotient_pfp_division_total_divisorcoefficients_entry * S ((S (fom_index_pfp_division_total_divisorcoefficients)) * bc) + (fom_value_pfp_division_total_divisorcoefficients))) /\ (exists fom_gap_pfp_division_total_divisorcoefficients_value_bound. fom_gap_pfp_division_total_divisorcoefficients_value_bound + S (fom_value_pfp_division_total_divisorcoefficients) = p))) /\ ((exists pfd_leading_division_total_divisor. ((((exists ff_h_pfp_division_total_divisorentry. ff_h_pfp_division_total_divisorentry + S (pfd_leading_division_total_divisor) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_total_divisorentry. bb = ff_q_pfp_division_total_divisorentry * S ((S (0)) * bc) + (pfd_leading_division_total_divisor))) /\ ((~(pfd_leading_division_total_divisor=0)))))))))) -> exists qb qc q rb rc R. (((forall fom_index_pfp_division_total_resultinput. (exists fom_gap_pfp_division_total_resultinput_index_bound. fom_gap_pfp_division_total_resultinput_index_bound + S (fom_index_pfp_division_total_resultinput) = L) -> exists fom_value_pfp_division_total_resultinput. ((((exists fom_beta_height_pfp_division_total_resultinput_entry. fom_beta_height_pfp_division_total_resultinput_entry + S (fom_value_pfp_division_total_resultinput) = S ((S (fom_index_pfp_division_total_resultinput)) * ac)) /\ exists fom_beta_quotient_pfp_division_total_resultinput_entry. ab = fom_beta_quotient_pfp_division_total_resultinput_entry * S ((S (fom_index_pfp_division_total_resultinput)) * ac) + (fom_value_pfp_division_total_resultinput))) /\ (exists fom_gap_pfp_division_total_resultinput_value_bound. fom_gap_pfp_division_total_resultinput_value_bound + S (fom_value_pfp_division_total_resultinput) = p))) /\ (((forall fom_index_pfp_division_total_resultdivisor. (exists fom_gap_pfp_division_total_resultdivisor_index_bound. fom_gap_pfp_division_total_resultdivisor_index_bound + S (fom_index_pfp_division_total_resultdivisor) = S (d)) -> exists fom_value_pfp_division_total_resultdivisor. ((((exists fom_beta_height_pfp_division_total_resultdivisor_entry. fom_beta_height_pfp_division_total_resultdivisor_entry + S (fom_value_pfp_division_total_resultdivisor) = S ((S (fom_index_pfp_division_total_resultdivisor)) * bc)) /\ exists fom_beta_quotient_pfp_division_total_resultdivisor_entry. bb = fom_beta_quotient_pfp_division_total_resultdivisor_entry * S ((S (fom_index_pfp_division_total_resultdivisor)) * bc) + (fom_value_pfp_division_total_resultdivisor))) /\ (exists fom_gap_pfp_division_total_resultdivisor_value_bound. fom_gap_pfp_division_total_resultdivisor_value_bound + S (fom_value_pfp_division_total_resultdivisor) = p))) /\ (((((((q)=0) /\ ((exists pfc_gap_division_total_resultlengthshort. pfc_gap_division_total_resultlengthshort+(L)=(d))))) \/ (((~((q)=0)) /\ (((q)+(d)=(L)))))) /\ ((exists pfd_head_division_total_result pfd_inverse_division_total_result pfd_product_code_division_total_result pfd_product_scale_division_total_result pfd_residual_code_division_total_result pfd_residual_scale_division_total_result pfd_cut_division_total_result. ((((exists ff_h_pfp_division_total_resulthead. ff_h_pfp_division_total_resulthead + S (pfd_head_division_total_result) = S ((S (0)) * bc)) /\ exists ff_q_pfp_division_total_resulthead. bb = ff_q_pfp_division_total_resulthead * S ((S (0)) * bc) + (pfd_head_division_total_result))) /\ (((((~((pfd_head_division_total_result) = 0)) /\ ((((exists pfa_gap_division_total_resultinversemultiplicationleft. pfa_gap_division_total_resultinversemultiplicationleft + S (pfd_head_division_total_result) = (p)) /\ (((exists pfa_gap_division_total_resultinversemultiplicationright. pfa_gap_division_total_resultinversemultiplicationright + S (pfd_inverse_division_total_result) = (p)) /\ ((((exists pfa_gap_division_total_resultinversemultiplicationresultbound. pfa_gap_division_total_resultinversemultiplicationresultbound + S (1) = (p)) /\ ((exists pfa_offset_left_division_total_resultinversemultiplicationresultcongruence pfa_offset_right_division_total_resultinversemultiplicationresultcongruence. ((pfd_head_division_total_result) * (pfd_inverse_division_total_result)) + (p) * pfa_offset_left_division_total_resultinversemultiplicationresultcongruence = (1) + (p) * pfa_offset_right_division_total_resultinversemultiplicationresultcongruence)))))))))))) /\ (((forall pfd_index_division_total_resultquotient. (exists pfa_gap_division_total_resultquotientbound. pfa_gap_division_total_resultquotientbound + S (pfd_index_division_total_resultquotient) = (q)) -> exists pfd_value_division_total_resultquotient. ((((exists ff_h_pfp_division_total_resultquotiententry. ff_h_pfp_division_total_resultquotiententry + S (pfd_value_division_total_resultquotient) = S ((S (pfd_index_division_total_resultquotient)) * qc)) /\ exists ff_q_pfp_division_total_resultquotiententry. qb = ff_q_pfp_division_total_resultquotiententry * S ((S (pfd_index_division_total_resultquotient)) * qc) + (pfd_value_division_total_resultquotient))) /\ ((exists pfd_input_division_total_resultquotientstep pfd_previous_division_total_resultquotientstep pfd_difference_division_total_resultquotientstep. ((((exists ff_h_pfp_division_total_resultquotientstepinput. ff_h_pfp_division_total_resultquotientstepinput + S (pfd_input_division_total_resultquotientstep) = S ((S (pfd_index_division_total_resultquotient)) * ac)) /\ exists ff_q_pfp_division_total_resultquotientstepinput. ab = ff_q_pfp_division_total_resultquotientstepinput * S ((S (pfd_index_division_total_resultquotient)) * ac) + (pfd_input_division_total_resultquotientstep))) /\ (((exists pfc_terms_code_division_total_resultquotientstepprevious pfc_terms_scale_division_total_resultquotientstepprevious pfc_natural_sum_division_total_resultquotientstepprevious. ((forall pfc_index_division_total_resultquotientsteppreviousdiagonal. (exists pfa_gap_division_total_resultquotientsteppreviousdiagonalbound. pfa_gap_division_total_resultquotientsteppreviousdiagonalbound + S (pfc_index_division_total_resultquotientsteppreviousdiagonal) = (S (pfd_index_division_total_resultquotient))) -> exists pfc_value_division_total_resultquotientsteppreviousdiagonal. ((((exists ff_h_pfp_division_total_resultquotientsteppreviousdiagonalentry. ff_h_pfp_division_total_resultquotientsteppreviousdiagonalentry + S (pfc_value_division_total_resultquotientsteppreviousdiagonal) = S ((S (pfc_index_division_total_resultquotientsteppreviousdiagonal)) * pfc_terms_scale_division_total_resultquotientstepprevious)) /\ exists ff_q_pfp_division_total_resultquotientsteppreviousdiagonalentry. pfc_terms_code_division_total_resultquotientstepprevious = ff_q_pfp_division_total_resultquotientsteppreviousdiagonalentry * S ((S (pfc_index_division_total_resultquotientsteppreviousdiagonal)) * pfc_terms_scale_division_total_resultquotientstepprevious) + (pfc_value_division_total_resultquotientsteppreviousdiagonal))) /\ ((exists pfc_complement_division_total_resultquotientsteppreviousdiagonalterm pfc_left_division_total_resultquotientsteppreviousdiagonalterm pfc_right_division_total_resultquotientsteppreviousdiagonalterm. (((pfc_index_division_total_resultquotientsteppreviousdiagonal)+pfc_complement_division_total_resultquotientsteppreviousdiagonalterm=(pfd_index_division_total_resultquotient)) /\ ((((((exists pfa_gap_division_total_resultquotientsteppreviousdiagonaltermleftinside. pfa_gap_division_total_resultquotientsteppreviousdiagonaltermleftinside + S (pfc_index_division_total_resultquotientsteppreviousdiagonal) = (pfd_index_division_total_resultquotient)) /\ ((((exists ff_h_pfp_division_total_resultquotientsteppreviousdiagonaltermleftentry. ff_h_pfp_division_total_resultquotientsteppreviousdiagonaltermleftentry + S (pfc_left_division_total_resultquotientsteppreviousdiagonalterm) = S ((S (pfc_index_division_total_resultquotientsteppreviousdiagonal)) * qc)) /\ exists ff_q_pfp_division_total_resultquotientsteppreviousdiagonaltermleftentry. qb = ff_q_pfp_division_total_resultquotientsteppreviousdiagonaltermleftentry * S ((S (pfc_index_division_total_resultquotientsteppreviousdiagonal)) * qc) + (pfc_left_division_total_resultquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_total_resultquotientsteppreviousdiagonaltermleftoutside. pfc_gap_division_total_resultquotientsteppreviousdiagonaltermleftoutside+(pfd_index_division_total_resultquotient)=(pfc_index_division_total_resultquotientsteppreviousdiagonal)) /\ (((pfc_left_division_total_resultquotientsteppreviousdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_total_resultquotientsteppreviousdiagonaltermrightinside. pfa_gap_division_total_resultquotientsteppreviousdiagonaltermrightinside + S (pfc_complement_division_total_resultquotientsteppreviousdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_total_resultquotientsteppreviousdiagonaltermrightentry. ff_h_pfp_division_total_resultquotientsteppreviousdiagonaltermrightentry + S (pfc_right_division_total_resultquotientsteppreviousdiagonalterm) = S ((S (pfc_complement_division_total_resultquotientsteppreviousdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_total_resultquotientsteppreviousdiagonaltermrightentry. bb = ff_q_pfp_division_total_resultquotientsteppreviousdiagonaltermrightentry * S ((S (pfc_complement_division_total_resultquotientsteppreviousdiagonalterm)) * bc) + (pfc_right_division_total_resultquotientsteppreviousdiagonalterm)))))) \/ (((exists pfc_gap_division_total_resultquotientsteppreviousdiagonaltermrightoutside. pfc_gap_division_total_resultquotientsteppreviousdiagonaltermrightoutside+(S (d))=(pfc_complement_division_total_resultquotientsteppreviousdiagonalterm)) /\ (((pfc_right_division_total_resultquotientsteppreviousdiagonalterm)=0))))) /\ (((pfc_value_division_total_resultquotientsteppreviousdiagonal)=pfc_left_division_total_resultquotientsteppreviousdiagonalterm*pfc_right_division_total_resultquotientsteppreviousdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_total_resultquotientstepprevioussum fs_v_pfc_division_total_resultquotientstepprevioussum. ((((exists fs_h_pfc_division_total_resultquotientstepprevioussum_body_start. fs_h_pfc_division_total_resultquotientstepprevioussum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_total_resultquotientstepprevioussum)) /\ exists fs_q_pfc_division_total_resultquotientstepprevioussum_body_start. fs_u_pfc_division_total_resultquotientstepprevioussum = fs_q_pfc_division_total_resultquotientstepprevioussum_body_start * S ((S (0)) * fs_v_pfc_division_total_resultquotientstepprevioussum) + (0))) /\ ((((exists fs_h_pfc_division_total_resultquotientstepprevioussum_body_terminal. fs_h_pfc_division_total_resultquotientstepprevioussum_body_terminal + S (pfc_natural_sum_division_total_resultquotientstepprevious) = S ((S (S (pfd_index_division_total_resultquotient))) * fs_v_pfc_division_total_resultquotientstepprevioussum)) /\ exists fs_q_pfc_division_total_resultquotientstepprevioussum_body_terminal. fs_u_pfc_division_total_resultquotientstepprevioussum = fs_q_pfc_division_total_resultquotientstepprevioussum_body_terminal * S ((S (S (pfd_index_division_total_resultquotient))) * fs_v_pfc_division_total_resultquotientstepprevioussum) + (pfc_natural_sum_division_total_resultquotientstepprevious))) /\ forall fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps. (exists fs_lt_pfc_division_total_resultquotientstepprevioussum_body_steps_bound. fs_lt_pfc_division_total_resultquotientstepprevioussum_body_steps_bound + S fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps = S (pfd_index_division_total_resultquotient)) -> exists fs_a_pfc_division_total_resultquotientstepprevioussum_body_steps fs_r_pfc_division_total_resultquotientstepprevioussum_body_steps fs_s_pfc_division_total_resultquotientstepprevioussum_body_steps. ((((exists fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_summand. fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_summand + S (fs_a_pfc_division_total_resultquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_total_resultquotientstepprevious)) /\ exists fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_summand. pfc_terms_code_division_total_resultquotientstepprevious = fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_summand * S ((S (fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * pfc_terms_scale_division_total_resultquotientstepprevious) + (fs_a_pfc_division_total_resultquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_partial. fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_partial + S (fs_r_pfc_division_total_resultquotientstepprevioussum_body_steps) = S ((S (fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * fs_v_pfc_division_total_resultquotientstepprevioussum)) /\ exists fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_partial. fs_u_pfc_division_total_resultquotientstepprevioussum = fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_partial * S ((S (fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * fs_v_pfc_division_total_resultquotientstepprevioussum) + (fs_r_pfc_division_total_resultquotientstepprevioussum_body_steps))) /\ ((((exists fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_successor. fs_h_pfc_division_total_resultquotientstepprevioussum_body_steps_successor + S (fs_s_pfc_division_total_resultquotientstepprevioussum_body_steps) = S ((S (S fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * fs_v_pfc_division_total_resultquotientstepprevioussum)) /\ exists fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_successor. fs_u_pfc_division_total_resultquotientstepprevioussum = fs_q_pfc_division_total_resultquotientstepprevioussum_body_steps_successor * S ((S (S fs_i_pfc_division_total_resultquotientstepprevioussum_body_steps)) * fs_v_pfc_division_total_resultquotientstepprevioussum) + (fs_s_pfc_division_total_resultquotientstepprevioussum_body_steps))) /\ fs_s_pfc_division_total_resultquotientstepprevioussum_body_steps = fs_r_pfc_division_total_resultquotientstepprevioussum_body_steps + fs_a_pfc_division_total_resultquotientstepprevioussum_body_steps)))))) /\ ((((exists pfa_gap_division_total_resultquotientsteppreviousresiduebound. pfa_gap_division_total_resultquotientsteppreviousresiduebound + S (pfd_previous_division_total_resultquotientstep) = (p)) /\ ((exists pfa_offset_left_division_total_resultquotientsteppreviousresiduecongruence pfa_offset_right_division_total_resultquotientsteppreviousresiduecongruence. (pfc_natural_sum_division_total_resultquotientstepprevious) + (p) * pfa_offset_left_division_total_resultquotientsteppreviousresiduecongruence = (pfd_previous_division_total_resultquotientstep) + (p) * pfa_offset_right_division_total_resultquotientsteppreviousresiduecongruence))))))))) /\ (((((exists pfa_gap_division_total_resultquotientstepsubtractleft. pfa_gap_division_total_resultquotientstepsubtractleft + S (pfd_previous_division_total_resultquotientstep) = (p)) /\ (((exists pfa_gap_division_total_resultquotientstepsubtractright. pfa_gap_division_total_resultquotientstepsubtractright + S (pfd_difference_division_total_resultquotientstep) = (p)) /\ ((((exists pfa_gap_division_total_resultquotientstepsubtractresultbound. pfa_gap_division_total_resultquotientstepsubtractresultbound + S (pfd_input_division_total_resultquotientstep) = (p)) /\ ((exists pfa_offset_left_division_total_resultquotientstepsubtractresultcongruence pfa_offset_right_division_total_resultquotientstepsubtractresultcongruence. ((pfd_previous_division_total_resultquotientstep) + (pfd_difference_division_total_resultquotientstep)) + (p) * pfa_offset_left_division_total_resultquotientstepsubtractresultcongruence = (pfd_input_division_total_resultquotientstep) + (p) * pfa_offset_right_division_total_resultquotientstepsubtractresultcongruence))))))))) /\ ((((exists pfa_gap_division_total_resultquotientstepmultiplyleft. pfa_gap_division_total_resultquotientstepmultiplyleft + S (pfd_inverse_division_total_result) = (p)) /\ (((exists pfa_gap_division_total_resultquotientstepmultiplyright. pfa_gap_division_total_resultquotientstepmultiplyright + S (pfd_difference_division_total_resultquotientstep) = (p)) /\ ((((exists pfa_gap_division_total_resultquotientstepmultiplyresultbound. pfa_gap_division_total_resultquotientstepmultiplyresultbound + S (pfd_value_division_total_resultquotient) = (p)) /\ ((exists pfa_offset_left_division_total_resultquotientstepmultiplyresultcongruence pfa_offset_right_division_total_resultquotientstepmultiplyresultcongruence. ((pfd_inverse_division_total_result) * (pfd_difference_division_total_resultquotientstep)) + (p) * pfa_offset_left_division_total_resultquotientstepmultiplyresultcongruence = (pfd_value_division_total_resultquotient) + (p) * pfa_offset_right_division_total_resultquotientstepmultiplyresultcongruence))))))))))))))))))) /\ (((forall pfc_index_division_total_resultproduct. (exists pfa_gap_division_total_resultproductbound. pfa_gap_division_total_resultproductbound + S (pfc_index_division_total_resultproduct) = (L)) -> exists pfc_value_division_total_resultproduct. ((((exists ff_h_pfp_division_total_resultproductentry. ff_h_pfp_division_total_resultproductentry + S (pfc_value_division_total_resultproduct) = S ((S (pfc_index_division_total_resultproduct)) * pfd_product_scale_division_total_result)) /\ exists ff_q_pfp_division_total_resultproductentry. pfd_product_code_division_total_result = ff_q_pfp_division_total_resultproductentry * S ((S (pfc_index_division_total_resultproduct)) * pfd_product_scale_division_total_result) + (pfc_value_division_total_resultproduct))) /\ ((exists pfc_terms_code_division_total_resultproductcoefficient pfc_terms_scale_division_total_resultproductcoefficient pfc_natural_sum_division_total_resultproductcoefficient. ((forall pfc_index_division_total_resultproductcoefficientdiagonal. (exists pfa_gap_division_total_resultproductcoefficientdiagonalbound. pfa_gap_division_total_resultproductcoefficientdiagonalbound + S (pfc_index_division_total_resultproductcoefficientdiagonal) = (S (pfc_index_division_total_resultproduct))) -> exists pfc_value_division_total_resultproductcoefficientdiagonal. ((((exists ff_h_pfp_division_total_resultproductcoefficientdiagonalentry. ff_h_pfp_division_total_resultproductcoefficientdiagonalentry + S (pfc_value_division_total_resultproductcoefficientdiagonal) = S ((S (pfc_index_division_total_resultproductcoefficientdiagonal)) * pfc_terms_scale_division_total_resultproductcoefficient)) /\ exists ff_q_pfp_division_total_resultproductcoefficientdiagonalentry. pfc_terms_code_division_total_resultproductcoefficient = ff_q_pfp_division_total_resultproductcoefficientdiagonalentry * S ((S (pfc_index_division_total_resultproductcoefficientdiagonal)) * pfc_terms_scale_division_total_resultproductcoefficient) + (pfc_value_division_total_resultproductcoefficientdiagonal))) /\ ((exists pfc_complement_division_total_resultproductcoefficientdiagonalterm pfc_left_division_total_resultproductcoefficientdiagonalterm pfc_right_division_total_resultproductcoefficientdiagonalterm. (((pfc_index_division_total_resultproductcoefficientdiagonal)+pfc_complement_division_total_resultproductcoefficientdiagonalterm=(pfc_index_division_total_resultproduct)) /\ ((((((exists pfa_gap_division_total_resultproductcoefficientdiagonaltermleftinside. pfa_gap_division_total_resultproductcoefficientdiagonaltermleftinside + S (pfc_index_division_total_resultproductcoefficientdiagonal) = (q)) /\ ((((exists ff_h_pfp_division_total_resultproductcoefficientdiagonaltermleftentry. ff_h_pfp_division_total_resultproductcoefficientdiagonaltermleftentry + S (pfc_left_division_total_resultproductcoefficientdiagonalterm) = S ((S (pfc_index_division_total_resultproductcoefficientdiagonal)) * qc)) /\ exists ff_q_pfp_division_total_resultproductcoefficientdiagonaltermleftentry. qb = ff_q_pfp_division_total_resultproductcoefficientdiagonaltermleftentry * S ((S (pfc_index_division_total_resultproductcoefficientdiagonal)) * qc) + (pfc_left_division_total_resultproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_total_resultproductcoefficientdiagonaltermleftoutside. pfc_gap_division_total_resultproductcoefficientdiagonaltermleftoutside+(q)=(pfc_index_division_total_resultproductcoefficientdiagonal)) /\ (((pfc_left_division_total_resultproductcoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_division_total_resultproductcoefficientdiagonaltermrightinside. pfa_gap_division_total_resultproductcoefficientdiagonaltermrightinside + S (pfc_complement_division_total_resultproductcoefficientdiagonalterm) = (S (d))) /\ ((((exists ff_h_pfp_division_total_resultproductcoefficientdiagonaltermrightentry. ff_h_pfp_division_total_resultproductcoefficientdiagonaltermrightentry + S (pfc_right_division_total_resultproductcoefficientdiagonalterm) = S ((S (pfc_complement_division_total_resultproductcoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_division_total_resultproductcoefficientdiagonaltermrightentry. bb = ff_q_pfp_division_total_resultproductcoefficientdiagonaltermrightentry * S ((S (pfc_complement_division_total_resultproductcoefficientdiagonalterm)) * bc) + (pfc_right_division_total_resultproductcoefficientdiagonalterm)))))) \/ (((exists pfc_gap_division_total_resultproductcoefficientdiagonaltermrightoutside. pfc_gap_division_total_resultproductcoefficientdiagonaltermrightoutside+(S (d))=(pfc_complement_division_total_resultproductcoefficientdiagonalterm)) /\ (((pfc_right_division_total_resultproductcoefficientdiagonalterm)=0))))) /\ (((pfc_value_division_total_resultproductcoefficientdiagonal)=pfc_left_division_total_resultproductcoefficientdiagonalterm*pfc_right_division_total_resultproductcoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_division_total_resultproductcoefficientsum fs_v_pfc_division_total_resultproductcoefficientsum. ((((exists fs_h_pfc_division_total_resultproductcoefficientsum_body_start. fs_h_pfc_division_total_resultproductcoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_division_total_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_total_resultproductcoefficientsum_body_start. fs_u_pfc_division_total_resultproductcoefficientsum = fs_q_pfc_division_total_resultproductcoefficientsum_body_start * S ((S (0)) * fs_v_pfc_division_total_resultproductcoefficientsum) + (0))) /\ ((((exists fs_h_pfc_division_total_resultproductcoefficientsum_body_terminal. fs_h_pfc_division_total_resultproductcoefficientsum_body_terminal + S (pfc_natural_sum_division_total_resultproductcoefficient) = S ((S (S (pfc_index_division_total_resultproduct))) * fs_v_pfc_division_total_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_total_resultproductcoefficientsum_body_terminal. fs_u_pfc_division_total_resultproductcoefficientsum = fs_q_pfc_division_total_resultproductcoefficientsum_body_terminal * S ((S (S (pfc_index_division_total_resultproduct))) * fs_v_pfc_division_total_resultproductcoefficientsum) + (pfc_natural_sum_division_total_resultproductcoefficient))) /\ forall fs_i_pfc_division_total_resultproductcoefficientsum_body_steps. (exists fs_lt_pfc_division_total_resultproductcoefficientsum_body_steps_bound. fs_lt_pfc_division_total_resultproductcoefficientsum_body_steps_bound + S fs_i_pfc_division_total_resultproductcoefficientsum_body_steps = S (pfc_index_division_total_resultproduct)) -> exists fs_a_pfc_division_total_resultproductcoefficientsum_body_steps fs_r_pfc_division_total_resultproductcoefficientsum_body_steps fs_s_pfc_division_total_resultproductcoefficientsum_body_steps. ((((exists fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_summand. fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_summand + S (fs_a_pfc_division_total_resultproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * pfc_terms_scale_division_total_resultproductcoefficient)) /\ exists fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_summand. pfc_terms_code_division_total_resultproductcoefficient = fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_summand * S ((S (fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * pfc_terms_scale_division_total_resultproductcoefficient) + (fs_a_pfc_division_total_resultproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_partial. fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_partial + S (fs_r_pfc_division_total_resultproductcoefficientsum_body_steps) = S ((S (fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_partial. fs_u_pfc_division_total_resultproductcoefficientsum = fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_partial * S ((S (fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_resultproductcoefficientsum) + (fs_r_pfc_division_total_resultproductcoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_successor. fs_h_pfc_division_total_resultproductcoefficientsum_body_steps_successor + S (fs_s_pfc_division_total_resultproductcoefficientsum_body_steps) = S ((S (S fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_resultproductcoefficientsum)) /\ exists fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_successor. fs_u_pfc_division_total_resultproductcoefficientsum = fs_q_pfc_division_total_resultproductcoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_division_total_resultproductcoefficientsum_body_steps)) * fs_v_pfc_division_total_resultproductcoefficientsum) + (fs_s_pfc_division_total_resultproductcoefficientsum_body_steps))) /\ fs_s_pfc_division_total_resultproductcoefficientsum_body_steps = fs_r_pfc_division_total_resultproductcoefficientsum_body_steps + fs_a_pfc_division_total_resultproductcoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_division_total_resultproductcoefficientresiduebound. pfa_gap_division_total_resultproductcoefficientresiduebound + S (pfc_value_division_total_resultproduct) = (p)) /\ ((exists pfa_offset_left_division_total_resultproductcoefficientresiduecongruence pfa_offset_right_division_total_resultproductcoefficientresiduecongruence. (pfc_natural_sum_division_total_resultproductcoefficient) + (p) * pfa_offset_left_division_total_resultproductcoefficientresiduecongruence = (pfc_value_division_total_resultproduct) + (p) * pfa_offset_right_division_total_resultproductcoefficientresiduecongruence)))))))))))) /\ (((forall pfs_index_division_total_resultdifference. (exists pfa_gap_division_total_resultdifferenceindex. pfa_gap_division_total_resultdifferenceindex + S (pfs_index_division_total_resultdifference) = (L)) -> exists pfs_left_division_total_resultdifference pfs_right_division_total_resultdifference pfs_result_division_total_resultdifference. ((((exists ff_h_pfp_division_total_resultdifferenceleft. ff_h_pfp_division_total_resultdifferenceleft + S (pfs_left_division_total_resultdifference) = S ((S (pfs_index_division_total_resultdifference)) * ac)) /\ exists ff_q_pfp_division_total_resultdifferenceleft. ab = ff_q_pfp_division_total_resultdifferenceleft * S ((S (pfs_index_division_total_resultdifference)) * ac) + (pfs_left_division_total_resultdifference))) /\ (((((exists ff_h_pfp_division_total_resultdifferenceright. ff_h_pfp_division_total_resultdifferenceright + S (pfs_right_division_total_resultdifference) = S ((S (pfs_index_division_total_resultdifference)) * pfd_product_scale_division_total_result)) /\ exists ff_q_pfp_division_total_resultdifferenceright. pfd_product_code_division_total_result = ff_q_pfp_division_total_resultdifferenceright * S ((S (pfs_index_division_total_resultdifference)) * pfd_product_scale_division_total_result) + (pfs_right_division_total_resultdifference))) /\ (((((exists ff_h_pfp_division_total_resultdifferenceresult. ff_h_pfp_division_total_resultdifferenceresult + S (pfs_result_division_total_resultdifference) = S ((S (pfs_index_division_total_resultdifference)) * pfd_residual_scale_division_total_result)) /\ exists ff_q_pfp_division_total_resultdifferenceresult. pfd_residual_code_division_total_result = ff_q_pfp_division_total_resultdifferenceresult * S ((S (pfs_index_division_total_resultdifference)) * pfd_residual_scale_division_total_result) + (pfs_result_division_total_resultdifference))) /\ ((((exists pfa_gap_division_total_resultdifferenceoperationleft. pfa_gap_division_total_resultdifferenceoperationleft + S (pfs_right_division_total_resultdifference) = (p)) /\ (((exists pfa_gap_division_total_resultdifferenceoperationright. pfa_gap_division_total_resultdifferenceoperationright + S (pfs_result_division_total_resultdifference) = (p)) /\ ((((exists pfa_gap_division_total_resultdifferenceoperationresultbound. pfa_gap_division_total_resultdifferenceoperationresultbound + S (pfs_left_division_total_resultdifference) = (p)) /\ ((exists pfa_offset_left_division_total_resultdifferenceoperationresultcongruence pfa_offset_right_division_total_resultdifferenceoperationresultcongruence. ((pfs_right_division_total_resultdifference) + (pfs_result_division_total_resultdifference)) + (p) * pfa_offset_left_division_total_resultdifferenceoperationresultcongruence = (pfs_left_division_total_resultdifference) + (p) * pfa_offset_right_division_total_resultdifferenceoperationresultcongruence)))))))))))))))) /\ (((((L)=(pfd_cut_division_total_result)+(R)) /\ (((forall fom_index_pfp_division_total_resulttriminput. (exists fom_gap_pfp_division_total_resulttriminput_index_bound. fom_gap_pfp_division_total_resulttriminput_index_bound + S (fom_index_pfp_division_total_resulttriminput) = L) -> exists fom_value_pfp_division_total_resulttriminput. ((((exists fom_beta_height_pfp_division_total_resulttriminput_entry. fom_beta_height_pfp_division_total_resulttriminput_entry + S (fom_value_pfp_division_total_resulttriminput) = S ((S (fom_index_pfp_division_total_resulttriminput)) * pfd_residual_scale_division_total_result)) /\ exists fom_beta_quotient_pfp_division_total_resulttriminput_entry. pfd_residual_code_division_total_result = fom_beta_quotient_pfp_division_total_resulttriminput_entry * S ((S (fom_index_pfp_division_total_resulttriminput)) * pfd_residual_scale_division_total_result) + (fom_value_pfp_division_total_resulttriminput))) /\ (exists fom_gap_pfp_division_total_resulttriminput_value_bound. fom_gap_pfp_division_total_resulttriminput_value_bound + S (fom_value_pfp_division_total_resulttriminput) = p))) /\ (((forall pfp_repeat_index_division_total_resulttrimremoved. (exists pfa_gap_division_total_resulttrimremovedindex. pfa_gap_division_total_resulttrimremovedindex + S (pfp_repeat_index_division_total_resulttrimremoved) = (pfd_cut_division_total_result)) -> (((exists ff_h_pfp_division_total_resulttrimremovedentry. ff_h_pfp_division_total_resulttrimremovedentry + S (0) = S ((S (pfp_repeat_index_division_total_resulttrimremoved)) * pfd_residual_scale_division_total_result)) /\ exists ff_q_pfp_division_total_resulttrimremovedentry. pfd_residual_code_division_total_result = ff_q_pfp_division_total_resulttrimremovedentry * S ((S (pfp_repeat_index_division_total_resulttrimremoved)) * pfd_residual_scale_division_total_result) + (0)))) /\ (((forall pftrim_index_division_total_resulttrimsuffix pftrim_value_division_total_resulttrimsuffix. (exists pfa_gap_division_total_resulttrimsuffixbound. pfa_gap_division_total_resulttrimsuffixbound + S (pftrim_index_division_total_resulttrimsuffix) = (R)) -> (((exists ff_h_pfp_division_total_resulttrimsuffixsource. ff_h_pfp_division_total_resulttrimsuffixsource + S (pftrim_value_division_total_resulttrimsuffix) = S ((S ((pfd_cut_division_total_result)+pftrim_index_division_total_resulttrimsuffix)) * pfd_residual_scale_division_total_result)) /\ exists ff_q_pfp_division_total_resulttrimsuffixsource. pfd_residual_code_division_total_result = ff_q_pfp_division_total_resulttrimsuffixsource * S ((S ((pfd_cut_division_total_result)+pftrim_index_division_total_resulttrimsuffix)) * pfd_residual_scale_division_total_result) + (pftrim_value_division_total_resulttrimsuffix))) -> (((exists ff_h_pfp_division_total_resulttrimsuffixoutput. ff_h_pfp_division_total_resulttrimsuffixoutput + S (pftrim_value_division_total_resulttrimsuffix) = S ((S (pftrim_index_division_total_resulttrimsuffix)) * rc)) /\ exists ff_q_pfp_division_total_resulttrimsuffixoutput. rb = ff_q_pfp_division_total_resulttrimsuffixoutput * S ((S (pftrim_index_division_total_resulttrimsuffix)) * rc) + (pftrim_value_division_total_resulttrimsuffix)))) /\ (((R)=0 \/ (exists pftrim_leading_division_total_resulttrimnormal. ((((exists ff_h_pfp_division_total_resulttrimnormalentry. ff_h_pfp_division_total_resulttrimnormalentry + S (pftrim_leading_division_total_resulttrimnormal) = S ((S (0)) * rc)) /\ exists ff_q_pfp_division_total_resulttrimnormalentry. rb = ff_q_pfp_division_total_resulttrimnormalentry * S ((S (0)) * rc) + (pftrim_leading_division_total_resulttrimnormal))) /\ ((~(pftrim_leading_division_total_resulttrimnormal=0)))))))))))))))))))))))))))))))))

Complete tactic proof in conservative notation

All 86 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

86 script commands · 26 reading checkpoints · 2 local claims

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

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
prime field polynomial division quotient data existsprime field polynomial division residual data exists
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro d
  8. L8
    intro hp
  9. L9
    intro ha
  10. L10
    intro hb
02Establish hquotientL11–20

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

  1. L11
    have hquotient : ∃ b. ∃ k. ∃ q. ∃ qb. ∃ qc. BetaAt(bb,bc,0,b) ∧ (FpInv(p,b,k) ∧ (PolynomialQuotientLength(L,d,q) ∧ FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,S d,qb,qc,q)))Definitions: BetaAt(bb,bc,0,b)FpInv(p,b,k)PolynomialQuotientLength(L,d,q)FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,S d,qb,qc,q)Original native command in the exact edition
  2. L12
    specialize prime_field_polynomial_division_quotient_data_exists (p)
  3. L13
    specialize prime_field_polynomial_division_quotient_data_exists (ab)
  4. L14
    specialize prime_field_polynomial_division_quotient_data_exists (ac)
  5. L15
    specialize prime_field_polynomial_division_quotient_data_exists (L)
  6. L16
    specialize prime_field_polynomial_division_quotient_data_exists (bb)
  7. L17
    specialize prime_field_polynomial_division_quotient_data_exists (bc)
  8. L18
    specialize prime_field_polynomial_division_quotient_data_exists (d)
  9. L19
    apply prime_field_polynomial_division_quotient_data_exists
  10. L20
    exact hp
03Use earlier factsL21–22

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

  1. L21
    exact ha
  2. L22
    exact hb
04Separate the logical casesL23–30

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

  1. L23
    cases hquotient
  2. L24
    cases hquotient_witness
  3. L25
    cases hquotient_witness_witness
  4. L26
    cases hquotient_witness_witness_witness
  5. L27
    cases hquotient_witness_witness_witness_witness
  6. L28
    cases hquotient_witness_witness_witness_witness_witness
  7. L29
    cases hquotient_witness_witness_witness_witness_witness_right
  8. L30
    cases hquotient_witness_witness_witness_witness_witness_right_right
05Establish hresidualL31–40

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

  1. L31
    have hresidual : ∃ pb. ∃ pc. ∃ ub. ∃ uc. ∃ t. ∃ rb. ∃ rc. ∃ R. FpConvolutionPrefix(p,x3,x4,x2,bb,bc,S d,pb,pc,L) ∧ (FpCoefficientSubtraction(p,ab,ac,pb,pc,ub,uc,L) ∧ FpPolynomialTrim(p,ub,uc,L,t,rb,rc,R))Definitions: FpConvolutionPrefix(p,x3,x4,x2,bb,bc,S d,pb,pc,L)FpCoefficientSubtraction(p,ab,ac,pb,pc,ub,uc,L)FpPolynomialTrim(p,ub,uc,L,t,rb,rc,R)Original native command in the exact edition
  2. L32
    specialize prime_field_polynomial_division_residual_data_exists (p)
  3. L33
    specialize prime_field_polynomial_division_residual_data_exists (ab)
  4. L34
    specialize prime_field_polynomial_division_residual_data_exists (ac)
  5. L35
    specialize prime_field_polynomial_division_residual_data_exists (L)
  6. L36
    specialize prime_field_polynomial_division_residual_data_exists (bb)
  7. L37
    specialize prime_field_polynomial_division_residual_data_exists (bc)
  8. L38
    specialize prime_field_polynomial_division_residual_data_exists (d)
  9. L39
    specialize prime_field_polynomial_division_residual_data_exists (x3)
  10. L40
    specialize prime_field_polynomial_division_residual_data_exists (x4)
06Use earlier factsL41–44

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

  1. L41
    specialize prime_field_polynomial_division_residual_data_exists (x2)
  2. L42
    apply prime_field_polynomial_division_residual_data_exists
  3. L43
    exact hp
  4. L44
    exact ha
07Separate the logical casesL45–54

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

  1. L45
    cases hresidual
  2. L46
    cases hresidual_witness
  3. L47
    cases hresidual_witness_witness
  4. L48
    cases hresidual_witness_witness_witness
  5. L49
    cases hresidual_witness_witness_witness_witness
  6. L50
    cases hresidual_witness_witness_witness_witness_witness
  7. L51
    cases hresidual_witness_witness_witness_witness_witness_witness
  8. L52
    cases hresidual_witness_witness_witness_witness_witness_witness_witness
  9. L53
    cases hresidual_witness_witness_witness_witness_witness_witness_witness_witness
  10. L54
    cases hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right
08Separate the logical casesL55–56

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

  1. L55
    cases hb
  2. L56
    cases hb_right
09Construct an explicit witnessL57–62

Supply the displayed value, then prove that it has the required property.

  1. L57
    exists x3
  2. L58
    exists x4
  3. L59
    exists x2
  4. L60
    exists x10
  5. L61
    exists x11
  6. L62
    exists x12
10Separate the logical casesL63–63

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

  1. L63
    split
11Use earlier factsL64–64

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

  1. L64
    exact ha
12Separate the logical casesL65–65

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

  1. L65
    split
13Use earlier factsL66–66

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

  1. L66
    exact hb_right_left
14Separate the logical casesL67–67

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

  1. L67
    split
15Use earlier factsL68–68

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

  1. L68
    exact hquotient_witness_witness_witness_witness_witness_right_right_left
16Construct an explicit witnessL69–75

Supply the displayed value, then prove that it has the required property.

  1. L69
    exists x
  2. L70
    exists x1
  3. L71
    exists x5
  4. L72
    exists x6
  5. L73
    exists x7
  6. L74
    exists x8
  7. L75
    exists x9
17Separate the logical casesL76–76

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

  1. L76
    split
18Use earlier factsL77–77

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

  1. L77
    exact hquotient_witness_witness_witness_witness_witness_left
19Separate the logical casesL78–78

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

  1. L78
    split
20Use earlier factsL79–79

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

  1. L79
    exact hquotient_witness_witness_witness_witness_witness_right_left
21Separate the logical casesL80–80

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

  1. L80
    split
22Use earlier factsL81–81

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

  1. L81
    exact hquotient_witness_witness_witness_witness_witness_right_right_right
23Separate the logical casesL82–82

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

  1. L82
    split
24Use earlier factsL83–83

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

  1. L83
    exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_left
25Separate the logical casesL84–84

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

  1. L84
    split
26Use earlier factsL85–86

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

  1. L85
    exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  2. L86
    exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right_right

Library-wide reading audit

Original defined command ledger · 86 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro d
  8. 0008intro hp
  9. 0009intro ha
  10. 0010intro hb
  11. 0011have hquotient : ∃ b. ∃ k. ∃ q. ∃ qb. ∃ qc. BetaAt(bb,bc,0,b) ∧ (FpInv(p,b,k) ∧ (PolynomialQuotientLength(L,d,q) ∧ FpPolynomialQuotientPrefix(p,k,ab,ac,bb,bc,S d,qb,qc,q)))
  12. 0012specialize prime_field_polynomial_division_quotient_data_exists (p)
  13. 0013specialize prime_field_polynomial_division_quotient_data_exists (ab)
  14. 0014specialize prime_field_polynomial_division_quotient_data_exists (ac)
  15. 0015specialize prime_field_polynomial_division_quotient_data_exists (L)
  16. 0016specialize prime_field_polynomial_division_quotient_data_exists (bb)
  17. 0017specialize prime_field_polynomial_division_quotient_data_exists (bc)
  18. 0018specialize prime_field_polynomial_division_quotient_data_exists (d)
  19. 0019apply prime_field_polynomial_division_quotient_data_exists
  20. 0020exact hp
  21. 0021exact ha
  22. 0022exact hb
  23. 0023cases hquotient
  24. 0024cases hquotient_witness
  25. 0025cases hquotient_witness_witness
  26. 0026cases hquotient_witness_witness_witness
  27. 0027cases hquotient_witness_witness_witness_witness
  28. 0028cases hquotient_witness_witness_witness_witness_witness
  29. 0029cases hquotient_witness_witness_witness_witness_witness_right
  30. 0030cases hquotient_witness_witness_witness_witness_witness_right_right
  31. 0031have hresidual : ∃ pb. ∃ pc. ∃ ub. ∃ uc. ∃ t. ∃ rb. ∃ rc. ∃ R. FpConvolutionPrefix(p,x3,x4,x2,bb,bc,S d,pb,pc,L) ∧ (FpCoefficientSubtraction(p,ab,ac,pb,pc,ub,uc,L) ∧ FpPolynomialTrim(p,ub,uc,L,t,rb,rc,R))
  32. 0032specialize prime_field_polynomial_division_residual_data_exists (p)
  33. 0033specialize prime_field_polynomial_division_residual_data_exists (ab)
  34. 0034specialize prime_field_polynomial_division_residual_data_exists (ac)
  35. 0035specialize prime_field_polynomial_division_residual_data_exists (L)
  36. 0036specialize prime_field_polynomial_division_residual_data_exists (bb)
  37. 0037specialize prime_field_polynomial_division_residual_data_exists (bc)
  38. 0038specialize prime_field_polynomial_division_residual_data_exists (d)
  39. 0039specialize prime_field_polynomial_division_residual_data_exists (x3)
  40. 0040specialize prime_field_polynomial_division_residual_data_exists (x4)
  41. 0041specialize prime_field_polynomial_division_residual_data_exists (x2)
  42. 0042apply prime_field_polynomial_division_residual_data_exists
  43. 0043exact hp
  44. 0044exact ha
  45. 0045cases hresidual
  46. 0046cases hresidual_witness
  47. 0047cases hresidual_witness_witness
  48. 0048cases hresidual_witness_witness_witness
  49. 0049cases hresidual_witness_witness_witness_witness
  50. 0050cases hresidual_witness_witness_witness_witness_witness
  51. 0051cases hresidual_witness_witness_witness_witness_witness_witness
  52. 0052cases hresidual_witness_witness_witness_witness_witness_witness_witness
  53. 0053cases hresidual_witness_witness_witness_witness_witness_witness_witness_witness
  54. 0054cases hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right
  55. 0055cases hb
  56. 0056cases hb_right
  57. 0057exists x3
  58. 0058exists x4
  59. 0059exists x2
  60. 0060exists x10
  61. 0061exists x11
  62. 0062exists x12
  63. 0063split
  64. 0064exact ha
  65. 0065split
  66. 0066exact hb_right_left
  67. 0067split
  68. 0068exact hquotient_witness_witness_witness_witness_witness_right_right_left
  69. 0069exists x
  70. 0070exists x1
  71. 0071exists x5
  72. 0072exists x6
  73. 0073exists x7
  74. 0074exists x8
  75. 0075exists x9
  76. 0076split
  77. 0077exact hquotient_witness_witness_witness_witness_witness_left
  78. 0078split
  79. 0079exact hquotient_witness_witness_witness_witness_witness_right_left
  80. 0080split
  81. 0081exact hquotient_witness_witness_witness_witness_witness_right_right_right
  82. 0082split
  83. 0083exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_left
  84. 0084split
  85. 0085exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right_left
  86. 0086exact hresidual_witness_witness_witness_witness_witness_witness_witness_witness_right_right