PG004E

polynomial_diagonal_left_constant_natural_sum

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

The actual finite natural sum equals k*a: construct its one-term sum and use the existing zero-tail invariant for every subsequent summand. The total need not itself be a canonical field coefficient.

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 k kb kc ab ac L i a db dc n. (((exists ff_h_pfp_left_constant_sum_K. ff_h_pfp_left_constant_sum_K + S (k) = S ((S (0)) * kc)) /\ exists ff_q_pfp_left_constant_sum_K. kb = ff_q_pfp_left_constant_sum_K * S ((S (0)) * kc) + (k))) -> (exists pfa_gap_left_constant_sum_index. pfa_gap_left_constant_sum_index + S (i) = (L)) -> (((exists ff_h_pfp_left_constant_sum_A. ff_h_pfp_left_constant_sum_A + S (a) = S ((S (i)) * ac)) /\ exists ff_q_pfp_left_constant_sum_A. ab = ff_q_pfp_left_constant_sum_A * S ((S (i)) * ac) + (a))) -> (forall pfc_index_left_constant_sum_diagonal. (exists pfa_gap_left_constant_sum_diagonalbound. pfa_gap_left_constant_sum_diagonalbound + S (pfc_index_left_constant_sum_diagonal) = (S i)) -> exists pfc_value_left_constant_sum_diagonal. ((((exists ff_h_pfp_left_constant_sum_diagonalentry. ff_h_pfp_left_constant_sum_diagonalentry + S (pfc_value_left_constant_sum_diagonal) = S ((S (pfc_index_left_constant_sum_diagonal)) * dc)) /\ exists ff_q_pfp_left_constant_sum_diagonalentry. db = ff_q_pfp_left_constant_sum_diagonalentry * S ((S (pfc_index_left_constant_sum_diagonal)) * dc) + (pfc_value_left_constant_sum_diagonal))) /\ ((exists pfc_complement_left_constant_sum_diagonalterm pfc_left_left_constant_sum_diagonalterm pfc_right_left_constant_sum_diagonalterm. (((pfc_index_left_constant_sum_diagonal)+pfc_complement_left_constant_sum_diagonalterm=(i)) /\ ((((((exists pfa_gap_left_constant_sum_diagonaltermleftinside. pfa_gap_left_constant_sum_diagonaltermleftinside + S (pfc_index_left_constant_sum_diagonal) = (1)) /\ ((((exists ff_h_pfp_left_constant_sum_diagonaltermleftentry. ff_h_pfp_left_constant_sum_diagonaltermleftentry + S (pfc_left_left_constant_sum_diagonalterm) = S ((S (pfc_index_left_constant_sum_diagonal)) * kc)) /\ exists ff_q_pfp_left_constant_sum_diagonaltermleftentry. kb = ff_q_pfp_left_constant_sum_diagonaltermleftentry * S ((S (pfc_index_left_constant_sum_diagonal)) * kc) + (pfc_left_left_constant_sum_diagonalterm)))))) \/ (((exists pfc_gap_left_constant_sum_diagonaltermleftoutside. pfc_gap_left_constant_sum_diagonaltermleftoutside+(1)=(pfc_index_left_constant_sum_diagonal)) /\ (((pfc_left_left_constant_sum_diagonalterm)=0))))) /\ ((((((exists pfa_gap_left_constant_sum_diagonaltermrightinside. pfa_gap_left_constant_sum_diagonaltermrightinside + S (pfc_complement_left_constant_sum_diagonalterm) = (L)) /\ ((((exists ff_h_pfp_left_constant_sum_diagonaltermrightentry. ff_h_pfp_left_constant_sum_diagonaltermrightentry + S (pfc_right_left_constant_sum_diagonalterm) = S ((S (pfc_complement_left_constant_sum_diagonalterm)) * ac)) /\ exists ff_q_pfp_left_constant_sum_diagonaltermrightentry. ab = ff_q_pfp_left_constant_sum_diagonaltermrightentry * S ((S (pfc_complement_left_constant_sum_diagonalterm)) * ac) + (pfc_right_left_constant_sum_diagonalterm)))))) \/ (((exists pfc_gap_left_constant_sum_diagonaltermrightoutside. pfc_gap_left_constant_sum_diagonaltermrightoutside+(L)=(pfc_complement_left_constant_sum_diagonalterm)) /\ (((pfc_right_left_constant_sum_diagonalterm)=0))))) /\ (((pfc_value_left_constant_sum_diagonal)=pfc_left_left_constant_sum_diagonalterm*pfc_right_left_constant_sum_diagonalterm))))))))))) -> (exists fs_u_pfc_left_constant_sum_actual fs_v_pfc_left_constant_sum_actual. ((((exists fs_h_pfc_left_constant_sum_actual_body_start. fs_h_pfc_left_constant_sum_actual_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_constant_sum_actual)) /\ exists fs_q_pfc_left_constant_sum_actual_body_start. fs_u_pfc_left_constant_sum_actual = fs_q_pfc_left_constant_sum_actual_body_start * S ((S (0)) * fs_v_pfc_left_constant_sum_actual) + (0))) /\ ((((exists fs_h_pfc_left_constant_sum_actual_body_terminal. fs_h_pfc_left_constant_sum_actual_body_terminal + S (n) = S ((S (S i)) * fs_v_pfc_left_constant_sum_actual)) /\ exists fs_q_pfc_left_constant_sum_actual_body_terminal. fs_u_pfc_left_constant_sum_actual = fs_q_pfc_left_constant_sum_actual_body_terminal * S ((S (S i)) * fs_v_pfc_left_constant_sum_actual) + (n))) /\ forall fs_i_pfc_left_constant_sum_actual_body_steps. (exists fs_lt_pfc_left_constant_sum_actual_body_steps_bound. fs_lt_pfc_left_constant_sum_actual_body_steps_bound + S fs_i_pfc_left_constant_sum_actual_body_steps = S i) -> exists fs_a_pfc_left_constant_sum_actual_body_steps fs_r_pfc_left_constant_sum_actual_body_steps fs_s_pfc_left_constant_sum_actual_body_steps. ((((exists fs_h_pfc_left_constant_sum_actual_body_steps_summand. fs_h_pfc_left_constant_sum_actual_body_steps_summand + S (fs_a_pfc_left_constant_sum_actual_body_steps) = S ((S (fs_i_pfc_left_constant_sum_actual_body_steps)) * dc)) /\ exists fs_q_pfc_left_constant_sum_actual_body_steps_summand. db = fs_q_pfc_left_constant_sum_actual_body_steps_summand * S ((S (fs_i_pfc_left_constant_sum_actual_body_steps)) * dc) + (fs_a_pfc_left_constant_sum_actual_body_steps))) /\ ((((exists fs_h_pfc_left_constant_sum_actual_body_steps_partial. fs_h_pfc_left_constant_sum_actual_body_steps_partial + S (fs_r_pfc_left_constant_sum_actual_body_steps) = S ((S (fs_i_pfc_left_constant_sum_actual_body_steps)) * fs_v_pfc_left_constant_sum_actual)) /\ exists fs_q_pfc_left_constant_sum_actual_body_steps_partial. fs_u_pfc_left_constant_sum_actual = fs_q_pfc_left_constant_sum_actual_body_steps_partial * S ((S (fs_i_pfc_left_constant_sum_actual_body_steps)) * fs_v_pfc_left_constant_sum_actual) + (fs_r_pfc_left_constant_sum_actual_body_steps))) /\ ((((exists fs_h_pfc_left_constant_sum_actual_body_steps_successor. fs_h_pfc_left_constant_sum_actual_body_steps_successor + S (fs_s_pfc_left_constant_sum_actual_body_steps) = S ((S (S fs_i_pfc_left_constant_sum_actual_body_steps)) * fs_v_pfc_left_constant_sum_actual)) /\ exists fs_q_pfc_left_constant_sum_actual_body_steps_successor. fs_u_pfc_left_constant_sum_actual = fs_q_pfc_left_constant_sum_actual_body_steps_successor * S ((S (S fs_i_pfc_left_constant_sum_actual_body_steps)) * fs_v_pfc_left_constant_sum_actual) + (fs_s_pfc_left_constant_sum_actual_body_steps))) /\ fs_s_pfc_left_constant_sum_actual_body_steps = fs_r_pfc_left_constant_sum_actual_body_steps + fs_a_pfc_left_constant_sum_actual_body_steps)))))) -> (n=k*a)

