PX0065

polynomial_diagonal_left_padding_right

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

The two actual antidiagonal tables differ by a proved trailing zero block and exact copied natural summands.

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 ab ac L bb bc M BB BC t i db dc eb ec. (((forall pfp_repeat_index_diagonal_actual_padding_rightzeros. (exists pfa_gap_diagonal_actual_padding_rightzerosindex. pfa_gap_diagonal_actual_padding_rightzerosindex + S (pfp_repeat_index_diagonal_actual_padding_rightzeros) = (t)) -> (((exists ff_h_pfp_diagonal_actual_padding_rightzerosentry. ff_h_pfp_diagonal_actual_padding_rightzerosentry + S (0) = S ((S (pfp_repeat_index_diagonal_actual_padding_rightzeros)) * BC)) /\ exists ff_q_pfp_diagonal_actual_padding_rightzerosentry. BB = ff_q_pfp_diagonal_actual_padding_rightzerosentry * S ((S (pfp_repeat_index_diagonal_actual_padding_rightzeros)) * BC) + (0)))) /\ ((forall pfrep_index_diagonal_actual_padding_right pfrep_value_diagonal_actual_padding_right. (exists pfa_gap_diagonal_actual_padding_rightbound. pfa_gap_diagonal_actual_padding_rightbound + S (pfrep_index_diagonal_actual_padding_right) = (M)) -> (((exists ff_h_pfp_diagonal_actual_padding_rightinput. ff_h_pfp_diagonal_actual_padding_rightinput + S (pfrep_value_diagonal_actual_padding_right) = S ((S (pfrep_index_diagonal_actual_padding_right)) * bc)) /\ exists ff_q_pfp_diagonal_actual_padding_rightinput. bb = ff_q_pfp_diagonal_actual_padding_rightinput * S ((S (pfrep_index_diagonal_actual_padding_right)) * bc) + (pfrep_value_diagonal_actual_padding_right))) -> (((exists ff_h_pfp_diagonal_actual_padding_rightoutput. ff_h_pfp_diagonal_actual_padding_rightoutput + S (pfrep_value_diagonal_actual_padding_right) = S ((S ((t)+pfrep_index_diagonal_actual_padding_right)) * BC)) /\ exists ff_q_pfp_diagonal_actual_padding_rightoutput. BB = ff_q_pfp_diagonal_actual_padding_rightoutput * S ((S ((t)+pfrep_index_diagonal_actual_padding_right)) * BC) + (pfrep_value_diagonal_actual_padding_right))))))) -> (forall pfc_index_diagonal_pad_old_right. (exists pfa_gap_diagonal_pad_old_rightbound. pfa_gap_diagonal_pad_old_rightbound + S (pfc_index_diagonal_pad_old_right) = (S i)) -> exists pfc_value_diagonal_pad_old_right. ((((exists ff_h_pfp_diagonal_pad_old_rightentry. ff_h_pfp_diagonal_pad_old_rightentry + S (pfc_value_diagonal_pad_old_right) = S ((S (pfc_index_diagonal_pad_old_right)) * dc)) /\ exists ff_q_pfp_diagonal_pad_old_rightentry. db = ff_q_pfp_diagonal_pad_old_rightentry * S ((S (pfc_index_diagonal_pad_old_right)) * dc) + (pfc_value_diagonal_pad_old_right))) /\ ((exists pfc_complement_diagonal_pad_old_rightterm pfc_left_diagonal_pad_old_rightterm pfc_right_diagonal_pad_old_rightterm. (((pfc_index_diagonal_pad_old_right)+pfc_complement_diagonal_pad_old_rightterm=(i)) /\ ((((((exists pfa_gap_diagonal_pad_old_righttermleftinside. pfa_gap_diagonal_pad_old_righttermleftinside + S (pfc_index_diagonal_pad_old_right) = (L)) /\ ((((exists ff_h_pfp_diagonal_pad_old_righttermleftentry. ff_h_pfp_diagonal_pad_old_righttermleftentry + S (pfc_left_diagonal_pad_old_rightterm) = S ((S (pfc_index_diagonal_pad_old_right)) * ac)) /\ exists ff_q_pfp_diagonal_pad_old_righttermleftentry. ab = ff_q_pfp_diagonal_pad_old_righttermleftentry * S ((S (pfc_index_diagonal_pad_old_right)) * ac) + (pfc_left_diagonal_pad_old_rightterm)))))) \/ (((exists pfc_gap_diagonal_pad_old_righttermleftoutside. pfc_gap_diagonal_pad_old_righttermleftoutside+(L)=(pfc_index_diagonal_pad_old_right)) /\ (((pfc_left_diagonal_pad_old_rightterm)=0))))) /\ ((((((exists pfa_gap_diagonal_pad_old_righttermrightinside. pfa_gap_diagonal_pad_old_righttermrightinside + S (pfc_complement_diagonal_pad_old_rightterm) = (M)) /\ ((((exists ff_h_pfp_diagonal_pad_old_righttermrightentry. ff_h_pfp_diagonal_pad_old_righttermrightentry + S (pfc_right_diagonal_pad_old_rightterm) = S ((S (pfc_complement_diagonal_pad_old_rightterm)) * bc)) /\ exists ff_q_pfp_diagonal_pad_old_righttermrightentry. bb = ff_q_pfp_diagonal_pad_old_righttermrightentry * S ((S (pfc_complement_diagonal_pad_old_rightterm)) * bc) + (pfc_right_diagonal_pad_old_rightterm)))))) \/ (((exists pfc_gap_diagonal_pad_old_righttermrightoutside. pfc_gap_diagonal_pad_old_righttermrightoutside+(M)=(pfc_complement_diagonal_pad_old_rightterm)) /\ (((pfc_right_diagonal_pad_old_rightterm)=0))))) /\ (((pfc_value_diagonal_pad_old_right)=pfc_left_diagonal_pad_old_rightterm*pfc_right_diagonal_pad_old_rightterm))))))))))) -> (forall pfc_index_diagonal_pad_new_right. (exists pfa_gap_diagonal_pad_new_rightbound. pfa_gap_diagonal_pad_new_rightbound + S (pfc_index_diagonal_pad_new_right) = (S (t+i))) -> exists pfc_value_diagonal_pad_new_right. ((((exists ff_h_pfp_diagonal_pad_new_rightentry. ff_h_pfp_diagonal_pad_new_rightentry + S (pfc_value_diagonal_pad_new_right) = S ((S (pfc_index_diagonal_pad_new_right)) * ec)) /\ exists ff_q_pfp_diagonal_pad_new_rightentry. eb = ff_q_pfp_diagonal_pad_new_rightentry * S ((S (pfc_index_diagonal_pad_new_right)) * ec) + (pfc_value_diagonal_pad_new_right))) /\ ((exists pfc_complement_diagonal_pad_new_rightterm pfc_left_diagonal_pad_new_rightterm pfc_right_diagonal_pad_new_rightterm. (((pfc_index_diagonal_pad_new_right)+pfc_complement_diagonal_pad_new_rightterm=(t+i)) /\ ((((((exists pfa_gap_diagonal_pad_new_righttermleftinside. pfa_gap_diagonal_pad_new_righttermleftinside + S (pfc_index_diagonal_pad_new_right) = (L)) /\ ((((exists ff_h_pfp_diagonal_pad_new_righttermleftentry. ff_h_pfp_diagonal_pad_new_righttermleftentry + S (pfc_left_diagonal_pad_new_rightterm) = S ((S (pfc_index_diagonal_pad_new_right)) * ac)) /\ exists ff_q_pfp_diagonal_pad_new_righttermleftentry. ab = ff_q_pfp_diagonal_pad_new_righttermleftentry * S ((S (pfc_index_diagonal_pad_new_right)) * ac) + (pfc_left_diagonal_pad_new_rightterm)))))) \/ (((exists pfc_gap_diagonal_pad_new_righttermleftoutside. pfc_gap_diagonal_pad_new_righttermleftoutside+(L)=(pfc_index_diagonal_pad_new_right)) /\ (((pfc_left_diagonal_pad_new_rightterm)=0))))) /\ ((((((exists pfa_gap_diagonal_pad_new_righttermrightinside. pfa_gap_diagonal_pad_new_righttermrightinside + S (pfc_complement_diagonal_pad_new_rightterm) = (t+M)) /\ ((((exists ff_h_pfp_diagonal_pad_new_righttermrightentry. ff_h_pfp_diagonal_pad_new_righttermrightentry + S (pfc_right_diagonal_pad_new_rightterm) = S ((S (pfc_complement_diagonal_pad_new_rightterm)) * BC)) /\ exists ff_q_pfp_diagonal_pad_new_righttermrightentry. BB = ff_q_pfp_diagonal_pad_new_righttermrightentry * S ((S (pfc_complement_diagonal_pad_new_rightterm)) * BC) + (pfc_right_diagonal_pad_new_rightterm)))))) \/ (((exists pfc_gap_diagonal_pad_new_righttermrightoutside. pfc_gap_diagonal_pad_new_righttermrightoutside+(t+M)=(pfc_complement_diagonal_pad_new_rightterm)) /\ (((pfc_right_diagonal_pad_new_rightterm)=0))))) /\ (((pfc_value_diagonal_pad_new_right)=pfc_left_diagonal_pad_new_rightterm*pfc_right_diagonal_pad_new_rightterm))))))))))) -> (((forall mdr_i_pfp_diagonal_pad_result_equal mdr_a_pfp_diagonal_pad_result_equal. (exists mdr_gap_pfp_diagonal_pad_result_equalb. mdr_gap_pfp_diagonal_pad_result_equalb + S (mdr_i_pfp_diagonal_pad_result_equal) = (S i)) -> (((exists ff_h_mdr_pfp_diagonal_pad_result_equalo. ff_h_mdr_pfp_diagonal_pad_result_equalo + S (mdr_a_pfp_diagonal_pad_result_equal) = S ((S (mdr_i_pfp_diagonal_pad_result_equal)) * dc)) /\ exists ff_q_mdr_pfp_diagonal_pad_result_equalo. db = ff_q_mdr_pfp_diagonal_pad_result_equalo * S ((S (mdr_i_pfp_diagonal_pad_result_equal)) * dc) + (mdr_a_pfp_diagonal_pad_result_equal))) -> (((exists ff_h_mdr_pfp_diagonal_pad_result_equaln. ff_h_mdr_pfp_diagonal_pad_result_equaln + S (mdr_a_pfp_diagonal_pad_result_equal) = S ((S (mdr_i_pfp_diagonal_pad_result_equal)) * ec)) /\ exists ff_q_mdr_pfp_diagonal_pad_result_equaln. eb = ff_q_mdr_pfp_diagonal_pad_result_equaln * S ((S (mdr_i_pfp_diagonal_pad_result_equal)) * ec) + (mdr_a_pfp_diagonal_pad_result_equal)))) /\ ((forall pfpad_tail_index_diagonal_pad_result_tail. (exists pfa_gap_diagonal_pad_result_tailbound. pfa_gap_diagonal_pad_result_tailbound + S (pfpad_tail_index_diagonal_pad_result_tail) = (t)) -> (((exists ff_h_pfp_diagonal_pad_result_tailzero. ff_h_pfp_diagonal_pad_result_tailzero + S (0) = S ((S ((S i)+pfpad_tail_index_diagonal_pad_result_tail)) * ec)) /\ exists ff_q_pfp_diagonal_pad_result_tailzero. eb = ff_q_pfp_diagonal_pad_result_tailzero * S ((S ((S i)+pfpad_tail_index_diagonal_pad_result_tail)) * ec) + (0)))))))

