Every actual product A*(k B) agrees coefficientwise with every actual scalar result k*(A*B), at the same proper length; no equality of beta codes follows.
Alpha v34 checked-use · first admitted v34 · 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 products and sums use actual beta-coded coefficients; equality is formal coefficient equivalence, not equality of evaluations or raw codes. The zero gcd is included. Uniqueness is up to formal equivalence, not unique Bézout coefficients. This proves the polynomial gcd component, not G091 irreducible-polynomial existence or arbitrary prime-power-field construction.
forall p k ab ac L bb bc M sb sc cb cc N db dc K eb ec. (((exists pfa_gap_scalar_comparison_inputscalar. pfa_gap_scalar_comparison_inputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_comparison_input. (exists pfa_gap_scalar_comparison_inputindex. pfa_gap_scalar_comparison_inputindex + S (pfp_index_scalar_comparison_input) = (M)) -> exists pfp_source_scalar_comparison_input pfp_value_scalar_comparison_input. ((((exists ff_h_pfp_scalar_comparison_inputsource. ff_h_pfp_scalar_comparison_inputsource + S (pfp_source_scalar_comparison_input) = S ((S (pfp_index_scalar_comparison_input)) * bc)) /\ exists ff_q_pfp_scalar_comparison_inputsource. bb = ff_q_pfp_scalar_comparison_inputsource * S ((S (pfp_index_scalar_comparison_input)) * bc) + (pfp_source_scalar_comparison_input))) /\ (((((exists ff_h_pfp_scalar_comparison_inputtarget. ff_h_pfp_scalar_comparison_inputtarget + S (pfp_value_scalar_comparison_input) = S ((S (pfp_index_scalar_comparison_input)) * sc)) /\ exists ff_q_pfp_scalar_comparison_inputtarget. sb = ff_q_pfp_scalar_comparison_inputtarget * S ((S (pfp_index_scalar_comparison_input)) * sc) + (pfp_value_scalar_comparison_input))) /\ ((((exists pfa_gap_scalar_comparison_inputoperationleft. pfa_gap_scalar_comparison_inputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_comparison_inputoperationright. pfa_gap_scalar_comparison_inputoperationright + S (pfp_source_scalar_comparison_input) = (p)) /\ ((((exists pfa_gap_scalar_comparison_inputoperationresultbound. pfa_gap_scalar_comparison_inputoperationresultbound + S (pfp_value_scalar_comparison_input) = (p)) /\ ((exists pfa_offset_left_scalar_comparison_inputoperationresultcongruence pfa_offset_right_scalar_comparison_inputoperationresultcongruence. ((k) * (pfp_source_scalar_comparison_input)) + (p) * pfa_offset_left_scalar_comparison_inputoperationresultcongruence = (pfp_value_scalar_comparison_input) + (p) * pfa_offset_right_scalar_comparison_inputoperationresultcongruence))))))))))))))))) -> (((forall fom_index_pfp_scalar_comparison_oldleft. (exists fom_gap_pfp_scalar_comparison_oldleft_index_bound. fom_gap_pfp_scalar_comparison_oldleft_index_bound + S (fom_index_pfp_scalar_comparison_oldleft) = L) -> exists fom_value_pfp_scalar_comparison_oldleft. ((((exists fom_beta_height_pfp_scalar_comparison_oldleft_entry. fom_beta_height_pfp_scalar_comparison_oldleft_entry + S (fom_value_pfp_scalar_comparison_oldleft) = S ((S (fom_index_pfp_scalar_comparison_oldleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_comparison_oldleft_entry. ab = fom_beta_quotient_pfp_scalar_comparison_oldleft_entry * S ((S (fom_index_pfp_scalar_comparison_oldleft)) * ac) + (fom_value_pfp_scalar_comparison_oldleft))) /\ (exists fom_gap_pfp_scalar_comparison_oldleft_value_bound. fom_gap_pfp_scalar_comparison_oldleft_value_bound + S (fom_value_pfp_scalar_comparison_oldleft) = p))) /\ (((forall fom_index_pfp_scalar_comparison_oldright. (exists fom_gap_pfp_scalar_comparison_oldright_index_bound. fom_gap_pfp_scalar_comparison_oldright_index_bound + S (fom_index_pfp_scalar_comparison_oldright) = M) -> exists fom_value_pfp_scalar_comparison_oldright. ((((exists fom_beta_height_pfp_scalar_comparison_oldright_entry. fom_beta_height_pfp_scalar_comparison_oldright_entry + S (fom_value_pfp_scalar_comparison_oldright) = S ((S (fom_index_pfp_scalar_comparison_oldright)) * bc)) /\ exists fom_beta_quotient_pfp_scalar_comparison_oldright_entry. bb = fom_beta_quotient_pfp_scalar_comparison_oldright_entry * S ((S (fom_index_pfp_scalar_comparison_oldright)) * bc) + (fom_value_pfp_scalar_comparison_oldright))) /\ (exists fom_gap_pfp_scalar_comparison_oldright_value_bound. fom_gap_pfp_scalar_comparison_oldright_value_bound + S (fom_value_pfp_scalar_comparison_oldright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((N)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (N)))))))) /\ ((forall pfc_index_scalar_comparison_oldcoefficients. (exists pfa_gap_scalar_comparison_oldcoefficientsbound. pfa_gap_scalar_comparison_oldcoefficientsbound + S (pfc_index_scalar_comparison_oldcoefficients) = (N)) -> exists pfc_value_scalar_comparison_oldcoefficients. ((((exists ff_h_pfp_scalar_comparison_oldcoefficientsentry. ff_h_pfp_scalar_comparison_oldcoefficientsentry + S (pfc_value_scalar_comparison_oldcoefficients) = S ((S (pfc_index_scalar_comparison_oldcoefficients)) * cc)) /\ exists ff_q_pfp_scalar_comparison_oldcoefficientsentry. cb = ff_q_pfp_scalar_comparison_oldcoefficientsentry * S ((S (pfc_index_scalar_comparison_oldcoefficients)) * cc) + (pfc_value_scalar_comparison_oldcoefficients))) /\ ((exists pfc_terms_code_scalar_comparison_oldcoefficientscoefficient pfc_terms_scale_scalar_comparison_oldcoefficientscoefficient pfc_natural_sum_scalar_comparison_oldcoefficientscoefficient. ((forall pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonalbound. pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_comparison_oldcoefficients))) -> exists pfc_value_scalar_comparison_oldcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_comparison_oldcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_comparison_oldcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_comparison_oldcoefficientscoefficient = ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_comparison_oldcoefficientscoefficient) + (pfc_value_scalar_comparison_oldcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm pfc_left_scalar_comparison_oldcoefficientscoefficientdiagonalterm pfc_right_scalar_comparison_oldcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)+pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm=(pfc_index_scalar_comparison_oldcoefficients)) /\ ((((((exists pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_comparison_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_comparison_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_comparison_oldcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_comparison_oldcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_comparison_oldcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm)) * bc)) /\ exists ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightentry. bb = ff_q_pfp_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm)) * bc) + (pfc_right_scalar_comparison_oldcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_comparison_oldcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_comparison_oldcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_comparison_oldcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_comparison_oldcoefficientscoefficientdiagonal)=pfc_left_scalar_comparison_oldcoefficientscoefficientdiagonalterm*pfc_right_scalar_comparison_oldcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_comparison_oldcoefficientscoefficientsum fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_comparison_oldcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_comparison_oldcoefficientscoefficient) = S ((S (S (pfc_index_scalar_comparison_oldcoefficients))) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_comparison_oldcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_comparison_oldcoefficients))) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum) + (pfc_natural_sum_scalar_comparison_oldcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_comparison_oldcoefficients)) -> exists fs_a_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_comparison_oldcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_comparison_oldcoefficientscoefficient = fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_comparison_oldcoefficientscoefficient) + (fs_a_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_comparison_oldcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum) + (fs_r_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_comparison_oldcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_oldcoefficientscoefficientsum) + (fs_s_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_comparison_oldcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_comparison_oldcoefficientscoefficientresiduebound. pfa_gap_scalar_comparison_oldcoefficientscoefficientresiduebound + S (pfc_value_scalar_comparison_oldcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_comparison_oldcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_comparison_oldcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_comparison_oldcoefficientscoefficient) + (p) * pfa_offset_left_scalar_comparison_oldcoefficientscoefficientresiduecongruence = (pfc_value_scalar_comparison_oldcoefficients) + (p) * pfa_offset_right_scalar_comparison_oldcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((forall fom_index_pfp_scalar_comparison_scaledleft. (exists fom_gap_pfp_scalar_comparison_scaledleft_index_bound. fom_gap_pfp_scalar_comparison_scaledleft_index_bound + S (fom_index_pfp_scalar_comparison_scaledleft) = L) -> exists fom_value_pfp_scalar_comparison_scaledleft. ((((exists fom_beta_height_pfp_scalar_comparison_scaledleft_entry. fom_beta_height_pfp_scalar_comparison_scaledleft_entry + S (fom_value_pfp_scalar_comparison_scaledleft) = S ((S (fom_index_pfp_scalar_comparison_scaledleft)) * ac)) /\ exists fom_beta_quotient_pfp_scalar_comparison_scaledleft_entry. ab = fom_beta_quotient_pfp_scalar_comparison_scaledleft_entry * S ((S (fom_index_pfp_scalar_comparison_scaledleft)) * ac) + (fom_value_pfp_scalar_comparison_scaledleft))) /\ (exists fom_gap_pfp_scalar_comparison_scaledleft_value_bound. fom_gap_pfp_scalar_comparison_scaledleft_value_bound + S (fom_value_pfp_scalar_comparison_scaledleft) = p))) /\ (((forall fom_index_pfp_scalar_comparison_scaledright. (exists fom_gap_pfp_scalar_comparison_scaledright_index_bound. fom_gap_pfp_scalar_comparison_scaledright_index_bound + S (fom_index_pfp_scalar_comparison_scaledright) = M) -> exists fom_value_pfp_scalar_comparison_scaledright. ((((exists fom_beta_height_pfp_scalar_comparison_scaledright_entry. fom_beta_height_pfp_scalar_comparison_scaledright_entry + S (fom_value_pfp_scalar_comparison_scaledright) = S ((S (fom_index_pfp_scalar_comparison_scaledright)) * sc)) /\ exists fom_beta_quotient_pfp_scalar_comparison_scaledright_entry. sb = fom_beta_quotient_pfp_scalar_comparison_scaledright_entry * S ((S (fom_index_pfp_scalar_comparison_scaledright)) * sc) + (fom_value_pfp_scalar_comparison_scaledright))) /\ (exists fom_gap_pfp_scalar_comparison_scaledright_value_bound. fom_gap_pfp_scalar_comparison_scaledright_value_bound + S (fom_value_pfp_scalar_comparison_scaledright) = p))) /\ (((((((L)=0 \/ (M)=0) /\ (((K)=0)))) \/ (((~((L)=0)) /\ (((~((M)=0)) /\ (((L)+(M)=S (K)))))))) /\ ((forall pfc_index_scalar_comparison_scaledcoefficients. (exists pfa_gap_scalar_comparison_scaledcoefficientsbound. pfa_gap_scalar_comparison_scaledcoefficientsbound + S (pfc_index_scalar_comparison_scaledcoefficients) = (K)) -> exists pfc_value_scalar_comparison_scaledcoefficients. ((((exists ff_h_pfp_scalar_comparison_scaledcoefficientsentry. ff_h_pfp_scalar_comparison_scaledcoefficientsentry + S (pfc_value_scalar_comparison_scaledcoefficients) = S ((S (pfc_index_scalar_comparison_scaledcoefficients)) * dc)) /\ exists ff_q_pfp_scalar_comparison_scaledcoefficientsentry. db = ff_q_pfp_scalar_comparison_scaledcoefficientsentry * S ((S (pfc_index_scalar_comparison_scaledcoefficients)) * dc) + (pfc_value_scalar_comparison_scaledcoefficients))) /\ ((exists pfc_terms_code_scalar_comparison_scaledcoefficientscoefficient pfc_terms_scale_scalar_comparison_scaledcoefficientscoefficient pfc_natural_sum_scalar_comparison_scaledcoefficientscoefficient. ((forall pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal. (exists pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonalbound. pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonalbound + S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal) = (S (pfc_index_scalar_comparison_scaledcoefficients))) -> exists pfc_value_scalar_comparison_scaledcoefficientscoefficientdiagonal. ((((exists ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonalentry. ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonalentry + S (pfc_value_scalar_comparison_scaledcoefficientscoefficientdiagonal) = S ((S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_comparison_scaledcoefficientscoefficient)) /\ exists ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonalentry. pfc_terms_code_scalar_comparison_scaledcoefficientscoefficient = ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonalentry * S ((S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)) * pfc_terms_scale_scalar_comparison_scaledcoefficientscoefficient) + (pfc_value_scalar_comparison_scaledcoefficientscoefficientdiagonal))) /\ ((exists pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm pfc_left_scalar_comparison_scaledcoefficientscoefficientdiagonalterm pfc_right_scalar_comparison_scaledcoefficientscoefficientdiagonalterm. (((pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)+pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm=(pfc_index_scalar_comparison_scaledcoefficients)) /\ ((((((exists pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftinside. pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftinside + S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal) = (L)) /\ ((((exists ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftentry. ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftentry + S (pfc_left_scalar_comparison_scaledcoefficientscoefficientdiagonalterm) = S ((S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)) * ac)) /\ exists ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftentry. ab = ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftentry * S ((S (pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)) * ac) + (pfc_left_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftoutside. pfc_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermleftoutside+(L)=(pfc_index_scalar_comparison_scaledcoefficientscoefficientdiagonal)) /\ (((pfc_left_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)=0))))) /\ ((((((exists pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightinside. pfa_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightinside + S (pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightentry. ff_h_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightentry + S (pfc_right_scalar_comparison_scaledcoefficientscoefficientdiagonalterm) = S ((S (pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)) * sc)) /\ exists ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightentry. sb = ff_q_pfp_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightentry * S ((S (pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)) * sc) + (pfc_right_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)))))) \/ (((exists pfc_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightoutside. pfc_gap_scalar_comparison_scaledcoefficientscoefficientdiagonaltermrightoutside+(M)=(pfc_complement_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)) /\ (((pfc_right_scalar_comparison_scaledcoefficientscoefficientdiagonalterm)=0))))) /\ (((pfc_value_scalar_comparison_scaledcoefficientscoefficientdiagonal)=pfc_left_scalar_comparison_scaledcoefficientscoefficientdiagonalterm*pfc_right_scalar_comparison_scaledcoefficientscoefficientdiagonalterm))))))))))) /\ (((exists fs_u_pfc_scalar_comparison_scaledcoefficientscoefficientsum fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum. ((((exists fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_start. fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_start. fs_u_pfc_scalar_comparison_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_start * S ((S (0)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum) + (0))) /\ ((((exists fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_terminal. fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_terminal + S (pfc_natural_sum_scalar_comparison_scaledcoefficientscoefficient) = S ((S (S (pfc_index_scalar_comparison_scaledcoefficients))) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_terminal. fs_u_pfc_scalar_comparison_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_terminal * S ((S (S (pfc_index_scalar_comparison_scaledcoefficients))) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum) + (pfc_natural_sum_scalar_comparison_scaledcoefficientscoefficient))) /\ forall fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps. (exists fs_lt_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_bound. fs_lt_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_bound + S fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps = S (pfc_index_scalar_comparison_scaledcoefficients)) -> exists fs_a_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps fs_r_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps fs_s_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps. ((((exists fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_summand. fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_summand + S (fs_a_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_comparison_scaledcoefficientscoefficient)) /\ exists fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_summand. pfc_terms_code_scalar_comparison_scaledcoefficientscoefficient = fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_summand * S ((S (fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * pfc_terms_scale_scalar_comparison_scaledcoefficientscoefficient) + (fs_a_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_partial. fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_partial + S (fs_r_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps) = S ((S (fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_partial. fs_u_pfc_scalar_comparison_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_partial * S ((S (fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum) + (fs_r_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps))) /\ ((((exists fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_successor. fs_h_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_successor + S (fs_s_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps) = S ((S (S fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum)) /\ exists fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_successor. fs_u_pfc_scalar_comparison_scaledcoefficientscoefficientsum = fs_q_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps_successor * S ((S (S fs_i_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)) * fs_v_pfc_scalar_comparison_scaledcoefficientscoefficientsum) + (fs_s_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps))) /\ fs_s_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps = fs_r_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps + fs_a_pfc_scalar_comparison_scaledcoefficientscoefficientsum_body_steps)))))) /\ ((((exists pfa_gap_scalar_comparison_scaledcoefficientscoefficientresiduebound. pfa_gap_scalar_comparison_scaledcoefficientscoefficientresiduebound + S (pfc_value_scalar_comparison_scaledcoefficients) = (p)) /\ ((exists pfa_offset_left_scalar_comparison_scaledcoefficientscoefficientresiduecongruence pfa_offset_right_scalar_comparison_scaledcoefficientscoefficientresiduecongruence. (pfc_natural_sum_scalar_comparison_scaledcoefficientscoefficient) + (p) * pfa_offset_left_scalar_comparison_scaledcoefficientscoefficientresiduecongruence = (pfc_value_scalar_comparison_scaledcoefficients) + (p) * pfa_offset_right_scalar_comparison_scaledcoefficientscoefficientresiduecongruence))))))))))))))))))) -> (((exists pfa_gap_scalar_comparison_outputscalar. pfa_gap_scalar_comparison_outputscalar + S (k) = (p)) /\ ((forall pfp_index_scalar_comparison_output. (exists pfa_gap_scalar_comparison_outputindex. pfa_gap_scalar_comparison_outputindex + S (pfp_index_scalar_comparison_output) = (N)) -> exists pfp_source_scalar_comparison_output pfp_value_scalar_comparison_output. ((((exists ff_h_pfp_scalar_comparison_outputsource. ff_h_pfp_scalar_comparison_outputsource + S (pfp_source_scalar_comparison_output) = S ((S (pfp_index_scalar_comparison_output)) * cc)) /\ exists ff_q_pfp_scalar_comparison_outputsource. cb = ff_q_pfp_scalar_comparison_outputsource * S ((S (pfp_index_scalar_comparison_output)) * cc) + (pfp_source_scalar_comparison_output))) /\ (((((exists ff_h_pfp_scalar_comparison_outputtarget. ff_h_pfp_scalar_comparison_outputtarget + S (pfp_value_scalar_comparison_output) = S ((S (pfp_index_scalar_comparison_output)) * ec)) /\ exists ff_q_pfp_scalar_comparison_outputtarget. eb = ff_q_pfp_scalar_comparison_outputtarget * S ((S (pfp_index_scalar_comparison_output)) * ec) + (pfp_value_scalar_comparison_output))) /\ ((((exists pfa_gap_scalar_comparison_outputoperationleft. pfa_gap_scalar_comparison_outputoperationleft + S (k) = (p)) /\ (((exists pfa_gap_scalar_comparison_outputoperationright. pfa_gap_scalar_comparison_outputoperationright + S (pfp_source_scalar_comparison_output) = (p)) /\ ((((exists pfa_gap_scalar_comparison_outputoperationresultbound. pfa_gap_scalar_comparison_outputoperationresultbound + S (pfp_value_scalar_comparison_output) = (p)) /\ ((exists pfa_offset_left_scalar_comparison_outputoperationresultcongruence pfa_offset_right_scalar_comparison_outputoperationresultcongruence. ((k) * (pfp_source_scalar_comparison_output)) + (p) * pfa_offset_left_scalar_comparison_outputoperationresultcongruence = (pfp_value_scalar_comparison_output) + (p) * pfa_offset_right_scalar_comparison_outputoperationresultcongruence))))))))))))))))) -> (((K=N) /\ ((forall mdr_i_pfp_scalar_comparison_result mdr_a_pfp_scalar_comparison_result. (exists mdr_gap_pfp_scalar_comparison_resultb. mdr_gap_pfp_scalar_comparison_resultb + S (mdr_i_pfp_scalar_comparison_result) = (N)) -> (((exists ff_h_mdr_pfp_scalar_comparison_resulto. ff_h_mdr_pfp_scalar_comparison_resulto + S (mdr_a_pfp_scalar_comparison_result) = S ((S (mdr_i_pfp_scalar_comparison_result)) * dc)) /\ exists ff_q_mdr_pfp_scalar_comparison_resulto. db = ff_q_mdr_pfp_scalar_comparison_resulto * S ((S (mdr_i_pfp_scalar_comparison_result)) * dc) + (mdr_a_pfp_scalar_comparison_result))) -> (((exists ff_h_mdr_pfp_scalar_comparison_resultn. ff_h_mdr_pfp_scalar_comparison_resultn + S (mdr_a_pfp_scalar_comparison_result) = S ((S (mdr_i_pfp_scalar_comparison_result)) * ec)) /\ exists ff_q_mdr_pfp_scalar_comparison_resultn. eb = ff_q_mdr_pfp_scalar_comparison_resultn * S ((S (mdr_i_pfp_scalar_comparison_result)) * ec) + (mdr_a_pfp_scalar_comparison_result)))))))
Complete tactic proof in conservative notation
All 58 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.