PG0010

beta_sum_pointwise_mod_scale

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Pointwise scalar congruences lift through two actual natural Sum traces at every modulus, including zero and the empty length; no new sum witness is assumed equal to a desired total.

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 expanded first-order arithmetic statement

forall p k ab ac bb bc L u v. (exists fs_u_pfc_scalar_sum_source fs_v_pfc_scalar_sum_source. ((((exists fs_h_pfc_scalar_sum_source_body_start. fs_h_pfc_scalar_sum_source_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_sum_source)) /\ exists fs_q_pfc_scalar_sum_source_body_start. fs_u_pfc_scalar_sum_source = fs_q_pfc_scalar_sum_source_body_start * S ((S (0)) * fs_v_pfc_scalar_sum_source) + (0))) /\ ((((exists fs_h_pfc_scalar_sum_source_body_terminal. fs_h_pfc_scalar_sum_source_body_terminal + S (u) = S ((S (L)) * fs_v_pfc_scalar_sum_source)) /\ exists fs_q_pfc_scalar_sum_source_body_terminal. fs_u_pfc_scalar_sum_source = fs_q_pfc_scalar_sum_source_body_terminal * S ((S (L)) * fs_v_pfc_scalar_sum_source) + (u))) /\ forall fs_i_pfc_scalar_sum_source_body_steps. (exists fs_lt_pfc_scalar_sum_source_body_steps_bound. fs_lt_pfc_scalar_sum_source_body_steps_bound + S fs_i_pfc_scalar_sum_source_body_steps = L) -> exists fs_a_pfc_scalar_sum_source_body_steps fs_r_pfc_scalar_sum_source_body_steps fs_s_pfc_scalar_sum_source_body_steps. ((((exists fs_h_pfc_scalar_sum_source_body_steps_summand. fs_h_pfc_scalar_sum_source_body_steps_summand + S (fs_a_pfc_scalar_sum_source_body_steps) = S ((S (fs_i_pfc_scalar_sum_source_body_steps)) * ac)) /\ exists fs_q_pfc_scalar_sum_source_body_steps_summand. ab = fs_q_pfc_scalar_sum_source_body_steps_summand * S ((S (fs_i_pfc_scalar_sum_source_body_steps)) * ac) + (fs_a_pfc_scalar_sum_source_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_source_body_steps_partial. fs_h_pfc_scalar_sum_source_body_steps_partial + S (fs_r_pfc_scalar_sum_source_body_steps) = S ((S (fs_i_pfc_scalar_sum_source_body_steps)) * fs_v_pfc_scalar_sum_source)) /\ exists fs_q_pfc_scalar_sum_source_body_steps_partial. fs_u_pfc_scalar_sum_source = fs_q_pfc_scalar_sum_source_body_steps_partial * S ((S (fs_i_pfc_scalar_sum_source_body_steps)) * fs_v_pfc_scalar_sum_source) + (fs_r_pfc_scalar_sum_source_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_source_body_steps_successor. fs_h_pfc_scalar_sum_source_body_steps_successor + S (fs_s_pfc_scalar_sum_source_body_steps) = S ((S (S fs_i_pfc_scalar_sum_source_body_steps)) * fs_v_pfc_scalar_sum_source)) /\ exists fs_q_pfc_scalar_sum_source_body_steps_successor. fs_u_pfc_scalar_sum_source = fs_q_pfc_scalar_sum_source_body_steps_successor * S ((S (S fs_i_pfc_scalar_sum_source_body_steps)) * fs_v_pfc_scalar_sum_source) + (fs_s_pfc_scalar_sum_source_body_steps))) /\ fs_s_pfc_scalar_sum_source_body_steps = fs_r_pfc_scalar_sum_source_body_steps + fs_a_pfc_scalar_sum_source_body_steps)))))) -> (exists fs_u_pfc_scalar_sum_target fs_v_pfc_scalar_sum_target. ((((exists fs_h_pfc_scalar_sum_target_body_start. fs_h_pfc_scalar_sum_target_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_sum_target)) /\ exists fs_q_pfc_scalar_sum_target_body_start. fs_u_pfc_scalar_sum_target = fs_q_pfc_scalar_sum_target_body_start * S ((S (0)) * fs_v_pfc_scalar_sum_target) + (0))) /\ ((((exists fs_h_pfc_scalar_sum_target_body_terminal. fs_h_pfc_scalar_sum_target_body_terminal + S (v) = S ((S (L)) * fs_v_pfc_scalar_sum_target)) /\ exists fs_q_pfc_scalar_sum_target_body_terminal. fs_u_pfc_scalar_sum_target = fs_q_pfc_scalar_sum_target_body_terminal * S ((S (L)) * fs_v_pfc_scalar_sum_target) + (v))) /\ forall fs_i_pfc_scalar_sum_target_body_steps. (exists fs_lt_pfc_scalar_sum_target_body_steps_bound. fs_lt_pfc_scalar_sum_target_body_steps_bound + S fs_i_pfc_scalar_sum_target_body_steps = L) -> exists fs_a_pfc_scalar_sum_target_body_steps fs_r_pfc_scalar_sum_target_body_steps fs_s_pfc_scalar_sum_target_body_steps. ((((exists fs_h_pfc_scalar_sum_target_body_steps_summand. fs_h_pfc_scalar_sum_target_body_steps_summand + S (fs_a_pfc_scalar_sum_target_body_steps) = S ((S (fs_i_pfc_scalar_sum_target_body_steps)) * bc)) /\ exists fs_q_pfc_scalar_sum_target_body_steps_summand. bb = fs_q_pfc_scalar_sum_target_body_steps_summand * S ((S (fs_i_pfc_scalar_sum_target_body_steps)) * bc) + (fs_a_pfc_scalar_sum_target_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_target_body_steps_partial. fs_h_pfc_scalar_sum_target_body_steps_partial + S (fs_r_pfc_scalar_sum_target_body_steps) = S ((S (fs_i_pfc_scalar_sum_target_body_steps)) * fs_v_pfc_scalar_sum_target)) /\ exists fs_q_pfc_scalar_sum_target_body_steps_partial. fs_u_pfc_scalar_sum_target = fs_q_pfc_scalar_sum_target_body_steps_partial * S ((S (fs_i_pfc_scalar_sum_target_body_steps)) * fs_v_pfc_scalar_sum_target) + (fs_r_pfc_scalar_sum_target_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_target_body_steps_successor. fs_h_pfc_scalar_sum_target_body_steps_successor + S (fs_s_pfc_scalar_sum_target_body_steps) = S ((S (S fs_i_pfc_scalar_sum_target_body_steps)) * fs_v_pfc_scalar_sum_target)) /\ exists fs_q_pfc_scalar_sum_target_body_steps_successor. fs_u_pfc_scalar_sum_target = fs_q_pfc_scalar_sum_target_body_steps_successor * S ((S (S fs_i_pfc_scalar_sum_target_body_steps)) * fs_v_pfc_scalar_sum_target) + (fs_s_pfc_scalar_sum_target_body_steps))) /\ fs_s_pfc_scalar_sum_target_body_steps = fs_r_pfc_scalar_sum_target_body_steps + fs_a_pfc_scalar_sum_target_body_steps)))))) -> (forall pfscalar_index_scalar_sum_points pfscalar_source_scalar_sum_points pfscalar_target_scalar_sum_points. (exists pfa_gap_scalar_sum_pointsindex. pfa_gap_scalar_sum_pointsindex + S (pfscalar_index_scalar_sum_points) = (L)) -> (((exists ff_h_pfp_scalar_sum_pointssource. ff_h_pfp_scalar_sum_pointssource + S (pfscalar_source_scalar_sum_points) = S ((S (pfscalar_index_scalar_sum_points)) * ac)) /\ exists ff_q_pfp_scalar_sum_pointssource. ab = ff_q_pfp_scalar_sum_pointssource * S ((S (pfscalar_index_scalar_sum_points)) * ac) + (pfscalar_source_scalar_sum_points))) -> (((exists ff_h_pfp_scalar_sum_pointstarget. ff_h_pfp_scalar_sum_pointstarget + S (pfscalar_target_scalar_sum_points) = S ((S (pfscalar_index_scalar_sum_points)) * bc)) /\ exists ff_q_pfp_scalar_sum_pointstarget. bb = ff_q_pfp_scalar_sum_pointstarget * S ((S (pfscalar_index_scalar_sum_points)) * bc) + (pfscalar_target_scalar_sum_points))) -> (exists pfa_offset_left_scalar_sum_pointscongruence pfa_offset_right_scalar_sum_pointscongruence. ((k)*pfscalar_source_scalar_sum_points) + (p) * pfa_offset_left_scalar_sum_pointscongruence = (pfscalar_target_scalar_sum_points) + (p) * pfa_offset_right_scalar_sum_pointscongruence)) -> (exists pfa_offset_left_scalar_sum_result pfa_offset_right_scalar_sum_result. (k*u) + (p) * pfa_offset_left_scalar_sum_result = (v) + (p) * pfa_offset_right_scalar_sum_result)