Constructive proof overview

Generated structural guide

The two actual antidiagonal tables differ by a proved trailing zero block and exact copied natural summands.

The unchanged tactic script uses 10 declared prerequisites and contains 130 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_entry Alpha theorem; checked-use authorized le_trans Alpha theorem; checked-use authorized succ_le_succ Alpha theorem; checked-use authorized polynomial_diagonal_term_functional Alpha theorem; checked-use authorized PX0061 polynomial_diagonal_term_left_padding_right PX0063 polynomial_diagonal_term_left_padding_zero_right le_add_left Alpha theorem; checked-use authorized add_succ_left Alpha theorem; checked-use authorized add_comm Alpha theorem; checked-use authorized matrix_recursive_lt_add_left Alpha theorem; checked-use authorized

Direct dependents

PX0067 prime_field_convolution_coefficient_left_padding_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

130 script commands · 25 reading checkpoints · 7 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 term left padding rightpolynomial diagonal term left padding zero right

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 ab
  2. L2
    intro ac
  3. L3
    intro L
  4. L4
    intro bb
  5. L5
    intro bc
  6. L6
    intro M
  7. L7
    intro BB
  8. L8
    intro BC
  9. L9
    intro t
  10. L10
    intro i
02Fix variables and assumptionsL11–17

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

  1. L11
    intro db
  2. L12
    intro dc
  3. L13
    intro eb
  4. L14
    intro ec
  5. L15
    intro hpad
  6. L16
    intro hold
  7. L17
    intro hnew