Constructive proof overview

Generated structural guide

The actual finite natural sum equals k*a: construct its one-term sum and use the existing zero-tail invariant for every subsequent summand. The total need not itself be a canonical field coefficient.

The unchanged tactic script uses 11 declared prerequisites and contains 137 exact native proof lines.

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

Proof neighborhood

Direct dependencies

PG004D polynomial_diagonal_left_constant_first_term PG002E polynomial_diagonal_left_unit_tail_term add_succ_left Alpha theorem; checked-use authorized zero_add Alpha theorem; checked-use authorized succ_le_succ Alpha theorem; checked-use authorized le_add_right Alpha theorem; checked-use authorized beta_sum_exists Alpha theorem; checked-use authorized beta_sum_succ_decompose Alpha theorem; checked-use authorized beta_sum_zero Alpha theorem; checked-use authorized beta_at_unique Alpha theorem; checked-use authorized polynomial_zero_tail_natural_sum_invariant Alpha theorem; checked-use authorized

Direct dependents

PG004F prime_field_convolution_coefficient_left_constant

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

137 script commands · 30 reading checkpoints · 13 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 constant first termpolynomial diagonal left unit tail term

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 k
  2. L2
    intro kb
  3. L3
    intro kc
  4. L4
    intro ab
  5. L5
    intro ac
  6. L6
    intro L
  7. L7
    intro i
  8. L8
    intro a
  9. L9
    intro db
  10. L10
    intro dc
