Three genuine convolution coefficients satisfy actual canonical field addition under left distributivity, proved from their independently witnessed natural sums and residues.
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 bb bc cb cc L db dc M i u v w. (forall pfp_index_coefficient_add_left_source. (exists pfa_gap_coefficient_add_left_sourceindex. pfa_gap_coefficient_add_left_sourceindex + S (pfp_index_coefficient_add_left_source) = (L)) -> exists pfp_left_coefficient_add_left_source pfp_right_coefficient_add_left_source pfp_value_coefficient_add_left_source. ((((exists ff_h_pfp_coefficient_add_left_sourceleft. ff_h_pfp_coefficient_add_left_sourceleft + S (pfp_left_coefficient_add_left_source) = S ((S (pfp_index_coefficient_add_left_source)) * ac)) /\ exists ff_q_pfp_coefficient_add_left_sourceleft. ab = ff_q_pfp_coefficient_add_left_sourceleft * S ((S (pfp_index_coefficient_add_left_source)) * ac) + (pfp_left_coefficient_add_left_source))) /\ (((((exists ff_h_pfp_coefficient_add_left_sourceright. ff_h_pfp_coefficient_add_left_sourceright + S (pfp_right_coefficient_add_left_source) = S ((S (pfp_index_coefficient_add_left_source)) * bc)) /\ exists ff_q_pfp_coefficient_add_left_sourceright. bb = ff_q_pfp_coefficient_add_left_sourceright * S ((S (pfp_index_coefficient_add_left_source)) * bc) + (pfp_right_coefficient_add_left_source))) /\ (((((exists ff_h_pfp_coefficient_add_left_sourcetarget. ff_h_pfp_coefficient_add_left_sourcetarget + S (pfp_value_coefficient_add_left_source) = S ((S (pfp_index_coefficient_add_left_source)) * cc)) /\ exists ff_q_pfp_coefficient_add_left_sourcetarget. cb = ff_q_pfp_coefficient_add_left_sourcetarget * S ((S (pfp_index_coefficient_add_left_source)) * cc) + (pfp_value_coefficient_add_left_source))) /\ ((((exists pfa_gap_coefficient_add_left_sourceoperationleft. pfa_gap_coefficient_add_left_sourceoperationleft + S (pfp_left_coefficient_add_left_source) = (p)) /\ (((exists pfa_gap_coefficient_add_left_sourceoperationright. pfa_gap_coefficient_add_left_sourceoperationright + S (pfp_right_coefficient_add_left_source) = (p)) /\ ((((exists pfa_gap_coefficient_add_left_sourceoperationresultbound. pfa_gap_coefficient_add_left_sourceoperationresultbound + S (pfp_value_coefficient_add_left_source) = (p)) /\ ((exists pfa_offset_left_coefficient_add_left_sourceoperationresultcongruence pfa_offset_right_coefficient_add_left_sourceoperationresultcongruence. ((pfp_left_coefficient_add_left_source) + (pfp_right_coefficient_add_left_source)) + (p) * pfa_offset_left_coefficient_add_left_sourceoperationresultcongruence = (pfp_value_coefficient_add_left_source) + (p) * pfa_offset_right_coefficient_add_left_sourceoperationresultcongruence)))))))))))))))) -> (exists pfc_terms_code_coefficient_add_left_u pfc_terms_scale_coefficient_add_left_u pfc_natural_sum_coefficient_add_left_u. ((forall pfc_index_coefficient_add_left_udiagonal. (exists pfa_gap_coefficient_add_left_udiagonalbound. pfa_gap_coefficient_add_left_udiagonalbound + S (pfc_index_coefficient_add_left_udiagonal) = (S (i))) -> exists pfc_value_coefficient_add_left_udiagonal. ((((exists ff_h_pfp_coefficient_add_left_udiagonalentry. ff_h_pfp_coefficient_add_left_udiagonalentry + S (pfc_value_coefficient_add_left_udiagonal) = S ((S (pfc_index_coefficient_add_left_udiagonal)) * pfc_terms_scale_coefficient_add_left_u)) /\ exists ff_q_pfp_coefficient_add_left_udiagonalentry. pfc_terms_code_coefficient_add_left_u = ff_q_pfp_coefficient_add_left_udiagonalentry * S ((S (pfc_index_coefficient_add_left_udiagonal)) * pfc_terms_scale_coefficient_add_left_u) + (pfc_value_coefficient_add_left_udiagonal))) /\ ((exists pfc_complement_coefficient_add_left_udiagonalterm pfc_left_coefficient_add_left_udiagonalterm pfc_right_coefficient_add_left_udiagonalterm. (((pfc_index_coefficient_add_left_udiagonal)+pfc_complement_coefficient_add_left_udiagonalterm=(i)) /\ ((((((exists pfa_gap_coefficient_add_left_udiagonaltermleftinside. pfa_gap_coefficient_add_left_udiagonaltermleftinside + S (pfc_index_coefficient_add_left_udiagonal) = (M)) /\ ((((exists ff_h_pfp_coefficient_add_left_udiagonaltermleftentry. ff_h_pfp_coefficient_add_left_udiagonaltermleftentry + S (pfc_left_coefficient_add_left_udiagonalterm) = S ((S (pfc_index_coefficient_add_left_udiagonal)) * dc)) /\ exists ff_q_pfp_coefficient_add_left_udiagonaltermleftentry. db = ff_q_pfp_coefficient_add_left_udiagonaltermleftentry * S ((S (pfc_index_coefficient_add_left_udiagonal)) * dc) + (pfc_left_coefficient_add_left_udiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_udiagonaltermleftoutside. pfc_gap_coefficient_add_left_udiagonaltermleftoutside+(M)=(pfc_index_coefficient_add_left_udiagonal)) /\ (((pfc_left_coefficient_add_left_udiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_add_left_udiagonaltermrightinside. pfa_gap_coefficient_add_left_udiagonaltermrightinside + S (pfc_complement_coefficient_add_left_udiagonalterm) = (L)) /\ ((((exists ff_h_pfp_coefficient_add_left_udiagonaltermrightentry. ff_h_pfp_coefficient_add_left_udiagonaltermrightentry + S (pfc_right_coefficient_add_left_udiagonalterm) = S ((S (pfc_complement_coefficient_add_left_udiagonalterm)) * ac)) /\ exists ff_q_pfp_coefficient_add_left_udiagonaltermrightentry. ab = ff_q_pfp_coefficient_add_left_udiagonaltermrightentry * S ((S (pfc_complement_coefficient_add_left_udiagonalterm)) * ac) + (pfc_right_coefficient_add_left_udiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_udiagonaltermrightoutside. pfc_gap_coefficient_add_left_udiagonaltermrightoutside+(L)=(pfc_complement_coefficient_add_left_udiagonalterm)) /\ (((pfc_right_coefficient_add_left_udiagonalterm)=0))))) /\ (((pfc_value_coefficient_add_left_udiagonal)=pfc_left_coefficient_add_left_udiagonalterm*pfc_right_coefficient_add_left_udiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_add_left_usum fs_v_pfc_coefficient_add_left_usum. ((((exists fs_h_pfc_coefficient_add_left_usum_body_start. fs_h_pfc_coefficient_add_left_usum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_add_left_usum)) /\ exists fs_q_pfc_coefficient_add_left_usum_body_start. fs_u_pfc_coefficient_add_left_usum = fs_q_pfc_coefficient_add_left_usum_body_start * S ((S (0)) * fs_v_pfc_coefficient_add_left_usum) + (0))) /\ ((((exists fs_h_pfc_coefficient_add_left_usum_body_terminal. fs_h_pfc_coefficient_add_left_usum_body_terminal + S (pfc_natural_sum_coefficient_add_left_u) = S ((S (S (i))) * fs_v_pfc_coefficient_add_left_usum)) /\ exists fs_q_pfc_coefficient_add_left_usum_body_terminal. fs_u_pfc_coefficient_add_left_usum = fs_q_pfc_coefficient_add_left_usum_body_terminal * S ((S (S (i))) * fs_v_pfc_coefficient_add_left_usum) + (pfc_natural_sum_coefficient_add_left_u))) /\ forall fs_i_pfc_coefficient_add_left_usum_body_steps. (exists fs_lt_pfc_coefficient_add_left_usum_body_steps_bound. fs_lt_pfc_coefficient_add_left_usum_body_steps_bound + S fs_i_pfc_coefficient_add_left_usum_body_steps = S (i)) -> exists fs_a_pfc_coefficient_add_left_usum_body_steps fs_r_pfc_coefficient_add_left_usum_body_steps fs_s_pfc_coefficient_add_left_usum_body_steps. ((((exists fs_h_pfc_coefficient_add_left_usum_body_steps_summand. fs_h_pfc_coefficient_add_left_usum_body_steps_summand + S (fs_a_pfc_coefficient_add_left_usum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_usum_body_steps)) * pfc_terms_scale_coefficient_add_left_u)) /\ exists fs_q_pfc_coefficient_add_left_usum_body_steps_summand. pfc_terms_code_coefficient_add_left_u = fs_q_pfc_coefficient_add_left_usum_body_steps_summand * S ((S (fs_i_pfc_coefficient_add_left_usum_body_steps)) * pfc_terms_scale_coefficient_add_left_u) + (fs_a_pfc_coefficient_add_left_usum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_usum_body_steps_partial. fs_h_pfc_coefficient_add_left_usum_body_steps_partial + S (fs_r_pfc_coefficient_add_left_usum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_usum_body_steps)) * fs_v_pfc_coefficient_add_left_usum)) /\ exists fs_q_pfc_coefficient_add_left_usum_body_steps_partial. fs_u_pfc_coefficient_add_left_usum = fs_q_pfc_coefficient_add_left_usum_body_steps_partial * S ((S (fs_i_pfc_coefficient_add_left_usum_body_steps)) * fs_v_pfc_coefficient_add_left_usum) + (fs_r_pfc_coefficient_add_left_usum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_usum_body_steps_successor. fs_h_pfc_coefficient_add_left_usum_body_steps_successor + S (fs_s_pfc_coefficient_add_left_usum_body_steps) = S ((S (S fs_i_pfc_coefficient_add_left_usum_body_steps)) * fs_v_pfc_coefficient_add_left_usum)) /\ exists fs_q_pfc_coefficient_add_left_usum_body_steps_successor. fs_u_pfc_coefficient_add_left_usum = fs_q_pfc_coefficient_add_left_usum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_add_left_usum_body_steps)) * fs_v_pfc_coefficient_add_left_usum) + (fs_s_pfc_coefficient_add_left_usum_body_steps))) /\ fs_s_pfc_coefficient_add_left_usum_body_steps = fs_r_pfc_coefficient_add_left_usum_body_steps + fs_a_pfc_coefficient_add_left_usum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_add_left_uresiduebound. pfa_gap_coefficient_add_left_uresiduebound + S (u) = (p)) /\ ((exists pfa_offset_left_coefficient_add_left_uresiduecongruence pfa_offset_right_coefficient_add_left_uresiduecongruence. (pfc_natural_sum_coefficient_add_left_u) + (p) * pfa_offset_left_coefficient_add_left_uresiduecongruence = (u) + (p) * pfa_offset_right_coefficient_add_left_uresiduecongruence))))))))) -> (exists pfc_terms_code_coefficient_add_left_v pfc_terms_scale_coefficient_add_left_v pfc_natural_sum_coefficient_add_left_v. ((forall pfc_index_coefficient_add_left_vdiagonal. (exists pfa_gap_coefficient_add_left_vdiagonalbound. pfa_gap_coefficient_add_left_vdiagonalbound + S (pfc_index_coefficient_add_left_vdiagonal) = (S (i))) -> exists pfc_value_coefficient_add_left_vdiagonal. ((((exists ff_h_pfp_coefficient_add_left_vdiagonalentry. ff_h_pfp_coefficient_add_left_vdiagonalentry + S (pfc_value_coefficient_add_left_vdiagonal) = S ((S (pfc_index_coefficient_add_left_vdiagonal)) * pfc_terms_scale_coefficient_add_left_v)) /\ exists ff_q_pfp_coefficient_add_left_vdiagonalentry. pfc_terms_code_coefficient_add_left_v = ff_q_pfp_coefficient_add_left_vdiagonalentry * S ((S (pfc_index_coefficient_add_left_vdiagonal)) * pfc_terms_scale_coefficient_add_left_v) + (pfc_value_coefficient_add_left_vdiagonal))) /\ ((exists pfc_complement_coefficient_add_left_vdiagonalterm pfc_left_coefficient_add_left_vdiagonalterm pfc_right_coefficient_add_left_vdiagonalterm. (((pfc_index_coefficient_add_left_vdiagonal)+pfc_complement_coefficient_add_left_vdiagonalterm=(i)) /\ ((((((exists pfa_gap_coefficient_add_left_vdiagonaltermleftinside. pfa_gap_coefficient_add_left_vdiagonaltermleftinside + S (pfc_index_coefficient_add_left_vdiagonal) = (M)) /\ ((((exists ff_h_pfp_coefficient_add_left_vdiagonaltermleftentry. ff_h_pfp_coefficient_add_left_vdiagonaltermleftentry + S (pfc_left_coefficient_add_left_vdiagonalterm) = S ((S (pfc_index_coefficient_add_left_vdiagonal)) * dc)) /\ exists ff_q_pfp_coefficient_add_left_vdiagonaltermleftentry. db = ff_q_pfp_coefficient_add_left_vdiagonaltermleftentry * S ((S (pfc_index_coefficient_add_left_vdiagonal)) * dc) + (pfc_left_coefficient_add_left_vdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_vdiagonaltermleftoutside. pfc_gap_coefficient_add_left_vdiagonaltermleftoutside+(M)=(pfc_index_coefficient_add_left_vdiagonal)) /\ (((pfc_left_coefficient_add_left_vdiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_add_left_vdiagonaltermrightinside. pfa_gap_coefficient_add_left_vdiagonaltermrightinside + S (pfc_complement_coefficient_add_left_vdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_coefficient_add_left_vdiagonaltermrightentry. ff_h_pfp_coefficient_add_left_vdiagonaltermrightentry + S (pfc_right_coefficient_add_left_vdiagonalterm) = S ((S (pfc_complement_coefficient_add_left_vdiagonalterm)) * bc)) /\ exists ff_q_pfp_coefficient_add_left_vdiagonaltermrightentry. bb = ff_q_pfp_coefficient_add_left_vdiagonaltermrightentry * S ((S (pfc_complement_coefficient_add_left_vdiagonalterm)) * bc) + (pfc_right_coefficient_add_left_vdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_vdiagonaltermrightoutside. pfc_gap_coefficient_add_left_vdiagonaltermrightoutside+(L)=(pfc_complement_coefficient_add_left_vdiagonalterm)) /\ (((pfc_right_coefficient_add_left_vdiagonalterm)=0))))) /\ (((pfc_value_coefficient_add_left_vdiagonal)=pfc_left_coefficient_add_left_vdiagonalterm*pfc_right_coefficient_add_left_vdiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_add_left_vsum fs_v_pfc_coefficient_add_left_vsum. ((((exists fs_h_pfc_coefficient_add_left_vsum_body_start. fs_h_pfc_coefficient_add_left_vsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_add_left_vsum)) /\ exists fs_q_pfc_coefficient_add_left_vsum_body_start. fs_u_pfc_coefficient_add_left_vsum = fs_q_pfc_coefficient_add_left_vsum_body_start * S ((S (0)) * fs_v_pfc_coefficient_add_left_vsum) + (0))) /\ ((((exists fs_h_pfc_coefficient_add_left_vsum_body_terminal. fs_h_pfc_coefficient_add_left_vsum_body_terminal + S (pfc_natural_sum_coefficient_add_left_v) = S ((S (S (i))) * fs_v_pfc_coefficient_add_left_vsum)) /\ exists fs_q_pfc_coefficient_add_left_vsum_body_terminal. fs_u_pfc_coefficient_add_left_vsum = fs_q_pfc_coefficient_add_left_vsum_body_terminal * S ((S (S (i))) * fs_v_pfc_coefficient_add_left_vsum) + (pfc_natural_sum_coefficient_add_left_v))) /\ forall fs_i_pfc_coefficient_add_left_vsum_body_steps. (exists fs_lt_pfc_coefficient_add_left_vsum_body_steps_bound. fs_lt_pfc_coefficient_add_left_vsum_body_steps_bound + S fs_i_pfc_coefficient_add_left_vsum_body_steps = S (i)) -> exists fs_a_pfc_coefficient_add_left_vsum_body_steps fs_r_pfc_coefficient_add_left_vsum_body_steps fs_s_pfc_coefficient_add_left_vsum_body_steps. ((((exists fs_h_pfc_coefficient_add_left_vsum_body_steps_summand. fs_h_pfc_coefficient_add_left_vsum_body_steps_summand + S (fs_a_pfc_coefficient_add_left_vsum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_vsum_body_steps)) * pfc_terms_scale_coefficient_add_left_v)) /\ exists fs_q_pfc_coefficient_add_left_vsum_body_steps_summand. pfc_terms_code_coefficient_add_left_v = fs_q_pfc_coefficient_add_left_vsum_body_steps_summand * S ((S (fs_i_pfc_coefficient_add_left_vsum_body_steps)) * pfc_terms_scale_coefficient_add_left_v) + (fs_a_pfc_coefficient_add_left_vsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_vsum_body_steps_partial. fs_h_pfc_coefficient_add_left_vsum_body_steps_partial + S (fs_r_pfc_coefficient_add_left_vsum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_vsum_body_steps)) * fs_v_pfc_coefficient_add_left_vsum)) /\ exists fs_q_pfc_coefficient_add_left_vsum_body_steps_partial. fs_u_pfc_coefficient_add_left_vsum = fs_q_pfc_coefficient_add_left_vsum_body_steps_partial * S ((S (fs_i_pfc_coefficient_add_left_vsum_body_steps)) * fs_v_pfc_coefficient_add_left_vsum) + (fs_r_pfc_coefficient_add_left_vsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_vsum_body_steps_successor. fs_h_pfc_coefficient_add_left_vsum_body_steps_successor + S (fs_s_pfc_coefficient_add_left_vsum_body_steps) = S ((S (S fs_i_pfc_coefficient_add_left_vsum_body_steps)) * fs_v_pfc_coefficient_add_left_vsum)) /\ exists fs_q_pfc_coefficient_add_left_vsum_body_steps_successor. fs_u_pfc_coefficient_add_left_vsum = fs_q_pfc_coefficient_add_left_vsum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_add_left_vsum_body_steps)) * fs_v_pfc_coefficient_add_left_vsum) + (fs_s_pfc_coefficient_add_left_vsum_body_steps))) /\ fs_s_pfc_coefficient_add_left_vsum_body_steps = fs_r_pfc_coefficient_add_left_vsum_body_steps + fs_a_pfc_coefficient_add_left_vsum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_add_left_vresiduebound. pfa_gap_coefficient_add_left_vresiduebound + S (v) = (p)) /\ ((exists pfa_offset_left_coefficient_add_left_vresiduecongruence pfa_offset_right_coefficient_add_left_vresiduecongruence. (pfc_natural_sum_coefficient_add_left_v) + (p) * pfa_offset_left_coefficient_add_left_vresiduecongruence = (v) + (p) * pfa_offset_right_coefficient_add_left_vresiduecongruence))))))))) -> (exists pfc_terms_code_coefficient_add_left_w pfc_terms_scale_coefficient_add_left_w pfc_natural_sum_coefficient_add_left_w. ((forall pfc_index_coefficient_add_left_wdiagonal. (exists pfa_gap_coefficient_add_left_wdiagonalbound. pfa_gap_coefficient_add_left_wdiagonalbound + S (pfc_index_coefficient_add_left_wdiagonal) = (S (i))) -> exists pfc_value_coefficient_add_left_wdiagonal. ((((exists ff_h_pfp_coefficient_add_left_wdiagonalentry. ff_h_pfp_coefficient_add_left_wdiagonalentry + S (pfc_value_coefficient_add_left_wdiagonal) = S ((S (pfc_index_coefficient_add_left_wdiagonal)) * pfc_terms_scale_coefficient_add_left_w)) /\ exists ff_q_pfp_coefficient_add_left_wdiagonalentry. pfc_terms_code_coefficient_add_left_w = ff_q_pfp_coefficient_add_left_wdiagonalentry * S ((S (pfc_index_coefficient_add_left_wdiagonal)) * pfc_terms_scale_coefficient_add_left_w) + (pfc_value_coefficient_add_left_wdiagonal))) /\ ((exists pfc_complement_coefficient_add_left_wdiagonalterm pfc_left_coefficient_add_left_wdiagonalterm pfc_right_coefficient_add_left_wdiagonalterm. (((pfc_index_coefficient_add_left_wdiagonal)+pfc_complement_coefficient_add_left_wdiagonalterm=(i)) /\ ((((((exists pfa_gap_coefficient_add_left_wdiagonaltermleftinside. pfa_gap_coefficient_add_left_wdiagonaltermleftinside + S (pfc_index_coefficient_add_left_wdiagonal) = (M)) /\ ((((exists ff_h_pfp_coefficient_add_left_wdiagonaltermleftentry. ff_h_pfp_coefficient_add_left_wdiagonaltermleftentry + S (pfc_left_coefficient_add_left_wdiagonalterm) = S ((S (pfc_index_coefficient_add_left_wdiagonal)) * dc)) /\ exists ff_q_pfp_coefficient_add_left_wdiagonaltermleftentry. db = ff_q_pfp_coefficient_add_left_wdiagonaltermleftentry * S ((S (pfc_index_coefficient_add_left_wdiagonal)) * dc) + (pfc_left_coefficient_add_left_wdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_wdiagonaltermleftoutside. pfc_gap_coefficient_add_left_wdiagonaltermleftoutside+(M)=(pfc_index_coefficient_add_left_wdiagonal)) /\ (((pfc_left_coefficient_add_left_wdiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_add_left_wdiagonaltermrightinside. pfa_gap_coefficient_add_left_wdiagonaltermrightinside + S (pfc_complement_coefficient_add_left_wdiagonalterm) = (L)) /\ ((((exists ff_h_pfp_coefficient_add_left_wdiagonaltermrightentry. ff_h_pfp_coefficient_add_left_wdiagonaltermrightentry + S (pfc_right_coefficient_add_left_wdiagonalterm) = S ((S (pfc_complement_coefficient_add_left_wdiagonalterm)) * cc)) /\ exists ff_q_pfp_coefficient_add_left_wdiagonaltermrightentry. cb = ff_q_pfp_coefficient_add_left_wdiagonaltermrightentry * S ((S (pfc_complement_coefficient_add_left_wdiagonalterm)) * cc) + (pfc_right_coefficient_add_left_wdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_add_left_wdiagonaltermrightoutside. pfc_gap_coefficient_add_left_wdiagonaltermrightoutside+(L)=(pfc_complement_coefficient_add_left_wdiagonalterm)) /\ (((pfc_right_coefficient_add_left_wdiagonalterm)=0))))) /\ (((pfc_value_coefficient_add_left_wdiagonal)=pfc_left_coefficient_add_left_wdiagonalterm*pfc_right_coefficient_add_left_wdiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_add_left_wsum fs_v_pfc_coefficient_add_left_wsum. ((((exists fs_h_pfc_coefficient_add_left_wsum_body_start. fs_h_pfc_coefficient_add_left_wsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_add_left_wsum)) /\ exists fs_q_pfc_coefficient_add_left_wsum_body_start. fs_u_pfc_coefficient_add_left_wsum = fs_q_pfc_coefficient_add_left_wsum_body_start * S ((S (0)) * fs_v_pfc_coefficient_add_left_wsum) + (0))) /\ ((((exists fs_h_pfc_coefficient_add_left_wsum_body_terminal. fs_h_pfc_coefficient_add_left_wsum_body_terminal + S (pfc_natural_sum_coefficient_add_left_w) = S ((S (S (i))) * fs_v_pfc_coefficient_add_left_wsum)) /\ exists fs_q_pfc_coefficient_add_left_wsum_body_terminal. fs_u_pfc_coefficient_add_left_wsum = fs_q_pfc_coefficient_add_left_wsum_body_terminal * S ((S (S (i))) * fs_v_pfc_coefficient_add_left_wsum) + (pfc_natural_sum_coefficient_add_left_w))) /\ forall fs_i_pfc_coefficient_add_left_wsum_body_steps. (exists fs_lt_pfc_coefficient_add_left_wsum_body_steps_bound. fs_lt_pfc_coefficient_add_left_wsum_body_steps_bound + S fs_i_pfc_coefficient_add_left_wsum_body_steps = S (i)) -> exists fs_a_pfc_coefficient_add_left_wsum_body_steps fs_r_pfc_coefficient_add_left_wsum_body_steps fs_s_pfc_coefficient_add_left_wsum_body_steps. ((((exists fs_h_pfc_coefficient_add_left_wsum_body_steps_summand. fs_h_pfc_coefficient_add_left_wsum_body_steps_summand + S (fs_a_pfc_coefficient_add_left_wsum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_wsum_body_steps)) * pfc_terms_scale_coefficient_add_left_w)) /\ exists fs_q_pfc_coefficient_add_left_wsum_body_steps_summand. pfc_terms_code_coefficient_add_left_w = fs_q_pfc_coefficient_add_left_wsum_body_steps_summand * S ((S (fs_i_pfc_coefficient_add_left_wsum_body_steps)) * pfc_terms_scale_coefficient_add_left_w) + (fs_a_pfc_coefficient_add_left_wsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_wsum_body_steps_partial. fs_h_pfc_coefficient_add_left_wsum_body_steps_partial + S (fs_r_pfc_coefficient_add_left_wsum_body_steps) = S ((S (fs_i_pfc_coefficient_add_left_wsum_body_steps)) * fs_v_pfc_coefficient_add_left_wsum)) /\ exists fs_q_pfc_coefficient_add_left_wsum_body_steps_partial. fs_u_pfc_coefficient_add_left_wsum = fs_q_pfc_coefficient_add_left_wsum_body_steps_partial * S ((S (fs_i_pfc_coefficient_add_left_wsum_body_steps)) * fs_v_pfc_coefficient_add_left_wsum) + (fs_r_pfc_coefficient_add_left_wsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_add_left_wsum_body_steps_successor. fs_h_pfc_coefficient_add_left_wsum_body_steps_successor + S (fs_s_pfc_coefficient_add_left_wsum_body_steps) = S ((S (S fs_i_pfc_coefficient_add_left_wsum_body_steps)) * fs_v_pfc_coefficient_add_left_wsum)) /\ exists fs_q_pfc_coefficient_add_left_wsum_body_steps_successor. fs_u_pfc_coefficient_add_left_wsum = fs_q_pfc_coefficient_add_left_wsum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_add_left_wsum_body_steps)) * fs_v_pfc_coefficient_add_left_wsum) + (fs_s_pfc_coefficient_add_left_wsum_body_steps))) /\ fs_s_pfc_coefficient_add_left_wsum_body_steps = fs_r_pfc_coefficient_add_left_wsum_body_steps + fs_a_pfc_coefficient_add_left_wsum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_add_left_wresiduebound. pfa_gap_coefficient_add_left_wresiduebound + S (w) = (p)) /\ ((exists pfa_offset_left_coefficient_add_left_wresiduecongruence pfa_offset_right_coefficient_add_left_wresiduecongruence. (pfc_natural_sum_coefficient_add_left_w) + (p) * pfa_offset_left_coefficient_add_left_wresiduecongruence = (w) + (p) * pfa_offset_right_coefficient_add_left_wresiduecongruence))))))))) -> (((exists pfa_gap_coefficient_add_left_resultleft. pfa_gap_coefficient_add_left_resultleft + S (u) = (p)) /\ (((exists pfa_gap_coefficient_add_left_resultright. pfa_gap_coefficient_add_left_resultright + S (v) = (p)) /\ ((((exists pfa_gap_coefficient_add_left_resultresultbound. pfa_gap_coefficient_add_left_resultresultbound + S (w) = (p)) /\ ((exists pfa_offset_left_coefficient_add_left_resultresultcongruence pfa_offset_right_coefficient_add_left_resultresultcongruence. ((u) + (v)) + (p) * pfa_offset_left_coefficient_add_left_resultresultcongruence = (w) + (p) * pfa_offset_right_coefficient_add_left_resultresultcongruence)))))))))
Complete tactic proof in conservative notation
All 100 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.