03Separate the logical casesL18–18

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

  1. L18
    split
04Fix variables and assumptionsL19–22

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

  1. L19
    intro j
  2. L20
    intro a
  3. L21
    intro hj
  4. L22
    intro ha
05Establish htermL23–32

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

  1. L23
    have hterm : PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,a)Definitions: PolynomialDiagonalTerm
  2. L24
    specialize polynomial_diagonal_prefix_entry (ab)
  3. L25
    specialize polynomial_diagonal_prefix_entry (ac)
  4. L26
    specialize polynomial_diagonal_prefix_entry (L)
  5. L27
    specialize polynomial_diagonal_prefix_entry (bb)
  6. L28
    specialize polynomial_diagonal_prefix_entry (bc)
  7. L29
    specialize polynomial_diagonal_prefix_entry (M)
  8. L30
    specialize polynomial_diagonal_prefix_entry (i)
  9. L31
    specialize polynomial_diagonal_prefix_entry (db)
  10. L32
    specialize polynomial_diagonal_prefix_entry (dc)
06Use earlier factsL33–39

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

  1. L33
    specialize polynomial_diagonal_prefix_entry (S i)
  2. L34
    specialize polynomial_diagonal_prefix_entry (j)
  3. L35
    specialize polynomial_diagonal_prefix_entry (a)
  4. L36
    apply polynomial_diagonal_prefix_entry
  5. L37
    exact hold
  6. L38
    exact hj
  7. L39
    exact ha