02Fix variables and assumptionsL11–16

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

  1. L11
    intro n
  2. L12
    intro hk
  3. L13
    intro hi
  4. L14
    intro ha
  5. L15
    intro hd
  6. L16
    intro hs
03Establish hheadL17–17

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

  1. L17
    have hhead : ((exists ff_h_pfp_left_constant_sum_head. ff_h_pfp_left_constant_sum_head + S (k*a) = S ((S (0)) * dc)) /\ exists ff_q_pfp_left_constant_sum_head. db = ff_q_pfp_left_constant_sum_head * S ((S (0)) * dc) + (k*a))
04Establish hvL18–20

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

  1. L18
    have hv : ∃ t. BetaAt(db,dc,0,t) ∧ PolynomialDiagonalTerm(kb,kc,1,ab,ac,L,i,0,t)Definitions: PolynomialDiagonalTermBetaAt
  2. L19
    specialize hd (0)
  3. L20
    apply hd
05Construct an explicit witnessL21–21

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

  1. L21
    exists i
06Calculate and transport equalitiesL22–22

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

  1. L22
    simp
07Separate the logical casesL23–24

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

  1. L23
    cases hv
  2. L24
    cases hv_witness
08Establish heqL25–34

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

  1. L25
    have heq : x=k*a
  2. L26
    specialize polynomial_diagonal_left_constant_first_term (k)
  3. L27
    specialize polynomial_diagonal_left_constant_first_term (kb)
  4. L28
    specialize polynomial_diagonal_left_constant_first_term (kc)
  5. L29
    specialize polynomial_diagonal_left_constant_first_term (ab)
  6. L30
    specialize polynomial_diagonal_left_constant_first_term (ac)
  7. L31
    specialize polynomial_diagonal_left_constant_first_term (L)
  8. L32
    specialize polynomial_diagonal_left_constant_first_term (i)
  9. L33
    specialize polynomial_diagonal_left_constant_first_term (a)
  10. L34
    specialize polynomial_diagonal_left_constant_first_term (x)
09Use earlier factsL35–39

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

  1. L35
    apply polynomial_diagonal_left_constant_first_term
  2. L36
    exact hk
  3. L37
    exact hi
  4. L38
    exact ha
  5. L39
    exact hv_witness_right
10Calculate and transport equalitiesL40–41

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

  1. L40
    rewrite heq at hv_witness_left
  2. L41
    rewrite heq at hv_witness_left
11Use earlier factsL42–42

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

  1. L42
    exact hv_witness_left
12Establish htailL43–45

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

  1. L43
    have htail : forall pfpad_tail_index_left_constant_sum_tail. (exists pfa_gap_left_constant_sum_tailbound. pfa_gap_left_constant_sum_tailbound + S (pfpad_tail_index_left_constant_sum_tail) = (i)) -> (((exists ff_h_pfp_left_constant_sum_tailzero. ff_h_pfp_left_constant_sum_tailzero + S (0) = S ((S ((1)+pfpad_tail_index_left_constant_sum_tail)) * dc)) /\ exists ff_q_pfp_left_constant_sum_tailzero. db = ff_q_pfp_left_constant_sum_tailzero * S ((S ((1)+pfpad_tail_index_left_constant_sum_tail)) * dc) + (0)))
  2. L44
    intro j
  3. L45
    intro hj
13Establish hvL46–48

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

  1. L46
    have hv : ∃ t. BetaAt(db,dc,1 + j,t) ∧ PolynomialDiagonalTerm(kb,kc,1,ab,ac,L,i,1 + j,t)Definitions: PolynomialDiagonalTermBetaAt
  2. L47
    specialize hd (1+j)
  3. L48
    apply hd
14Establish hindexL49–55

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

  1. L49
    have hindex : 1+j=S j
  2. L50
    simp [add_succ_left,zero_add]
  3. L51
    rewrite hindex
  4. L52
    specialize succ_le_succ (S j)
  5. L53
    specialize succ_le_succ (i)
  6. L54
    apply succ_le_succ
  7. L55
    exact hj
15Separate the logical casesL56–57

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

  1. L56
    cases hv
  2. L57
    cases hv_witness
16Establish heqL58–67

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply polynomial diagonal left unit tail term.

  1. L58
    have heq : x=0
  2. L59
    specialize polynomial_diagonal_left_unit_tail_term (kb)
  3. L60
    specialize polynomial_diagonal_left_unit_tail_term (kc)
  4. L61
    specialize polynomial_diagonal_left_unit_tail_term (ab)
  5. L62
    specialize polynomial_diagonal_left_unit_tail_term (ac)
  6. L63
    specialize polynomial_diagonal_left_unit_tail_term (L)
  7. L64
    specialize polynomial_diagonal_left_unit_tail_term (i)
  8. L65
    specialize polynomial_diagonal_left_unit_tail_term (1+j)
  9. L66
    specialize polynomial_diagonal_left_unit_tail_term (x)
  10. L67
    apply polynomial_diagonal_left_unit_tail_term
