PX0004 — prime_field_convolution_coefficient_append_invariant

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 p ab ac AB AC bb bc M N i r. (forall mdr_i_pfp_tri_append_equal mdr_a_pfp_tri_append_equal. (exists mdr_gap_pfp_tri_append_equalb. mdr_gap_pfp_tri_append_equalb + S (mdr_i_pfp_tri_append_equal) = (N)) -> (((exists ff_h_mdr_pfp_tri_append_equalo. ff_h_mdr_pfp_tri_append_equalo + S (mdr_a_pfp_tri_append_equal) = S ((S (mdr_i_pfp_tri_append_equal)) * ac)) /\ exists ff_q_mdr_pfp_tri_append_equalo. ab = ff_q_mdr_pfp_tri_append_equalo * S ((S (mdr_i_pfp_tri_append_equal)) * ac) + (mdr_a_pfp_tri_append_equal))) -> (((exists ff_h_mdr_pfp_tri_append_equaln. ff_h_mdr_pfp_tri_append_equaln + S (mdr_a_pfp_tri_append_equal) = S ((S (mdr_i_pfp_tri_append_equal)) * AC)) /\ exists ff_q_mdr_pfp_tri_append_equaln. AB = ff_q_mdr_pfp_tri_append_equaln * S ((S (mdr_i_pfp_tri_append_equal)) * AC) + (mdr_a_pfp_tri_append_equal)))) -> (exists pfa_gap_tri_append_earlier_index. pfa_gap_tri_append_earlier_index + S (i) = (N)) -> (exists pfc_terms_code_tri_append_earlier_old pfc_terms_scale_tri_append_earlier_old pfc_natural_sum_tri_append_earlier_old. ((forall pfc_index_tri_append_earlier_olddiagonal. (exists pfa_gap_tri_append_earlier_olddiagonalbound. pfa_gap_tri_append_earlier_olddiagonalbound + S (pfc_index_tri_append_earlier_olddiagonal) = (S (i))) -> exists pfc_value_tri_append_earlier_olddiagonal. ((((exists ff_h_pfp_tri_append_earlier_olddiagonalentry. ff_h_pfp_tri_append_earlier_olddiagonalentry + S (pfc_value_tri_append_earlier_olddiagonal) = S ((S (pfc_index_tri_append_earlier_olddiagonal)) * pfc_terms_scale_tri_append_earlier_old)) /\ exists ff_q_pfp_tri_append_earlier_olddiagonalentry. pfc_terms_code_tri_append_earlier_old = ff_q_pfp_tri_append_earlier_olddiagonalentry * S ((S (pfc_index_tri_append_earlier_olddiagonal)) * pfc_terms_scale_tri_append_earlier_old) + (pfc_value_tri_append_earlier_olddiagonal))) /\ ((exists pfc_complement_tri_append_earlier_olddiagonalterm pfc_left_tri_append_earlier_olddiagonalterm pfc_right_tri_append_earlier_olddiagonalterm. (((pfc_index_tri_append_earlier_olddiagonal)+pfc_complement_tri_append_earlier_olddiagonalterm=(i)) /\ ((((((exists pfa_gap_tri_append_earlier_olddiagonaltermleftinside. pfa_gap_tri_append_earlier_olddiagonaltermleftinside + S (pfc_index_tri_append_earlier_olddiagonal) = (N)) /\ ((((exists ff_h_pfp_tri_append_earlier_olddiagonaltermleftentry. ff_h_pfp_tri_append_earlier_olddiagonaltermleftentry + S (pfc_left_tri_append_earlier_olddiagonalterm) = S ((S (pfc_index_tri_append_earlier_olddiagonal)) * ac)) /\ exists ff_q_pfp_tri_append_earlier_olddiagonaltermleftentry. ab = ff_q_pfp_tri_append_earlier_olddiagonaltermleftentry * S ((S (pfc_index_tri_append_earlier_olddiagonal)) * ac) + (pfc_left_tri_append_earlier_olddiagonalterm)))))) \/ (((exists pfc_gap_tri_append_earlier_olddiagonaltermleftoutside. pfc_gap_tri_append_earlier_olddiagonaltermleftoutside+(N)=(pfc_index_tri_append_earlier_olddiagonal)) /\ (((pfc_left_tri_append_earlier_olddiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_append_earlier_olddiagonaltermrightinside. pfa_gap_tri_append_earlier_olddiagonaltermrightinside + S (pfc_complement_tri_append_earlier_olddiagonalterm) = (M)) /\ ((((exists ff_h_pfp_tri_append_earlier_olddiagonaltermrightentry. ff_h_pfp_tri_append_earlier_olddiagonaltermrightentry + S (pfc_right_tri_append_earlier_olddiagonalterm) = S ((S (pfc_complement_tri_append_earlier_olddiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_append_earlier_olddiagonaltermrightentry. bb = ff_q_pfp_tri_append_earlier_olddiagonaltermrightentry * S ((S (pfc_complement_tri_append_earlier_olddiagonalterm)) * bc) + (pfc_right_tri_append_earlier_olddiagonalterm)))))) \/ (((exists pfc_gap_tri_append_earlier_olddiagonaltermrightoutside. pfc_gap_tri_append_earlier_olddiagonaltermrightoutside+(M)=(pfc_complement_tri_append_earlier_olddiagonalterm)) /\ (((pfc_right_tri_append_earlier_olddiagonalterm)=0))))) /\ (((pfc_value_tri_append_earlier_olddiagonal)=pfc_left_tri_append_earlier_olddiagonalterm*pfc_right_tri_append_earlier_olddiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_append_earlier_oldsum fs_v_pfc_tri_append_earlier_oldsum. ((((exists fs_h_pfc_tri_append_earlier_oldsum_body_start. fs_h_pfc_tri_append_earlier_oldsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_append_earlier_oldsum)) /\ exists fs_q_pfc_tri_append_earlier_oldsum_body_start. fs_u_pfc_tri_append_earlier_oldsum = fs_q_pfc_tri_append_earlier_oldsum_body_start * S ((S (0)) * fs_v_pfc_tri_append_earlier_oldsum) + (0))) /\ ((((exists fs_h_pfc_tri_append_earlier_oldsum_body_terminal. fs_h_pfc_tri_append_earlier_oldsum_body_terminal + S (pfc_natural_sum_tri_append_earlier_old) = S ((S (S (i))) * fs_v_pfc_tri_append_earlier_oldsum)) /\ exists fs_q_pfc_tri_append_earlier_oldsum_body_terminal. fs_u_pfc_tri_append_earlier_oldsum = fs_q_pfc_tri_append_earlier_oldsum_body_terminal * S ((S (S (i))) * fs_v_pfc_tri_append_earlier_oldsum) + (pfc_natural_sum_tri_append_earlier_old))) /\ forall fs_i_pfc_tri_append_earlier_oldsum_body_steps. (exists fs_lt_pfc_tri_append_earlier_oldsum_body_steps_bound. fs_lt_pfc_tri_append_earlier_oldsum_body_steps_bound + S fs_i_pfc_tri_append_earlier_oldsum_body_steps = S (i)) -> exists fs_a_pfc_tri_append_earlier_oldsum_body_steps fs_r_pfc_tri_append_earlier_oldsum_body_steps fs_s_pfc_tri_append_earlier_oldsum_body_steps. ((((exists fs_h_pfc_tri_append_earlier_oldsum_body_steps_summand. fs_h_pfc_tri_append_earlier_oldsum_body_steps_summand + S (fs_a_pfc_tri_append_earlier_oldsum_body_steps) = S ((S (fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * pfc_terms_scale_tri_append_earlier_old)) /\ exists fs_q_pfc_tri_append_earlier_oldsum_body_steps_summand. pfc_terms_code_tri_append_earlier_old = fs_q_pfc_tri_append_earlier_oldsum_body_steps_summand * S ((S (fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * pfc_terms_scale_tri_append_earlier_old) + (fs_a_pfc_tri_append_earlier_oldsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_earlier_oldsum_body_steps_partial. fs_h_pfc_tri_append_earlier_oldsum_body_steps_partial + S (fs_r_pfc_tri_append_earlier_oldsum_body_steps) = S ((S (fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * fs_v_pfc_tri_append_earlier_oldsum)) /\ exists fs_q_pfc_tri_append_earlier_oldsum_body_steps_partial. fs_u_pfc_tri_append_earlier_oldsum = fs_q_pfc_tri_append_earlier_oldsum_body_steps_partial * S ((S (fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * fs_v_pfc_tri_append_earlier_oldsum) + (fs_r_pfc_tri_append_earlier_oldsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_earlier_oldsum_body_steps_successor. fs_h_pfc_tri_append_earlier_oldsum_body_steps_successor + S (fs_s_pfc_tri_append_earlier_oldsum_body_steps) = S ((S (S fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * fs_v_pfc_tri_append_earlier_oldsum)) /\ exists fs_q_pfc_tri_append_earlier_oldsum_body_steps_successor. fs_u_pfc_tri_append_earlier_oldsum = fs_q_pfc_tri_append_earlier_oldsum_body_steps_successor * S ((S (S fs_i_pfc_tri_append_earlier_oldsum_body_steps)) * fs_v_pfc_tri_append_earlier_oldsum) + (fs_s_pfc_tri_append_earlier_oldsum_body_steps))) /\ fs_s_pfc_tri_append_earlier_oldsum_body_steps = fs_r_pfc_tri_append_earlier_oldsum_body_steps + fs_a_pfc_tri_append_earlier_oldsum_body_steps)))))) /\ ((((exists pfa_gap_tri_append_earlier_oldresiduebound. pfa_gap_tri_append_earlier_oldresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_append_earlier_oldresiduecongruence pfa_offset_right_tri_append_earlier_oldresiduecongruence. (pfc_natural_sum_tri_append_earlier_old) + (p) * pfa_offset_left_tri_append_earlier_oldresiduecongruence = (r) + (p) * pfa_offset_right_tri_append_earlier_oldresiduecongruence))))))))) -> (exists pfc_terms_code_tri_append_earlier_new pfc_terms_scale_tri_append_earlier_new pfc_natural_sum_tri_append_earlier_new. ((forall pfc_index_tri_append_earlier_newdiagonal. (exists pfa_gap_tri_append_earlier_newdiagonalbound. pfa_gap_tri_append_earlier_newdiagonalbound + S (pfc_index_tri_append_earlier_newdiagonal) = (S (i))) -> exists pfc_value_tri_append_earlier_newdiagonal. ((((exists ff_h_pfp_tri_append_earlier_newdiagonalentry. ff_h_pfp_tri_append_earlier_newdiagonalentry + S (pfc_value_tri_append_earlier_newdiagonal) = S ((S (pfc_index_tri_append_earlier_newdiagonal)) * pfc_terms_scale_tri_append_earlier_new)) /\ exists ff_q_pfp_tri_append_earlier_newdiagonalentry. pfc_terms_code_tri_append_earlier_new = ff_q_pfp_tri_append_earlier_newdiagonalentry * S ((S (pfc_index_tri_append_earlier_newdiagonal)) * pfc_terms_scale_tri_append_earlier_new) + (pfc_value_tri_append_earlier_newdiagonal))) /\ ((exists pfc_complement_tri_append_earlier_newdiagonalterm pfc_left_tri_append_earlier_newdiagonalterm pfc_right_tri_append_earlier_newdiagonalterm. (((pfc_index_tri_append_earlier_newdiagonal)+pfc_complement_tri_append_earlier_newdiagonalterm=(i)) /\ ((((((exists pfa_gap_tri_append_earlier_newdiagonaltermleftinside. pfa_gap_tri_append_earlier_newdiagonaltermleftinside + S (pfc_index_tri_append_earlier_newdiagonal) = (S N)) /\ ((((exists ff_h_pfp_tri_append_earlier_newdiagonaltermleftentry. ff_h_pfp_tri_append_earlier_newdiagonaltermleftentry + S (pfc_left_tri_append_earlier_newdiagonalterm) = S ((S (pfc_index_tri_append_earlier_newdiagonal)) * AC)) /\ exists ff_q_pfp_tri_append_earlier_newdiagonaltermleftentry. AB = ff_q_pfp_tri_append_earlier_newdiagonaltermleftentry * S ((S (pfc_index_tri_append_earlier_newdiagonal)) * AC) + (pfc_left_tri_append_earlier_newdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_earlier_newdiagonaltermleftoutside. pfc_gap_tri_append_earlier_newdiagonaltermleftoutside+(S N)=(pfc_index_tri_append_earlier_newdiagonal)) /\ (((pfc_left_tri_append_earlier_newdiagonalterm)=0))))) /\ ((((((exists pfa_gap_tri_append_earlier_newdiagonaltermrightinside. pfa_gap_tri_append_earlier_newdiagonaltermrightinside + S (pfc_complement_tri_append_earlier_newdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_tri_append_earlier_newdiagonaltermrightentry. ff_h_pfp_tri_append_earlier_newdiagonaltermrightentry + S (pfc_right_tri_append_earlier_newdiagonalterm) = S ((S (pfc_complement_tri_append_earlier_newdiagonalterm)) * bc)) /\ exists ff_q_pfp_tri_append_earlier_newdiagonaltermrightentry. bb = ff_q_pfp_tri_append_earlier_newdiagonaltermrightentry * S ((S (pfc_complement_tri_append_earlier_newdiagonalterm)) * bc) + (pfc_right_tri_append_earlier_newdiagonalterm)))))) \/ (((exists pfc_gap_tri_append_earlier_newdiagonaltermrightoutside. pfc_gap_tri_append_earlier_newdiagonaltermrightoutside+(M)=(pfc_complement_tri_append_earlier_newdiagonalterm)) /\ (((pfc_right_tri_append_earlier_newdiagonalterm)=0))))) /\ (((pfc_value_tri_append_earlier_newdiagonal)=pfc_left_tri_append_earlier_newdiagonalterm*pfc_right_tri_append_earlier_newdiagonalterm))))))))))) /\ (((exists fs_u_pfc_tri_append_earlier_newsum fs_v_pfc_tri_append_earlier_newsum. ((((exists fs_h_pfc_tri_append_earlier_newsum_body_start. fs_h_pfc_tri_append_earlier_newsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_tri_append_earlier_newsum)) /\ exists fs_q_pfc_tri_append_earlier_newsum_body_start. fs_u_pfc_tri_append_earlier_newsum = fs_q_pfc_tri_append_earlier_newsum_body_start * S ((S (0)) * fs_v_pfc_tri_append_earlier_newsum) + (0))) /\ ((((exists fs_h_pfc_tri_append_earlier_newsum_body_terminal. fs_h_pfc_tri_append_earlier_newsum_body_terminal + S (pfc_natural_sum_tri_append_earlier_new) = S ((S (S (i))) * fs_v_pfc_tri_append_earlier_newsum)) /\ exists fs_q_pfc_tri_append_earlier_newsum_body_terminal. fs_u_pfc_tri_append_earlier_newsum = fs_q_pfc_tri_append_earlier_newsum_body_terminal * S ((S (S (i))) * fs_v_pfc_tri_append_earlier_newsum) + (pfc_natural_sum_tri_append_earlier_new))) /\ forall fs_i_pfc_tri_append_earlier_newsum_body_steps. (exists fs_lt_pfc_tri_append_earlier_newsum_body_steps_bound. fs_lt_pfc_tri_append_earlier_newsum_body_steps_bound + S fs_i_pfc_tri_append_earlier_newsum_body_steps = S (i)) -> exists fs_a_pfc_tri_append_earlier_newsum_body_steps fs_r_pfc_tri_append_earlier_newsum_body_steps fs_s_pfc_tri_append_earlier_newsum_body_steps. ((((exists fs_h_pfc_tri_append_earlier_newsum_body_steps_summand. fs_h_pfc_tri_append_earlier_newsum_body_steps_summand + S (fs_a_pfc_tri_append_earlier_newsum_body_steps) = S ((S (fs_i_pfc_tri_append_earlier_newsum_body_steps)) * pfc_terms_scale_tri_append_earlier_new)) /\ exists fs_q_pfc_tri_append_earlier_newsum_body_steps_summand. pfc_terms_code_tri_append_earlier_new = fs_q_pfc_tri_append_earlier_newsum_body_steps_summand * S ((S (fs_i_pfc_tri_append_earlier_newsum_body_steps)) * pfc_terms_scale_tri_append_earlier_new) + (fs_a_pfc_tri_append_earlier_newsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_earlier_newsum_body_steps_partial. fs_h_pfc_tri_append_earlier_newsum_body_steps_partial + S (fs_r_pfc_tri_append_earlier_newsum_body_steps) = S ((S (fs_i_pfc_tri_append_earlier_newsum_body_steps)) * fs_v_pfc_tri_append_earlier_newsum)) /\ exists fs_q_pfc_tri_append_earlier_newsum_body_steps_partial. fs_u_pfc_tri_append_earlier_newsum = fs_q_pfc_tri_append_earlier_newsum_body_steps_partial * S ((S (fs_i_pfc_tri_append_earlier_newsum_body_steps)) * fs_v_pfc_tri_append_earlier_newsum) + (fs_r_pfc_tri_append_earlier_newsum_body_steps))) /\ ((((exists fs_h_pfc_tri_append_earlier_newsum_body_steps_successor. fs_h_pfc_tri_append_earlier_newsum_body_steps_successor + S (fs_s_pfc_tri_append_earlier_newsum_body_steps) = S ((S (S fs_i_pfc_tri_append_earlier_newsum_body_steps)) * fs_v_pfc_tri_append_earlier_newsum)) /\ exists fs_q_pfc_tri_append_earlier_newsum_body_steps_successor. fs_u_pfc_tri_append_earlier_newsum = fs_q_pfc_tri_append_earlier_newsum_body_steps_successor * S ((S (S fs_i_pfc_tri_append_earlier_newsum_body_steps)) * fs_v_pfc_tri_append_earlier_newsum) + (fs_s_pfc_tri_append_earlier_newsum_body_steps))) /\ fs_s_pfc_tri_append_earlier_newsum_body_steps = fs_r_pfc_tri_append_earlier_newsum_body_steps + fs_a_pfc_tri_append_earlier_newsum_body_steps)))))) /\ ((((exists pfa_gap_tri_append_earlier_newresiduebound. pfa_gap_tri_append_earlier_newresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_tri_append_earlier_newresiduecongruence pfa_offset_right_tri_append_earlier_newresiduecongruence. (pfc_natural_sum_tri_append_earlier_new) + (p) * pfa_offset_left_tri_append_earlier_newresiduecongruence = (r) + (p) * pfa_offset_right_tri_append_earlier_newresiduecongruence)))))))))

Constructive proof overview

Generated structural guide

Appending one quotient coefficient cannot alter any already constructed earlier convolution coefficient.

The unchanged tactic script uses 3 declared prerequisites and contains 38 exact native proof lines.

Alpha v34 checked-use · first admitted v33 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

PX0003 prime_field_convolution_coefficient_prefix_transport le_refl Alpha theorem; checked-use authorized le_succ Alpha theorem; checked-use authorized

Direct dependents

none

Formal 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

38 script commands · 5 reading checkpoints · 0 local claims

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.

Named ingredients (1)

prime field convolution coefficient prefix transport

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.