Constructive proof overview

Generated structural guide

Pointwise scalar congruences lift through two actual natural Sum traces at every modulus, including zero and the empty length; no new sum witness is assumed equal to a desired total.

The unchanged tactic script uses 6 declared prerequisites and contains 102 exact native proof lines.

Alpha v34 checked-use · first admitted v34 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

beta_sum_zero Alpha theorem; checked-use authorized beta_sum_succ_decompose Alpha theorem; checked-use authorized le_succ Alpha theorem; checked-use authorized le_refl Alpha theorem; checked-use authorized mod_eq_add Alpha theorem; checked-use authorized mul_add Alpha theorem; checked-use authorized

Direct dependents

PG0013 polynomial_diagonal_sum_right_scale_congruent

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

102 script commands · 18 reading checkpoints · 8 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.

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–6

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

  1. L1
    intro p
  2. L2
    intro k
  3. L3
    intro ab
  4. L4
    intro ac
  5. L5
    intro bb
  6. L6
    intro bc
02Induction on LL7–12

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L7
    induction L
  2. L8
    intro u
  3. L9
    intro v
  4. L10
    intro hu
  5. L11
    intro hv
  6. L12
    intro hw
03Establish hu0L13–18

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

  1. L13
    have hu0 : u=0
  2. L14
    specialize beta_sum_zero (ab)
  3. L15
    specialize beta_sum_zero (ac)
  4. L16
    specialize beta_sum_zero (u)
  5. L17
    apply beta_sum_zero
  6. L18
    exact hu