17Use earlier factsL68–71

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

  1. L68
    specialize le_add_right (1)
  2. L69
    specialize le_add_right (j)
  3. L70
    apply le_add_right
  4. L71
    exact hv_witness_right
18Calculate and transport equalitiesL72–73

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

  1. L72
    rewrite heq at hv_witness_left
  2. L73
    rewrite heq at hv_witness_left
19Use earlier factsL74–74

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

  1. L74
    exact hv_witness_left
20Establish hsingleL75–79

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

  1. L75
    have hsingle : ∃ m. Sum(db,dc,1,m)Definitions: Sum
  2. L76
    specialize beta_sum_exists (db)
  3. L77
    specialize beta_sum_exists (dc)
  4. L78
    specialize beta_sum_exists (1)
  5. L79
    apply beta_sum_exists
21Separate the logical casesL80–80

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

  1. L80
    cases hsingle
22Establish hdecompL81–87

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

  1. L81
    have hdecomp : ∃ t. ∃ s. BetaAt(db,dc,0,t) ∧ (Sum(db,dc,0,s) ∧ x = s + t)Definitions: BetaAtSum
  2. L82
    specialize beta_sum_succ_decompose (db)
  3. L83
    specialize beta_sum_succ_decompose (dc)
  4. L84
    specialize beta_sum_succ_decompose (0)
  5. L85
    specialize beta_sum_succ_decompose (x)
  6. L86
    apply beta_sum_succ_decompose
  7. L87
    exact hsingle_witness
23Separate the logical casesL88–91

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

  1. L88
    cases hdecomp
  2. L89
    cases hdecomp_witness
  3. L90
    cases hdecomp_witness_witness
  4. L91
    cases hdecomp_witness_witness_right
24Establish hzeroL92–97

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

  1. L92
    have hzero : x2=0
  2. L93
    specialize beta_sum_zero (db)
  3. L94
    specialize beta_sum_zero (dc)
  4. L95
    specialize beta_sum_zero (x2)
  5. L96
    apply beta_sum_zero
  6. L97
    exact hdecomp_witness_witness_right_left
25Establish hentryL98–106

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

  1. L98
    have hentry : x1=k*a
  2. L99
    specialize beta_at_unique (db)
  3. L100
    specialize beta_at_unique (dc)
  4. L101
    specialize beta_at_unique (0)
  5. L102
    specialize beta_at_unique (x1)
  6. L103
    specialize beta_at_unique (k*a)
  7. L104
    apply beta_at_unique
  8. L105
    exact hdecomp_witness_witness_left
  9. L106
    exact hhead
26Establish hvalueL107–116

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

  1. L107
    have hvalue : x=k*a
  2. L108
    trans x2+x1
  3. L109
    exact hdecomp_witness_witness_right_right
  4. L110
    rewrite hzero
  5. L111
    trans x1
  6. L112
    apply zero_add
  7. L113
    exact hentry
  8. L114
    trans x
  9. L115
    specialize polynomial_zero_tail_natural_sum_invariant (db)
  10. L116
    specialize polynomial_zero_tail_natural_sum_invariant (dc)
27Use earlier factsL117–123

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

  1. L117
    specialize polynomial_zero_tail_natural_sum_invariant (db)
  2. L118
    specialize polynomial_zero_tail_natural_sum_invariant (dc)
  3. L119
    specialize polynomial_zero_tail_natural_sum_invariant (1)
  4. L120
    specialize polynomial_zero_tail_natural_sum_invariant (i)
  5. L121
    specialize polynomial_zero_tail_natural_sum_invariant (x)
  6. L122
    specialize polynomial_zero_tail_natural_sum_invariant (n)
  7. L123
    apply polynomial_zero_tail_natural_sum_invariant
28Fix variables and assumptionsL124–127

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

  1. L124
    intro j0
  2. L125
    intro v0
  3. L126
    intro hj0
  4. L127
    intro hv0
29Use earlier factsL128–130

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

  1. L128
    exact hv0
  2. L129
    exact htail
  3. L130
    exact hsingle_witness
30Establish hlengthL131–137

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

  1. L131
    have hlength : 1+i=S i
  2. L132
    simp [add_succ_left,zero_add]
  3. L133
    rewrite hlength
  4. L134
    rewrite hlength
  5. L135
    rewrite hlength
  6. L136
    exact hs
  7. L137
    exact hvalue

Library-wide reading audit

