Independent beta recodings of every input and output preserve the actual aligned coefficient operation.
Alpha v34 checked-use · first admitted v32 · 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.
All coefficients retain the established highest-degree-first order. Trimming handles empty and all-zero prefixes; monic normalization requires a nonzero leading coefficient. Synthetic division has a nonempty input of length S n and a quotient of length n, unique in decoded values. Its coefficient recurrence, actual evaluation remainder and positive-degree drop are checked. General polynomial Euclidean division, gcd/Bezout, an arbitrary-convolution factor theorem, irreducible-polynomial existence and the full G091 prime-power-field endpoint remain open. These exact theorems are first admitted to Alpha v32; Stable remains unchanged.
forall p ab ac bb bc rb rc AB AC BB BC RB RC l. (forall mdr_i_pfp_subtract_transport_ab mdr_a_pfp_subtract_transport_ab. (exists mdr_gap_pfp_subtract_transport_abb. mdr_gap_pfp_subtract_transport_abb + S (mdr_i_pfp_subtract_transport_ab) = (l)) -> (((exists ff_h_mdr_pfp_subtract_transport_abo. ff_h_mdr_pfp_subtract_transport_abo + S (mdr_a_pfp_subtract_transport_ab) = S ((S (mdr_i_pfp_subtract_transport_ab)) * ac)) /\ exists ff_q_mdr_pfp_subtract_transport_abo. ab = ff_q_mdr_pfp_subtract_transport_abo * S ((S (mdr_i_pfp_subtract_transport_ab)) * ac) + (mdr_a_pfp_subtract_transport_ab))) -> (((exists ff_h_mdr_pfp_subtract_transport_abn. ff_h_mdr_pfp_subtract_transport_abn + S (mdr_a_pfp_subtract_transport_ab) = S ((S (mdr_i_pfp_subtract_transport_ab)) * AC)) /\ exists ff_q_mdr_pfp_subtract_transport_abn. AB = ff_q_mdr_pfp_subtract_transport_abn * S ((S (mdr_i_pfp_subtract_transport_ab)) * AC) + (mdr_a_pfp_subtract_transport_ab)))) -> (forall mdr_i_pfp_subtract_transport_bb mdr_a_pfp_subtract_transport_bb. (exists mdr_gap_pfp_subtract_transport_bbb. mdr_gap_pfp_subtract_transport_bbb + S (mdr_i_pfp_subtract_transport_bb) = (l)) -> (((exists ff_h_mdr_pfp_subtract_transport_bbo. ff_h_mdr_pfp_subtract_transport_bbo + S (mdr_a_pfp_subtract_transport_bb) = S ((S (mdr_i_pfp_subtract_transport_bb)) * bc)) /\ exists ff_q_mdr_pfp_subtract_transport_bbo. bb = ff_q_mdr_pfp_subtract_transport_bbo * S ((S (mdr_i_pfp_subtract_transport_bb)) * bc) + (mdr_a_pfp_subtract_transport_bb))) -> (((exists ff_h_mdr_pfp_subtract_transport_bbn. ff_h_mdr_pfp_subtract_transport_bbn + S (mdr_a_pfp_subtract_transport_bb) = S ((S (mdr_i_pfp_subtract_transport_bb)) * BC)) /\ exists ff_q_mdr_pfp_subtract_transport_bbn. BB = ff_q_mdr_pfp_subtract_transport_bbn * S ((S (mdr_i_pfp_subtract_transport_bb)) * BC) + (mdr_a_pfp_subtract_transport_bb)))) -> (forall mdr_i_pfp_subtract_transport_rb mdr_a_pfp_subtract_transport_rb. (exists mdr_gap_pfp_subtract_transport_rbb. mdr_gap_pfp_subtract_transport_rbb + S (mdr_i_pfp_subtract_transport_rb) = (l)) -> (((exists ff_h_mdr_pfp_subtract_transport_rbo. ff_h_mdr_pfp_subtract_transport_rbo + S (mdr_a_pfp_subtract_transport_rb) = S ((S (mdr_i_pfp_subtract_transport_rb)) * rc)) /\ exists ff_q_mdr_pfp_subtract_transport_rbo. rb = ff_q_mdr_pfp_subtract_transport_rbo * S ((S (mdr_i_pfp_subtract_transport_rb)) * rc) + (mdr_a_pfp_subtract_transport_rb))) -> (((exists ff_h_mdr_pfp_subtract_transport_rbn. ff_h_mdr_pfp_subtract_transport_rbn + S (mdr_a_pfp_subtract_transport_rb) = S ((S (mdr_i_pfp_subtract_transport_rb)) * RC)) /\ exists ff_q_mdr_pfp_subtract_transport_rbn. RB = ff_q_mdr_pfp_subtract_transport_rbn * S ((S (mdr_i_pfp_subtract_transport_rb)) * RC) + (mdr_a_pfp_subtract_transport_rb)))) -> (forall pfs_index_subtract_transport_old. (exists pfa_gap_subtract_transport_oldindex. pfa_gap_subtract_transport_oldindex + S (pfs_index_subtract_transport_old) = (l)) -> exists pfs_left_subtract_transport_old pfs_right_subtract_transport_old pfs_result_subtract_transport_old. ((((exists ff_h_pfp_subtract_transport_oldleft. ff_h_pfp_subtract_transport_oldleft + S (pfs_left_subtract_transport_old) = S ((S (pfs_index_subtract_transport_old)) * ac)) /\ exists ff_q_pfp_subtract_transport_oldleft. ab = ff_q_pfp_subtract_transport_oldleft * S ((S (pfs_index_subtract_transport_old)) * ac) + (pfs_left_subtract_transport_old))) /\ (((((exists ff_h_pfp_subtract_transport_oldright. ff_h_pfp_subtract_transport_oldright + S (pfs_right_subtract_transport_old) = S ((S (pfs_index_subtract_transport_old)) * bc)) /\ exists ff_q_pfp_subtract_transport_oldright. bb = ff_q_pfp_subtract_transport_oldright * S ((S (pfs_index_subtract_transport_old)) * bc) + (pfs_right_subtract_transport_old))) /\ (((((exists ff_h_pfp_subtract_transport_oldresult. ff_h_pfp_subtract_transport_oldresult + S (pfs_result_subtract_transport_old) = S ((S (pfs_index_subtract_transport_old)) * rc)) /\ exists ff_q_pfp_subtract_transport_oldresult. rb = ff_q_pfp_subtract_transport_oldresult * S ((S (pfs_index_subtract_transport_old)) * rc) + (pfs_result_subtract_transport_old))) /\ ((((exists pfa_gap_subtract_transport_oldoperationleft. pfa_gap_subtract_transport_oldoperationleft + S (pfs_right_subtract_transport_old) = (p)) /\ (((exists pfa_gap_subtract_transport_oldoperationright. pfa_gap_subtract_transport_oldoperationright + S (pfs_result_subtract_transport_old) = (p)) /\ ((((exists pfa_gap_subtract_transport_oldoperationresultbound. pfa_gap_subtract_transport_oldoperationresultbound + S (pfs_left_subtract_transport_old) = (p)) /\ ((exists pfa_offset_left_subtract_transport_oldoperationresultcongruence pfa_offset_right_subtract_transport_oldoperationresultcongruence. ((pfs_right_subtract_transport_old) + (pfs_result_subtract_transport_old)) + (p) * pfa_offset_left_subtract_transport_oldoperationresultcongruence = (pfs_left_subtract_transport_old) + (p) * pfa_offset_right_subtract_transport_oldoperationresultcongruence)))))))))))))))) -> (forall pfs_index_subtract_transport_new. (exists pfa_gap_subtract_transport_newindex. pfa_gap_subtract_transport_newindex + S (pfs_index_subtract_transport_new) = (l)) -> exists pfs_left_subtract_transport_new pfs_right_subtract_transport_new pfs_result_subtract_transport_new. ((((exists ff_h_pfp_subtract_transport_newleft. ff_h_pfp_subtract_transport_newleft + S (pfs_left_subtract_transport_new) = S ((S (pfs_index_subtract_transport_new)) * AC)) /\ exists ff_q_pfp_subtract_transport_newleft. AB = ff_q_pfp_subtract_transport_newleft * S ((S (pfs_index_subtract_transport_new)) * AC) + (pfs_left_subtract_transport_new))) /\ (((((exists ff_h_pfp_subtract_transport_newright. ff_h_pfp_subtract_transport_newright + S (pfs_right_subtract_transport_new) = S ((S (pfs_index_subtract_transport_new)) * BC)) /\ exists ff_q_pfp_subtract_transport_newright. BB = ff_q_pfp_subtract_transport_newright * S ((S (pfs_index_subtract_transport_new)) * BC) + (pfs_right_subtract_transport_new))) /\ (((((exists ff_h_pfp_subtract_transport_newresult. ff_h_pfp_subtract_transport_newresult + S (pfs_result_subtract_transport_new) = S ((S (pfs_index_subtract_transport_new)) * RC)) /\ exists ff_q_pfp_subtract_transport_newresult. RB = ff_q_pfp_subtract_transport_newresult * S ((S (pfs_index_subtract_transport_new)) * RC) + (pfs_result_subtract_transport_new))) /\ ((((exists pfa_gap_subtract_transport_newoperationleft. pfa_gap_subtract_transport_newoperationleft + S (pfs_right_subtract_transport_new) = (p)) /\ (((exists pfa_gap_subtract_transport_newoperationright. pfa_gap_subtract_transport_newoperationright + S (pfs_result_subtract_transport_new) = (p)) /\ ((((exists pfa_gap_subtract_transport_newoperationresultbound. pfa_gap_subtract_transport_newoperationresultbound + S (pfs_left_subtract_transport_new) = (p)) /\ ((exists pfa_offset_left_subtract_transport_newoperationresultcongruence pfa_offset_right_subtract_transport_newoperationresultcongruence. ((pfs_right_subtract_transport_new) + (pfs_result_subtract_transport_new)) + (p) * pfa_offset_left_subtract_transport_newoperationresultcongruence = (pfs_left_subtract_transport_new) + (p) * pfa_offset_right_subtract_transport_newoperationresultcongruence))))))))))))))))
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.
01Fix variables and assumptionsL1–10
Work with arbitrary variables or the premises of the current implication.