04Establish hv0L19–26

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

  1. L19
    have hv0 : v=0
  2. L20
    specialize beta_sum_zero (bb)
  3. L21
    specialize beta_sum_zero (bc)
  4. L22
    specialize beta_sum_zero (v)
  5. L23
    apply beta_sum_zero
  6. L24
    exact hv
  7. L25
    rewrite hu0
  8. L26
    rewrite hv0
05Construct an explicit witnessL27–28

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

  1. L27
    exists 0
  2. L28
    exists 0
06Calculate and transport equalitiesL29–29

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L29
    simp
07Fix variables and assumptionsL30–34

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

  1. L30
    intro u
  2. L31
    intro v
  3. L32
    intro hu
  4. L33
    intro hv
  5. L34
    intro hw
08Establish hfirstL35–41

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

  1. L35
    have hfirst : ∃ a. ∃ n. BetaAt(ab,ac,L,a) ∧ (Sum(ab,ac,L,n) ∧ u = n + a)Definitions: BetaAtSum
  2. L36
    specialize beta_sum_succ_decompose (ab)
  3. L37
    specialize beta_sum_succ_decompose (ac)
  4. L38
    specialize beta_sum_succ_decompose (L)
  5. L39
    specialize beta_sum_succ_decompose (u)
  6. L40
    apply beta_sum_succ_decompose
  7. L41
    exact hu
09Separate the logical casesL42–45

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

  1. L42
    cases hfirst
  2. L43
    cases hfirst_witness
  3. L44
    cases hfirst_witness_witness
  4. L45
    cases hfirst_witness_witness_right
10Establish hsecondL46–52

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

  1. L46
    have hsecond : ∃ a. ∃ n. BetaAt(bb,bc,L,a) ∧ (Sum(bb,bc,L,n) ∧ v = n + a)Definitions: BetaAtSum
  2. L47
    specialize beta_sum_succ_decompose (bb)
  3. L48
    specialize beta_sum_succ_decompose (bc)
  4. L49
    specialize beta_sum_succ_decompose (L)
  5. L50
    specialize beta_sum_succ_decompose (v)
  6. L51
    apply beta_sum_succ_decompose
  7. L52
    exact hv
