PA00CT · theorem

beta_sum_transport_prefix

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

Pointwise-equal decoded prefixes preserve an exact relational 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

∀ b. ∀ c. ∀ z. ∀ e. ∀ l. ∀ n. Sum(b,c,l,n) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(z,e,x,y)) → Sum(z,e,l,n)

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

PD0002 Lt PD0013 BetaAt PD0015 Sum

5 occurrences

In local proof propositions

PD0013 BetaAt

3 occurrences

Exact expanded native-PA statement
forall b c z e l n. (exists ff_u_transport_source ff_v_transport_source. ((((exists ff_h_transport_source_start. ff_h_transport_source_start + S (0) = S ((S (0)) * ff_v_transport_source)) /\ exists ff_q_transport_source_start. ff_u_transport_source = ff_q_transport_source_start * S ((S (0)) * ff_v_transport_source) + (0))) /\ ((((exists ff_h_transport_source_terminal. ff_h_transport_source_terminal + S (n) = S ((S (l)) * ff_v_transport_source)) /\ exists ff_q_transport_source_terminal. ff_u_transport_source = ff_q_transport_source_terminal * S ((S (l)) * ff_v_transport_source) + (n))) /\ forall ff_i_transport_source. (exists ff_lt_transport_source_bound. ff_lt_transport_source_bound + S ff_i_transport_source = l) -> exists ff_a_transport_source ff_r_transport_source ff_s_transport_source. ((((exists ff_h_transport_source_summand. ff_h_transport_source_summand + S (ff_a_transport_source) = S ((S (ff_i_transport_source)) * c)) /\ exists ff_q_transport_source_summand. b = ff_q_transport_source_summand * S ((S (ff_i_transport_source)) * c) + (ff_a_transport_source))) /\ ((((exists ff_h_transport_source_partial. ff_h_transport_source_partial + S (ff_r_transport_source) = S ((S (ff_i_transport_source)) * ff_v_transport_source)) /\ exists ff_q_transport_source_partial. ff_u_transport_source = ff_q_transport_source_partial * S ((S (ff_i_transport_source)) * ff_v_transport_source) + (ff_r_transport_source))) /\ ((((exists ff_h_transport_source_successor. ff_h_transport_source_successor + S (ff_s_transport_source) = S ((S (S ff_i_transport_source)) * ff_v_transport_source)) /\ exists ff_q_transport_source_successor. ff_u_transport_source = ff_q_transport_source_successor * S ((S (S ff_i_transport_source)) * ff_v_transport_source) + (ff_s_transport_source))) /\ ff_s_transport_source = ff_r_transport_source + ff_a_transport_source)))))) -> (forall i a. (exists h. h + S i = l) -> (((exists ff_h_transport_source_entry. ff_h_transport_source_entry + S (a) = S ((S (i)) * c)) /\ exists ff_q_transport_source_entry. b = ff_q_transport_source_entry * S ((S (i)) * c) + (a))) -> (((exists ff_h_transport_target_entry. ff_h_transport_target_entry + S (a) = S ((S (i)) * e)) /\ exists ff_q_transport_target_entry. z = ff_q_transport_target_entry * S ((S (i)) * e) + (a)))) -> (exists ff_u_transport_target ff_v_transport_target. ((((exists ff_h_transport_target_start. ff_h_transport_target_start + S (0) = S ((S (0)) * ff_v_transport_target)) /\ exists ff_q_transport_target_start. ff_u_transport_target = ff_q_transport_target_start * S ((S (0)) * ff_v_transport_target) + (0))) /\ ((((exists ff_h_transport_target_terminal. ff_h_transport_target_terminal + S (n) = S ((S (l)) * ff_v_transport_target)) /\ exists ff_q_transport_target_terminal. ff_u_transport_target = ff_q_transport_target_terminal * S ((S (l)) * ff_v_transport_target) + (n))) /\ forall ff_i_transport_target. (exists ff_lt_transport_target_bound. ff_lt_transport_target_bound + S ff_i_transport_target = l) -> exists ff_a_transport_target ff_r_transport_target ff_s_transport_target. ((((exists ff_h_transport_target_summand. ff_h_transport_target_summand + S (ff_a_transport_target) = S ((S (ff_i_transport_target)) * e)) /\ exists ff_q_transport_target_summand. z = ff_q_transport_target_summand * S ((S (ff_i_transport_target)) * e) + (ff_a_transport_target))) /\ ((((exists ff_h_transport_target_partial. ff_h_transport_target_partial + S (ff_r_transport_target) = S ((S (ff_i_transport_target)) * ff_v_transport_target)) /\ exists ff_q_transport_target_partial. ff_u_transport_target = ff_q_transport_target_partial * S ((S (ff_i_transport_target)) * ff_v_transport_target) + (ff_r_transport_target))) /\ ((((exists ff_h_transport_target_successor. ff_h_transport_target_successor + S (ff_s_transport_target) = S ((S (S ff_i_transport_target)) * ff_v_transport_target)) /\ exists ff_q_transport_target_successor. ff_u_transport_target = ff_q_transport_target_successor * S ((S (S ff_i_transport_target)) * ff_v_transport_target) + (ff_s_transport_target))) /\ ff_s_transport_target = ff_r_transport_target + ff_a_transport_target))))))

Proof neighborhood

Direct theorem prerequisites

none

Direct theorem dependents

