PA00EL · theorem

beta_repeat_sum_exists_exact

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

Every value and length admit a constant prefix with its exact sum.

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

∀ a. ∀ l. ∃ b. ∃ c. ∃ 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

PD0015 Sum PD0019 Repeat

2 occurrences

Exact expanded native-PA statement
forall a l. exists b c n. (forall ff_i_repeatsum_exists_repeat. (exists ff_lt_repeatsum_exists_repeat_bound. ff_lt_repeatsum_exists_repeat_bound + S ff_i_repeatsum_exists_repeat = l) -> (((exists ff_h_repeatsum_exists_repeat_decoded. ff_h_repeatsum_exists_repeat_decoded + S (a) = S ((S (ff_i_repeatsum_exists_repeat)) * c)) /\ exists ff_q_repeatsum_exists_repeat_decoded. b = ff_q_repeatsum_exists_repeat_decoded * S ((S (ff_i_repeatsum_exists_repeat)) * c) + (a)))) /\ ((exists ff_u_repeatsum_exists_sum ff_v_repeatsum_exists_sum. ((((exists ff_h_repeatsum_exists_sum_start. ff_h_repeatsum_exists_sum_start + S (0) = S ((S (0)) * ff_v_repeatsum_exists_sum)) /\ exists ff_q_repeatsum_exists_sum_start. ff_u_repeatsum_exists_sum = ff_q_repeatsum_exists_sum_start * S ((S (0)) * ff_v_repeatsum_exists_sum) + (0))) /\ ((((exists ff_h_repeatsum_exists_sum_terminal. ff_h_repeatsum_exists_sum_terminal + S (n) = S ((S (l)) * ff_v_repeatsum_exists_sum)) /\ exists ff_q_repeatsum_exists_sum_terminal. ff_u_repeatsum_exists_sum = ff_q_repeatsum_exists_sum_terminal * S ((S (l)) * ff_v_repeatsum_exists_sum) + (n))) /\ forall ff_i_repeatsum_exists_sum. (exists ff_lt_repeatsum_exists_sum_bound. ff_lt_repeatsum_exists_sum_bound + S ff_i_repeatsum_exists_sum = l) -> exists ff_a_repeatsum_exists_sum ff_r_repeatsum_exists_sum ff_s_repeatsum_exists_sum. ((((exists ff_h_repeatsum_exists_sum_summand. ff_h_repeatsum_exists_sum_summand + S (ff_a_repeatsum_exists_sum) = S ((S (ff_i_repeatsum_exists_sum)) * c)) /\ exists ff_q_repeatsum_exists_sum_summand. b = ff_q_repeatsum_exists_sum_summand * S ((S (ff_i_repeatsum_exists_sum)) * c) + (ff_a_repeatsum_exists_sum))) /\ ((((exists ff_h_repeatsum_exists_sum_partial. ff_h_repeatsum_exists_sum_partial + S (ff_r_repeatsum_exists_sum) = S ((S (ff_i_repeatsum_exists_sum)) * ff_v_repeatsum_exists_sum)) /\ exists ff_q_repeatsum_exists_sum_partial. ff_u_repeatsum_exists_sum = ff_q_repeatsum_exists_sum_partial * S ((S (ff_i_repeatsum_exists_sum)) * ff_v_repeatsum_exists_sum) + (ff_r_repeatsum_exists_sum))) /\ ((((exists ff_h_repeatsum_exists_sum_successor. ff_h_repeatsum_exists_sum_successor + S (ff_s_repeatsum_exists_sum) = S ((S (S ff_i_repeatsum_exists_sum)) * ff_v_repeatsum_exists_sum)) /\ exists ff_q_repeatsum_exists_sum_successor. ff_u_repeatsum_exists_sum = ff_q_repeatsum_exists_sum_successor * S ((S (S ff_i_repeatsum_exists_sum)) * ff_v_repeatsum_exists_sum) + (ff_s_repeatsum_exists_sum))) /\ ff_s_repeatsum_exists_sum = ff_r_repeatsum_exists_sum + ff_a_repeatsum_exists_sum)))))) /\ n = l * a)