Original exact command ledger · 137 lines
  1. 0001intro k
  2. 0002intro kb
  3. 0003intro kc
  4. 0004intro ab
  5. 0005intro ac
  6. 0006intro L
  7. 0007intro i
  8. 0008intro a
  9. 0009intro db
  10. 0010intro dc
  11. 0011intro n
  12. 0012intro hk
  13. 0013intro hi
  14. 0014intro ha
  15. 0015intro hd
  16. 0016intro hs
  17. 0017have hhead : ((exists ff_h_pfp_left_constant_sum_head. ff_h_pfp_left_constant_sum_head + S (k*a) = S ((S (0)) * dc)) /\ exists ff_q_pfp_left_constant_sum_head. db = ff_q_pfp_left_constant_sum_head * S ((S (0)) * dc) + (k*a))
  18. 0018have hv : exists t. ((((exists ff_h_pfp_left_constant_sum_first_entry. ff_h_pfp_left_constant_sum_first_entry + S (t) = S ((S (0)) * dc)) /\ exists ff_q_pfp_left_constant_sum_first_entry. db = ff_q_pfp_left_constant_sum_first_entry * S ((S (0)) * dc) + (t))) /\ ((exists pfc_complement_left_constant_sum_first_term pfc_left_left_constant_sum_first_term pfc_right_left_constant_sum_first_term. (((0)+pfc_complement_left_constant_sum_first_term=(i)) /\ ((((((exists pfa_gap_left_constant_sum_first_termleftinside. pfa_gap_left_constant_sum_first_termleftinside + S (0) = (1)) /\ ((((exists ff_h_pfp_left_constant_sum_first_termleftentry. ff_h_pfp_left_constant_sum_first_termleftentry + S (pfc_left_left_constant_sum_first_term) = S ((S (0)) * kc)) /\ exists ff_q_pfp_left_constant_sum_first_termleftentry. kb = ff_q_pfp_left_constant_sum_first_termleftentry * S ((S (0)) * kc) + (pfc_left_left_constant_sum_first_term)))))) \/ (((exists pfc_gap_left_constant_sum_first_termleftoutside. pfc_gap_left_constant_sum_first_termleftoutside+(1)=(0)) /\ (((pfc_left_left_constant_sum_first_term)=0))))) /\ ((((((exists pfa_gap_left_constant_sum_first_termrightinside. pfa_gap_left_constant_sum_first_termrightinside + S (pfc_complement_left_constant_sum_first_term) = (L)) /\ ((((exists ff_h_pfp_left_constant_sum_first_termrightentry. ff_h_pfp_left_constant_sum_first_termrightentry + S (pfc_right_left_constant_sum_first_term) = S ((S (pfc_complement_left_constant_sum_first_term)) * ac)) /\ exists ff_q_pfp_left_constant_sum_first_termrightentry. ab = ff_q_pfp_left_constant_sum_first_termrightentry * S ((S (pfc_complement_left_constant_sum_first_term)) * ac) + (pfc_right_left_constant_sum_first_term)))))) \/ (((exists pfc_gap_left_constant_sum_first_termrightoutside. pfc_gap_left_constant_sum_first_termrightoutside+(L)=(pfc_complement_left_constant_sum_first_term)) /\ (((pfc_right_left_constant_sum_first_term)=0))))) /\ (((t)=pfc_left_left_constant_sum_first_term*pfc_right_left_constant_sum_first_term))))))))))
  19. 0019specialize hd (0)
  20. 0020apply hd
  21. 0021exists i
  22. 0022simp
  23. 0023cases hv
  24. 0024cases hv_witness
  25. 0025have heq : x=k*a
  26. 0026specialize polynomial_diagonal_left_constant_first_term (k)
  27. 0027specialize polynomial_diagonal_left_constant_first_term (kb)
  28. 0028specialize polynomial_diagonal_left_constant_first_term (kc)
  29. 0029specialize polynomial_diagonal_left_constant_first_term (ab)
  30. 0030specialize polynomial_diagonal_left_constant_first_term (ac)
  31. 0031specialize polynomial_diagonal_left_constant_first_term (L)
  32. 0032specialize polynomial_diagonal_left_constant_first_term (i)
  33. 0033specialize polynomial_diagonal_left_constant_first_term (a)
  34. 0034specialize polynomial_diagonal_left_constant_first_term (x)
  35. 0035apply polynomial_diagonal_left_constant_first_term
  36. 0036exact hk
  37. 0037exact hi
  38. 0038exact ha
  39. 0039exact hv_witness_right
  40. 0040rewrite heq at hv_witness_left
  41. 0041rewrite heq at hv_witness_left
  42. 0042exact hv_witness_left
  43. 0043have htail : forall pfpad_tail_index_left_constant_sum_tail. (exists pfa_gap_left_constant_sum_tailbound. pfa_gap_left_constant_sum_tailbound + S (pfpad_tail_index_left_constant_sum_tail) = (i)) -> (((exists ff_h_pfp_left_constant_sum_tailzero. ff_h_pfp_left_constant_sum_tailzero + S (0) = S ((S ((1)+pfpad_tail_index_left_constant_sum_tail)) * dc)) /\ exists ff_q_pfp_left_constant_sum_tailzero. db = ff_q_pfp_left_constant_sum_tailzero * S ((S ((1)+pfpad_tail_index_left_constant_sum_tail)) * dc) + (0)))
  44. 0044intro j
  45. 0045intro hj
  46. 0046have hv : exists t. ((((exists ff_h_pfp_left_constant_sum_tail_entry. ff_h_pfp_left_constant_sum_tail_entry + S (t) = S ((S (1+j)) * dc)) /\ exists ff_q_pfp_left_constant_sum_tail_entry. db = ff_q_pfp_left_constant_sum_tail_entry * S ((S (1+j)) * dc) + (t))) /\ ((exists pfc_complement_left_constant_sum_tail_term pfc_left_left_constant_sum_tail_term pfc_right_left_constant_sum_tail_term. (((1+j)+pfc_complement_left_constant_sum_tail_term=(i)) /\ ((((((exists pfa_gap_left_constant_sum_tail_termleftinside. pfa_gap_left_constant_sum_tail_termleftinside + S (1+j) = (1)) /\ ((((exists ff_h_pfp_left_constant_sum_tail_termleftentry. ff_h_pfp_left_constant_sum_tail_termleftentry + S (pfc_left_left_constant_sum_tail_term) = S ((S (1+j)) * kc)) /\ exists ff_q_pfp_left_constant_sum_tail_termleftentry. kb = ff_q_pfp_left_constant_sum_tail_termleftentry * S ((S (1+j)) * kc) + (pfc_left_left_constant_sum_tail_term)))))) \/ (((exists pfc_gap_left_constant_sum_tail_termleftoutside. pfc_gap_left_constant_sum_tail_termleftoutside+(1)=(1+j)) /\ (((pfc_left_left_constant_sum_tail_term)=0))))) /\ ((((((exists pfa_gap_left_constant_sum_tail_termrightinside. pfa_gap_left_constant_sum_tail_termrightinside + S (pfc_complement_left_constant_sum_tail_term) = (L)) /\ ((((exists ff_h_pfp_left_constant_sum_tail_termrightentry. ff_h_pfp_left_constant_sum_tail_termrightentry + S (pfc_right_left_constant_sum_tail_term) = S ((S (pfc_complement_left_constant_sum_tail_term)) * ac)) /\ exists ff_q_pfp_left_constant_sum_tail_termrightentry. ab = ff_q_pfp_left_constant_sum_tail_termrightentry * S ((S (pfc_complement_left_constant_sum_tail_term)) * ac) + (pfc_right_left_constant_sum_tail_term)))))) \/ (((exists pfc_gap_left_constant_sum_tail_termrightoutside. pfc_gap_left_constant_sum_tail_termrightoutside+(L)=(pfc_complement_left_constant_sum_tail_term)) /\ (((pfc_right_left_constant_sum_tail_term)=0))))) /\ (((t)=pfc_left_left_constant_sum_tail_term*pfc_right_left_constant_sum_tail_term))))))))))
  47. 0047specialize hd (1+j)
  48. 0048apply hd
  49. 0049have hindex : 1+j=S j
  50. 0050simp [add_succ_left,zero_add]
  51. 0051rewrite hindex
  52. 0052specialize succ_le_succ (S j)
  53. 0053specialize succ_le_succ (i)
  54. 0054apply succ_le_succ
  55. 0055exact hj
  56. 0056cases hv
  57. 0057cases hv_witness
  58. 0058have heq : x=0
  59. 0059specialize polynomial_diagonal_left_unit_tail_term (kb)
  60. 0060specialize polynomial_diagonal_left_unit_tail_term (kc)
  61. 0061specialize polynomial_diagonal_left_unit_tail_term (ab)
  62. 0062specialize polynomial_diagonal_left_unit_tail_term (ac)
  63. 0063specialize polynomial_diagonal_left_unit_tail_term (L)
  64. 0064specialize polynomial_diagonal_left_unit_tail_term (i)
  65. 0065specialize polynomial_diagonal_left_unit_tail_term (1+j)
  66. 0066specialize polynomial_diagonal_left_unit_tail_term (x)
  67. 0067apply polynomial_diagonal_left_unit_tail_term
  68. 0068specialize le_add_right (1)
  69. 0069specialize le_add_right (j)
  70. 0070apply le_add_right
  71. 0071exact hv_witness_right
  72. 0072rewrite heq at hv_witness_left
  73. 0073rewrite heq at hv_witness_left
  74. 0074exact hv_witness_left
  75. 0075have hsingle : exists m. (exists fs_u_pfc_left_constant_single_sum fs_v_pfc_left_constant_single_sum. ((((exists fs_h_pfc_left_constant_single_sum_body_start. fs_h_pfc_left_constant_single_sum_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_constant_single_sum)) /\ exists fs_q_pfc_left_constant_single_sum_body_start. fs_u_pfc_left_constant_single_sum = fs_q_pfc_left_constant_single_sum_body_start * S ((S (0)) * fs_v_pfc_left_constant_single_sum) + (0))) /\ ((((exists fs_h_pfc_left_constant_single_sum_body_terminal. fs_h_pfc_left_constant_single_sum_body_terminal + S (m) = S ((S (1)) * fs_v_pfc_left_constant_single_sum)) /\ exists fs_q_pfc_left_constant_single_sum_body_terminal. fs_u_pfc_left_constant_single_sum = fs_q_pfc_left_constant_single_sum_body_terminal * S ((S (1)) * fs_v_pfc_left_constant_single_sum) + (m))) /\ forall fs_i_pfc_left_constant_single_sum_body_steps. (exists fs_lt_pfc_left_constant_single_sum_body_steps_bound. fs_lt_pfc_left_constant_single_sum_body_steps_bound + S fs_i_pfc_left_constant_single_sum_body_steps = 1) -> exists fs_a_pfc_left_constant_single_sum_body_steps fs_r_pfc_left_constant_single_sum_body_steps fs_s_pfc_left_constant_single_sum_body_steps. ((((exists fs_h_pfc_left_constant_single_sum_body_steps_summand. fs_h_pfc_left_constant_single_sum_body_steps_summand + S (fs_a_pfc_left_constant_single_sum_body_steps) = S ((S (fs_i_pfc_left_constant_single_sum_body_steps)) * dc)) /\ exists fs_q_pfc_left_constant_single_sum_body_steps_summand. db = fs_q_pfc_left_constant_single_sum_body_steps_summand * S ((S (fs_i_pfc_left_constant_single_sum_body_steps)) * dc) + (fs_a_pfc_left_constant_single_sum_body_steps))) /\ ((((exists fs_h_pfc_left_constant_single_sum_body_steps_partial. fs_h_pfc_left_constant_single_sum_body_steps_partial + S (fs_r_pfc_left_constant_single_sum_body_steps) = S ((S (fs_i_pfc_left_constant_single_sum_body_steps)) * fs_v_pfc_left_constant_single_sum)) /\ exists fs_q_pfc_left_constant_single_sum_body_steps_partial. fs_u_pfc_left_constant_single_sum = fs_q_pfc_left_constant_single_sum_body_steps_partial * S ((S (fs_i_pfc_left_constant_single_sum_body_steps)) * fs_v_pfc_left_constant_single_sum) + (fs_r_pfc_left_constant_single_sum_body_steps))) /\ ((((exists fs_h_pfc_left_constant_single_sum_body_steps_successor. fs_h_pfc_left_constant_single_sum_body_steps_successor + S (fs_s_pfc_left_constant_single_sum_body_steps) = S ((S (S fs_i_pfc_left_constant_single_sum_body_steps)) * fs_v_pfc_left_constant_single_sum)) /\ exists fs_q_pfc_left_constant_single_sum_body_steps_successor. fs_u_pfc_left_constant_single_sum = fs_q_pfc_left_constant_single_sum_body_steps_successor * S ((S (S fs_i_pfc_left_constant_single_sum_body_steps)) * fs_v_pfc_left_constant_single_sum) + (fs_s_pfc_left_constant_single_sum_body_steps))) /\ fs_s_pfc_left_constant_single_sum_body_steps = fs_r_pfc_left_constant_single_sum_body_steps + fs_a_pfc_left_constant_single_sum_body_steps))))))
  76. 0076specialize beta_sum_exists (db)
  77. 0077specialize beta_sum_exists (dc)
  78. 0078specialize beta_sum_exists (1)
  79. 0079apply beta_sum_exists
  80. 0080cases hsingle
  81. 0081have hdecomp : exists t s. ((((exists ff_h_pfp_left_constant_single_entry. ff_h_pfp_left_constant_single_entry + S (t) = S ((S (0)) * dc)) /\ exists ff_q_pfp_left_constant_single_entry. db = ff_q_pfp_left_constant_single_entry * S ((S (0)) * dc) + (t))) /\ (((exists fs_u_pfc_left_constant_single_empty fs_v_pfc_left_constant_single_empty. ((((exists fs_h_pfc_left_constant_single_empty_body_start. fs_h_pfc_left_constant_single_empty_body_start + S (0) = S ((S (0)) * fs_v_pfc_left_constant_single_empty)) /\ exists fs_q_pfc_left_constant_single_empty_body_start. fs_u_pfc_left_constant_single_empty = fs_q_pfc_left_constant_single_empty_body_start * S ((S (0)) * fs_v_pfc_left_constant_single_empty) + (0))) /\ ((((exists fs_h_pfc_left_constant_single_empty_body_terminal. fs_h_pfc_left_constant_single_empty_body_terminal + S (s) = S ((S (0)) * fs_v_pfc_left_constant_single_empty)) /\ exists fs_q_pfc_left_constant_single_empty_body_terminal. fs_u_pfc_left_constant_single_empty = fs_q_pfc_left_constant_single_empty_body_terminal * S ((S (0)) * fs_v_pfc_left_constant_single_empty) + (s))) /\ forall fs_i_pfc_left_constant_single_empty_body_steps. (exists fs_lt_pfc_left_constant_single_empty_body_steps_bound. fs_lt_pfc_left_constant_single_empty_body_steps_bound + S fs_i_pfc_left_constant_single_empty_body_steps = 0) -> exists fs_a_pfc_left_constant_single_empty_body_steps fs_r_pfc_left_constant_single_empty_body_steps fs_s_pfc_left_constant_single_empty_body_steps. ((((exists fs_h_pfc_left_constant_single_empty_body_steps_summand. fs_h_pfc_left_constant_single_empty_body_steps_summand + S (fs_a_pfc_left_constant_single_empty_body_steps) = S ((S (fs_i_pfc_left_constant_single_empty_body_steps)) * dc)) /\ exists fs_q_pfc_left_constant_single_empty_body_steps_summand. db = fs_q_pfc_left_constant_single_empty_body_steps_summand * S ((S (fs_i_pfc_left_constant_single_empty_body_steps)) * dc) + (fs_a_pfc_left_constant_single_empty_body_steps))) /\ ((((exists fs_h_pfc_left_constant_single_empty_body_steps_partial. fs_h_pfc_left_constant_single_empty_body_steps_partial + S (fs_r_pfc_left_constant_single_empty_body_steps) = S ((S (fs_i_pfc_left_constant_single_empty_body_steps)) * fs_v_pfc_left_constant_single_empty)) /\ exists fs_q_pfc_left_constant_single_empty_body_steps_partial. fs_u_pfc_left_constant_single_empty = fs_q_pfc_left_constant_single_empty_body_steps_partial * S ((S (fs_i_pfc_left_constant_single_empty_body_steps)) * fs_v_pfc_left_constant_single_empty) + (fs_r_pfc_left_constant_single_empty_body_steps))) /\ ((((exists fs_h_pfc_left_constant_single_empty_body_steps_successor. fs_h_pfc_left_constant_single_empty_body_steps_successor + S (fs_s_pfc_left_constant_single_empty_body_steps) = S ((S (S fs_i_pfc_left_constant_single_empty_body_steps)) * fs_v_pfc_left_constant_single_empty)) /\ exists fs_q_pfc_left_constant_single_empty_body_steps_successor. fs_u_pfc_left_constant_single_empty = fs_q_pfc_left_constant_single_empty_body_steps_successor * S ((S (S fs_i_pfc_left_constant_single_empty_body_steps)) * fs_v_pfc_left_constant_single_empty) + (fs_s_pfc_left_constant_single_empty_body_steps))) /\ fs_s_pfc_left_constant_single_empty_body_steps = fs_r_pfc_left_constant_single_empty_body_steps + fs_a_pfc_left_constant_single_empty_body_steps)))))) /\ ((x=s+t)))))
  82. 0082specialize beta_sum_succ_decompose (db)
  83. 0083specialize beta_sum_succ_decompose (dc)
  84. 0084specialize beta_sum_succ_decompose (0)
  85. 0085specialize beta_sum_succ_decompose (x)
  86. 0086apply beta_sum_succ_decompose
  87. 0087exact hsingle_witness
  88. 0088cases hdecomp
  89. 0089cases hdecomp_witness
  90. 0090cases hdecomp_witness_witness
  91. 0091cases hdecomp_witness_witness_right
  92. 0092have hzero : x2=0
  93. 0093specialize beta_sum_zero (db)
  94. 0094specialize beta_sum_zero (dc)
  95. 0095specialize beta_sum_zero (x2)
  96. 0096apply beta_sum_zero
  97. 0097exact hdecomp_witness_witness_right_left
  98. 0098have hentry : x1=k*a
  99. 0099specialize beta_at_unique (db)
  100. 0100specialize beta_at_unique (dc)
  101. 0101specialize beta_at_unique (0)
  102. 0102specialize beta_at_unique (x1)
  103. 0103specialize beta_at_unique (k*a)
  104. 0104apply beta_at_unique
  105. 0105exact hdecomp_witness_witness_left
  106. 0106exact hhead
  107. 0107have hvalue : x=k*a
  108. 0108trans x2+x1
  109. 0109exact hdecomp_witness_witness_right_right
  110. 0110rewrite hzero
  111. 0111trans x1
  112. 0112apply zero_add
  113. 0113exact hentry
  114. 0114trans x
  115. 0115specialize polynomial_zero_tail_natural_sum_invariant (db)
  116. 0116specialize polynomial_zero_tail_natural_sum_invariant (dc)
  117. 0117specialize polynomial_zero_tail_natural_sum_invariant (db)
  118. 0118specialize polynomial_zero_tail_natural_sum_invariant (dc)
  119. 0119specialize polynomial_zero_tail_natural_sum_invariant (1)
  120. 0120specialize polynomial_zero_tail_natural_sum_invariant (i)
  121. 0121specialize polynomial_zero_tail_natural_sum_invariant (x)
  122. 0122specialize polynomial_zero_tail_natural_sum_invariant (n)
  123. 0123apply polynomial_zero_tail_natural_sum_invariant
  124. 0124intro j0
  125. 0125intro v0
  126. 0126intro hj0
  127. 0127intro hv0
  128. 0128exact hv0
  129. 0129exact htail
  130. 0130exact hsingle_witness
  131. 0131have hlength : 1+i=S i
  132. 0132simp [add_succ_left,zero_add]
  133. 0133rewrite hlength
  134. 0134rewrite hlength
  135. 0135rewrite hlength
  136. 0136exact hs
  137. 0137exact hvalue