PX0065

polynomial_diagonal_left_padding_right

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Coefficients are highest-degree-first. The divisor has a nonzero decoded head; primality supplies its actual inverse. Empty quotients and remainders are included. Functionality compares the constructed execution lengths and decoded coefficients, never arbitrary beta codes. Formal polynomial equivalence compares every coefficient, not evaluations on a finite field. The formal identity and remainder-degree bound are proved separately, not assumed by the execution graph. Arbitrary quotient/remainder-pair uniqueness from a formal identity, multiplication associativity, gcd/Bezout, irreducible-polynomial existence, and the full G091 prime-power-field goal remain open. The seven displayed new names are conservative first-order notation, not new kernel primitives.

Exact theorem in conservative defined notation

∀ ab. ∀ ac. ∀ L. ∀ bb. ∀ bc. ∀ M. ∀ BB. ∀ BC. ∀ t. ∀ i. ∀ db. ∀ dc. ∀ eb. ∀ ec. PolynomialLeftPad(bb,bc,M,t,BB,BC) → PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,S i) → PolynomialDiagonalPrefix(ab,ac,L,BB,BC,t + M,t + i,eb,ec,S (t + i)) → BetaPrefixEqual(db,dc,eb,ec,S i) ∧ (∀ x. Lt(x,t) → BetaAt(eb,ec,S i + x,0))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

BetaPrefixEqual(b,c,d,e,l) · 1PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,t) · 3PolynomialDiagonalPrefix(ab,ac,L,bb,bc,M,i,db,dc,l) · 2PolynomialLeftPad(b,c,L,t,d,e) · 1Lt(a,b) · 2BetaAt(b,c,i,x) · 3

Actual proof prerequisites

polynomial_diagonal_prefix_entry · checked external prerequisitele_trans · checked external prerequisitesucc_le_succ · checked external prerequisitepolynomial_diagonal_term_functional · checked external prerequisitepolynomial_diagonal_term_left_padding_rightpolynomial_diagonal_term_left_padding_zero_rightle_add_left · checked external prerequisiteadd_succ_left · checked external prerequisiteadd_comm · checked external prerequisitematrix_recursive_lt_add_left · checked external prerequisite
Original expanded first-order 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)))))))

Complete tactic proof in conservative notation

All 130 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.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
polynomial diagonal term left padding rightpolynomial diagonal term left padding zero right
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(ab,ac,L,bb,bc,M,i,j,a)Original native command in the exact edition
  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: BetaAt(eb,ec,j,z)PolynomialDiagonalTerm(ab,ac,L,BB,BC,t + M,t + i,j,z)Original native command in the exact edition
  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: BetaAt(eb,ec,S i + j,z)PolynomialDiagonalTerm(ab,ac,L,BB,BC,t + M,t + i,S i + j,z)Original native command in the exact edition
  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 : Lt(S i + j,S i + t)Definitions: Lt(S i + j,S i + t)Original native command in the exact edition
  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 defined 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 : PolynomialDiagonalTerm(ab,ac,L,bb,bc,M,i,j,a)
  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 : ∃ z. BetaAt(eb,ec,j,z) ∧ PolynomialDiagonalTerm(ab,ac,L,BB,BC,t + M,t + i,j,z)
  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 : ∃ z. BetaAt(eb,ec,S i + j,z) ∧ PolynomialDiagonalTerm(ab,ac,L,BB,BC,t + M,t + i,S i + j,z)
  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 : Lt(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