PA00EL

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.

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

Structural proof guide

Generated structural guide

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

Use the direct prerequisites beta_repeat_exists, beta_sum_exists, beta_repeat_sum_exact as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (3).

Referenced ingredients

PA0045 beta_repeat_exists PA003H beta_sum_exists PA00EK beta_repeat_sum_exact

Proof neighborhood

Direct dependencies

PA0045 beta_repeat_exists PA003H beta_sum_exists PA00EK beta_repeat_sum_exact

Direct dependents

PA00EQ eisenstein_rectangle_plus_column_count_total

Formal native tactic body

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

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.

Named ingredients (3)
beta repeat existsbeta sum existsbeta repeat sum exact

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–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 : 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))))
  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
  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 exact command ledger · 31 lines
  1. 0001intro a
  2. 0002intro l
  3. 0003have 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 : 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