Proof neighborhood

Direct theorem prerequisites

PA0045 beta_repeat_exists PA003H beta_sum_exists PA00EK beta_repeat_sum_exact

Direct theorem dependents

PA00EQ eisenstein_rectangle_plus_column_count_total

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

31 script commands · 11 reading checkpoints · 3 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 (3)
beta repeat existsbeta sum existsbeta repeat sum exact
01Fix variables and assumptionsL1–2

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

  1. L1
    intro a
  2. L2
    intro l
02Establish hrepeatL3–6

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

  1. L3
    have hrepeat : ∃ b. ∃ c. Repeat(b,c,a,l)Definitions: Repeat(b,c,a,l)Original native command in the exact edition
  2. L4
    specialize beta_repeat_exists a
  3. L5
    specialize beta_repeat_exists l
  4. L6
    exact beta_repeat_exists
03Separate the logical casesL7–8

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

  1. L7
    cases hrepeat
  2. L8
    cases hrepeat_witness
04Establish hsumL9–13

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

  1. L9
    have hsum : ∃ n. Sum(x,x1,l,n)Definitions: Sum(x,x1,l,n)Original native command in the exact edition
  2. L10
    specialize beta_sum_exists x
  3. L11
    specialize beta_sum_exists x1
  4. L12
    specialize beta_sum_exists l
  5. L13
    exact beta_sum_exists
05Separate the logical casesL14–14

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

  1. L14
    cases hsum
06Establish hexactL15–23

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

  1. L15
    have hexact : x2 = l * a
  2. L16
    specialize beta_repeat_sum_exact x
  3. L17
    specialize beta_repeat_sum_exact x1
  4. L18
    specialize beta_repeat_sum_exact a
  5. L19
    specialize beta_repeat_sum_exact l
  6. L20
    specialize beta_repeat_sum_exact x2
  7. L21
    apply beta_repeat_sum_exact
  8. L22
    exact hrepeat_witness_witness
  9. L23
    exact hsum_witness
07Construct an explicit witnessL24–26

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

  1. L24
    exists x
  2. L25
    exists x1
  3. L26
    exists x2
08Separate the logical casesL27–27

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

  1. L27
    split
09Use earlier factsL28–28

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

  1. L28
    exact hrepeat_witness_witness
10Separate the logical casesL29–29

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

  1. L29
    split
11Use earlier factsL30–31

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

  1. L30
    exact hsum_witness
  2. L31
    exact hexact

Library-wide reading audit

