Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall b c L d e M. (forall pfrep_power_equivalent_symmetric_old pfrep_left_equivalent_symmetric_old pfrep_right_equivalent_symmetric_old. ((exists pfrep_position_equivalent_symmetric_oldfirst. ((pfrep_position_equivalent_symmetric_oldfirst+S (pfrep_power_equivalent_symmetric_old)=(L)) /\ ((((exists ff_h_pfp_equivalent_symmetric_oldfirstentry. ff_h_pfp_equivalent_symmetric_oldfirstentry + S (pfrep_left_equivalent_symmetric_old) = S ((S (pfrep_position_equivalent_symmetric_oldfirst)) * c)) /\ exists ff_q_pfp_equivalent_symmetric_oldfirstentry. b = ff_q_pfp_equivalent_symmetric_oldfirstentry * S ((S (pfrep_position_equivalent_symmetric_oldfirst)) * c) + (pfrep_left_equivalent_symmetric_old)))))) \/ (((exists pfrep_gap_equivalent_symmetric_oldfirstoutside. pfrep_gap_equivalent_symmetric_oldfirstoutside+(L)=(pfrep_power_equivalent_symmetric_old)) /\ (((pfrep_left_equivalent_symmetric_old)=0))))) -> ((exists pfrep_position_equivalent_symmetric_oldsecond. ((pfrep_position_equivalent_symmetric_oldsecond+S (pfrep_power_equivalent_symmetric_old)=(M)) /\ ((((exists ff_h_pfp_equivalent_symmetric_oldsecondentry. ff_h_pfp_equivalent_symmetric_oldsecondentry + S (pfrep_right_equivalent_symmetric_old) = S ((S (pfrep_position_equivalent_symmetric_oldsecond)) * e)) /\ exists ff_q_pfp_equivalent_symmetric_oldsecondentry. d = ff_q_pfp_equivalent_symmetric_oldsecondentry * S ((S (pfrep_position_equivalent_symmetric_oldsecond)) * e) + (pfrep_right_equivalent_symmetric_old)))))) \/ (((exists pfrep_gap_equivalent_symmetric_oldsecondoutside. pfrep_gap_equivalent_symmetric_oldsecondoutside+(M)=(pfrep_power_equivalent_symmetric_old)) /\ (((pfrep_right_equivalent_symmetric_old)=0))))) -> pfrep_left_equivalent_symmetric_old=pfrep_right_equivalent_symmetric_old) -> (forall pfrep_power_equivalent_symmetric_new pfrep_left_equivalent_symmetric_new pfrep_right_equivalent_symmetric_new. ((exists pfrep_position_equivalent_symmetric_newfirst. ((pfrep_position_equivalent_symmetric_newfirst+S (pfrep_power_equivalent_symmetric_new)=(M)) /\ ((((exists ff_h_pfp_equivalent_symmetric_newfirstentry. ff_h_pfp_equivalent_symmetric_newfirstentry + S (pfrep_left_equivalent_symmetric_new) = S ((S (pfrep_position_equivalent_symmetric_newfirst)) * e)) /\ exists ff_q_pfp_equivalent_symmetric_newfirstentry. d = ff_q_pfp_equivalent_symmetric_newfirstentry * S ((S (pfrep_position_equivalent_symmetric_newfirst)) * e) + (pfrep_left_equivalent_symmetric_new)))))) \/ (((exists pfrep_gap_equivalent_symmetric_newfirstoutside. pfrep_gap_equivalent_symmetric_newfirstoutside+(M)=(pfrep_power_equivalent_symmetric_new)) /\ (((pfrep_left_equivalent_symmetric_new)=0))))) -> ((exists pfrep_position_equivalent_symmetric_newsecond. ((pfrep_position_equivalent_symmetric_newsecond+S (pfrep_power_equivalent_symmetric_new)=(L)) /\ ((((exists ff_h_pfp_equivalent_symmetric_newsecondentry. ff_h_pfp_equivalent_symmetric_newsecondentry + S (pfrep_right_equivalent_symmetric_new) = S ((S (pfrep_position_equivalent_symmetric_newsecond)) * c)) /\ exists ff_q_pfp_equivalent_symmetric_newsecondentry. b = ff_q_pfp_equivalent_symmetric_newsecondentry * S ((S (pfrep_position_equivalent_symmetric_newsecond)) * c) + (pfrep_right_equivalent_symmetric_new)))))) \/ (((exists pfrep_gap_equivalent_symmetric_newsecondoutside. pfrep_gap_equivalent_symmetric_newsecondoutside+(L)=(pfrep_power_equivalent_symmetric_new)) /\ (((pfrep_right_equivalent_symmetric_new)=0))))) -> pfrep_left_equivalent_symmetric_new=pfrep_right_equivalent_symmetric_new)Constructive proof overview
Generated structural guide
Formal coefficient equivalence is symmetric without choosing canonical raw beta codes.
The unchanged tactic script uses 0 declared prerequisites and contains 21 exact native proof lines.
Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
none
Direct dependents
PX001C prime_field_polynomial_trim_equivalent PX006E prime_field_polynomial_convolution_left_padding_equivalent_left PX006F prime_field_polynomial_convolution_left_padding_equivalent_right PX0072 prime_field_polynomial_equivalent_implies_left_pad PX0075 prime_field_polynomial_add_equivalent_congruent PX0076 prime_field_polynomial_subtract_equivalent_congruent PX0077 prime_field_polynomial_convolution_equivalent_congruent_left PX0078 prime_field_polynomial_convolution_equivalent_congruent_rightFormal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
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.