07Establish hvL40–49

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

  1. L40
    have hv : ∃ z. BetaAt(eb,ec,j,z) ∧ PolynomialDiagonalTerm(ab,ac,L,BB,BC,t + M,t + i,j,z)Definitions: PolynomialDiagonalTermBetaAt
  2. L41
    specialize hnew (j)
  3. L42
    apply hnew
  4. L43
    specialize le_trans (S j)
  5. L44
    specialize le_trans (S i)
  6. L45
    specialize le_trans (S (t+i))
  7. L46
    apply le_trans
  8. L47
    exact hj
  9. L48
    specialize succ_le_succ (i)
  10. L49
    specialize succ_le_succ (t+i)
08Use earlier factsL50–53

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

  1. L50
    apply succ_le_succ
  2. L51
    specialize le_add_left (i)
  3. L52
    specialize le_add_left (t)
  4. L53
    apply le_add_left
09Separate the logical casesL54–55

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

  1. L54
    cases hv
  2. L55
    cases hv_witness
10Establish heqL56–65

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

  1. L56
    have heq : x=a
  2. L57
    specialize polynomial_diagonal_term_functional (ab)
  3. L58
    specialize polynomial_diagonal_term_functional (ac)
  4. L59
    specialize polynomial_diagonal_term_functional (L)
  5. L60
    specialize polynomial_diagonal_term_functional (BB)
  6. L61
    specialize polynomial_diagonal_term_functional (BC)
  7. L62
    specialize polynomial_diagonal_term_functional (t+M)
  8. L63
    specialize polynomial_diagonal_term_functional (t+i)
  9. L64
    specialize polynomial_diagonal_term_functional (j)
  10. L65
    specialize polynomial_diagonal_term_functional (x)
11Use earlier factsL66–75

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

  1. L66
    specialize polynomial_diagonal_term_functional (a)
  2. L67
    apply polynomial_diagonal_term_functional
  3. L68
    exact hv_witness_right
  4. L69
    specialize polynomial_diagonal_term_left_padding_right (ab)
  5. L70
    specialize polynomial_diagonal_term_left_padding_right (ac)
  6. L71
    specialize polynomial_diagonal_term_left_padding_right (L)
  7. L72
    specialize polynomial_diagonal_term_left_padding_right (bb)
  8. L73
    specialize polynomial_diagonal_term_left_padding_right (bc)
  9. L74
    specialize polynomial_diagonal_term_left_padding_right (M)
  10. L75
    specialize polynomial_diagonal_term_left_padding_right (BB)
12Use earlier factsL76–83

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

  1. L76
    specialize polynomial_diagonal_term_left_padding_right (BC)
  2. L77
    specialize polynomial_diagonal_term_left_padding_right (t)
  3. L78
    specialize polynomial_diagonal_term_left_padding_right (i)
  4. L79
    specialize polynomial_diagonal_term_left_padding_right (j)
  5. L80
    specialize polynomial_diagonal_term_left_padding_right (a)
  6. L81
    apply polynomial_diagonal_term_left_padding_right
  7. L82
    exact hpad
  8. L83
    exact hterm