11Separate the logical casesL53–56

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

  1. L53
    cases hsecond
  2. L54
    cases hsecond_witness
  3. L55
    cases hsecond_witness_witness
  4. L56
    cases hsecond_witness_witness_right
12Establish hprefixL57–66

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

  1. L57
    have hprefix : exists pfa_offset_left_scalar_sum_prefix_congruence pfa_offset_right_scalar_sum_prefix_congruence. (k*x1) + (p) * pfa_offset_left_scalar_sum_prefix_congruence = (x3) + (p) * pfa_offset_right_scalar_sum_prefix_congruence
  2. L58
    specialize IH (x1)
  3. L59
    specialize IH (x3)
  4. L60
    apply IH
  5. L61
    exact hfirst_witness_witness_right_left
  6. L62
    exact hsecond_witness_witness_right_left
  7. L63
    intro i
  8. L64
    intro a
  9. L65
    intro b
  10. L66
    intro hi
13Fix variables and assumptionsL67–68

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

  1. L67
    intro ha
  2. L68
    intro hb
14Use earlier factsL69–78

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

  1. L69
    specialize hw (i)
  2. L70
    specialize hw (a)
  3. L71
    specialize hw (b)
  4. L72
    apply hw
  5. L73
    specialize le_succ (S i)
  6. L74
    specialize le_succ (L)
  7. L75
    apply le_succ
  8. L76
    exact hi
  9. L77
    exact ha
  10. L78
    exact hb
15Establish hlastL79–87

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

  1. L79
    have hlast : exists pfa_offset_left_scalar_sum_last_congruence pfa_offset_right_scalar_sum_last_congruence. (k*x) + (p) * pfa_offset_left_scalar_sum_last_congruence = (x2) + (p) * pfa_offset_right_scalar_sum_last_congruence
  2. L80
    specialize hw (L)
  3. L81
    specialize hw (x)
  4. L82
    specialize hw (x2)
  5. L83
    apply hw
  6. L84
    specialize le_refl (S L)
  7. L85
    apply le_refl
  8. L86
    exact hfirst_witness_witness_left
  9. L87
    exact hsecond_witness_witness_left
16Establish hcombinedL88–97

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq add.

  1. L88
    have hcombined : exists pfa_offset_left_scalar_sum_combined pfa_offset_right_scalar_sum_combined. (k*x1+k*x) + (p) * pfa_offset_left_scalar_sum_combined = (x3+x2) + (p) * pfa_offset_right_scalar_sum_combined
  2. L89
    specialize mod_eq_add (p)
  3. L90
    specialize mod_eq_add (k*x1)
  4. L91
    specialize mod_eq_add (x3)
  5. L92
    specialize mod_eq_add (k*x)
  6. L93
    specialize mod_eq_add (x2)
  7. L94
    apply mod_eq_add
  8. L95
    exact hprefix
  9. L96
    exact hlast
  10. L97
    rewrite hfirst_witness_witness_right_right
17Calculate and transport equalitiesL98–98

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L98
    rewrite hsecond_witness_witness_right_right
18Establish hdistributeL99–102

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul add.

  1. L99
    have hdistribute : k*(x1+x)=k*x1+k*x
  2. L100
    apply mul_add
  3. L101
    rewrite hdistribute
  4. L102
    exact hcombined

Library-wide reading audit

