SS000D

divisor_signed_sum_empty_value

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

The empty signed prefix sum is exactly canonical zero, regardless of the packed component streams.

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 F z. (exists dst_positive_code_empty_sum dst_positive_scale_empty_sum dst_negative_code_empty_sum dst_negative_scale_empty_sum dst_positive_sum_empty_sum dst_negative_sum_empty_sum. (((F) = (((((dst_positive_code_empty_sum) + (dst_positive_scale_empty_sum)) * S ((dst_positive_code_empty_sum) + (dst_positive_scale_empty_sum)) + ((dst_positive_scale_empty_sum) + (dst_positive_scale_empty_sum))) + (((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) * S ((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) + ((dst_negative_scale_empty_sum) + (dst_negative_scale_empty_sum)))) * S ((((dst_positive_code_empty_sum) + (dst_positive_scale_empty_sum)) * S ((dst_positive_code_empty_sum) + (dst_positive_scale_empty_sum)) + ((dst_positive_scale_empty_sum) + (dst_positive_scale_empty_sum))) + (((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) * S ((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) + ((dst_negative_scale_empty_sum) + (dst_negative_scale_empty_sum)))) + ((((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) * S ((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) + ((dst_negative_scale_empty_sum) + (dst_negative_scale_empty_sum))) + (((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) * S ((dst_negative_code_empty_sum) + (dst_negative_scale_empty_sum)) + ((dst_negative_scale_empty_sum) + (dst_negative_scale_empty_sum)))))) /\ (((exists fs_u_dst_empty_sumpositive fs_v_dst_empty_sumpositive. ((((exists fs_h_dst_empty_sumpositive_body_start. fs_h_dst_empty_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_empty_sumpositive)) /\ exists fs_q_dst_empty_sumpositive_body_start. fs_u_dst_empty_sumpositive = fs_q_dst_empty_sumpositive_body_start * S ((S (0)) * fs_v_dst_empty_sumpositive) + (0))) /\ ((((exists fs_h_dst_empty_sumpositive_body_terminal. fs_h_dst_empty_sumpositive_body_terminal + S (dst_positive_sum_empty_sum) = S ((S (0)) * fs_v_dst_empty_sumpositive)) /\ exists fs_q_dst_empty_sumpositive_body_terminal. fs_u_dst_empty_sumpositive = fs_q_dst_empty_sumpositive_body_terminal * S ((S (0)) * fs_v_dst_empty_sumpositive) + (dst_positive_sum_empty_sum))) /\ forall fs_i_dst_empty_sumpositive_body_steps. (exists fs_lt_dst_empty_sumpositive_body_steps_bound. fs_lt_dst_empty_sumpositive_body_steps_bound + S fs_i_dst_empty_sumpositive_body_steps = 0) -> exists fs_a_dst_empty_sumpositive_body_steps fs_r_dst_empty_sumpositive_body_steps fs_s_dst_empty_sumpositive_body_steps. ((((exists fs_h_dst_empty_sumpositive_body_steps_summand. fs_h_dst_empty_sumpositive_body_steps_summand + S (fs_a_dst_empty_sumpositive_body_steps) = S ((S (fs_i_dst_empty_sumpositive_body_steps)) * dst_positive_scale_empty_sum)) /\ exists fs_q_dst_empty_sumpositive_body_steps_summand. dst_positive_code_empty_sum = fs_q_dst_empty_sumpositive_body_steps_summand * S ((S (fs_i_dst_empty_sumpositive_body_steps)) * dst_positive_scale_empty_sum) + (fs_a_dst_empty_sumpositive_body_steps))) /\ ((((exists fs_h_dst_empty_sumpositive_body_steps_partial. fs_h_dst_empty_sumpositive_body_steps_partial + S (fs_r_dst_empty_sumpositive_body_steps) = S ((S (fs_i_dst_empty_sumpositive_body_steps)) * fs_v_dst_empty_sumpositive)) /\ exists fs_q_dst_empty_sumpositive_body_steps_partial. fs_u_dst_empty_sumpositive = fs_q_dst_empty_sumpositive_body_steps_partial * S ((S (fs_i_dst_empty_sumpositive_body_steps)) * fs_v_dst_empty_sumpositive) + (fs_r_dst_empty_sumpositive_body_steps))) /\ ((((exists fs_h_dst_empty_sumpositive_body_steps_successor. fs_h_dst_empty_sumpositive_body_steps_successor + S (fs_s_dst_empty_sumpositive_body_steps) = S ((S (S fs_i_dst_empty_sumpositive_body_steps)) * fs_v_dst_empty_sumpositive)) /\ exists fs_q_dst_empty_sumpositive_body_steps_successor. fs_u_dst_empty_sumpositive = fs_q_dst_empty_sumpositive_body_steps_successor * S ((S (S fs_i_dst_empty_sumpositive_body_steps)) * fs_v_dst_empty_sumpositive) + (fs_s_dst_empty_sumpositive_body_steps))) /\ fs_s_dst_empty_sumpositive_body_steps = fs_r_dst_empty_sumpositive_body_steps + fs_a_dst_empty_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_empty_sumnegative fs_v_dst_empty_sumnegative. ((((exists fs_h_dst_empty_sumnegative_body_start. fs_h_dst_empty_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_empty_sumnegative)) /\ exists fs_q_dst_empty_sumnegative_body_start. fs_u_dst_empty_sumnegative = fs_q_dst_empty_sumnegative_body_start * S ((S (0)) * fs_v_dst_empty_sumnegative) + (0))) /\ ((((exists fs_h_dst_empty_sumnegative_body_terminal. fs_h_dst_empty_sumnegative_body_terminal + S (dst_negative_sum_empty_sum) = S ((S (0)) * fs_v_dst_empty_sumnegative)) /\ exists fs_q_dst_empty_sumnegative_body_terminal. fs_u_dst_empty_sumnegative = fs_q_dst_empty_sumnegative_body_terminal * S ((S (0)) * fs_v_dst_empty_sumnegative) + (dst_negative_sum_empty_sum))) /\ forall fs_i_dst_empty_sumnegative_body_steps. (exists fs_lt_dst_empty_sumnegative_body_steps_bound. fs_lt_dst_empty_sumnegative_body_steps_bound + S fs_i_dst_empty_sumnegative_body_steps = 0) -> exists fs_a_dst_empty_sumnegative_body_steps fs_r_dst_empty_sumnegative_body_steps fs_s_dst_empty_sumnegative_body_steps. ((((exists fs_h_dst_empty_sumnegative_body_steps_summand. fs_h_dst_empty_sumnegative_body_steps_summand + S (fs_a_dst_empty_sumnegative_body_steps) = S ((S (fs_i_dst_empty_sumnegative_body_steps)) * dst_negative_scale_empty_sum)) /\ exists fs_q_dst_empty_sumnegative_body_steps_summand. dst_negative_code_empty_sum = fs_q_dst_empty_sumnegative_body_steps_summand * S ((S (fs_i_dst_empty_sumnegative_body_steps)) * dst_negative_scale_empty_sum) + (fs_a_dst_empty_sumnegative_body_steps))) /\ ((((exists fs_h_dst_empty_sumnegative_body_steps_partial. fs_h_dst_empty_sumnegative_body_steps_partial + S (fs_r_dst_empty_sumnegative_body_steps) = S ((S (fs_i_dst_empty_sumnegative_body_steps)) * fs_v_dst_empty_sumnegative)) /\ exists fs_q_dst_empty_sumnegative_body_steps_partial. fs_u_dst_empty_sumnegative = fs_q_dst_empty_sumnegative_body_steps_partial * S ((S (fs_i_dst_empty_sumnegative_body_steps)) * fs_v_dst_empty_sumnegative) + (fs_r_dst_empty_sumnegative_body_steps))) /\ ((((exists fs_h_dst_empty_sumnegative_body_steps_successor. fs_h_dst_empty_sumnegative_body_steps_successor + S (fs_s_dst_empty_sumnegative_body_steps) = S ((S (S fs_i_dst_empty_sumnegative_body_steps)) * fs_v_dst_empty_sumnegative)) /\ exists fs_q_dst_empty_sumnegative_body_steps_successor. fs_u_dst_empty_sumnegative = fs_q_dst_empty_sumnegative_body_steps_successor * S ((S (S fs_i_dst_empty_sumnegative_body_steps)) * fs_v_dst_empty_sumnegative) + (fs_s_dst_empty_sumnegative_body_steps))) /\ fs_s_dst_empty_sumnegative_body_steps = fs_r_dst_empty_sumnegative_body_steps + fs_a_dst_empty_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_empty_sumresult ge_balance_negative_empty_sumresult. (((((z) = 2 * (ge_balance_positive_empty_sumresult) /\ (ge_balance_negative_empty_sumresult) = 0) \/ exists ge_signed_half_empty_sumresultdecode. (((z) = 2 * ge_signed_half_empty_sumresultdecode + 1 /\ (ge_balance_positive_empty_sumresult) = 0) /\ (ge_balance_negative_empty_sumresult) = S ge_signed_half_empty_sumresultdecode))) /\ ((dst_positive_sum_empty_sum) + ge_balance_negative_empty_sumresult = (dst_negative_sum_empty_sum) + ge_balance_positive_empty_sumresult))))))))) -> z = 0

Constructive proof overview

Generated structural guide

The empty signed prefix sum is exactly canonical zero, regardless of the packed component streams.

The unchanged tactic script uses 2 declared prerequisites and contains 36 exact native proof lines.

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

Proof neighborhood

Direct dependencies

beta_sum_zero Stable theorem; checked-use authorized signed_balance_zero_iff Alpha theorem; checked-use authorized

Direct dependents

SS000E divisor_signed_sum_empty_exists

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

36 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.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro F
  2. L2
    intro z
  3. L3
    intro h
02Separate the logical casesL4–12

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

  1. L4
    cases h
  2. L5
    cases h_witness
  3. L6
    cases h_witness_witness
  4. L7
    cases h_witness_witness_witness
  5. L8
    cases h_witness_witness_witness_witness
  6. L9
    cases h_witness_witness_witness_witness_witness
  7. L10
    cases h_witness_witness_witness_witness_witness_witness
  8. L11
    cases h_witness_witness_witness_witness_witness_witness_right
  9. L12
    cases h_witness_witness_witness_witness_witness_witness_right_right
03Establish hpL13–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 hp : x4 = 0
  2. L14
    specialize beta_sum_zero (x)
  3. L15
    specialize beta_sum_zero (x1)
  4. L16
    specialize beta_sum_zero (x4)
  5. L17
    apply beta_sum_zero
  6. L18
    exact h_witness_witness_witness_witness_witness_witness_right_left
04Establish hnL19–24

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

  1. L19
    have hn : x5 = 0
  2. L20
    specialize beta_sum_zero (x2)
  3. L21
    specialize beta_sum_zero (x3)
  4. L22
    specialize beta_sum_zero (x5)
  5. L23
    apply beta_sum_zero
  6. L24
    exact h_witness_witness_witness_witness_witness_witness_right_right_left
05Establish hzeroL25–30

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

  1. L25
    have hzero : (z = 0 -> x4 = x5) /\ (x4 = x5 -> z = 0)
  2. L26
    specialize signed_balance_zero_iff (z)
  3. L27
    specialize signed_balance_zero_iff (x4)
  4. L28
    specialize signed_balance_zero_iff (x5)
  5. L29
    apply signed_balance_zero_iff
  6. L30
    exact h_witness_witness_witness_witness_witness_witness_right_right_right
06Separate the logical casesL31–31

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

  1. L31
    cases hzero
07Use earlier factsL32–32

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

  1. L32
    apply hzero_right
08Calculate and transport equalitiesL33–33

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

  1. L33
    trans 0
09Use earlier factsL34–34

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

  1. L34
    exact hp
10Calculate and transport equalitiesL35–35

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

  1. L35
    symm
11Use earlier factsL36–36

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

  1. L36
    exact hn

Library-wide reading audit

Original exact command ledger · 36 lines
  1. 0001intro F
  2. 0002intro z
  3. 0003intro h
  4. 0004cases h
  5. 0005cases h_witness
  6. 0006cases h_witness_witness
  7. 0007cases h_witness_witness_witness
  8. 0008cases h_witness_witness_witness_witness
  9. 0009cases h_witness_witness_witness_witness_witness
  10. 0010cases h_witness_witness_witness_witness_witness_witness
  11. 0011cases h_witness_witness_witness_witness_witness_witness_right
  12. 0012cases h_witness_witness_witness_witness_witness_witness_right_right
  13. 0013have hp : x4 = 0
  14. 0014specialize beta_sum_zero (x)
  15. 0015specialize beta_sum_zero (x1)
  16. 0016specialize beta_sum_zero (x4)
  17. 0017apply beta_sum_zero
  18. 0018exact h_witness_witness_witness_witness_witness_witness_right_left
  19. 0019have hn : x5 = 0
  20. 0020specialize beta_sum_zero (x2)
  21. 0021specialize beta_sum_zero (x3)
  22. 0022specialize beta_sum_zero (x5)
  23. 0023apply beta_sum_zero
  24. 0024exact h_witness_witness_witness_witness_witness_witness_right_right_left
  25. 0025have hzero : (z = 0 -> x4 = x5) /\ (x4 = x5 -> z = 0)
  26. 0026specialize signed_balance_zero_iff (z)
  27. 0027specialize signed_balance_zero_iff (x4)
  28. 0028specialize signed_balance_zero_iff (x5)
  29. 0029apply signed_balance_zero_iff
  30. 0030exact h_witness_witness_witness_witness_witness_witness_right_right_right
  31. 0031cases hzero
  32. 0032apply hzero_right
  33. 0033trans 0
  34. 0034exact hp
  35. 0035symm
  36. 0036exact hn