13Calculate and transport equalitiesL84–85

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

  1. L84
    rewrite heq at hv_witness_left
  2. L85
    rewrite heq at hv_witness_left
14Use earlier factsL86–86

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

  1. L86
    exact hv_witness_left
15Fix variables and assumptionsL87–88

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

  1. L87
    intro j
  2. L88
    intro hj
16Establish hvL89–91

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

  1. L89
    have hv : ∃ z. BetaAt(eb,ec,S i + j,z) ∧ PolynomialDiagonalTerm(ab,ac,L,BB,BC,t + M,t + i,S i + j,z)Definitions: PolynomialDiagonalTermBetaAt
  2. L90
    specialize hnew (S i+j)
  3. L91
    apply hnew
17Establish hlengthL92–93

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

  1. L92
    have hlength : S i+t=S (t+i)
  2. L93
    simp [add_succ_left,add_comm]
18Establish hboundL94–101

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply matrix recursive lt add left.

  1. L94
    have hbound : exists pfa_gap_diagonal_tail_bound. pfa_gap_diagonal_tail_bound + S (S i+j) = (S i+t)
  2. L95
    specialize matrix_recursive_lt_add_left (j)
  3. L96
    specialize matrix_recursive_lt_add_left (t)
  4. L97
    specialize matrix_recursive_lt_add_left (S i)
  5. L98
    apply matrix_recursive_lt_add_left
  6. L99
    exact hj
  7. L100
    rewrite hlength at hbound
  8. L101
    exact hbound
19Separate the logical casesL102–103

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

  1. L102
    cases hv
  2. L103
    cases hv_witness
20Establish hzL104–113

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

  1. L104
    have hz : x=0
  2. L105
    specialize polynomial_diagonal_term_left_padding_zero_right (ab)
  3. L106
    specialize polynomial_diagonal_term_left_padding_zero_right (ac)
  4. L107
    specialize polynomial_diagonal_term_left_padding_zero_right (L)
  5. L108
    specialize polynomial_diagonal_term_left_padding_zero_right (bb)
  6. L109
    specialize polynomial_diagonal_term_left_padding_zero_right (bc)
  7. L110
    specialize polynomial_diagonal_term_left_padding_zero_right (M)
  8. L111
    specialize polynomial_diagonal_term_left_padding_zero_right (BB)
  9. L112
    specialize polynomial_diagonal_term_left_padding_zero_right (BC)
  10. L113
    specialize polynomial_diagonal_term_left_padding_zero_right (t)
21Use earlier factsL114–122

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

  1. L114
    specialize polynomial_diagonal_term_left_padding_zero_right (t+i)
  2. L115
    specialize polynomial_diagonal_term_left_padding_zero_right (S i+j)
  3. L116
    specialize polynomial_diagonal_term_left_padding_zero_right (x)
  4. L117
    apply polynomial_diagonal_term_left_padding_zero_right
  5. L118
    exact hpad
  6. L119
    specialize matrix_recursive_lt_add_left (i)
  7. L120
    specialize matrix_recursive_lt_add_left (S i+j)
  8. L121
    specialize matrix_recursive_lt_add_left (t)
  9. L122
    apply matrix_recursive_lt_add_left
22Construct an explicit witnessL123–123

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

  1. L123
    exists j
23Use earlier factsL124–127

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

  1. L124
    specialize add_comm (j)
  2. L125
    specialize add_comm (S i)
  3. L126
    apply add_comm
  4. L127
    exact hv_witness_right
24Calculate and transport equalitiesL128–129

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

  1. L128
    rewrite hz at hv_witness_left
  2. L129
    rewrite hz at hv_witness_left
25Use earlier factsL130–130

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

  1. L130
    exact hv_witness_left

Library-wide reading audit