PA00CU beta_sum_replace_balance PA00E4 distinct_odd_prime_quotient_sum_transports_to_rectangle PA00ES eisenstein_zero_width_rectangle_sum_zero 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

44 script commands · 17 reading checkpoints · 1 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.

01Fix variables and assumptionsL1–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro z
  4. L4
    intro e
  5. L5
    intro l
  6. L6
    intro n
  7. L7
    intro hsum
  8. L8
    intro hpres
02Separate the logical casesL9–12

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

  1. L9
    cases hsum
  2. L10
    cases hsum_witness
  3. L11
    cases hsum_witness_witness
  4. L12
    cases hsum_witness_witness_right
03Construct an explicit witnessL13–14

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

  1. L13
    exists x
  2. L14
    exists x1
04Separate the logical casesL15–15

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

  1. L15
    split
05Use earlier factsL16–16

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

  1. L16
    exact hsum_witness_witness_left
06Separate the logical casesL17–17

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

  1. L17
    split
07Use earlier factsL18–18

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

  1. L18
    exact hsum_witness_witness_right_left
08Fix variables and assumptionsL19–20

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

  1. L19
    intro i
  2. L20
    intro hi
09Establish hstepL21–24

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

  1. L21
    have hstep : ∃ a. ∃ r. ∃ s. BetaAt(b,c,i,a) ∧ (BetaAt(x,x1,i,r) ∧ (BetaAt(x,x1,S i,s) ∧ s = r + a))Definitions: BetaAt(b,c,i,a)BetaAt(x,x1,i,r)BetaAt(x,x1,S i,s)Original native command in the exact edition
  2. L22
    specialize hsum_witness_witness_right_right i
  3. L23
    apply hsum_witness_witness_right_right
  4. L24
    exact hi
10Separate the logical casesL25–30

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

  1. L25
    cases hstep
  2. L26
    cases hstep_witness
  3. L27
    cases hstep_witness_witness
  4. L28
    cases hstep_witness_witness_witness
  5. L29
    cases hstep_witness_witness_witness_right
  6. L30
    cases hstep_witness_witness_witness_right_right
11Construct an explicit witnessL31–33

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

  1. L31
    exists x2
  2. L32
    exists x3
  3. L33
    exists x4
12Separate the logical casesL34–34

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

  1. L34
    split
13Use earlier factsL35–39

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

  1. L35
    specialize hpres i
  2. L36
    specialize hpres x2
  3. L37
    apply hpres
  4. L38
    exact hi
  5. L39
    exact hstep_witness_witness_witness_left
14Separate the logical casesL40–40

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

  1. L40
    split
15Use earlier factsL41–41

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

  1. L41
    exact hstep_witness_witness_witness_right_left
16Separate the logical casesL42–42

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

  1. L42
    split
17Use earlier factsL43–44

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

  1. L43
    exact hstep_witness_witness_witness_right_right_left
  2. L44
    exact hstep_witness_witness_witness_right_right_right

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro e
  5. 0005intro l
  6. 0006intro n
  7. 0007intro hsum
  8. 0008intro hpres
  9. 0009cases hsum
  10. 0010cases hsum_witness
  11. 0011cases hsum_witness_witness
  12. 0012cases hsum_witness_witness_right
  13. 0013exists x
  14. 0014exists x1
  15. 0015split
  16. 0016exact hsum_witness_witness_left
  17. 0017split
  18. 0018exact hsum_witness_witness_right_left
  19. 0019intro i
  20. 0020intro hi
  21. 0021have hstep : ∃ a. ∃ r. ∃ s. BetaAt(b,c,i,a) ∧ (BetaAt(x,x1,i,r) ∧ (BetaAt(x,x1,S i,s) ∧ s = r + a))
    Exact native replay linehave hstep : exists a r s. ((((exists ff_h_transport_step_source. ff_h_transport_step_source + S (a) = S ((S (i)) * c)) /\ exists ff_q_transport_step_source. b = ff_q_transport_step_source * S ((S (i)) * c) + (a))) /\ ((((exists ff_h_transport_step_partial. ff_h_transport_step_partial + S (r) = S ((S (i)) * x1)) /\ exists ff_q_transport_step_partial. x = ff_q_transport_step_partial * S ((S (i)) * x1) + (r))) /\ ((((exists ff_h_transport_step_successor. ff_h_transport_step_successor + S (s) = S ((S (S i)) * x1)) /\ exists ff_q_transport_step_successor. x = ff_q_transport_step_successor * S ((S (S i)) * x1) + (s))) /\ s = r + a)))
  22. 0022specialize hsum_witness_witness_right_right i
  23. 0023apply hsum_witness_witness_right_right
  24. 0024exact hi
  25. 0025cases hstep
  26. 0026cases hstep_witness
  27. 0027cases hstep_witness_witness
  28. 0028cases hstep_witness_witness_witness
  29. 0029cases hstep_witness_witness_witness_right
  30. 0030cases hstep_witness_witness_witness_right_right
  31. 0031exists x2
  32. 0032exists x3
  33. 0033exists x4
  34. 0034split
  35. 0035specialize hpres i
  36. 0036specialize hpres x2
  37. 0037apply hpres
  38. 0038exact hi
  39. 0039exact hstep_witness_witness_witness_left
  40. 0040split
  41. 0041exact hstep_witness_witness_witness_right_left
  42. 0042split
  43. 0043exact hstep_witness_witness_witness_right_right_left
  44. 0044exact hstep_witness_witness_witness_right_right_right