PX0067

prime_field_convolution_coefficient_left_padding_right

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Construct an actual padded antidiagonal table and actual sum trace, proving the shifted coefficient has the same canonical residue without assuming an equality of sums.

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 L bb bc M BB BC t i r. (((forall pfp_repeat_index_coefficient_padding_rightzeros. (exists pfa_gap_coefficient_padding_rightzerosindex. pfa_gap_coefficient_padding_rightzerosindex + S (pfp_repeat_index_coefficient_padding_rightzeros) = (t)) -> (((exists ff_h_pfp_coefficient_padding_rightzerosentry. ff_h_pfp_coefficient_padding_rightzerosentry + S (0) = S ((S (pfp_repeat_index_coefficient_padding_rightzeros)) * BC)) /\ exists ff_q_pfp_coefficient_padding_rightzerosentry. BB = ff_q_pfp_coefficient_padding_rightzerosentry * S ((S (pfp_repeat_index_coefficient_padding_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_coefficient_padding_right pfrep_value_coefficient_padding_right. (exists pfa_gap_coefficient_padding_rightbound. pfa_gap_coefficient_padding_rightbound + S (pfrep_index_coefficient_padding_right) = (M)) -> (((exists ff_h_pfp_coefficient_padding_rightinput. ff_h_pfp_coefficient_padding_rightinput + S (pfrep_value_coefficient_padding_right) = S ((S (pfrep_index_coefficient_padding_right)) * bc)) /\ exists ff_q_pfp_coefficient_padding_rightinput. bb = ff_q_pfp_coefficient_padding_rightinput * S ((S (pfrep_index_coefficient_padding_right)) * bc) + (pfrep_value_coefficient_padding_right))) -> (((exists ff_h_pfp_coefficient_padding_rightoutput. ff_h_pfp_coefficient_padding_rightoutput + S (pfrep_value_coefficient_padding_right) = S ((S ((t)+pfrep_index_coefficient_padding_right)) * BC)) /\ exists ff_q_pfp_coefficient_padding_rightoutput. BB = ff_q_pfp_coefficient_padding_rightoutput * S ((S ((t)+pfrep_index_coefficient_padding_right)) * BC) + (pfrep_value_coefficient_padding_right))))))) -> (exists pfc_terms_code_coefficient_original_right pfc_terms_scale_coefficient_original_right pfc_natural_sum_coefficient_original_right. ((forall pfc_index_coefficient_original_rightdiagonal. (exists pfa_gap_coefficient_original_rightdiagonalbound. pfa_gap_coefficient_original_rightdiagonalbound + S (pfc_index_coefficient_original_rightdiagonal) = (S (i))) -> exists pfc_value_coefficient_original_rightdiagonal. ((((exists ff_h_pfp_coefficient_original_rightdiagonalentry. ff_h_pfp_coefficient_original_rightdiagonalentry + S (pfc_value_coefficient_original_rightdiagonal) = S ((S (pfc_index_coefficient_original_rightdiagonal)) * pfc_terms_scale_coefficient_original_right)) /\ exists ff_q_pfp_coefficient_original_rightdiagonalentry. pfc_terms_code_coefficient_original_right = ff_q_pfp_coefficient_original_rightdiagonalentry * S ((S (pfc_index_coefficient_original_rightdiagonal)) * pfc_terms_scale_coefficient_original_right) + (pfc_value_coefficient_original_rightdiagonal))) /\ ((exists pfc_complement_coefficient_original_rightdiagonalterm pfc_left_coefficient_original_rightdiagonalterm pfc_right_coefficient_original_rightdiagonalterm. (((pfc_index_coefficient_original_rightdiagonal)+pfc_complement_coefficient_original_rightdiagonalterm=(i)) /\ ((((((exists pfa_gap_coefficient_original_rightdiagonaltermleftinside. pfa_gap_coefficient_original_rightdiagonaltermleftinside + S (pfc_index_coefficient_original_rightdiagonal) = (L)) /\ ((((exists ff_h_pfp_coefficient_original_rightdiagonaltermleftentry. ff_h_pfp_coefficient_original_rightdiagonaltermleftentry + S (pfc_left_coefficient_original_rightdiagonalterm) = S ((S (pfc_index_coefficient_original_rightdiagonal)) * ac)) /\ exists ff_q_pfp_coefficient_original_rightdiagonaltermleftentry. ab = ff_q_pfp_coefficient_original_rightdiagonaltermleftentry * S ((S (pfc_index_coefficient_original_rightdiagonal)) * ac) + (pfc_left_coefficient_original_rightdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_original_rightdiagonaltermleftoutside. pfc_gap_coefficient_original_rightdiagonaltermleftoutside+(L)=(pfc_index_coefficient_original_rightdiagonal)) /\ (((pfc_left_coefficient_original_rightdiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_original_rightdiagonaltermrightinside. pfa_gap_coefficient_original_rightdiagonaltermrightinside + S (pfc_complement_coefficient_original_rightdiagonalterm) = (M)) /\ ((((exists ff_h_pfp_coefficient_original_rightdiagonaltermrightentry. ff_h_pfp_coefficient_original_rightdiagonaltermrightentry + S (pfc_right_coefficient_original_rightdiagonalterm) = S ((S (pfc_complement_coefficient_original_rightdiagonalterm)) * bc)) /\ exists ff_q_pfp_coefficient_original_rightdiagonaltermrightentry. bb = ff_q_pfp_coefficient_original_rightdiagonaltermrightentry * S ((S (pfc_complement_coefficient_original_rightdiagonalterm)) * bc) + (pfc_right_coefficient_original_rightdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_original_rightdiagonaltermrightoutside. pfc_gap_coefficient_original_rightdiagonaltermrightoutside+(M)=(pfc_complement_coefficient_original_rightdiagonalterm)) /\ (((pfc_right_coefficient_original_rightdiagonalterm)=0))))) /\ (((pfc_value_coefficient_original_rightdiagonal)=pfc_left_coefficient_original_rightdiagonalterm*pfc_right_coefficient_original_rightdiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_original_rightsum fs_v_pfc_coefficient_original_rightsum. ((((exists fs_h_pfc_coefficient_original_rightsum_body_start. fs_h_pfc_coefficient_original_rightsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_original_rightsum)) /\ exists fs_q_pfc_coefficient_original_rightsum_body_start. fs_u_pfc_coefficient_original_rightsum = fs_q_pfc_coefficient_original_rightsum_body_start * S ((S (0)) * fs_v_pfc_coefficient_original_rightsum) + (0))) /\ ((((exists fs_h_pfc_coefficient_original_rightsum_body_terminal. fs_h_pfc_coefficient_original_rightsum_body_terminal + S (pfc_natural_sum_coefficient_original_right) = S ((S (S (i))) * fs_v_pfc_coefficient_original_rightsum)) /\ exists fs_q_pfc_coefficient_original_rightsum_body_terminal. fs_u_pfc_coefficient_original_rightsum = fs_q_pfc_coefficient_original_rightsum_body_terminal * S ((S (S (i))) * fs_v_pfc_coefficient_original_rightsum) + (pfc_natural_sum_coefficient_original_right))) /\ forall fs_i_pfc_coefficient_original_rightsum_body_steps. (exists fs_lt_pfc_coefficient_original_rightsum_body_steps_bound. fs_lt_pfc_coefficient_original_rightsum_body_steps_bound + S fs_i_pfc_coefficient_original_rightsum_body_steps = S (i)) -> exists fs_a_pfc_coefficient_original_rightsum_body_steps fs_r_pfc_coefficient_original_rightsum_body_steps fs_s_pfc_coefficient_original_rightsum_body_steps. ((((exists fs_h_pfc_coefficient_original_rightsum_body_steps_summand. fs_h_pfc_coefficient_original_rightsum_body_steps_summand + S (fs_a_pfc_coefficient_original_rightsum_body_steps) = S ((S (fs_i_pfc_coefficient_original_rightsum_body_steps)) * pfc_terms_scale_coefficient_original_right)) /\ exists fs_q_pfc_coefficient_original_rightsum_body_steps_summand. pfc_terms_code_coefficient_original_right = fs_q_pfc_coefficient_original_rightsum_body_steps_summand * S ((S (fs_i_pfc_coefficient_original_rightsum_body_steps)) * pfc_terms_scale_coefficient_original_right) + (fs_a_pfc_coefficient_original_rightsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_original_rightsum_body_steps_partial. fs_h_pfc_coefficient_original_rightsum_body_steps_partial + S (fs_r_pfc_coefficient_original_rightsum_body_steps) = S ((S (fs_i_pfc_coefficient_original_rightsum_body_steps)) * fs_v_pfc_coefficient_original_rightsum)) /\ exists fs_q_pfc_coefficient_original_rightsum_body_steps_partial. fs_u_pfc_coefficient_original_rightsum = fs_q_pfc_coefficient_original_rightsum_body_steps_partial * S ((S (fs_i_pfc_coefficient_original_rightsum_body_steps)) * fs_v_pfc_coefficient_original_rightsum) + (fs_r_pfc_coefficient_original_rightsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_original_rightsum_body_steps_successor. fs_h_pfc_coefficient_original_rightsum_body_steps_successor + S (fs_s_pfc_coefficient_original_rightsum_body_steps) = S ((S (S fs_i_pfc_coefficient_original_rightsum_body_steps)) * fs_v_pfc_coefficient_original_rightsum)) /\ exists fs_q_pfc_coefficient_original_rightsum_body_steps_successor. fs_u_pfc_coefficient_original_rightsum = fs_q_pfc_coefficient_original_rightsum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_original_rightsum_body_steps)) * fs_v_pfc_coefficient_original_rightsum) + (fs_s_pfc_coefficient_original_rightsum_body_steps))) /\ fs_s_pfc_coefficient_original_rightsum_body_steps = fs_r_pfc_coefficient_original_rightsum_body_steps + fs_a_pfc_coefficient_original_rightsum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_original_rightresiduebound. pfa_gap_coefficient_original_rightresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_coefficient_original_rightresiduecongruence pfa_offset_right_coefficient_original_rightresiduecongruence. (pfc_natural_sum_coefficient_original_right) + (p) * pfa_offset_left_coefficient_original_rightresiduecongruence = (r) + (p) * pfa_offset_right_coefficient_original_rightresiduecongruence))))))))) -> (exists pfc_terms_code_coefficient_shifted_right pfc_terms_scale_coefficient_shifted_right pfc_natural_sum_coefficient_shifted_right. ((forall pfc_index_coefficient_shifted_rightdiagonal. (exists pfa_gap_coefficient_shifted_rightdiagonalbound. pfa_gap_coefficient_shifted_rightdiagonalbound + S (pfc_index_coefficient_shifted_rightdiagonal) = (S (t+i))) -> exists pfc_value_coefficient_shifted_rightdiagonal. ((((exists ff_h_pfp_coefficient_shifted_rightdiagonalentry. ff_h_pfp_coefficient_shifted_rightdiagonalentry + S (pfc_value_coefficient_shifted_rightdiagonal) = S ((S (pfc_index_coefficient_shifted_rightdiagonal)) * pfc_terms_scale_coefficient_shifted_right)) /\ exists ff_q_pfp_coefficient_shifted_rightdiagonalentry. pfc_terms_code_coefficient_shifted_right = ff_q_pfp_coefficient_shifted_rightdiagonalentry * S ((S (pfc_index_coefficient_shifted_rightdiagonal)) * pfc_terms_scale_coefficient_shifted_right) + (pfc_value_coefficient_shifted_rightdiagonal))) /\ ((exists pfc_complement_coefficient_shifted_rightdiagonalterm pfc_left_coefficient_shifted_rightdiagonalterm pfc_right_coefficient_shifted_rightdiagonalterm. (((pfc_index_coefficient_shifted_rightdiagonal)+pfc_complement_coefficient_shifted_rightdiagonalterm=(t+i)) /\ ((((((exists pfa_gap_coefficient_shifted_rightdiagonaltermleftinside. pfa_gap_coefficient_shifted_rightdiagonaltermleftinside + S (pfc_index_coefficient_shifted_rightdiagonal) = (L)) /\ ((((exists ff_h_pfp_coefficient_shifted_rightdiagonaltermleftentry. ff_h_pfp_coefficient_shifted_rightdiagonaltermleftentry + S (pfc_left_coefficient_shifted_rightdiagonalterm) = S ((S (pfc_index_coefficient_shifted_rightdiagonal)) * ac)) /\ exists ff_q_pfp_coefficient_shifted_rightdiagonaltermleftentry. ab = ff_q_pfp_coefficient_shifted_rightdiagonaltermleftentry * S ((S (pfc_index_coefficient_shifted_rightdiagonal)) * ac) + (pfc_left_coefficient_shifted_rightdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_shifted_rightdiagonaltermleftoutside. pfc_gap_coefficient_shifted_rightdiagonaltermleftoutside+(L)=(pfc_index_coefficient_shifted_rightdiagonal)) /\ (((pfc_left_coefficient_shifted_rightdiagonalterm)=0))))) /\ ((((((exists pfa_gap_coefficient_shifted_rightdiagonaltermrightinside. pfa_gap_coefficient_shifted_rightdiagonaltermrightinside + S (pfc_complement_coefficient_shifted_rightdiagonalterm) = (t+M)) /\ ((((exists ff_h_pfp_coefficient_shifted_rightdiagonaltermrightentry. ff_h_pfp_coefficient_shifted_rightdiagonaltermrightentry + S (pfc_right_coefficient_shifted_rightdiagonalterm) = S ((S (pfc_complement_coefficient_shifted_rightdiagonalterm)) * BC)) /\ exists ff_q_pfp_coefficient_shifted_rightdiagonaltermrightentry. BB = ff_q_pfp_coefficient_shifted_rightdiagonaltermrightentry * S ((S (pfc_complement_coefficient_shifted_rightdiagonalterm)) * BC) + (pfc_right_coefficient_shifted_rightdiagonalterm)))))) \/ (((exists pfc_gap_coefficient_shifted_rightdiagonaltermrightoutside. pfc_gap_coefficient_shifted_rightdiagonaltermrightoutside+(t+M)=(pfc_complement_coefficient_shifted_rightdiagonalterm)) /\ (((pfc_right_coefficient_shifted_rightdiagonalterm)=0))))) /\ (((pfc_value_coefficient_shifted_rightdiagonal)=pfc_left_coefficient_shifted_rightdiagonalterm*pfc_right_coefficient_shifted_rightdiagonalterm))))))))))) /\ (((exists fs_u_pfc_coefficient_shifted_rightsum fs_v_pfc_coefficient_shifted_rightsum. ((((exists fs_h_pfc_coefficient_shifted_rightsum_body_start. fs_h_pfc_coefficient_shifted_rightsum_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_shifted_rightsum)) /\ exists fs_q_pfc_coefficient_shifted_rightsum_body_start. fs_u_pfc_coefficient_shifted_rightsum = fs_q_pfc_coefficient_shifted_rightsum_body_start * S ((S (0)) * fs_v_pfc_coefficient_shifted_rightsum) + (0))) /\ ((((exists fs_h_pfc_coefficient_shifted_rightsum_body_terminal. fs_h_pfc_coefficient_shifted_rightsum_body_terminal + S (pfc_natural_sum_coefficient_shifted_right) = S ((S (S (t+i))) * fs_v_pfc_coefficient_shifted_rightsum)) /\ exists fs_q_pfc_coefficient_shifted_rightsum_body_terminal. fs_u_pfc_coefficient_shifted_rightsum = fs_q_pfc_coefficient_shifted_rightsum_body_terminal * S ((S (S (t+i))) * fs_v_pfc_coefficient_shifted_rightsum) + (pfc_natural_sum_coefficient_shifted_right))) /\ forall fs_i_pfc_coefficient_shifted_rightsum_body_steps. (exists fs_lt_pfc_coefficient_shifted_rightsum_body_steps_bound. fs_lt_pfc_coefficient_shifted_rightsum_body_steps_bound + S fs_i_pfc_coefficient_shifted_rightsum_body_steps = S (t+i)) -> exists fs_a_pfc_coefficient_shifted_rightsum_body_steps fs_r_pfc_coefficient_shifted_rightsum_body_steps fs_s_pfc_coefficient_shifted_rightsum_body_steps. ((((exists fs_h_pfc_coefficient_shifted_rightsum_body_steps_summand. fs_h_pfc_coefficient_shifted_rightsum_body_steps_summand + S (fs_a_pfc_coefficient_shifted_rightsum_body_steps) = S ((S (fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * pfc_terms_scale_coefficient_shifted_right)) /\ exists fs_q_pfc_coefficient_shifted_rightsum_body_steps_summand. pfc_terms_code_coefficient_shifted_right = fs_q_pfc_coefficient_shifted_rightsum_body_steps_summand * S ((S (fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * pfc_terms_scale_coefficient_shifted_right) + (fs_a_pfc_coefficient_shifted_rightsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_shifted_rightsum_body_steps_partial. fs_h_pfc_coefficient_shifted_rightsum_body_steps_partial + S (fs_r_pfc_coefficient_shifted_rightsum_body_steps) = S ((S (fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * fs_v_pfc_coefficient_shifted_rightsum)) /\ exists fs_q_pfc_coefficient_shifted_rightsum_body_steps_partial. fs_u_pfc_coefficient_shifted_rightsum = fs_q_pfc_coefficient_shifted_rightsum_body_steps_partial * S ((S (fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * fs_v_pfc_coefficient_shifted_rightsum) + (fs_r_pfc_coefficient_shifted_rightsum_body_steps))) /\ ((((exists fs_h_pfc_coefficient_shifted_rightsum_body_steps_successor. fs_h_pfc_coefficient_shifted_rightsum_body_steps_successor + S (fs_s_pfc_coefficient_shifted_rightsum_body_steps) = S ((S (S fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * fs_v_pfc_coefficient_shifted_rightsum)) /\ exists fs_q_pfc_coefficient_shifted_rightsum_body_steps_successor. fs_u_pfc_coefficient_shifted_rightsum = fs_q_pfc_coefficient_shifted_rightsum_body_steps_successor * S ((S (S fs_i_pfc_coefficient_shifted_rightsum_body_steps)) * fs_v_pfc_coefficient_shifted_rightsum) + (fs_s_pfc_coefficient_shifted_rightsum_body_steps))) /\ fs_s_pfc_coefficient_shifted_rightsum_body_steps = fs_r_pfc_coefficient_shifted_rightsum_body_steps + fs_a_pfc_coefficient_shifted_rightsum_body_steps)))))) /\ ((((exists pfa_gap_coefficient_shifted_rightresiduebound. pfa_gap_coefficient_shifted_rightresiduebound + S (r) = (p)) /\ ((exists pfa_offset_left_coefficient_shifted_rightresiduecongruence pfa_offset_right_coefficient_shifted_rightresiduecongruence. (pfc_natural_sum_coefficient_shifted_right) + (p) * pfa_offset_left_coefficient_shifted_rightresiduecongruence = (r) + (p) * pfa_offset_right_coefficient_shifted_rightresiduecongruence)))))))))

Constructive proof overview

Generated structural guide

Construct an actual padded antidiagonal table and actual sum trace, proving the shifted coefficient has the same canonical residue without assuming an equality of sums.

The unchanged tactic script uses 6 declared prerequisites and contains 85 exact native proof lines.

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

Proof neighborhood

Direct dependencies

polynomial_diagonal_prefix_exists Alpha theorem; checked-use authorized beta_sum_exists Alpha theorem; checked-use authorized PX0065 polynomial_diagonal_left_padding_right PX005F polynomial_zero_tail_natural_sum_invariant add_succ_left Alpha theorem; checked-use authorized add_comm Alpha theorem; checked-use authorized

Direct dependents

PX006D prime_field_polynomial_convolution_left_padding_nonempty_right

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

85 script commands · 20 reading checkpoints · 5 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 (2)
polynomial diagonal left padding rightpolynomial zero tail natural sum invariant

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro ab
  3. L3
    intro ac
  4. L4
    intro L
  5. L5
    intro bb
  6. L6
    intro bc
  7. L7
    intro M
  8. L8
    intro BB
  9. L9
    intro BC
  10. L10
    intro t
02Fix variables and assumptionsL11–14

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

  1. L11
    intro i
  2. L12
    intro r
  3. L13
    intro hpad
  4. L14
    intro hc
03Separate the logical casesL15–19

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L15
    cases hc
  2. L16
    cases hc_witness
  3. L17
    cases hc_witness_witness
  4. L18
    cases hc_witness_witness_witness
  5. L19
    cases hc_witness_witness_witness_right
04Establish hdL20–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial diagonal prefix exists.

  1. L20
    have hd : ∃ eb. ∃ ec. PolynomialDiagonalPrefix(ab,ac,L,BB,BC,t + M,t + i,eb,ec,S (t + i))Definitions: PolynomialDiagonalPrefix
  2. L21
    specialize polynomial_diagonal_prefix_exists (ab)
  3. L22
    specialize polynomial_diagonal_prefix_exists (ac)
  4. L23
    specialize polynomial_diagonal_prefix_exists (L)
  5. L24
    specialize polynomial_diagonal_prefix_exists (BB)
  6. L25
    specialize polynomial_diagonal_prefix_exists (BC)
  7. L26
    specialize polynomial_diagonal_prefix_exists (t+M)
  8. L27
    specialize polynomial_diagonal_prefix_exists (t+i)
  9. L28
    apply polynomial_diagonal_prefix_exists
05Separate the logical casesL29–30

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    cases hd
  2. L30
    cases hd_witness
06Establish hsL31–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta sum exists.

  1. L31
    have hs : ∃ n. Sum(x3,x4,S (t + i),n)Definitions: Sum
  2. L32
    specialize beta_sum_exists (x3)
  3. L33
    specialize beta_sum_exists (x4)
  4. L34
    specialize beta_sum_exists (S (t+i))
  5. L35
    apply beta_sum_exists
07Separate the logical casesL36–36

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L36
    cases hs
08Establish hdataL37–46

Establish this local claim before using it. It is not an additional assumption.

  1. L37
    have hdata : BetaPrefixEqual(x,x1,x3,x4,S i) ∧ (∀ y. Lt(y,t) → BetaAt(x3,x4,S i + y,0))Definitions: BetaPrefixEqualLtBetaAt
  2. L38
    specialize polynomial_diagonal_left_padding_right (ab)
  3. L39
    specialize polynomial_diagonal_left_padding_right (ac)
  4. L40
    specialize polynomial_diagonal_left_padding_right (L)
  5. L41
    specialize polynomial_diagonal_left_padding_right (bb)
  6. L42
    specialize polynomial_diagonal_left_padding_right (bc)
  7. L43
    specialize polynomial_diagonal_left_padding_right (M)
  8. L44
    specialize polynomial_diagonal_left_padding_right (BB)
  9. L45
    specialize polynomial_diagonal_left_padding_right (BC)
  10. L46
    specialize polynomial_diagonal_left_padding_right (t)
09Use earlier factsL47–55

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L47
    specialize polynomial_diagonal_left_padding_right (i)
  2. L48
    specialize polynomial_diagonal_left_padding_right (x)
  3. L49
    specialize polynomial_diagonal_left_padding_right (x1)
  4. L50
    specialize polynomial_diagonal_left_padding_right (x3)
  5. L51
    specialize polynomial_diagonal_left_padding_right (x4)
  6. L52
    apply polynomial_diagonal_left_padding_right
  7. L53
    exact hpad
  8. L54
    exact hc_witness_witness_witness_left
  9. L55
    exact hd_witness_witness
10Establish heqL56–56

Establish this local claim before using it. It is not an additional assumption.

  1. L56
    have heq : x5=x2
11Separate the logical casesL57–57

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L57
    cases hdata
12Use earlier factsL58–67

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L58
    specialize polynomial_zero_tail_natural_sum_invariant (x)
  2. L59
    specialize polynomial_zero_tail_natural_sum_invariant (x1)
  3. L60
    specialize polynomial_zero_tail_natural_sum_invariant (x3)
  4. L61
    specialize polynomial_zero_tail_natural_sum_invariant (x4)
  5. L62
    specialize polynomial_zero_tail_natural_sum_invariant (S i)
  6. L63
    specialize polynomial_zero_tail_natural_sum_invariant (t)
  7. L64
    specialize polynomial_zero_tail_natural_sum_invariant (x2)
  8. L65
    specialize polynomial_zero_tail_natural_sum_invariant (x5)
  9. L66
    apply polynomial_zero_tail_natural_sum_invariant
  10. L67
    exact hdata_left
13Use earlier factsL68–69

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L68
    exact hdata_right
  2. L69
    exact hc_witness_witness_witness_right_left
14Establish hlengthL70–75

Establish this local claim before using it. It is not an additional assumption.

  1. L70
    have hlength : S i+t=S (t+i)
  2. L71
    simp [add_succ_left,add_comm]
  3. L72
    rewrite hlength
  4. L73
    rewrite hlength
  5. L74
    rewrite hlength
  6. L75
    exact hs_witness
15Construct an explicit witnessL76–78

Supply the displayed value, then prove that it has the required property.

  1. L76
    exists x3
  2. L77
    exists x4
  3. L78
    exists x2
16Separate the logical casesL79–79

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L79
    split
17Use earlier factsL80–80

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L80
    exact hd_witness_witness
18Separate the logical casesL81–81

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L81
    split
19Calculate and transport equalitiesL82–83

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L82
    rewrite heq at hs_witness
  2. L83
    rewrite heq at hs_witness
20Use earlier factsL84–85

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L84
    exact hs_witness
  2. L85
    exact hc_witness_witness_witness_right_right

Library-wide reading audit

Original exact command ledger · 85 lines
  1. 0001intro p
  2. 0002intro ab
  3. 0003intro ac
  4. 0004intro L
  5. 0005intro bb
  6. 0006intro bc
  7. 0007intro M
  8. 0008intro BB
  9. 0009intro BC
  10. 0010intro t
  11. 0011intro i
  12. 0012intro r
  13. 0013intro hpad
  14. 0014intro hc
  15. 0015cases hc
  16. 0016cases hc_witness
  17. 0017cases hc_witness_witness
  18. 0018cases hc_witness_witness_witness
  19. 0019cases hc_witness_witness_witness_right
  20. 0020have hd : exists eb ec. forall pfc_index_coefficient_padded_diagonal_right. (exists pfa_gap_coefficient_padded_diagonal_rightbound. pfa_gap_coefficient_padded_diagonal_rightbound + S (pfc_index_coefficient_padded_diagonal_right) = (S (t+i))) -> exists pfc_value_coefficient_padded_diagonal_right. ((((exists ff_h_pfp_coefficient_padded_diagonal_rightentry. ff_h_pfp_coefficient_padded_diagonal_rightentry + S (pfc_value_coefficient_padded_diagonal_right) = S ((S (pfc_index_coefficient_padded_diagonal_right)) * ec)) /\ exists ff_q_pfp_coefficient_padded_diagonal_rightentry. eb = ff_q_pfp_coefficient_padded_diagonal_rightentry * S ((S (pfc_index_coefficient_padded_diagonal_right)) * ec) + (pfc_value_coefficient_padded_diagonal_right))) /\ ((exists pfc_complement_coefficient_padded_diagonal_rightterm pfc_left_coefficient_padded_diagonal_rightterm pfc_right_coefficient_padded_diagonal_rightterm. (((pfc_index_coefficient_padded_diagonal_right)+pfc_complement_coefficient_padded_diagonal_rightterm=(t+i)) /\ ((((((exists pfa_gap_coefficient_padded_diagonal_righttermleftinside. pfa_gap_coefficient_padded_diagonal_righttermleftinside + S (pfc_index_coefficient_padded_diagonal_right) = (L)) /\ ((((exists ff_h_pfp_coefficient_padded_diagonal_righttermleftentry. ff_h_pfp_coefficient_padded_diagonal_righttermleftentry + S (pfc_left_coefficient_padded_diagonal_rightterm) = S ((S (pfc_index_coefficient_padded_diagonal_right)) * ac)) /\ exists ff_q_pfp_coefficient_padded_diagonal_righttermleftentry. ab = ff_q_pfp_coefficient_padded_diagonal_righttermleftentry * S ((S (pfc_index_coefficient_padded_diagonal_right)) * ac) + (pfc_left_coefficient_padded_diagonal_rightterm)))))) \/ (((exists pfc_gap_coefficient_padded_diagonal_righttermleftoutside. pfc_gap_coefficient_padded_diagonal_righttermleftoutside+(L)=(pfc_index_coefficient_padded_diagonal_right)) /\ (((pfc_left_coefficient_padded_diagonal_rightterm)=0))))) /\ ((((((exists pfa_gap_coefficient_padded_diagonal_righttermrightinside. pfa_gap_coefficient_padded_diagonal_righttermrightinside + S (pfc_complement_coefficient_padded_diagonal_rightterm) = (t+M)) /\ ((((exists ff_h_pfp_coefficient_padded_diagonal_righttermrightentry. ff_h_pfp_coefficient_padded_diagonal_righttermrightentry + S (pfc_right_coefficient_padded_diagonal_rightterm) = S ((S (pfc_complement_coefficient_padded_diagonal_rightterm)) * BC)) /\ exists ff_q_pfp_coefficient_padded_diagonal_righttermrightentry. BB = ff_q_pfp_coefficient_padded_diagonal_righttermrightentry * S ((S (pfc_complement_coefficient_padded_diagonal_rightterm)) * BC) + (pfc_right_coefficient_padded_diagonal_rightterm)))))) \/ (((exists pfc_gap_coefficient_padded_diagonal_righttermrightoutside. pfc_gap_coefficient_padded_diagonal_righttermrightoutside+(t+M)=(pfc_complement_coefficient_padded_diagonal_rightterm)) /\ (((pfc_right_coefficient_padded_diagonal_rightterm)=0))))) /\ (((pfc_value_coefficient_padded_diagonal_right)=pfc_left_coefficient_padded_diagonal_rightterm*pfc_right_coefficient_padded_diagonal_rightterm))))))))))
  21. 0021specialize polynomial_diagonal_prefix_exists (ab)
  22. 0022specialize polynomial_diagonal_prefix_exists (ac)
  23. 0023specialize polynomial_diagonal_prefix_exists (L)
  24. 0024specialize polynomial_diagonal_prefix_exists (BB)
  25. 0025specialize polynomial_diagonal_prefix_exists (BC)
  26. 0026specialize polynomial_diagonal_prefix_exists (t+M)
  27. 0027specialize polynomial_diagonal_prefix_exists (t+i)
  28. 0028apply polynomial_diagonal_prefix_exists
  29. 0029cases hd
  30. 0030cases hd_witness
  31. 0031have hs : exists n. exists fs_u_pfc_coefficient_padded_sum_right fs_v_pfc_coefficient_padded_sum_right. ((((exists fs_h_pfc_coefficient_padded_sum_right_body_start. fs_h_pfc_coefficient_padded_sum_right_body_start + S (0) = S ((S (0)) * fs_v_pfc_coefficient_padded_sum_right)) /\ exists fs_q_pfc_coefficient_padded_sum_right_body_start. fs_u_pfc_coefficient_padded_sum_right = fs_q_pfc_coefficient_padded_sum_right_body_start * S ((S (0)) * fs_v_pfc_coefficient_padded_sum_right) + (0))) /\ ((((exists fs_h_pfc_coefficient_padded_sum_right_body_terminal. fs_h_pfc_coefficient_padded_sum_right_body_terminal + S (n) = S ((S (S (t+i))) * fs_v_pfc_coefficient_padded_sum_right)) /\ exists fs_q_pfc_coefficient_padded_sum_right_body_terminal. fs_u_pfc_coefficient_padded_sum_right = fs_q_pfc_coefficient_padded_sum_right_body_terminal * S ((S (S (t+i))) * fs_v_pfc_coefficient_padded_sum_right) + (n))) /\ forall fs_i_pfc_coefficient_padded_sum_right_body_steps. (exists fs_lt_pfc_coefficient_padded_sum_right_body_steps_bound. fs_lt_pfc_coefficient_padded_sum_right_body_steps_bound + S fs_i_pfc_coefficient_padded_sum_right_body_steps = S (t+i)) -> exists fs_a_pfc_coefficient_padded_sum_right_body_steps fs_r_pfc_coefficient_padded_sum_right_body_steps fs_s_pfc_coefficient_padded_sum_right_body_steps. ((((exists fs_h_pfc_coefficient_padded_sum_right_body_steps_summand. fs_h_pfc_coefficient_padded_sum_right_body_steps_summand + S (fs_a_pfc_coefficient_padded_sum_right_body_steps) = S ((S (fs_i_pfc_coefficient_padded_sum_right_body_steps)) * x4)) /\ exists fs_q_pfc_coefficient_padded_sum_right_body_steps_summand. x3 = fs_q_pfc_coefficient_padded_sum_right_body_steps_summand * S ((S (fs_i_pfc_coefficient_padded_sum_right_body_steps)) * x4) + (fs_a_pfc_coefficient_padded_sum_right_body_steps))) /\ ((((exists fs_h_pfc_coefficient_padded_sum_right_body_steps_partial. fs_h_pfc_coefficient_padded_sum_right_body_steps_partial + S (fs_r_pfc_coefficient_padded_sum_right_body_steps) = S ((S (fs_i_pfc_coefficient_padded_sum_right_body_steps)) * fs_v_pfc_coefficient_padded_sum_right)) /\ exists fs_q_pfc_coefficient_padded_sum_right_body_steps_partial. fs_u_pfc_coefficient_padded_sum_right = fs_q_pfc_coefficient_padded_sum_right_body_steps_partial * S ((S (fs_i_pfc_coefficient_padded_sum_right_body_steps)) * fs_v_pfc_coefficient_padded_sum_right) + (fs_r_pfc_coefficient_padded_sum_right_body_steps))) /\ ((((exists fs_h_pfc_coefficient_padded_sum_right_body_steps_successor. fs_h_pfc_coefficient_padded_sum_right_body_steps_successor + S (fs_s_pfc_coefficient_padded_sum_right_body_steps) = S ((S (S fs_i_pfc_coefficient_padded_sum_right_body_steps)) * fs_v_pfc_coefficient_padded_sum_right)) /\ exists fs_q_pfc_coefficient_padded_sum_right_body_steps_successor. fs_u_pfc_coefficient_padded_sum_right = fs_q_pfc_coefficient_padded_sum_right_body_steps_successor * S ((S (S fs_i_pfc_coefficient_padded_sum_right_body_steps)) * fs_v_pfc_coefficient_padded_sum_right) + (fs_s_pfc_coefficient_padded_sum_right_body_steps))) /\ fs_s_pfc_coefficient_padded_sum_right_body_steps = fs_r_pfc_coefficient_padded_sum_right_body_steps + fs_a_pfc_coefficient_padded_sum_right_body_steps)))))
  32. 0032specialize beta_sum_exists (x3)
  33. 0033specialize beta_sum_exists (x4)
  34. 0034specialize beta_sum_exists (S (t+i))
  35. 0035apply beta_sum_exists
  36. 0036cases hs
  37. 0037have hdata : ((forall mdr_i_pfp_coefficient_diagonal_equal mdr_a_pfp_coefficient_diagonal_equal. (exists mdr_gap_pfp_coefficient_diagonal_equalb. mdr_gap_pfp_coefficient_diagonal_equalb + S (mdr_i_pfp_coefficient_diagonal_equal) = (S i)) -> (((exists ff_h_mdr_pfp_coefficient_diagonal_equalo. ff_h_mdr_pfp_coefficient_diagonal_equalo + S (mdr_a_pfp_coefficient_diagonal_equal) = S ((S (mdr_i_pfp_coefficient_diagonal_equal)) * x1)) /\ exists ff_q_mdr_pfp_coefficient_diagonal_equalo. x = ff_q_mdr_pfp_coefficient_diagonal_equalo * S ((S (mdr_i_pfp_coefficient_diagonal_equal)) * x1) + (mdr_a_pfp_coefficient_diagonal_equal))) -> (((exists ff_h_mdr_pfp_coefficient_diagonal_equaln. ff_h_mdr_pfp_coefficient_diagonal_equaln + S (mdr_a_pfp_coefficient_diagonal_equal) = S ((S (mdr_i_pfp_coefficient_diagonal_equal)) * x4)) /\ exists ff_q_mdr_pfp_coefficient_diagonal_equaln. x3 = ff_q_mdr_pfp_coefficient_diagonal_equaln * S ((S (mdr_i_pfp_coefficient_diagonal_equal)) * x4) + (mdr_a_pfp_coefficient_diagonal_equal)))) /\ ((forall pfpad_tail_index_coefficient_diagonal_tail. (exists pfa_gap_coefficient_diagonal_tailbound. pfa_gap_coefficient_diagonal_tailbound + S (pfpad_tail_index_coefficient_diagonal_tail) = (t)) -> (((exists ff_h_pfp_coefficient_diagonal_tailzero. ff_h_pfp_coefficient_diagonal_tailzero + S (0) = S ((S ((S i)+pfpad_tail_index_coefficient_diagonal_tail)) * x4)) /\ exists ff_q_pfp_coefficient_diagonal_tailzero. x3 = ff_q_pfp_coefficient_diagonal_tailzero * S ((S ((S i)+pfpad_tail_index_coefficient_diagonal_tail)) * x4) + (0))))))
  38. 0038specialize polynomial_diagonal_left_padding_right (ab)
  39. 0039specialize polynomial_diagonal_left_padding_right (ac)
  40. 0040specialize polynomial_diagonal_left_padding_right (L)
  41. 0041specialize polynomial_diagonal_left_padding_right (bb)
  42. 0042specialize polynomial_diagonal_left_padding_right (bc)
  43. 0043specialize polynomial_diagonal_left_padding_right (M)
  44. 0044specialize polynomial_diagonal_left_padding_right (BB)
  45. 0045specialize polynomial_diagonal_left_padding_right (BC)
  46. 0046specialize polynomial_diagonal_left_padding_right (t)
  47. 0047specialize polynomial_diagonal_left_padding_right (i)
  48. 0048specialize polynomial_diagonal_left_padding_right (x)
  49. 0049specialize polynomial_diagonal_left_padding_right (x1)
  50. 0050specialize polynomial_diagonal_left_padding_right (x3)
  51. 0051specialize polynomial_diagonal_left_padding_right (x4)
  52. 0052apply polynomial_diagonal_left_padding_right
  53. 0053exact hpad
  54. 0054exact hc_witness_witness_witness_left
  55. 0055exact hd_witness_witness
  56. 0056have heq : x5=x2
  57. 0057cases hdata
  58. 0058specialize polynomial_zero_tail_natural_sum_invariant (x)
  59. 0059specialize polynomial_zero_tail_natural_sum_invariant (x1)
  60. 0060specialize polynomial_zero_tail_natural_sum_invariant (x3)
  61. 0061specialize polynomial_zero_tail_natural_sum_invariant (x4)
  62. 0062specialize polynomial_zero_tail_natural_sum_invariant (S i)
  63. 0063specialize polynomial_zero_tail_natural_sum_invariant (t)
  64. 0064specialize polynomial_zero_tail_natural_sum_invariant (x2)
  65. 0065specialize polynomial_zero_tail_natural_sum_invariant (x5)
  66. 0066apply polynomial_zero_tail_natural_sum_invariant
  67. 0067exact hdata_left
  68. 0068exact hdata_right
  69. 0069exact hc_witness_witness_witness_right_left
  70. 0070have hlength : S i+t=S (t+i)
  71. 0071simp [add_succ_left,add_comm]
  72. 0072rewrite hlength
  73. 0073rewrite hlength
  74. 0074rewrite hlength
  75. 0075exact hs_witness
  76. 0076exists x3
  77. 0077exists x4
  78. 0078exists x2
  79. 0079split
  80. 0080exact hd_witness_witness
  81. 0081split
  82. 0082rewrite heq at hs_witness
  83. 0083rewrite heq at hs_witness
  84. 0084exact hs_witness
  85. 0085exact hc_witness_witness_witness_right_right