PA00EK · theorem

beta_repeat_sum_exact

Alpha v34 checked-use theorem · independently closed; not Stable

A constant beta prefix has exact relational sum length times value.

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 original first-admission records.

Statement with defined notation

∀ b. ∀ c. ∀ a. ∀ l. ∀ n. Repeat(b,c,a,l) → Sum(b,c,l,n) → n = l · a

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0015 Sum PD0019 Repeat

2 occurrences

In local proof propositions

PD0013 BetaAt PD0015 Sum PD0019 Repeat

3 occurrences

Exact expanded native-PA statement
forall b c a l n. (forall ff_i_repeatsum_repeat. (exists ff_lt_repeatsum_repeat_bound. ff_lt_repeatsum_repeat_bound + S ff_i_repeatsum_repeat = l) -> (((exists ff_h_repeatsum_repeat_decoded. ff_h_repeatsum_repeat_decoded + S (a) = S ((S (ff_i_repeatsum_repeat)) * c)) /\ exists ff_q_repeatsum_repeat_decoded. b = ff_q_repeatsum_repeat_decoded * S ((S (ff_i_repeatsum_repeat)) * c) + (a)))) -> (exists ff_u_repeatsum_sum ff_v_repeatsum_sum. ((((exists ff_h_repeatsum_sum_start. ff_h_repeatsum_sum_start + S (0) = S ((S (0)) * ff_v_repeatsum_sum)) /\ exists ff_q_repeatsum_sum_start. ff_u_repeatsum_sum = ff_q_repeatsum_sum_start * S ((S (0)) * ff_v_repeatsum_sum) + (0))) /\ ((((exists ff_h_repeatsum_sum_terminal. ff_h_repeatsum_sum_terminal + S (n) = S ((S (l)) * ff_v_repeatsum_sum)) /\ exists ff_q_repeatsum_sum_terminal. ff_u_repeatsum_sum = ff_q_repeatsum_sum_terminal * S ((S (l)) * ff_v_repeatsum_sum) + (n))) /\ forall ff_i_repeatsum_sum. (exists ff_lt_repeatsum_sum_bound. ff_lt_repeatsum_sum_bound + S ff_i_repeatsum_sum = l) -> exists ff_a_repeatsum_sum ff_r_repeatsum_sum ff_s_repeatsum_sum. ((((exists ff_h_repeatsum_sum_summand. ff_h_repeatsum_sum_summand + S (ff_a_repeatsum_sum) = S ((S (ff_i_repeatsum_sum)) * c)) /\ exists ff_q_repeatsum_sum_summand. b = ff_q_repeatsum_sum_summand * S ((S (ff_i_repeatsum_sum)) * c) + (ff_a_repeatsum_sum))) /\ ((((exists ff_h_repeatsum_sum_partial. ff_h_repeatsum_sum_partial + S (ff_r_repeatsum_sum) = S ((S (ff_i_repeatsum_sum)) * ff_v_repeatsum_sum)) /\ exists ff_q_repeatsum_sum_partial. ff_u_repeatsum_sum = ff_q_repeatsum_sum_partial * S ((S (ff_i_repeatsum_sum)) * ff_v_repeatsum_sum) + (ff_r_repeatsum_sum))) /\ ((((exists ff_h_repeatsum_sum_successor. ff_h_repeatsum_sum_successor + S (ff_s_repeatsum_sum) = S ((S (S ff_i_repeatsum_sum)) * ff_v_repeatsum_sum)) /\ exists ff_q_repeatsum_sum_successor. ff_u_repeatsum_sum = ff_q_repeatsum_sum_successor * S ((S (S ff_i_repeatsum_sum)) * ff_v_repeatsum_sum) + (ff_s_repeatsum_sum))) /\ ff_s_repeatsum_sum = ff_r_repeatsum_sum + ff_a_repeatsum_sum)))))) -> n = l * a

Proof neighborhood

Direct theorem prerequisites

PA0047 beta_sum_zero PA003Y beta_sum_succ_decompose PA002O le_succ PA001A le_refl PA004C beta_repeat_entry_eq PA000D mul_zero_left PA000G mul_succ_left

Direct theorem dependents

PA00EL beta_repeat_sum_exists_exact PA00ES eisenstein_zero_width_rectangle_sum_zero

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

Read the argument

Proof checkpoints

64 script commands · 14 reading checkpoints · 5 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

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 (7)
beta sum zerobeta sum succ decomposele succle reflbeta repeat entry eqmul zero leftmul succ left
01Fix variables and assumptionsL1–3

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro a
02Induction on lL4–7

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction l
  2. L5
    intro n
  3. L6
    intro hrepeat
  4. L7
    intro hsum
03Establish hnL8–17

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

  1. L8
    have hn : n = 0
  2. L9
    specialize beta_sum_zero b
  3. L10
    specialize beta_sum_zero c
  4. L11
    specialize beta_sum_zero n
  5. L12
    apply beta_sum_zero
  6. L13
    exact hsum
  7. L14
    rewrite hn
  8. L15
    symm
  9. L16
    specialize mul_zero_left a
  10. L17
    exact mul_zero_left