Original exact command ledger · 130 lines
  1. 0001intro ab
  2. 0002intro ac
  3. 0003intro L
  4. 0004intro bb
  5. 0005intro bc
  6. 0006intro M
  7. 0007intro BB
  8. 0008intro BC
  9. 0009intro t
  10. 0010intro i
  11. 0011intro db
  12. 0012intro dc
  13. 0013intro eb
  14. 0014intro ec
  15. 0015intro hpad
  16. 0016intro hold
  17. 0017intro hnew
  18. 0018split
  19. 0019intro j
  20. 0020intro a
  21. 0021intro hj
  22. 0022intro ha
  23. 0023have hterm : exists pfc_complement_diagonal_copy_old pfc_left_diagonal_copy_old pfc_right_diagonal_copy_old. (((j)+pfc_complement_diagonal_copy_old=(i)) /\ ((((((exists pfa_gap_diagonal_copy_oldleftinside. pfa_gap_diagonal_copy_oldleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_diagonal_copy_oldleftentry. ff_h_pfp_diagonal_copy_oldleftentry + S (pfc_left_diagonal_copy_old) = S ((S (j)) * ac)) /\ exists ff_q_pfp_diagonal_copy_oldleftentry. ab = ff_q_pfp_diagonal_copy_oldleftentry * S ((S (j)) * ac) + (pfc_left_diagonal_copy_old)))))) \/ (((exists pfc_gap_diagonal_copy_oldleftoutside. pfc_gap_diagonal_copy_oldleftoutside+(L)=(j)) /\ (((pfc_left_diagonal_copy_old)=0))))) /\ ((((((exists pfa_gap_diagonal_copy_oldrightinside. pfa_gap_diagonal_copy_oldrightinside + S (pfc_complement_diagonal_copy_old) = (M)) /\ ((((exists ff_h_pfp_diagonal_copy_oldrightentry. ff_h_pfp_diagonal_copy_oldrightentry + S (pfc_right_diagonal_copy_old) = S ((S (pfc_complement_diagonal_copy_old)) * bc)) /\ exists ff_q_pfp_diagonal_copy_oldrightentry. bb = ff_q_pfp_diagonal_copy_oldrightentry * S ((S (pfc_complement_diagonal_copy_old)) * bc) + (pfc_right_diagonal_copy_old)))))) \/ (((exists pfc_gap_diagonal_copy_oldrightoutside. pfc_gap_diagonal_copy_oldrightoutside+(M)=(pfc_complement_diagonal_copy_old)) /\ (((pfc_right_diagonal_copy_old)=0))))) /\ (((a)=pfc_left_diagonal_copy_old*pfc_right_diagonal_copy_old)))))))
  24. 0024specialize polynomial_diagonal_prefix_entry (ab)
  25. 0025specialize polynomial_diagonal_prefix_entry (ac)
  26. 0026specialize polynomial_diagonal_prefix_entry (L)
  27. 0027specialize polynomial_diagonal_prefix_entry (bb)
  28. 0028specialize polynomial_diagonal_prefix_entry (bc)
  29. 0029specialize polynomial_diagonal_prefix_entry (M)
  30. 0030specialize polynomial_diagonal_prefix_entry (i)
  31. 0031specialize polynomial_diagonal_prefix_entry (db)
  32. 0032specialize polynomial_diagonal_prefix_entry (dc)
  33. 0033specialize polynomial_diagonal_prefix_entry (S i)
  34. 0034specialize polynomial_diagonal_prefix_entry (j)
  35. 0035specialize polynomial_diagonal_prefix_entry (a)
  36. 0036apply polynomial_diagonal_prefix_entry
  37. 0037exact hold
  38. 0038exact hj
  39. 0039exact ha
  40. 0040have hv : exists z. ((((exists ff_h_pfp_diagonal_copy_entry. ff_h_pfp_diagonal_copy_entry + S (z) = S ((S (j)) * ec)) /\ exists ff_q_pfp_diagonal_copy_entry. eb = ff_q_pfp_diagonal_copy_entry * S ((S (j)) * ec) + (z))) /\ ((exists pfc_complement_diagonal_copy_actual pfc_left_diagonal_copy_actual pfc_right_diagonal_copy_actual. (((j)+pfc_complement_diagonal_copy_actual=(t+i)) /\ ((((((exists pfa_gap_diagonal_copy_actualleftinside. pfa_gap_diagonal_copy_actualleftinside + S (j) = (L)) /\ ((((exists ff_h_pfp_diagonal_copy_actualleftentry. ff_h_pfp_diagonal_copy_actualleftentry + S (pfc_left_diagonal_copy_actual) = S ((S (j)) * ac)) /\ exists ff_q_pfp_diagonal_copy_actualleftentry. ab = ff_q_pfp_diagonal_copy_actualleftentry * S ((S (j)) * ac) + (pfc_left_diagonal_copy_actual)))))) \/ (((exists pfc_gap_diagonal_copy_actualleftoutside. pfc_gap_diagonal_copy_actualleftoutside+(L)=(j)) /\ (((pfc_left_diagonal_copy_actual)=0))))) /\ ((((((exists pfa_gap_diagonal_copy_actualrightinside. pfa_gap_diagonal_copy_actualrightinside + S (pfc_complement_diagonal_copy_actual) = (t+M)) /\ ((((exists ff_h_pfp_diagonal_copy_actualrightentry. ff_h_pfp_diagonal_copy_actualrightentry + S (pfc_right_diagonal_copy_actual) = S ((S (pfc_complement_diagonal_copy_actual)) * BC)) /\ exists ff_q_pfp_diagonal_copy_actualrightentry. BB = ff_q_pfp_diagonal_copy_actualrightentry * S ((S (pfc_complement_diagonal_copy_actual)) * BC) + (pfc_right_diagonal_copy_actual)))))) \/ (((exists pfc_gap_diagonal_copy_actualrightoutside. pfc_gap_diagonal_copy_actualrightoutside+(t+M)=(pfc_complement_diagonal_copy_actual)) /\ (((pfc_right_diagonal_copy_actual)=0))))) /\ (((z)=pfc_left_diagonal_copy_actual*pfc_right_diagonal_copy_actual))))))))))
  41. 0041specialize hnew (j)
  42. 0042apply hnew
  43. 0043specialize le_trans (S j)
  44. 0044specialize le_trans (S i)
  45. 0045specialize le_trans (S (t+i))
  46. 0046apply le_trans
  47. 0047exact hj
  48. 0048specialize succ_le_succ (i)
  49. 0049specialize succ_le_succ (t+i)
  50. 0050apply succ_le_succ
  51. 0051specialize le_add_left (i)
  52. 0052specialize le_add_left (t)
  53. 0053apply le_add_left
  54. 0054cases hv
  55. 0055cases hv_witness
  56. 0056have heq : x=a
  57. 0057specialize polynomial_diagonal_term_functional (ab)
  58. 0058specialize polynomial_diagonal_term_functional (ac)
  59. 0059specialize polynomial_diagonal_term_functional (L)
  60. 0060specialize polynomial_diagonal_term_functional (BB)
  61. 0061specialize polynomial_diagonal_term_functional (BC)
  62. 0062specialize polynomial_diagonal_term_functional (t+M)
  63. 0063specialize polynomial_diagonal_term_functional (t+i)
  64. 0064specialize polynomial_diagonal_term_functional (j)
  65. 0065specialize polynomial_diagonal_term_functional (x)
  66. 0066specialize polynomial_diagonal_term_functional (a)
  67. 0067apply polynomial_diagonal_term_functional
  68. 0068exact hv_witness_right
  69. 0069specialize polynomial_diagonal_term_left_padding_right (ab)
  70. 0070specialize polynomial_diagonal_term_left_padding_right (ac)
  71. 0071specialize polynomial_diagonal_term_left_padding_right (L)
  72. 0072specialize polynomial_diagonal_term_left_padding_right (bb)
  73. 0073specialize polynomial_diagonal_term_left_padding_right (bc)
  74. 0074specialize polynomial_diagonal_term_left_padding_right (M)
  75. 0075specialize polynomial_diagonal_term_left_padding_right (BB)
  76. 0076specialize polynomial_diagonal_term_left_padding_right (BC)
  77. 0077specialize polynomial_diagonal_term_left_padding_right (t)
  78. 0078specialize polynomial_diagonal_term_left_padding_right (i)
  79. 0079specialize polynomial_diagonal_term_left_padding_right (j)
  80. 0080specialize polynomial_diagonal_term_left_padding_right (a)
  81. 0081apply polynomial_diagonal_term_left_padding_right
  82. 0082exact hpad
  83. 0083exact hterm
  84. 0084rewrite heq at hv_witness_left
  85. 0085rewrite heq at hv_witness_left
  86. 0086exact hv_witness_left
  87. 0087intro j
  88. 0088intro hj
  89. 0089have hv : exists z. ((((exists ff_h_pfp_diagonal_tail_entry. ff_h_pfp_diagonal_tail_entry + S (z) = S ((S (S i+j)) * ec)) /\ exists ff_q_pfp_diagonal_tail_entry. eb = ff_q_pfp_diagonal_tail_entry * S ((S (S i+j)) * ec) + (z))) /\ ((exists pfc_complement_diagonal_tail_actual pfc_left_diagonal_tail_actual pfc_right_diagonal_tail_actual. (((S i+j)+pfc_complement_diagonal_tail_actual=(t+i)) /\ ((((((exists pfa_gap_diagonal_tail_actualleftinside. pfa_gap_diagonal_tail_actualleftinside + S (S i+j) = (L)) /\ ((((exists ff_h_pfp_diagonal_tail_actualleftentry. ff_h_pfp_diagonal_tail_actualleftentry + S (pfc_left_diagonal_tail_actual) = S ((S (S i+j)) * ac)) /\ exists ff_q_pfp_diagonal_tail_actualleftentry. ab = ff_q_pfp_diagonal_tail_actualleftentry * S ((S (S i+j)) * ac) + (pfc_left_diagonal_tail_actual)))))) \/ (((exists pfc_gap_diagonal_tail_actualleftoutside. pfc_gap_diagonal_tail_actualleftoutside+(L)=(S i+j)) /\ (((pfc_left_diagonal_tail_actual)=0))))) /\ ((((((exists pfa_gap_diagonal_tail_actualrightinside. pfa_gap_diagonal_tail_actualrightinside + S (pfc_complement_diagonal_tail_actual) = (t+M)) /\ ((((exists ff_h_pfp_diagonal_tail_actualrightentry. ff_h_pfp_diagonal_tail_actualrightentry + S (pfc_right_diagonal_tail_actual) = S ((S (pfc_complement_diagonal_tail_actual)) * BC)) /\ exists ff_q_pfp_diagonal_tail_actualrightentry. BB = ff_q_pfp_diagonal_tail_actualrightentry * S ((S (pfc_complement_diagonal_tail_actual)) * BC) + (pfc_right_diagonal_tail_actual)))))) \/ (((exists pfc_gap_diagonal_tail_actualrightoutside. pfc_gap_diagonal_tail_actualrightoutside+(t+M)=(pfc_complement_diagonal_tail_actual)) /\ (((pfc_right_diagonal_tail_actual)=0))))) /\ (((z)=pfc_left_diagonal_tail_actual*pfc_right_diagonal_tail_actual))))))))))
  90. 0090specialize hnew (S i+j)
  91. 0091apply hnew
  92. 0092have hlength : S i+t=S (t+i)
  93. 0093simp [add_succ_left,add_comm]
  94. 0094have hbound : exists pfa_gap_diagonal_tail_bound. pfa_gap_diagonal_tail_bound + S (S i+j) = (S i+t)
  95. 0095specialize matrix_recursive_lt_add_left (j)
  96. 0096specialize matrix_recursive_lt_add_left (t)
  97. 0097specialize matrix_recursive_lt_add_left (S i)
  98. 0098apply matrix_recursive_lt_add_left
  99. 0099exact hj
  100. 0100rewrite hlength at hbound
  101. 0101exact hbound
  102. 0102cases hv
  103. 0103cases hv_witness
  104. 0104have hz : x=0
  105. 0105specialize polynomial_diagonal_term_left_padding_zero_right (ab)
  106. 0106specialize polynomial_diagonal_term_left_padding_zero_right (ac)
  107. 0107specialize polynomial_diagonal_term_left_padding_zero_right (L)
  108. 0108specialize polynomial_diagonal_term_left_padding_zero_right (bb)
  109. 0109specialize polynomial_diagonal_term_left_padding_zero_right (bc)
  110. 0110specialize polynomial_diagonal_term_left_padding_zero_right (M)
  111. 0111specialize polynomial_diagonal_term_left_padding_zero_right (BB)
  112. 0112specialize polynomial_diagonal_term_left_padding_zero_right (BC)
  113. 0113specialize polynomial_diagonal_term_left_padding_zero_right (t)
  114. 0114specialize polynomial_diagonal_term_left_padding_zero_right (t+i)
  115. 0115specialize polynomial_diagonal_term_left_padding_zero_right (S i+j)
  116. 0116specialize polynomial_diagonal_term_left_padding_zero_right (x)
  117. 0117apply polynomial_diagonal_term_left_padding_zero_right
  118. 0118exact hpad
  119. 0119specialize matrix_recursive_lt_add_left (i)
  120. 0120specialize matrix_recursive_lt_add_left (S i+j)
  121. 0121specialize matrix_recursive_lt_add_left (t)
  122. 0122apply matrix_recursive_lt_add_left
  123. 0123exists j
  124. 0124specialize add_comm (j)
  125. 0125specialize add_comm (S i)
  126. 0126apply add_comm
  127. 0127exact hv_witness_right
  128. 0128rewrite hz at hv_witness_left
  129. 0129rewrite hz at hv_witness_left
  130. 0130exact hv_witness_left