PA00EK

beta_repeat_sum_exact

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

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

Exact expanded 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

Structural proof guide

Generated structural guide

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

Use the direct prerequisites beta_sum_zero, beta_sum_succ_decompose, le_succ, le_refl, beta_repeat_entry_eq, mul_zero_left, mul_succ_left as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (4), intermediate claims (5), equality transport (4).

Referenced ingredients

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

Proof neighborhood

Direct dependencies

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 dependents

PA00EL beta_repeat_sum_exists_exact PA00ES eisenstein_zero_width_rectangle_sum_zero

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

  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 : 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 : 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