04Fix variables and assumptionsL18–20

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

  1. L18
    intro n
  2. L19
    intro hrepeat
  3. L20
    intro hsum
05Establish hdecompL21–27

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

  1. L21
    have hdecomp : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Sum(b,c,l,r) ∧ n = r + a)Definitions: BetaAt(b,c,l,a)Sum(b,c,l,r)Original native command in the exact edition
  2. L22
    specialize beta_sum_succ_decompose b
  3. L23
    specialize beta_sum_succ_decompose c
  4. L24
    specialize beta_sum_succ_decompose l
  5. L25
    specialize beta_sum_succ_decompose n
  6. L26
    apply beta_sum_succ_decompose
  7. L27
    exact hsum
06Separate the logical casesL28–31

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

  1. L28
    cases hdecomp
  2. L29
    cases hdecomp_witness
  3. L30
    cases hdecomp_witness_witness
  4. L31
    cases hdecomp_witness_witness_right
07Establish hprefix_repeatL32–40

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

  1. L32
    have hprefix_repeat : Repeat(b,c,a,l)Definitions: Repeat(b,c,a,l)Original native command in the exact edition
  2. L33
    intro i
  3. L34
    intro hi
  4. L35
    specialize hrepeat i
  5. L36
    apply hrepeat
  6. L37
    specialize le_succ (S i)
  7. L38
    specialize le_succ l
  8. L39
    apply le_succ
  9. L40
    exact hi
08Establish hprefixL41–45

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

  1. L41
    have hprefix : x1 = l * a
  2. L42
    specialize IH x1
  3. L43
    apply IH
  4. L44
    exact hprefix_repeat
  5. L45
    exact hdecomp_witness_witness_right_left
09Establish hlastL46–55

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

  1. L46
    have hlast : x = a
  2. L47
    specialize beta_repeat_entry_eq b
  3. L48
    specialize beta_repeat_entry_eq c
  4. L49
    specialize beta_repeat_entry_eq a
  5. L50
    specialize beta_repeat_entry_eq (S l)
  6. L51
    specialize beta_repeat_entry_eq l
  7. L52
    specialize beta_repeat_entry_eq x
  8. L53
    apply beta_repeat_entry_eq
  9. L54
    exact hrepeat
  10. L55
    specialize le_refl (S l)
10Use earlier factsL56–57

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

  1. L56
    exact le_refl
  2. L57
    exact hdecomp_witness_witness_left
11Calculate and transport equalitiesL58–60

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

  1. L58
    rewrite hdecomp_witness_witness_right_right
  2. L59
    rewrite hprefix
  3. L60
    rewrite hlast
12Use earlier factsL61–62

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

  1. L61
    specialize mul_succ_left l
  2. L62
    specialize mul_succ_left a
13Calculate and transport equalitiesL63–63

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

  1. L63
    symm
14Use earlier factsL64–64

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

  1. L64
    exact mul_succ_left

Library-wide reading audit