Original defined command ledger · 31 lines
  1. 0001intro a
  2. 0002intro l
  3. 0003have hrepeat : ∃ b. ∃ c. Repeat(b,c,a,l)
    Exact native replay linehave hrepeat : exists b c. (forall ff_i_repeatsum_exists_repeat. (exists ff_lt_repeatsum_exists_repeat_bound. ff_lt_repeatsum_exists_repeat_bound + S ff_i_repeatsum_exists_repeat = l) -> (((exists ff_h_repeatsum_exists_repeat_decoded. ff_h_repeatsum_exists_repeat_decoded + S (a) = S ((S (ff_i_repeatsum_exists_repeat)) * c)) /\ exists ff_q_repeatsum_exists_repeat_decoded. b = ff_q_repeatsum_exists_repeat_decoded * S ((S (ff_i_repeatsum_exists_repeat)) * c) + (a))))
  4. 0004specialize beta_repeat_exists a
  5. 0005specialize beta_repeat_exists l
  6. 0006exact beta_repeat_exists
  7. 0007cases hrepeat
  8. 0008cases hrepeat_witness
  9. 0009have hsum : ∃ n. Sum(x,x1,l,n)
    Exact native replay linehave hsum : exists n. (exists ff_u_repeatsum_exists_trace ff_v_repeatsum_exists_trace. ((((exists ff_h_repeatsum_exists_trace_start. ff_h_repeatsum_exists_trace_start + S (0) = S ((S (0)) * ff_v_repeatsum_exists_trace)) /\ exists ff_q_repeatsum_exists_trace_start. ff_u_repeatsum_exists_trace = ff_q_repeatsum_exists_trace_start * S ((S (0)) * ff_v_repeatsum_exists_trace) + (0))) /\ ((((exists ff_h_repeatsum_exists_trace_terminal. ff_h_repeatsum_exists_trace_terminal + S (n) = S ((S (l)) * ff_v_repeatsum_exists_trace)) /\ exists ff_q_repeatsum_exists_trace_terminal. ff_u_repeatsum_exists_trace = ff_q_repeatsum_exists_trace_terminal * S ((S (l)) * ff_v_repeatsum_exists_trace) + (n))) /\ forall ff_i_repeatsum_exists_trace. (exists ff_lt_repeatsum_exists_trace_bound. ff_lt_repeatsum_exists_trace_bound + S ff_i_repeatsum_exists_trace = l) -> exists ff_a_repeatsum_exists_trace ff_r_repeatsum_exists_trace ff_s_repeatsum_exists_trace. ((((exists ff_h_repeatsum_exists_trace_summand. ff_h_repeatsum_exists_trace_summand + S (ff_a_repeatsum_exists_trace) = S ((S (ff_i_repeatsum_exists_trace)) * x1)) /\ exists ff_q_repeatsum_exists_trace_summand. x = ff_q_repeatsum_exists_trace_summand * S ((S (ff_i_repeatsum_exists_trace)) * x1) + (ff_a_repeatsum_exists_trace))) /\ ((((exists ff_h_repeatsum_exists_trace_partial. ff_h_repeatsum_exists_trace_partial + S (ff_r_repeatsum_exists_trace) = S ((S (ff_i_repeatsum_exists_trace)) * ff_v_repeatsum_exists_trace)) /\ exists ff_q_repeatsum_exists_trace_partial. ff_u_repeatsum_exists_trace = ff_q_repeatsum_exists_trace_partial * S ((S (ff_i_repeatsum_exists_trace)) * ff_v_repeatsum_exists_trace) + (ff_r_repeatsum_exists_trace))) /\ ((((exists ff_h_repeatsum_exists_trace_successor. ff_h_repeatsum_exists_trace_successor + S (ff_s_repeatsum_exists_trace) = S ((S (S ff_i_repeatsum_exists_trace)) * ff_v_repeatsum_exists_trace)) /\ exists ff_q_repeatsum_exists_trace_successor. ff_u_repeatsum_exists_trace = ff_q_repeatsum_exists_trace_successor * S ((S (S ff_i_repeatsum_exists_trace)) * ff_v_repeatsum_exists_trace) + (ff_s_repeatsum_exists_trace))) /\ ff_s_repeatsum_exists_trace = ff_r_repeatsum_exists_trace + ff_a_repeatsum_exists_trace))))))
  10. 0010specialize beta_sum_exists x
  11. 0011specialize beta_sum_exists x1
  12. 0012specialize beta_sum_exists l
  13. 0013exact beta_sum_exists
  14. 0014cases hsum
  15. 0015have hexact : x2 = l * a
  16. 0016specialize beta_repeat_sum_exact x
  17. 0017specialize beta_repeat_sum_exact x1
  18. 0018specialize beta_repeat_sum_exact a
  19. 0019specialize beta_repeat_sum_exact l
  20. 0020specialize beta_repeat_sum_exact x2
  21. 0021apply beta_repeat_sum_exact
  22. 0022exact hrepeat_witness_witness
  23. 0023exact hsum_witness
  24. 0024exists x
  25. 0025exists x1
  26. 0026exists x2
  27. 0027split
  28. 0028exact hrepeat_witness_witness
  29. 0029split
  30. 0030exact hsum_witness
  31. 0031exact hexact