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. ∀ AB. ∀ AC. ∀ bb. ∀ bc. ∀ M. ∀ N. ∀ i. ∀ r. BetaPrefixEqual(ab,ac,AB,AC,N) → Lt(i,N) → FpConvolutionCoefficient(p,ab,ac,N,bb,bc,M,i,r) → FpConvolutionCoefficient(p,AB,AC,S N,bb,bc,M,i,r)
Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
BetaPrefixEqual(b,c,d,e,l) · 1FpConvolutionCoefficient(p,ab,ac,L,bb,bc,M,i,r) · 2Lt(a,b) · 1
Actual proof prerequisites
Original expanded first-order statement
forall p ab ac AB AC bb bc M N i r. (forall mdr_i_pfp_tri_append_equal mdr_a_pfp_tri_append_equal. (exists mdr_gap_pfp_tri_append_equalb. mdr_gap_pfp_tri_append_equalb + S (mdr_i_pfp_tri_append_equal) = (N)) -> (((exists ff_h_mdr_pfp_tri_append_equalo. ff_h_mdr_pfp_tri_append_equalo + S (mdr_a_pfp_tri_append_equal) = S ((S (mdr_i_pfp_tri_append_equal)) * ac)) /\ exists ff_q_mdr_pfp_tri_append_equalo. ab = ff_q_mdr_pfp_tri_append_equalo * S ((S (mdr_i_pfp_tri_append_equal)) * ac) + (mdr_a_pfp_tri_append_equal))) -> (((exists ff_h_mdr_pfp_tri_append_equaln. ff_h_mdr_pfp_tri_append_equaln + S (mdr_a_pfp_tri_append_equal) = S ((S (mdr_i_pfp_tri_append_equal)) * AC)) /\ exists ff_q_mdr_pfp_tri_append_equaln. AB = ff_q_mdr_pfp_tri_append_equaln * S ((S (mdr_i_pfp_tri_append_equal)) * AC) + (mdr_a_pfp_tri_append_equal)))) -> (exists pfa_gap_tri_append_earlier_index. pfa_gap_tri_append_earlier_index + S (i) = (N)) -> (exists pfc_terms_code_tri_append_earlier_old pfc_terms_scale_tri_append_earlier_old pfc_natural_sum_tri_append_earlier_old. ((forall pfc_index_tri_append_earlier_olddiagonal. (exists pfa_gap_tri_append_earlier_olddiagonalbound. pfa_gap_tri_append_earlier_olddiagonalbound + S (pfc_index_tri_append_earlier_olddiagonal) = (S (i))) -> exists pfc_value_tri_append_earlier_olddiagonal. ((((exists ff_h_pfp_tri_append_earlier_olddiagonalentry. ff_h_pfp_tri_append_earlier_olddiagonalentry + S (pfc_value_tri_append_earlier_olddiagonal) = S ((S (pfc_index_tri_append_earlier_olddiagonal)) * pfc_terms_scale_tri_append_earlier_old)) /\ exists ff_q_pfp_tri_append_earlier_olddiagonalentry. pfc_terms_code_tri_append_earlier_old = ff_q_pfp_tri_append_earlier_olddiagonalentry * S ((S (pfc_index_tri_append_earlier_olddiagonal)) * pfc_terms_scale_tri_append_earlier_old) + (pfc_value_tri_append_earlier_olddiagonal))) /\ ((exists pfc_complement_tri_append_earlier_olddiagonalterm pfc_left_tri_append_earlier_olddiagonalterm pfc_right_tri_append_earlier_olddiagonalterm. (((pfc_index_tri_append_earlier_olddiagonal)+pfc_complement_tri_append_earlier_olddiagonalterm=(i)) /\ ((((((exists pfa_gap_tri_append_earlier_olddiagonaltermleftinside. pfa_gap_tri_append_earlier_olddiagonaltermleftinside + S (pfc_index_tri_append_earlier_olddiagonal) = (N)) /\ ((((exists ff_h_pfp_tri_append_earlier_olddiagonaltermleftentry. ff_h_pfp_tri_append_earlier_olddiagonaltermleftentry + S (pfc_left_tri_append_earlier_olddiagonalterm) = S ((S (pfc_index_tri_append_earlier_olddiagonal)) * ac)) /\ exists ff_q_pfp_tri_append_earlier_olddiagonaltermleftentry. ab = ff_q_pfp_tri_append_earlier_olddiagonaltermleftentry * S ((S (pfc_index_tri_append_earlier_olddiagonal)) * ac) + (pfc_left_tri_append_earlier_olddiagonalterm)))))) \/ (((exists pfc_gap_tri_append_earlier_olddiagonaltermleftoutside. pfc_gap_tri_append_earlier_olddiagonaltermleftoutside+(N)=(pfc_index_tri_append_earlier_olddiagonal)) /\ (((pfc_left_tri_append_earlier_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_append_earlier_olddiagonaltermrightinside. pfa_gap_tri_append_earlier_olddiagonaltermrightinside + S (pfc_complement_tri_append_earlier_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_tri_append_earlier_olddiagonaltermrightentry. ff_h_pfp_tri_append_earlier_olddiagonaltermrightentry + S (pfc_right_tri_append_earlier_olddiagonalterm) = S ((S (pfc_complement_tri_append_earlier_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_append_earlier_olddiagonaltermrightentry. bb = ff_q_pfp_tri_append_earlier_olddiagonaltermrightentry * S ((S (pfc_complement_tri_append_earlier_olddiagonalterm)) * bc) + (pfc_right_tri_append_earlier_olddiagonalterm)))))) \/ (((exists pfc_gap_tri_append_earlier_olddiagonaltermrightoutside. pfc_gap_tri_append_earlier_olddiagonaltermrightoutside+(M)=(pfc_complement_tri_append_earlier_olddiagonalterm)) /\ (((pfc_right_tri_append_earlier_olddiagonalterm)=0))))) /\ (((pfc_value_tri_append_earlier_olddiagonal)=pfc_left_tri_append_earlier_olddiagonalterm*pfc_right_tri_append_earlier_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_append_earlier_oldsum fs_v_pfc_tri_append_earlier_oldsum. ((((exists fs_h_pfc_tri_append_earlier_oldsum_body_start. fs_h_pfc_tri_append_earlier_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_append_earlier_oldsum)) /\ exists fs_q_pfc_tri_append_earlier_oldsum_body_start. fs_u_pfc_tri_append_earlier_oldsum = fs_q_pfc_tri_append_earlier_oldsum_body_start * S ((S (0)) * fs_v_pfc_tri_append_earlier_oldsum) + (0))) /\ ((((exists fs_h_pfc_tri_append_earlier_oldsum_body_terminal. fs_h_pfc_tri_append_earlier_oldsum_body_terminal + S (pfc_natural_sum_tri_append_earlier_old) = S ((S (S (i))) * fs_v_pfc_tri_append_earlier_oldsum)) /\ exists fs_q_pfc_tri_append_earlier_oldsum_body_terminal. fs_u_pfc_tri_append_earlier_oldsum = fs_q_pfc_tri_append_earlier_oldsum_body_terminal * S ((S (S (i))) * fs_v_pfc_tri_append_earlier_oldsum) + (pfc_natural_sum_tri_append_earlier_old))) /\ forall fs_i_pfc_tri_append_earlier_oldsum_body_steps. (exists fs_lt_pfc_tri_append_earlier_oldsum_body_steps_bound. fs_lt_pfc_tri_append_earlier_oldsum_body_steps_bound + S fs_i_pfc_tri_append_earlier_oldsum_body_steps = S (i)) -> exists fs_a_pfc_tri_append_earlier_oldsum_body_steps fs_r_pfc_tri_append_earlier_oldsum_body_steps fs_s_pfc_tri_append_earlier_oldsum_body_steps. ((((exists fs_h_pfc_tri_append_earlier_oldsum_body_steps_summand. fs_h_pfc_tri_append_earlier_oldsum_body_steps_summand + S (fs_a_pfc_tri_append_earlier_oldsum_body_steps) = S ((S (fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * pfc_terms_scale_tri_append_earlier_old)) /\ exists fs_q_pfc_tri_append_earlier_oldsum_body_steps_summand. pfc_terms_code_tri_append_earlier_old = fs_q_pfc_tri_append_earlier_oldsum_body_steps_summand * S ((S (fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * pfc_terms_scale_tri_append_earlier_old) + (fs_a_pfc_tri_append_earlier_oldsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_earlier_oldsum_body_steps_partial. fs_h_pfc_tri_append_earlier_oldsum_body_steps_partial + S (fs_r_pfc_tri_append_earlier_oldsum_body_steps) = S ((S (fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * fs_v_pfc_tri_append_earlier_oldsum)) /\ exists fs_q_pfc_tri_append_earlier_oldsum_body_steps_partial. fs_u_pfc_tri_append_earlier_oldsum = fs_q_pfc_tri_append_earlier_oldsum_body_steps_partial * S ((S (fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * fs_v_pfc_tri_append_earlier_oldsum) + (fs_r_pfc_tri_append_earlier_oldsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_earlier_oldsum_body_steps_successor. fs_h_pfc_tri_append_earlier_oldsum_body_steps_successor + S (fs_s_pfc_tri_append_earlier_oldsum_body_steps) = S ((S (S fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * fs_v_pfc_tri_append_earlier_oldsum)) /\ exists fs_q_pfc_tri_append_earlier_oldsum_body_steps_successor. fs_u_pfc_tri_append_earlier_oldsum = fs_q_pfc_tri_append_earlier_oldsum_body_steps_successor * S ((S (S fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * fs_v_pfc_tri_append_earlier_oldsum) + (fs_s_pfc_tri_append_earlier_oldsum_body_steps))) /\ fs_s_pfc_tri_append_earlier_oldsum_body_steps = fs_r_pfc_tri_append_earlier_oldsum_body_steps + fs_a_pfc_tri_append_earlier_oldsum_body_steps)))))) /\ ((((exists pfa_gap_tri_append_earlier_oldresiduebound. pfa_gap_tri_append_earlier_oldresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_append_earlier_oldresiduecongruence pfa_offset_right_tri_append_earlier_oldresiduecongruence. (pfc_natural_sum_tri_append_earlier_old) + (p) * pfa_offset_left_tri_append_earlier_oldresiduecongruence = (r) + (p) * pfa_offset_right_tri_append_earlier_oldresiduecongruence))))))))) -> (exists pfc_terms_code_tri_append_earlier_new pfc_terms_scale_tri_append_earlier_new pfc_natural_sum_tri_append_earlier_new. ((forall pfc_index_tri_append_earlier_newdiagonal. (exists pfa_gap_tri_append_earlier_newdiagonalbound. pfa_gap_tri_append_earlier_newdiagonalbound + S (pfc_index_tri_append_earlier_newdiagonal) = (S (i))) -> exists pfc_value_tri_append_earlier_newdiagonal. ((((exists ff_h_pfp_tri_append_earlier_newdiagonalentry. ff_h_pfp_tri_append_earlier_newdiagonalentry + S (pfc_value_tri_append_earlier_newdiagonal) = S ((S (pfc_index_tri_append_earlier_newdiagonal)) * pfc_terms_scale_tri_append_earlier_new)) /\ exists ff_q_pfp_tri_append_earlier_newdiagonalentry. pfc_terms_code_tri_append_earlier_new = ff_q_pfp_tri_append_earlier_newdiagonalentry * S ((S (pfc_index_tri_append_earlier_newdiagonal)) * pfc_terms_scale_tri_append_earlier_new) + (pfc_value_tri_append_earlier_newdiagonal))) /\ ((exists pfc_complement_tri_append_earlier_newdiagonalterm pfc_left_tri_append_earlier_newdiagonalterm pfc_right_tri_append_earlier_newdiagonalterm. (((pfc_index_tri_append_earlier_newdiagonal)+pfc_complement_tri_append_earlier_newdiagonalterm=(i)) /\ ((((((exists pfa_gap_tri_append_earlier_newdiagonaltermleftinside. pfa_gap_tri_append_earlier_newdiagonaltermleftinside + S (pfc_index_tri_append_earlier_newdiagonal) = (S N)) /\ ((((exists ff_h_pfp_tri_append_earlier_newdiagonaltermleftentry. ff_h_pfp_tri_append_earlier_newdiagonaltermleftentry + S (pfc_left_tri_append_earlier_newdiagonalterm) = S ((S (pfc_index_tri_append_earlier_newdiagonal)) * AC)) /\ exists ff_q_pfp_tri_append_earlier_newdiagonaltermleftentry. AB = ff_q_pfp_tri_append_earlier_newdiagonaltermleftentry * S ((S (pfc_index_tri_append_earlier_newdiagonal)) * AC) + (pfc_left_tri_append_earlier_newdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_earlier_newdiagonaltermleftoutside. pfc_gap_tri_append_earlier_newdiagonaltermleftoutside+(S N)=(pfc_index_tri_append_earlier_newdiagonal)) /\ (((pfc_left_tri_append_earlier_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_append_earlier_newdiagonaltermrightinside. pfa_gap_tri_append_earlier_newdiagonaltermrightinside + S (pfc_complement_tri_append_earlier_newdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_tri_append_earlier_newdiagonaltermrightentry. ff_h_pfp_tri_append_earlier_newdiagonaltermrightentry + S (pfc_right_tri_append_earlier_newdiagonalterm) = S ((S (pfc_complement_tri_append_earlier_newdiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_append_earlier_newdiagonaltermrightentry. bb = ff_q_pfp_tri_append_earlier_newdiagonaltermrightentry * S ((S (pfc_complement_tri_append_earlier_newdiagonalterm)) * bc) + (pfc_right_tri_append_earlier_newdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_earlier_newdiagonaltermrightoutside. pfc_gap_tri_append_earlier_newdiagonaltermrightoutside+(M)=(pfc_complement_tri_append_earlier_newdiagonalterm)) /\ (((pfc_right_tri_append_earlier_newdiagonalterm)=0))))) /\ (((pfc_value_tri_append_earlier_newdiagonal)=pfc_left_tri_append_earlier_newdiagonalterm*pfc_right_tri_append_earlier_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_append_earlier_newsum fs_v_pfc_tri_append_earlier_newsum. ((((exists fs_h_pfc_tri_append_earlier_newsum_body_start. fs_h_pfc_tri_append_earlier_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_append_earlier_newsum)) /\ exists fs_q_pfc_tri_append_earlier_newsum_body_start. fs_u_pfc_tri_append_earlier_newsum = fs_q_pfc_tri_append_earlier_newsum_body_start * S ((S (0)) * fs_v_pfc_tri_append_earlier_newsum) + (0))) /\ ((((exists fs_h_pfc_tri_append_earlier_newsum_body_terminal. fs_h_pfc_tri_append_earlier_newsum_body_terminal + S (pfc_natural_sum_tri_append_earlier_new) = S ((S (S (i))) * fs_v_pfc_tri_append_earlier_newsum)) /\ exists fs_q_pfc_tri_append_earlier_newsum_body_terminal. fs_u_pfc_tri_append_earlier_newsum = fs_q_pfc_tri_append_earlier_newsum_body_terminal * S ((S (S (i))) * fs_v_pfc_tri_append_earlier_newsum) + (pfc_natural_sum_tri_append_earlier_new))) /\ forall fs_i_pfc_tri_append_earlier_newsum_body_steps. (exists fs_lt_pfc_tri_append_earlier_newsum_body_steps_bound. fs_lt_pfc_tri_append_earlier_newsum_body_steps_bound + S fs_i_pfc_tri_append_earlier_newsum_body_steps = S (i)) -> exists fs_a_pfc_tri_append_earlier_newsum_body_steps fs_r_pfc_tri_append_earlier_newsum_body_steps fs_s_pfc_tri_append_earlier_newsum_body_steps. ((((exists fs_h_pfc_tri_append_earlier_newsum_body_steps_summand. fs_h_pfc_tri_append_earlier_newsum_body_steps_summand + S (fs_a_pfc_tri_append_earlier_newsum_body_steps) = S ((S (fs_i_pfc_tri_append_earlier_newsum_body_steps)) * pfc_terms_scale_tri_append_earlier_new)) /\ exists fs_q_pfc_tri_append_earlier_newsum_body_steps_summand. pfc_terms_code_tri_append_earlier_new = fs_q_pfc_tri_append_earlier_newsum_body_steps_summand * S ((S (fs_i_pfc_tri_append_earlier_newsum_body_steps)) * pfc_terms_scale_tri_append_earlier_new) + (fs_a_pfc_tri_append_earlier_newsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_earlier_newsum_body_steps_partial. fs_h_pfc_tri_append_earlier_newsum_body_steps_partial + S (fs_r_pfc_tri_append_earlier_newsum_body_steps) = S ((S (fs_i_pfc_tri_append_earlier_newsum_body_steps)) * fs_v_pfc_tri_append_earlier_newsum)) /\ exists fs_q_pfc_tri_append_earlier_newsum_body_steps_partial. fs_u_pfc_tri_append_earlier_newsum = fs_q_pfc_tri_append_earlier_newsum_body_steps_partial * S ((S (fs_i_pfc_tri_append_earlier_newsum_body_steps)) * fs_v_pfc_tri_append_earlier_newsum) + (fs_r_pfc_tri_append_earlier_newsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_earlier_newsum_body_steps_successor. fs_h_pfc_tri_append_earlier_newsum_body_steps_successor + S (fs_s_pfc_tri_append_earlier_newsum_body_steps) = S ((S (S fs_i_pfc_tri_append_earlier_newsum_body_steps)) * fs_v_pfc_tri_append_earlier_newsum)) /\ exists fs_q_pfc_tri_append_earlier_newsum_body_steps_successor. fs_u_pfc_tri_append_earlier_newsum = fs_q_pfc_tri_append_earlier_newsum_body_steps_successor * S ((S (S fs_i_pfc_tri_append_earlier_newsum_body_steps)) * fs_v_pfc_tri_append_earlier_newsum) + (fs_s_pfc_tri_append_earlier_newsum_body_steps))) /\ fs_s_pfc_tri_append_earlier_newsum_body_steps = fs_r_pfc_tri_append_earlier_newsum_body_steps + fs_a_pfc_tri_append_earlier_newsum_body_steps)))))) /\ ((((exists pfa_gap_tri_append_earlier_newresiduebound. pfa_gap_tri_append_earlier_newresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_append_earlier_newresiduecongruence pfa_offset_right_tri_append_earlier_newresiduecongruence. (pfc_natural_sum_tri_append_earlier_new) + (p) * pfa_offset_left_tri_append_earlier_newresiduecongruence = (r) + (p) * pfa_offset_right_tri_append_earlier_newresiduecongruence)))))))))