Original defined command ledger · 64 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004induction l
  5. 0005intro n
  6. 0006intro hrepeat
  7. 0007intro hsum
  8. 0008have hn : n = 0
  9. 0009specialize beta_sum_zero b
  10. 0010specialize beta_sum_zero c
  11. 0011specialize beta_sum_zero n
  12. 0012apply beta_sum_zero
  13. 0013exact hsum
  14. 0014rewrite hn
  15. 0015symm
  16. 0016specialize mul_zero_left a
  17. 0017exact mul_zero_left
  18. 0018intro n
  19. 0019intro hrepeat
  20. 0020intro hsum
  21. 0021have hdecomp : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Sum(b,c,l,r) ∧ n = r + a)
    Exact native replay linehave hdecomp : exists a r. (((exists ff_h_repeatsum_decomp_entry. ff_h_repeatsum_decomp_entry + S (a) = S ((S (l)) * c)) /\ exists ff_q_repeatsum_decomp_entry. b = ff_q_repeatsum_decomp_entry * S ((S (l)) * c) + (a))) /\ ((exists ff_u_repeatsum_decomp_prefix ff_v_repeatsum_decomp_prefix. ((((exists ff_h_repeatsum_decomp_prefix_start. ff_h_repeatsum_decomp_prefix_start + S (0) = S ((S (0)) * ff_v_repeatsum_decomp_prefix)) /\ exists ff_q_repeatsum_decomp_prefix_start. ff_u_repeatsum_decomp_prefix = ff_q_repeatsum_decomp_prefix_start * S ((S (0)) * ff_v_repeatsum_decomp_prefix) + (0))) /\ ((((exists ff_h_repeatsum_decomp_prefix_terminal. ff_h_repeatsum_decomp_prefix_terminal + S (r) = S ((S (l)) * ff_v_repeatsum_decomp_prefix)) /\ exists ff_q_repeatsum_decomp_prefix_terminal. ff_u_repeatsum_decomp_prefix = ff_q_repeatsum_decomp_prefix_terminal * S ((S (l)) * ff_v_repeatsum_decomp_prefix) + (r))) /\ forall ff_i_repeatsum_decomp_prefix. (exists ff_lt_repeatsum_decomp_prefix_bound. ff_lt_repeatsum_decomp_prefix_bound + S ff_i_repeatsum_decomp_prefix = l) -> exists ff_a_repeatsum_decomp_prefix ff_r_repeatsum_decomp_prefix ff_s_repeatsum_decomp_prefix. ((((exists ff_h_repeatsum_decomp_prefix_summand. ff_h_repeatsum_decomp_prefix_summand + S (ff_a_repeatsum_decomp_prefix) = S ((S (ff_i_repeatsum_decomp_prefix)) * c)) /\ exists ff_q_repeatsum_decomp_prefix_summand. b = ff_q_repeatsum_decomp_prefix_summand * S ((S (ff_i_repeatsum_decomp_prefix)) * c) + (ff_a_repeatsum_decomp_prefix))) /\ ((((exists ff_h_repeatsum_decomp_prefix_partial. ff_h_repeatsum_decomp_prefix_partial + S (ff_r_repeatsum_decomp_prefix) = S ((S (ff_i_repeatsum_decomp_prefix)) * ff_v_repeatsum_decomp_prefix)) /\ exists ff_q_repeatsum_decomp_prefix_partial. ff_u_repeatsum_decomp_prefix = ff_q_repeatsum_decomp_prefix_partial * S ((S (ff_i_repeatsum_decomp_prefix)) * ff_v_repeatsum_decomp_prefix) + (ff_r_repeatsum_decomp_prefix))) /\ ((((exists ff_h_repeatsum_decomp_prefix_successor. ff_h_repeatsum_decomp_prefix_successor + S (ff_s_repeatsum_decomp_prefix) = S ((S (S ff_i_repeatsum_decomp_prefix)) * ff_v_repeatsum_decomp_prefix)) /\ exists ff_q_repeatsum_decomp_prefix_successor. ff_u_repeatsum_decomp_prefix = ff_q_repeatsum_decomp_prefix_successor * S ((S (S ff_i_repeatsum_decomp_prefix)) * ff_v_repeatsum_decomp_prefix) + (ff_s_repeatsum_decomp_prefix))) /\ ff_s_repeatsum_decomp_prefix = ff_r_repeatsum_decomp_prefix + ff_a_repeatsum_decomp_prefix)))))) /\ n = r + a)
  22. 0022specialize beta_sum_succ_decompose b
  23. 0023specialize beta_sum_succ_decompose c
  24. 0024specialize beta_sum_succ_decompose l
  25. 0025specialize beta_sum_succ_decompose n
  26. 0026apply beta_sum_succ_decompose
  27. 0027exact hsum
  28. 0028cases hdecomp
  29. 0029cases hdecomp_witness
  30. 0030cases hdecomp_witness_witness
  31. 0031cases hdecomp_witness_witness_right
  32. 0032have hprefix_repeat : Repeat(b,c,a,l)
    Exact native replay linehave hprefix_repeat : forall ff_i_repeatsum_prefix_repeat. (exists ff_lt_repeatsum_prefix_repeat_bound. ff_lt_repeatsum_prefix_repeat_bound + S ff_i_repeatsum_prefix_repeat = l) -> (((exists ff_h_repeatsum_prefix_repeat_decoded. ff_h_repeatsum_prefix_repeat_decoded + S (a) = S ((S (ff_i_repeatsum_prefix_repeat)) * c)) /\ exists ff_q_repeatsum_prefix_repeat_decoded. b = ff_q_repeatsum_prefix_repeat_decoded * S ((S (ff_i_repeatsum_prefix_repeat)) * c) + (a)))
  33. 0033intro i
  34. 0034intro hi
  35. 0035specialize hrepeat i
  36. 0036apply hrepeat
  37. 0037specialize le_succ (S i)
  38. 0038specialize le_succ l
  39. 0039apply le_succ
  40. 0040exact hi
  41. 0041have hprefix : x1 = l * a
  42. 0042specialize IH x1
  43. 0043apply IH
  44. 0044exact hprefix_repeat
  45. 0045exact hdecomp_witness_witness_right_left
  46. 0046have hlast : x = a
  47. 0047specialize beta_repeat_entry_eq b
  48. 0048specialize beta_repeat_entry_eq c
  49. 0049specialize beta_repeat_entry_eq a
  50. 0050specialize beta_repeat_entry_eq (S l)
  51. 0051specialize beta_repeat_entry_eq l
  52. 0052specialize beta_repeat_entry_eq x
  53. 0053apply beta_repeat_entry_eq
  54. 0054exact hrepeat
  55. 0055specialize le_refl (S l)
  56. 0056exact le_refl
  57. 0057exact hdecomp_witness_witness_left
  58. 0058rewrite hdecomp_witness_witness_right_right
  59. 0059rewrite hprefix
  60. 0060rewrite hlast
  61. 0061specialize mul_succ_left l
  62. 0062specialize mul_succ_left a
  63. 0063symm
  64. 0064exact mul_succ_left