Original exact command ledger · 102 lines
  1. 0001intro p
  2. 0002intro k
  3. 0003intro ab
  4. 0004intro ac
  5. 0005intro bb
  6. 0006intro bc
  7. 0007induction L
  8. 0008intro u
  9. 0009intro v
  10. 0010intro hu
  11. 0011intro hv
  12. 0012intro hw
  13. 0013have hu0 : u=0
  14. 0014specialize beta_sum_zero (ab)
  15. 0015specialize beta_sum_zero (ac)
  16. 0016specialize beta_sum_zero (u)
  17. 0017apply beta_sum_zero
  18. 0018exact hu
  19. 0019have hv0 : v=0
  20. 0020specialize beta_sum_zero (bb)
  21. 0021specialize beta_sum_zero (bc)
  22. 0022specialize beta_sum_zero (v)
  23. 0023apply beta_sum_zero
  24. 0024exact hv
  25. 0025rewrite hu0
  26. 0026rewrite hv0
  27. 0027exists 0
  28. 0028exists 0
  29. 0029simp
  30. 0030intro u
  31. 0031intro v
  32. 0032intro hu
  33. 0033intro hv
  34. 0034intro hw
  35. 0035have hfirst : exists a n. ((((exists ff_h_pfp_scalar_sum_old_last. ff_h_pfp_scalar_sum_old_last + S (a) = S ((S (L)) * ac)) /\ exists ff_q_pfp_scalar_sum_old_last. ab = ff_q_pfp_scalar_sum_old_last * S ((S (L)) * ac) + (a))) /\ (((exists fs_u_pfc_scalar_sum_old_prefix fs_v_pfc_scalar_sum_old_prefix. ((((exists fs_h_pfc_scalar_sum_old_prefix_body_start. fs_h_pfc_scalar_sum_old_prefix_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_sum_old_prefix)) /\ exists fs_q_pfc_scalar_sum_old_prefix_body_start. fs_u_pfc_scalar_sum_old_prefix = fs_q_pfc_scalar_sum_old_prefix_body_start * S ((S (0)) * fs_v_pfc_scalar_sum_old_prefix) + (0))) /\ ((((exists fs_h_pfc_scalar_sum_old_prefix_body_terminal. fs_h_pfc_scalar_sum_old_prefix_body_terminal + S (n) = S ((S (L)) * fs_v_pfc_scalar_sum_old_prefix)) /\ exists fs_q_pfc_scalar_sum_old_prefix_body_terminal. fs_u_pfc_scalar_sum_old_prefix = fs_q_pfc_scalar_sum_old_prefix_body_terminal * S ((S (L)) * fs_v_pfc_scalar_sum_old_prefix) + (n))) /\ forall fs_i_pfc_scalar_sum_old_prefix_body_steps. (exists fs_lt_pfc_scalar_sum_old_prefix_body_steps_bound. fs_lt_pfc_scalar_sum_old_prefix_body_steps_bound + S fs_i_pfc_scalar_sum_old_prefix_body_steps = L) -> exists fs_a_pfc_scalar_sum_old_prefix_body_steps fs_r_pfc_scalar_sum_old_prefix_body_steps fs_s_pfc_scalar_sum_old_prefix_body_steps. ((((exists fs_h_pfc_scalar_sum_old_prefix_body_steps_summand. fs_h_pfc_scalar_sum_old_prefix_body_steps_summand + S (fs_a_pfc_scalar_sum_old_prefix_body_steps) = S ((S (fs_i_pfc_scalar_sum_old_prefix_body_steps)) * ac)) /\ exists fs_q_pfc_scalar_sum_old_prefix_body_steps_summand. ab = fs_q_pfc_scalar_sum_old_prefix_body_steps_summand * S ((S (fs_i_pfc_scalar_sum_old_prefix_body_steps)) * ac) + (fs_a_pfc_scalar_sum_old_prefix_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_old_prefix_body_steps_partial. fs_h_pfc_scalar_sum_old_prefix_body_steps_partial + S (fs_r_pfc_scalar_sum_old_prefix_body_steps) = S ((S (fs_i_pfc_scalar_sum_old_prefix_body_steps)) * fs_v_pfc_scalar_sum_old_prefix)) /\ exists fs_q_pfc_scalar_sum_old_prefix_body_steps_partial. fs_u_pfc_scalar_sum_old_prefix = fs_q_pfc_scalar_sum_old_prefix_body_steps_partial * S ((S (fs_i_pfc_scalar_sum_old_prefix_body_steps)) * fs_v_pfc_scalar_sum_old_prefix) + (fs_r_pfc_scalar_sum_old_prefix_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_old_prefix_body_steps_successor. fs_h_pfc_scalar_sum_old_prefix_body_steps_successor + S (fs_s_pfc_scalar_sum_old_prefix_body_steps) = S ((S (S fs_i_pfc_scalar_sum_old_prefix_body_steps)) * fs_v_pfc_scalar_sum_old_prefix)) /\ exists fs_q_pfc_scalar_sum_old_prefix_body_steps_successor. fs_u_pfc_scalar_sum_old_prefix = fs_q_pfc_scalar_sum_old_prefix_body_steps_successor * S ((S (S fs_i_pfc_scalar_sum_old_prefix_body_steps)) * fs_v_pfc_scalar_sum_old_prefix) + (fs_s_pfc_scalar_sum_old_prefix_body_steps))) /\ fs_s_pfc_scalar_sum_old_prefix_body_steps = fs_r_pfc_scalar_sum_old_prefix_body_steps + fs_a_pfc_scalar_sum_old_prefix_body_steps)))))) /\ ((u=n+a)))))
  36. 0036specialize beta_sum_succ_decompose (ab)
  37. 0037specialize beta_sum_succ_decompose (ac)
  38. 0038specialize beta_sum_succ_decompose (L)
  39. 0039specialize beta_sum_succ_decompose (u)
  40. 0040apply beta_sum_succ_decompose
  41. 0041exact hu
  42. 0042cases hfirst
  43. 0043cases hfirst_witness
  44. 0044cases hfirst_witness_witness
  45. 0045cases hfirst_witness_witness_right
  46. 0046have hsecond : exists a n. ((((exists ff_h_pfp_scalar_sum_new_last. ff_h_pfp_scalar_sum_new_last + S (a) = S ((S (L)) * bc)) /\ exists ff_q_pfp_scalar_sum_new_last. bb = ff_q_pfp_scalar_sum_new_last * S ((S (L)) * bc) + (a))) /\ (((exists fs_u_pfc_scalar_sum_new_prefix fs_v_pfc_scalar_sum_new_prefix. ((((exists fs_h_pfc_scalar_sum_new_prefix_body_start. fs_h_pfc_scalar_sum_new_prefix_body_start + S (0) = S ((S (0)) * fs_v_pfc_scalar_sum_new_prefix)) /\ exists fs_q_pfc_scalar_sum_new_prefix_body_start. fs_u_pfc_scalar_sum_new_prefix = fs_q_pfc_scalar_sum_new_prefix_body_start * S ((S (0)) * fs_v_pfc_scalar_sum_new_prefix) + (0))) /\ ((((exists fs_h_pfc_scalar_sum_new_prefix_body_terminal. fs_h_pfc_scalar_sum_new_prefix_body_terminal + S (n) = S ((S (L)) * fs_v_pfc_scalar_sum_new_prefix)) /\ exists fs_q_pfc_scalar_sum_new_prefix_body_terminal. fs_u_pfc_scalar_sum_new_prefix = fs_q_pfc_scalar_sum_new_prefix_body_terminal * S ((S (L)) * fs_v_pfc_scalar_sum_new_prefix) + (n))) /\ forall fs_i_pfc_scalar_sum_new_prefix_body_steps. (exists fs_lt_pfc_scalar_sum_new_prefix_body_steps_bound. fs_lt_pfc_scalar_sum_new_prefix_body_steps_bound + S fs_i_pfc_scalar_sum_new_prefix_body_steps = L) -> exists fs_a_pfc_scalar_sum_new_prefix_body_steps fs_r_pfc_scalar_sum_new_prefix_body_steps fs_s_pfc_scalar_sum_new_prefix_body_steps. ((((exists fs_h_pfc_scalar_sum_new_prefix_body_steps_summand. fs_h_pfc_scalar_sum_new_prefix_body_steps_summand + S (fs_a_pfc_scalar_sum_new_prefix_body_steps) = S ((S (fs_i_pfc_scalar_sum_new_prefix_body_steps)) * bc)) /\ exists fs_q_pfc_scalar_sum_new_prefix_body_steps_summand. bb = fs_q_pfc_scalar_sum_new_prefix_body_steps_summand * S ((S (fs_i_pfc_scalar_sum_new_prefix_body_steps)) * bc) + (fs_a_pfc_scalar_sum_new_prefix_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_new_prefix_body_steps_partial. fs_h_pfc_scalar_sum_new_prefix_body_steps_partial + S (fs_r_pfc_scalar_sum_new_prefix_body_steps) = S ((S (fs_i_pfc_scalar_sum_new_prefix_body_steps)) * fs_v_pfc_scalar_sum_new_prefix)) /\ exists fs_q_pfc_scalar_sum_new_prefix_body_steps_partial. fs_u_pfc_scalar_sum_new_prefix = fs_q_pfc_scalar_sum_new_prefix_body_steps_partial * S ((S (fs_i_pfc_scalar_sum_new_prefix_body_steps)) * fs_v_pfc_scalar_sum_new_prefix) + (fs_r_pfc_scalar_sum_new_prefix_body_steps))) /\ ((((exists fs_h_pfc_scalar_sum_new_prefix_body_steps_successor. fs_h_pfc_scalar_sum_new_prefix_body_steps_successor + S (fs_s_pfc_scalar_sum_new_prefix_body_steps) = S ((S (S fs_i_pfc_scalar_sum_new_prefix_body_steps)) * fs_v_pfc_scalar_sum_new_prefix)) /\ exists fs_q_pfc_scalar_sum_new_prefix_body_steps_successor. fs_u_pfc_scalar_sum_new_prefix = fs_q_pfc_scalar_sum_new_prefix_body_steps_successor * S ((S (S fs_i_pfc_scalar_sum_new_prefix_body_steps)) * fs_v_pfc_scalar_sum_new_prefix) + (fs_s_pfc_scalar_sum_new_prefix_body_steps))) /\ fs_s_pfc_scalar_sum_new_prefix_body_steps = fs_r_pfc_scalar_sum_new_prefix_body_steps + fs_a_pfc_scalar_sum_new_prefix_body_steps)))))) /\ ((v=n+a)))))
  47. 0047specialize beta_sum_succ_decompose (bb)
  48. 0048specialize beta_sum_succ_decompose (bc)
  49. 0049specialize beta_sum_succ_decompose (L)
  50. 0050specialize beta_sum_succ_decompose (v)
  51. 0051apply beta_sum_succ_decompose
  52. 0052exact hv
  53. 0053cases hsecond
  54. 0054cases hsecond_witness
  55. 0055cases hsecond_witness_witness
  56. 0056cases hsecond_witness_witness_right
  57. 0057have hprefix : exists pfa_offset_left_scalar_sum_prefix_congruence pfa_offset_right_scalar_sum_prefix_congruence. (k*x1) + (p) * pfa_offset_left_scalar_sum_prefix_congruence = (x3) + (p) * pfa_offset_right_scalar_sum_prefix_congruence
  58. 0058specialize IH (x1)
  59. 0059specialize IH (x3)
  60. 0060apply IH
  61. 0061exact hfirst_witness_witness_right_left
  62. 0062exact hsecond_witness_witness_right_left
  63. 0063intro i
  64. 0064intro a
  65. 0065intro b
  66. 0066intro hi
  67. 0067intro ha
  68. 0068intro hb
  69. 0069specialize hw (i)
  70. 0070specialize hw (a)
  71. 0071specialize hw (b)
  72. 0072apply hw
  73. 0073specialize le_succ (S i)
  74. 0074specialize le_succ (L)
  75. 0075apply le_succ
  76. 0076exact hi
  77. 0077exact ha
  78. 0078exact hb
  79. 0079have hlast : exists pfa_offset_left_scalar_sum_last_congruence pfa_offset_right_scalar_sum_last_congruence. (k*x) + (p) * pfa_offset_left_scalar_sum_last_congruence = (x2) + (p) * pfa_offset_right_scalar_sum_last_congruence
  80. 0080specialize hw (L)
  81. 0081specialize hw (x)
  82. 0082specialize hw (x2)
  83. 0083apply hw
  84. 0084specialize le_refl (S L)
  85. 0085apply le_refl
  86. 0086exact hfirst_witness_witness_left
  87. 0087exact hsecond_witness_witness_left
  88. 0088have hcombined : exists pfa_offset_left_scalar_sum_combined pfa_offset_right_scalar_sum_combined. (k*x1+k*x) + (p) * pfa_offset_left_scalar_sum_combined = (x3+x2) + (p) * pfa_offset_right_scalar_sum_combined
  89. 0089specialize mod_eq_add (p)
  90. 0090specialize mod_eq_add (k*x1)
  91. 0091specialize mod_eq_add (x3)
  92. 0092specialize mod_eq_add (k*x)
  93. 0093specialize mod_eq_add (x2)
  94. 0094apply mod_eq_add
  95. 0095exact hprefix
  96. 0096exact hlast
  97. 0097rewrite hfirst_witness_witness_right_right
  98. 0098rewrite hsecond_witness_witness_right_right
  99. 0099have hdistribute : k*(x1+x)=k*x1+k*x
  100. 0100apply mul_add
  101. 0101rewrite hdistribute
  102. 0102exact hcombined