Appending a quotient coefficient changes its new convolution position by exactly its actual field product with the divisor head; all sum and residue witnesses are real.
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 AB AC bb bc d N a b c t r. (forall mdr_i_pfp_tri_append_prefix mdr_a_pfp_tri_append_prefix. (exists mdr_gap_pfp_tri_append_prefixb. mdr_gap_pfp_tri_append_prefixb + S (mdr_i_pfp_tri_append_prefix) = (N)) -> (((exists ff_h_mdr_pfp_tri_append_prefixo. ff_h_mdr_pfp_tri_append_prefixo + S (mdr_a_pfp_tri_append_prefix) = S ((S (mdr_i_pfp_tri_append_prefix)) * ac)) /\ exists ff_q_mdr_pfp_tri_append_prefixo. ab = ff_q_mdr_pfp_tri_append_prefixo * S ((S (mdr_i_pfp_tri_append_prefix)) * ac) + (mdr_a_pfp_tri_append_prefix))) -> (((exists ff_h_mdr_pfp_tri_append_prefixn. ff_h_mdr_pfp_tri_append_prefixn + S (mdr_a_pfp_tri_append_prefix) = S ((S (mdr_i_pfp_tri_append_prefix)) * AC)) /\ exists ff_q_mdr_pfp_tri_append_prefixn. AB = ff_q_mdr_pfp_tri_append_prefixn * S ((S (mdr_i_pfp_tri_append_prefix)) * AC) + (mdr_a_pfp_tri_append_prefix)))) -> (((exists ff_h_pfp_tri_append_actual_entry. ff_h_pfp_tri_append_actual_entry + S (a) = S ((S (N)) * AC)) /\ exists ff_q_pfp_tri_append_actual_entry. AB = ff_q_pfp_tri_append_actual_entry * S ((S (N)) * AC) + (a))) -> (((exists ff_h_pfp_tri_append_actual_head. ff_h_pfp_tri_append_actual_head + S (b) = S ((S (0)) * bc)) /\ exists ff_q_pfp_tri_append_actual_head. bb = ff_q_pfp_tri_append_actual_head * S ((S (0)) * bc) + (b))) -> (exists pfc_terms_code_tri_append_previous_coefficient pfc_terms_scale_tri_append_previous_coefficient pfc_natural_sum_tri_append_previous_coefficient. ((forall pfc_index_tri_append_previous_coefficientdiagonal. (exists pfa_gap_tri_append_previous_coefficientdiagonalbound. pfa_gap_tri_append_previous_coefficientdiagonalbound + S (pfc_index_tri_append_previous_coefficientdiagonal) = (S (N))) -> exists pfc_value_tri_append_previous_coefficientdiagonal. ((((exists ff_h_pfp_tri_append_previous_coefficientdiagonalentry. ff_h_pfp_tri_append_previous_coefficientdiagonalentry + S (pfc_value_tri_append_previous_coefficientdiagonal) = S ((S (pfc_index_tri_append_previous_coefficientdiagonal)) * pfc_terms_scale_tri_append_previous_coefficient)) /\ exists ff_q_pfp_tri_append_previous_coefficientdiagonalentry. pfc_terms_code_tri_append_previous_coefficient = ff_q_pfp_tri_append_previous_coefficientdiagonalentry * S ((S (pfc_index_tri_append_previous_coefficientdiagonal)) * pfc_terms_scale_tri_append_previous_coefficient) + (pfc_value_tri_append_previous_coefficientdiagonal))) /\ ((exists pfc_complement_tri_append_previous_coefficientdiagonalterm pfc_left_tri_append_previous_coefficientdiagonalterm pfc_right_tri_append_previous_coefficientdiagonalterm. (((pfc_index_tri_append_previous_coefficientdiagonal)+pfc_complement_tri_append_previous_coefficientdiagonalterm=(N)) /\ ((((((exists pfa_gap_tri_append_previous_coefficientdiagonaltermleftinside. pfa_gap_tri_append_previous_coefficientdiagonaltermleftinside + S (pfc_index_tri_append_previous_coefficientdiagonal) = (N)) /\ ((((exists ff_h_pfp_tri_append_previous_coefficientdiagonaltermleftentry. ff_h_pfp_tri_append_previous_coefficientdiagonaltermleftentry + S (pfc_left_tri_append_previous_coefficientdiagonalterm) = S ((S (pfc_index_tri_append_previous_coefficientdiagonal)) * ac)) /\ exists ff_q_pfp_tri_append_previous_coefficientdiagonaltermleftentry. ab = ff_q_pfp_tri_append_previous_coefficientdiagonaltermleftentry * S ((S (pfc_index_tri_append_previous_coefficientdiagonal)) * ac) + (pfc_left_tri_append_previous_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_previous_coefficientdiagonaltermleftoutside. pfc_gap_tri_append_previous_coefficientdiagonaltermleftoutside+(N)=(pfc_index_tri_append_previous_coefficientdiagonal)) /\ (((pfc_left_tri_append_previous_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_append_previous_coefficientdiagonaltermrightinside. pfa_gap_tri_append_previous_coefficientdiagonaltermrightinside + S (pfc_complement_tri_append_previous_coefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_tri_append_previous_coefficientdiagonaltermrightentry. ff_h_pfp_tri_append_previous_coefficientdiagonaltermrightentry + S (pfc_right_tri_append_previous_coefficientdiagonalterm) = S ((S (pfc_complement_tri_append_previous_coefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_append_previous_coefficientdiagonaltermrightentry. bb = ff_q_pfp_tri_append_previous_coefficientdiagonaltermrightentry * S ((S (pfc_complement_tri_append_previous_coefficientdiagonalterm)) * bc) + (pfc_right_tri_append_previous_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_previous_coefficientdiagonaltermrightoutside. pfc_gap_tri_append_previous_coefficientdiagonaltermrightoutside+(S d)=(pfc_complement_tri_append_previous_coefficientdiagonalterm)) /\ (((pfc_right_tri_append_previous_coefficientdiagonalterm)=0))))) /\ (((pfc_value_tri_append_previous_coefficientdiagonal)=pfc_left_tri_append_previous_coefficientdiagonalterm*pfc_right_tri_append_previous_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_append_previous_coefficientsum fs_v_pfc_tri_append_previous_coefficientsum. ((((exists fs_h_pfc_tri_append_previous_coefficientsum_body_start. fs_h_pfc_tri_append_previous_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_append_previous_coefficientsum)) /\ exists fs_q_pfc_tri_append_previous_coefficientsum_body_start. fs_u_pfc_tri_append_previous_coefficientsum = fs_q_pfc_tri_append_previous_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_tri_append_previous_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_tri_append_previous_coefficientsum_body_terminal. fs_h_pfc_tri_append_previous_coefficientsum_body_terminal + S (pfc_natural_sum_tri_append_previous_coefficient) = S ((S (S (N))) * fs_v_pfc_tri_append_previous_coefficientsum)) /\ exists fs_q_pfc_tri_append_previous_coefficientsum_body_terminal. fs_u_pfc_tri_append_previous_coefficientsum = fs_q_pfc_tri_append_previous_coefficientsum_body_terminal * S ((S (S (N))) * fs_v_pfc_tri_append_previous_coefficientsum) + (pfc_natural_sum_tri_append_previous_coefficient))) /\ forall fs_i_pfc_tri_append_previous_coefficientsum_body_steps. (exists fs_lt_pfc_tri_append_previous_coefficientsum_body_steps_bound. fs_lt_pfc_tri_append_previous_coefficientsum_body_steps_bound + S fs_i_pfc_tri_append_previous_coefficientsum_body_steps = S (N)) -> exists fs_a_pfc_tri_append_previous_coefficientsum_body_steps fs_r_pfc_tri_append_previous_coefficientsum_body_steps fs_s_pfc_tri_append_previous_coefficientsum_body_steps. ((((exists fs_h_pfc_tri_append_previous_coefficientsum_body_steps_summand. fs_h_pfc_tri_append_previous_coefficientsum_body_steps_summand + S (fs_a_pfc_tri_append_previous_coefficientsum_body_steps) = S ((S (fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * pfc_terms_scale_tri_append_previous_coefficient)) /\ exists fs_q_pfc_tri_append_previous_coefficientsum_body_steps_summand. pfc_terms_code_tri_append_previous_coefficient = fs_q_pfc_tri_append_previous_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * pfc_terms_scale_tri_append_previous_coefficient) + (fs_a_pfc_tri_append_previous_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_previous_coefficientsum_body_steps_partial. fs_h_pfc_tri_append_previous_coefficientsum_body_steps_partial + S (fs_r_pfc_tri_append_previous_coefficientsum_body_steps) = S ((S (fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * fs_v_pfc_tri_append_previous_coefficientsum)) /\ exists fs_q_pfc_tri_append_previous_coefficientsum_body_steps_partial. fs_u_pfc_tri_append_previous_coefficientsum = fs_q_pfc_tri_append_previous_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * fs_v_pfc_tri_append_previous_coefficientsum) + (fs_r_pfc_tri_append_previous_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_previous_coefficientsum_body_steps_successor. fs_h_pfc_tri_append_previous_coefficientsum_body_steps_successor + S (fs_s_pfc_tri_append_previous_coefficientsum_body_steps) = S ((S (S fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * fs_v_pfc_tri_append_previous_coefficientsum)) /\ exists fs_q_pfc_tri_append_previous_coefficientsum_body_steps_successor. fs_u_pfc_tri_append_previous_coefficientsum = fs_q_pfc_tri_append_previous_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_tri_append_previous_coefficientsum_body_steps)) * fs_v_pfc_tri_append_previous_coefficientsum) + (fs_s_pfc_tri_append_previous_coefficientsum_body_steps))) /\ fs_s_pfc_tri_append_previous_coefficientsum_body_steps = fs_r_pfc_tri_append_previous_coefficientsum_body_steps + fs_a_pfc_tri_append_previous_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_tri_append_previous_coefficientresiduebound. pfa_gap_tri_append_previous_coefficientresiduebound + S (c) = (p)) /\ ((exists pfa_offset_left_tri_append_previous_coefficientresiduecongruence pfa_offset_right_tri_append_previous_coefficientresiduecongruence. (pfc_natural_sum_tri_append_previous_coefficient) + (p) * pfa_offset_left_tri_append_previous_coefficientresiduecongruence = (c) + (p) * pfa_offset_right_tri_append_previous_coefficientresiduecongruence))))))))) -> (exists pfc_terms_code_tri_append_actual_coefficient pfc_terms_scale_tri_append_actual_coefficient pfc_natural_sum_tri_append_actual_coefficient. ((forall pfc_index_tri_append_actual_coefficientdiagonal. (exists pfa_gap_tri_append_actual_coefficientdiagonalbound. pfa_gap_tri_append_actual_coefficientdiagonalbound + S (pfc_index_tri_append_actual_coefficientdiagonal) = (S (N))) -> exists pfc_value_tri_append_actual_coefficientdiagonal. ((((exists ff_h_pfp_tri_append_actual_coefficientdiagonalentry. ff_h_pfp_tri_append_actual_coefficientdiagonalentry + S (pfc_value_tri_append_actual_coefficientdiagonal) = S ((S (pfc_index_tri_append_actual_coefficientdiagonal)) * pfc_terms_scale_tri_append_actual_coefficient)) /\ exists ff_q_pfp_tri_append_actual_coefficientdiagonalentry. pfc_terms_code_tri_append_actual_coefficient = ff_q_pfp_tri_append_actual_coefficientdiagonalentry * S ((S (pfc_index_tri_append_actual_coefficientdiagonal)) * pfc_terms_scale_tri_append_actual_coefficient) + (pfc_value_tri_append_actual_coefficientdiagonal))) /\ ((exists pfc_complement_tri_append_actual_coefficientdiagonalterm pfc_left_tri_append_actual_coefficientdiagonalterm pfc_right_tri_append_actual_coefficientdiagonalterm. (((pfc_index_tri_append_actual_coefficientdiagonal)+pfc_complement_tri_append_actual_coefficientdiagonalterm=(N)) /\ ((((((exists pfa_gap_tri_append_actual_coefficientdiagonaltermleftinside. pfa_gap_tri_append_actual_coefficientdiagonaltermleftinside + S (pfc_index_tri_append_actual_coefficientdiagonal) = (S N)) /\ ((((exists ff_h_pfp_tri_append_actual_coefficientdiagonaltermleftentry. ff_h_pfp_tri_append_actual_coefficientdiagonaltermleftentry + S (pfc_left_tri_append_actual_coefficientdiagonalterm) = S ((S (pfc_index_tri_append_actual_coefficientdiagonal)) * AC)) /\ exists ff_q_pfp_tri_append_actual_coefficientdiagonaltermleftentry. AB = ff_q_pfp_tri_append_actual_coefficientdiagonaltermleftentry * S ((S (pfc_index_tri_append_actual_coefficientdiagonal)) * AC) + (pfc_left_tri_append_actual_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_actual_coefficientdiagonaltermleftoutside. pfc_gap_tri_append_actual_coefficientdiagonaltermleftoutside+(S N)=(pfc_index_tri_append_actual_coefficientdiagonal)) /\ (((pfc_left_tri_append_actual_coefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_append_actual_coefficientdiagonaltermrightinside. pfa_gap_tri_append_actual_coefficientdiagonaltermrightinside + S (pfc_complement_tri_append_actual_coefficientdiagonalterm) = (S d)) /\ ((((exists ff_h_pfp_tri_append_actual_coefficientdiagonaltermrightentry. ff_h_pfp_tri_append_actual_coefficientdiagonaltermrightentry + S (pfc_right_tri_append_actual_coefficientdiagonalterm) = S ((S (pfc_complement_tri_append_actual_coefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_append_actual_coefficientdiagonaltermrightentry. bb = ff_q_pfp_tri_append_actual_coefficientdiagonaltermrightentry * S ((S (pfc_complement_tri_append_actual_coefficientdiagonalterm)) * bc) + (pfc_right_tri_append_actual_coefficientdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_actual_coefficientdiagonaltermrightoutside. pfc_gap_tri_append_actual_coefficientdiagonaltermrightoutside+(S d)=(pfc_complement_tri_append_actual_coefficientdiagonalterm)) /\ (((pfc_right_tri_append_actual_coefficientdiagonalterm)=0))))) /\ (((pfc_value_tri_append_actual_coefficientdiagonal)=pfc_left_tri_append_actual_coefficientdiagonalterm*pfc_right_tri_append_actual_coefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_append_actual_coefficientsum fs_v_pfc_tri_append_actual_coefficientsum. ((((exists fs_h_pfc_tri_append_actual_coefficientsum_body_start. fs_h_pfc_tri_append_actual_coefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_append_actual_coefficientsum)) /\ exists fs_q_pfc_tri_append_actual_coefficientsum_body_start. fs_u_pfc_tri_append_actual_coefficientsum = fs_q_pfc_tri_append_actual_coefficientsum_body_start * S ((S (0)) * fs_v_pfc_tri_append_actual_coefficientsum) + (0))) /\ ((((exists fs_h_pfc_tri_append_actual_coefficientsum_body_terminal. fs_h_pfc_tri_append_actual_coefficientsum_body_terminal + S (pfc_natural_sum_tri_append_actual_coefficient) = S ((S (S (N))) * fs_v_pfc_tri_append_actual_coefficientsum)) /\ exists fs_q_pfc_tri_append_actual_coefficientsum_body_terminal. fs_u_pfc_tri_append_actual_coefficientsum = fs_q_pfc_tri_append_actual_coefficientsum_body_terminal * S ((S (S (N))) * fs_v_pfc_tri_append_actual_coefficientsum) + (pfc_natural_sum_tri_append_actual_coefficient))) /\ forall fs_i_pfc_tri_append_actual_coefficientsum_body_steps. (exists fs_lt_pfc_tri_append_actual_coefficientsum_body_steps_bound. fs_lt_pfc_tri_append_actual_coefficientsum_body_steps_bound + S fs_i_pfc_tri_append_actual_coefficientsum_body_steps = S (N)) -> exists fs_a_pfc_tri_append_actual_coefficientsum_body_steps fs_r_pfc_tri_append_actual_coefficientsum_body_steps fs_s_pfc_tri_append_actual_coefficientsum_body_steps. ((((exists fs_h_pfc_tri_append_actual_coefficientsum_body_steps_summand. fs_h_pfc_tri_append_actual_coefficientsum_body_steps_summand + S (fs_a_pfc_tri_append_actual_coefficientsum_body_steps) = S ((S (fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * pfc_terms_scale_tri_append_actual_coefficient)) /\ exists fs_q_pfc_tri_append_actual_coefficientsum_body_steps_summand. pfc_terms_code_tri_append_actual_coefficient = fs_q_pfc_tri_append_actual_coefficientsum_body_steps_summand * S ((S (fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * pfc_terms_scale_tri_append_actual_coefficient) + (fs_a_pfc_tri_append_actual_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_actual_coefficientsum_body_steps_partial. fs_h_pfc_tri_append_actual_coefficientsum_body_steps_partial + S (fs_r_pfc_tri_append_actual_coefficientsum_body_steps) = S ((S (fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * fs_v_pfc_tri_append_actual_coefficientsum)) /\ exists fs_q_pfc_tri_append_actual_coefficientsum_body_steps_partial. fs_u_pfc_tri_append_actual_coefficientsum = fs_q_pfc_tri_append_actual_coefficientsum_body_steps_partial * S ((S (fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * fs_v_pfc_tri_append_actual_coefficientsum) + (fs_r_pfc_tri_append_actual_coefficientsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_actual_coefficientsum_body_steps_successor. fs_h_pfc_tri_append_actual_coefficientsum_body_steps_successor + S (fs_s_pfc_tri_append_actual_coefficientsum_body_steps) = S ((S (S fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * fs_v_pfc_tri_append_actual_coefficientsum)) /\ exists fs_q_pfc_tri_append_actual_coefficientsum_body_steps_successor. fs_u_pfc_tri_append_actual_coefficientsum = fs_q_pfc_tri_append_actual_coefficientsum_body_steps_successor * S ((S (S fs_i_pfc_tri_append_actual_coefficientsum_body_steps)) * fs_v_pfc_tri_append_actual_coefficientsum) + (fs_s_pfc_tri_append_actual_coefficientsum_body_steps))) /\ fs_s_pfc_tri_append_actual_coefficientsum_body_steps = fs_r_pfc_tri_append_actual_coefficientsum_body_steps + fs_a_pfc_tri_append_actual_coefficientsum_body_steps)))))) /\ ((((exists pfa_gap_tri_append_actual_coefficientresiduebound. pfa_gap_tri_append_actual_coefficientresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_append_actual_coefficientresiduecongruence pfa_offset_right_tri_append_actual_coefficientresiduecongruence. (pfc_natural_sum_tri_append_actual_coefficient) + (p) * pfa_offset_left_tri_append_actual_coefficientresiduecongruence = (r) + (p) * pfa_offset_right_tri_append_actual_coefficientresiduecongruence))))))))) -> (((exists pfa_gap_tri_append_actual_productleft. pfa_gap_tri_append_actual_productleft + S (a) = (p)) /\ (((exists pfa_gap_tri_append_actual_productright. pfa_gap_tri_append_actual_productright + S (b) = (p)) /\ ((((exists pfa_gap_tri_append_actual_productresultbound. pfa_gap_tri_append_actual_productresultbound + S (t) = (p)) /\ ((exists pfa_offset_left_tri_append_actual_productresultcongruence pfa_offset_right_tri_append_actual_productresultcongruence. ((a) * (b)) + (p) * pfa_offset_left_tri_append_actual_productresultcongruence = (t) + (p) * pfa_offset_right_tri_append_actual_productresultcongruence))))))))) -> (((exists pfa_gap_tri_append_resultleft. pfa_gap_tri_append_resultleft + S (c) = (p)) /\ (((exists pfa_gap_tri_append_resultright. pfa_gap_tri_append_resultright + S (t) = (p)) /\ ((((exists pfa_gap_tri_append_resultresultbound. pfa_gap_tri_append_resultresultbound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_append_resultresultcongruence pfa_offset_right_tri_append_resultresultcongruence. ((c) + (t)) + (p) * pfa_offset_left_tri_append_resultresultcongruence = (r) + (p) * pfa_offset_right_tri_append_resultresultcongruence)))))))))
Complete tactic proof in conservative notation
All 85 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.