PA006P · theorem

beta_sum_functional

Stable checked-use theorem · independently closed

The relational finite sum has a unique natural 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. ∀ l. ∀ n. ∀ m. Sum(b,c,l,n) → Sum(b,c,l,m) → n = m

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

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall b c l n m. (exists ff_u_l ff_v_l. ((((exists ff_h_l_start. ff_h_l_start + S (0) = S ((S (0)) * ff_v_l)) /\ exists ff_q_l_start. ff_u_l = ff_q_l_start * S ((S (0)) * ff_v_l) + (0))) /\ ((((exists ff_h_l_terminal. ff_h_l_terminal + S (n) = S ((S (l)) * ff_v_l)) /\ exists ff_q_l_terminal. ff_u_l = ff_q_l_terminal * S ((S (l)) * ff_v_l) + (n))) /\ forall ff_i_l. (exists ff_lt_l_bound. ff_lt_l_bound + S ff_i_l = l) -> exists ff_a_l ff_r_l ff_s_l. ((((exists ff_h_l_summand. ff_h_l_summand + S (ff_a_l) = S ((S (ff_i_l)) * c)) /\ exists ff_q_l_summand. b = ff_q_l_summand * S ((S (ff_i_l)) * c) + (ff_a_l))) /\ ((((exists ff_h_l_partial. ff_h_l_partial + S (ff_r_l) = S ((S (ff_i_l)) * ff_v_l)) /\ exists ff_q_l_partial. ff_u_l = ff_q_l_partial * S ((S (ff_i_l)) * ff_v_l) + (ff_r_l))) /\ ((((exists ff_h_l_successor. ff_h_l_successor + S (ff_s_l) = S ((S (S ff_i_l)) * ff_v_l)) /\ exists ff_q_l_successor. ff_u_l = ff_q_l_successor * S ((S (S ff_i_l)) * ff_v_l) + (ff_s_l))) /\ ff_s_l = ff_r_l + ff_a_l)))))) -> (exists ff_u_r ff_v_r. ((((exists ff_h_r_start. ff_h_r_start + S (0) = S ((S (0)) * ff_v_r)) /\ exists ff_q_r_start. ff_u_r = ff_q_r_start * S ((S (0)) * ff_v_r) + (0))) /\ ((((exists ff_h_r_terminal. ff_h_r_terminal + S (m) = S ((S (l)) * ff_v_r)) /\ exists ff_q_r_terminal. ff_u_r = ff_q_r_terminal * S ((S (l)) * ff_v_r) + (m))) /\ forall ff_i_r. (exists ff_lt_r_bound. ff_lt_r_bound + S ff_i_r = l) -> exists ff_a_r ff_r_r ff_s_r. ((((exists ff_h_r_summand. ff_h_r_summand + S (ff_a_r) = S ((S (ff_i_r)) * c)) /\ exists ff_q_r_summand. b = ff_q_r_summand * S ((S (ff_i_r)) * c) + (ff_a_r))) /\ ((((exists ff_h_r_partial. ff_h_r_partial + S (ff_r_r) = S ((S (ff_i_r)) * ff_v_r)) /\ exists ff_q_r_partial. ff_u_r = ff_q_r_partial * S ((S (ff_i_r)) * ff_v_r) + (ff_r_r))) /\ ((((exists ff_h_r_successor. ff_h_r_successor + S (ff_s_r) = S ((S (S ff_i_r)) * ff_v_r)) /\ exists ff_q_r_successor. ff_u_r = ff_q_r_successor * S ((S (S ff_i_r)) * ff_v_r) + (ff_s_r))) /\ ff_s_r = ff_r_r + ff_a_r)))))) -> n = m

Proof neighborhood

Direct theorem prerequisites

PA006K beta_sum_trace_functional

Direct theorem dependents

PA006Q bit_count_functional PA00E5 distinct_odd_prime_quotient_sum_equals_rectangle_total PA00F6 eisenstein_transposed_column_counts_extensional PA00FB eisenstein_successor_terminal_sum_matches_last_column

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

23 script commands · 4 reading checkpoints · 0 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 (1)
beta sum trace functional
01Fix variables and assumptionsL1–7

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro n
  5. L5
    intro m
  6. L6
    intro hn
  7. L7
    intro hm
02Separate the logical casesL8–11

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

  1. L8
    cases hn
  2. L9
    cases hn_witness
  3. L10
    cases hm
  4. L11
    cases hm_witness
03Use earlier factsL12–21

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

  1. L12
    specialize beta_sum_trace_functional b
  2. L13
    specialize beta_sum_trace_functional c
  3. L14
    specialize beta_sum_trace_functional l
  4. L15
    specialize beta_sum_trace_functional n
  5. L16
    specialize beta_sum_trace_functional x
  6. L17
    specialize beta_sum_trace_functional x1
  7. L18
    specialize beta_sum_trace_functional m
  8. L19
    specialize beta_sum_trace_functional x2
  9. L20
    specialize beta_sum_trace_functional x3
  10. L21
    apply beta_sum_trace_functional
04Use earlier factsL22–23

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

  1. L22
    exact hn_witness_witness
  2. L23
    exact hm_witness_witness

Library-wide reading audit

Original defined command ledger · 23 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro m
  6. 0006intro hn
  7. 0007intro hm
  8. 0008cases hn
  9. 0009cases hn_witness
  10. 0010cases hm
  11. 0011cases hm_witness
  12. 0012specialize beta_sum_trace_functional b
  13. 0013specialize beta_sum_trace_functional c
  14. 0014specialize beta_sum_trace_functional l
  15. 0015specialize beta_sum_trace_functional n
  16. 0016specialize beta_sum_trace_functional x
  17. 0017specialize beta_sum_trace_functional x1
  18. 0018specialize beta_sum_trace_functional m
  19. 0019specialize beta_sum_trace_functional x2
  20. 0020specialize beta_sum_trace_functional x3
  21. 0021apply beta_sum_trace_functional
  22. 0022exact hn_witness_witness
  23. 0023exact hm_witness_witness