ZS0007

signed_prefix_sum_last_value

If a prefix is zero, its next actual sum is precisely the actual last entry, including the l=0 boundary.

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

The zero window is half-open and its order hypothesis is essential. All folds retain actual beta-coded traces. These are support lemmas for the separately verified full inversion endpoint.

Exact theorem in conservative defined notation

∀ F. ∀ l. ∀ a. ∀ z. SignedZeroWindow(F,0,l) → ArithAt(F,l,a) → SignedPrefixSum(F,S l,z) → z = a

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

SignedAdd(a,b,c) · 1ArithAt(F,i,z) · 2SignedPrefixSum(F,l,z) · 2SignedZeroWindow(F,k,l) · 1

Actual proof prerequisites

divisor_signed_sum_successor_decompose · checked external prerequisitesigned_prefix_sum_zero_valuedivisor_signed_table_at_functional · checked external prerequisitesigned_add_functional · checked external prerequisitesigned_add_zero_left · checked external prerequisite
Original expanded first-order statement 
forall F l a z. (forall sfs_index_last_zeros sfs_value_last_zeros. (exists pvs_le_gap_last_zeroslower. pvs_le_gap_last_zeroslower + (0) = (sfs_index_last_zeros)) -> (exists pvs_gap_last_zerosupper. pvs_gap_last_zerosupper + S (sfs_index_last_zeros) = (l)) -> (exists dst_positive_code_last_zerosentry dst_positive_scale_last_zerosentry dst_negative_code_last_zerosentry dst_negative_scale_last_zerosentry dst_positive_last_zerosentry dst_negative_last_zerosentry. (((F) = (((((dst_positive_code_last_zerosentry) + (dst_positive_scale_last_zerosentry)) * S ((dst_positive_code_last_zerosentry) + (dst_positive_scale_last_zerosentry)) + ((dst_positive_scale_last_zerosentry) + (dst_positive_scale_last_zerosentry))) + (((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) * S ((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) + ((dst_negative_scale_last_zerosentry) + (dst_negative_scale_last_zerosentry)))) * S ((((dst_positive_code_last_zerosentry) + (dst_positive_scale_last_zerosentry)) * S ((dst_positive_code_last_zerosentry) + (dst_positive_scale_last_zerosentry)) + ((dst_positive_scale_last_zerosentry) + (dst_positive_scale_last_zerosentry))) + (((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) * S ((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) + ((dst_negative_scale_last_zerosentry) + (dst_negative_scale_last_zerosentry)))) + ((((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) * S ((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) + ((dst_negative_scale_last_zerosentry) + (dst_negative_scale_last_zerosentry))) + (((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) * S ((dst_negative_code_last_zerosentry) + (dst_negative_scale_last_zerosentry)) + ((dst_negative_scale_last_zerosentry) + (dst_negative_scale_last_zerosentry)))))) /\ (((((exists ff_h_pvs_last_zerosentrypositive. ff_h_pvs_last_zerosentrypositive + S (dst_positive_last_zerosentry) = S ((S (sfs_index_last_zeros)) * dst_positive_scale_last_zerosentry)) /\ exists ff_q_pvs_last_zerosentrypositive. dst_positive_code_last_zerosentry = ff_q_pvs_last_zerosentrypositive * S ((S (sfs_index_last_zeros)) * dst_positive_scale_last_zerosentry) + (dst_positive_last_zerosentry))) /\ (((((exists ff_h_pvs_last_zerosentrynegative. ff_h_pvs_last_zerosentrynegative + S (dst_negative_last_zerosentry) = S ((S (sfs_index_last_zeros)) * dst_negative_scale_last_zerosentry)) /\ exists ff_q_pvs_last_zerosentrynegative. dst_negative_code_last_zerosentry = ff_q_pvs_last_zerosentrynegative * S ((S (sfs_index_last_zeros)) * dst_negative_scale_last_zerosentry) + (dst_negative_last_zerosentry))) /\ (exists ge_balance_positive_last_zerosentryvalue ge_balance_negative_last_zerosentryvalue. (((((sfs_value_last_zeros) = 2 * (ge_balance_positive_last_zerosentryvalue) /\ (ge_balance_negative_last_zerosentryvalue) = 0) \/ exists ge_signed_half_last_zerosentryvaluedecode. (((sfs_value_last_zeros) = 2 * ge_signed_half_last_zerosentryvaluedecode + 1 /\ (ge_balance_positive_last_zerosentryvalue) = 0) /\ (ge_balance_negative_last_zerosentryvalue) = S ge_signed_half_last_zerosentryvaluedecode))) /\ ((dst_positive_last_zerosentry) + ge_balance_negative_last_zerosentryvalue = (dst_negative_last_zerosentry) + ge_balance_positive_last_zerosentryvalue))))))))) -> sfs_value_last_zeros=0) -> (exists dst_positive_code_last_value dst_positive_scale_last_value dst_negative_code_last_value dst_negative_scale_last_value dst_positive_last_value dst_negative_last_value. (((F) = (((((dst_positive_code_last_value) + (dst_positive_scale_last_value)) * S ((dst_positive_code_last_value) + (dst_positive_scale_last_value)) + ((dst_positive_scale_last_value) + (dst_positive_scale_last_value))) + (((dst_negative_code_last_value) + (dst_negative_scale_last_value)) * S ((dst_negative_code_last_value) + (dst_negative_scale_last_value)) + ((dst_negative_scale_last_value) + (dst_negative_scale_last_value)))) * S ((((dst_positive_code_last_value) + (dst_positive_scale_last_value)) * S ((dst_positive_code_last_value) + (dst_positive_scale_last_value)) + ((dst_positive_scale_last_value) + (dst_positive_scale_last_value))) + (((dst_negative_code_last_value) + (dst_negative_scale_last_value)) * S ((dst_negative_code_last_value) + (dst_negative_scale_last_value)) + ((dst_negative_scale_last_value) + (dst_negative_scale_last_value)))) + ((((dst_negative_code_last_value) + (dst_negative_scale_last_value)) * S ((dst_negative_code_last_value) + (dst_negative_scale_last_value)) + ((dst_negative_scale_last_value) + (dst_negative_scale_last_value))) + (((dst_negative_code_last_value) + (dst_negative_scale_last_value)) * S ((dst_negative_code_last_value) + (dst_negative_scale_last_value)) + ((dst_negative_scale_last_value) + (dst_negative_scale_last_value)))))) /\ (((((exists ff_h_pvs_last_valuepositive. ff_h_pvs_last_valuepositive + S (dst_positive_last_value) = S ((S (l)) * dst_positive_scale_last_value)) /\ exists ff_q_pvs_last_valuepositive. dst_positive_code_last_value = ff_q_pvs_last_valuepositive * S ((S (l)) * dst_positive_scale_last_value) + (dst_positive_last_value))) /\ (((((exists ff_h_pvs_last_valuenegative. ff_h_pvs_last_valuenegative + S (dst_negative_last_value) = S ((S (l)) * dst_negative_scale_last_value)) /\ exists ff_q_pvs_last_valuenegative. dst_negative_code_last_value = ff_q_pvs_last_valuenegative * S ((S (l)) * dst_negative_scale_last_value) + (dst_negative_last_value))) /\ (exists ge_balance_positive_last_valuevalue ge_balance_negative_last_valuevalue. (((((a) = 2 * (ge_balance_positive_last_valuevalue) /\ (ge_balance_negative_last_valuevalue) = 0) \/ exists ge_signed_half_last_valuevaluedecode. (((a) = 2 * ge_signed_half_last_valuevaluedecode + 1 /\ (ge_balance_positive_last_valuevalue) = 0) /\ (ge_balance_negative_last_valuevalue) = S ge_signed_half_last_valuevaluedecode))) /\ ((dst_positive_last_value) + ge_balance_negative_last_valuevalue = (dst_negative_last_value) + ge_balance_positive_last_valuevalue))))))))) -> (exists dst_positive_code_last_sum dst_positive_scale_last_sum dst_negative_code_last_sum dst_negative_scale_last_sum dst_positive_sum_last_sum dst_negative_sum_last_sum. (((F) = (((((dst_positive_code_last_sum) + (dst_positive_scale_last_sum)) * S ((dst_positive_code_last_sum) + (dst_positive_scale_last_sum)) + ((dst_positive_scale_last_sum) + (dst_positive_scale_last_sum))) + (((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) * S ((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) + ((dst_negative_scale_last_sum) + (dst_negative_scale_last_sum)))) * S ((((dst_positive_code_last_sum) + (dst_positive_scale_last_sum)) * S ((dst_positive_code_last_sum) + (dst_positive_scale_last_sum)) + ((dst_positive_scale_last_sum) + (dst_positive_scale_last_sum))) + (((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) * S ((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) + ((dst_negative_scale_last_sum) + (dst_negative_scale_last_sum)))) + ((((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) * S ((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) + ((dst_negative_scale_last_sum) + (dst_negative_scale_last_sum))) + (((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) * S ((dst_negative_code_last_sum) + (dst_negative_scale_last_sum)) + ((dst_negative_scale_last_sum) + (dst_negative_scale_last_sum)))))) /\ (((exists fs_u_dst_last_sumpositive fs_v_dst_last_sumpositive. ((((exists fs_h_dst_last_sumpositive_body_start. fs_h_dst_last_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_last_sumpositive)) /\ exists fs_q_dst_last_sumpositive_body_start. fs_u_dst_last_sumpositive = fs_q_dst_last_sumpositive_body_start * S ((S (0)) * fs_v_dst_last_sumpositive) + (0))) /\ ((((exists fs_h_dst_last_sumpositive_body_terminal. fs_h_dst_last_sumpositive_body_terminal + S (dst_positive_sum_last_sum) = S ((S (S l)) * fs_v_dst_last_sumpositive)) /\ exists fs_q_dst_last_sumpositive_body_terminal. fs_u_dst_last_sumpositive = fs_q_dst_last_sumpositive_body_terminal * S ((S (S l)) * fs_v_dst_last_sumpositive) + (dst_positive_sum_last_sum))) /\ forall fs_i_dst_last_sumpositive_body_steps. (exists fs_lt_dst_last_sumpositive_body_steps_bound. fs_lt_dst_last_sumpositive_body_steps_bound + S fs_i_dst_last_sumpositive_body_steps = S l) -> exists fs_a_dst_last_sumpositive_body_steps fs_r_dst_last_sumpositive_body_steps fs_s_dst_last_sumpositive_body_steps. ((((exists fs_h_dst_last_sumpositive_body_steps_summand. fs_h_dst_last_sumpositive_body_steps_summand + S (fs_a_dst_last_sumpositive_body_steps) = S ((S (fs_i_dst_last_sumpositive_body_steps)) * dst_positive_scale_last_sum)) /\ exists fs_q_dst_last_sumpositive_body_steps_summand. dst_positive_code_last_sum = fs_q_dst_last_sumpositive_body_steps_summand * S ((S (fs_i_dst_last_sumpositive_body_steps)) * dst_positive_scale_last_sum) + (fs_a_dst_last_sumpositive_body_steps))) /\ ((((exists fs_h_dst_last_sumpositive_body_steps_partial. fs_h_dst_last_sumpositive_body_steps_partial + S (fs_r_dst_last_sumpositive_body_steps) = S ((S (fs_i_dst_last_sumpositive_body_steps)) * fs_v_dst_last_sumpositive)) /\ exists fs_q_dst_last_sumpositive_body_steps_partial. fs_u_dst_last_sumpositive = fs_q_dst_last_sumpositive_body_steps_partial * S ((S (fs_i_dst_last_sumpositive_body_steps)) * fs_v_dst_last_sumpositive) + (fs_r_dst_last_sumpositive_body_steps))) /\ ((((exists fs_h_dst_last_sumpositive_body_steps_successor. fs_h_dst_last_sumpositive_body_steps_successor + S (fs_s_dst_last_sumpositive_body_steps) = S ((S (S fs_i_dst_last_sumpositive_body_steps)) * fs_v_dst_last_sumpositive)) /\ exists fs_q_dst_last_sumpositive_body_steps_successor. fs_u_dst_last_sumpositive = fs_q_dst_last_sumpositive_body_steps_successor * S ((S (S fs_i_dst_last_sumpositive_body_steps)) * fs_v_dst_last_sumpositive) + (fs_s_dst_last_sumpositive_body_steps))) /\ fs_s_dst_last_sumpositive_body_steps = fs_r_dst_last_sumpositive_body_steps + fs_a_dst_last_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_last_sumnegative fs_v_dst_last_sumnegative. ((((exists fs_h_dst_last_sumnegative_body_start. fs_h_dst_last_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_last_sumnegative)) /\ exists fs_q_dst_last_sumnegative_body_start. fs_u_dst_last_sumnegative = fs_q_dst_last_sumnegative_body_start * S ((S (0)) * fs_v_dst_last_sumnegative) + (0))) /\ ((((exists fs_h_dst_last_sumnegative_body_terminal. fs_h_dst_last_sumnegative_body_terminal + S (dst_negative_sum_last_sum) = S ((S (S l)) * fs_v_dst_last_sumnegative)) /\ exists fs_q_dst_last_sumnegative_body_terminal. fs_u_dst_last_sumnegative = fs_q_dst_last_sumnegative_body_terminal * S ((S (S l)) * fs_v_dst_last_sumnegative) + (dst_negative_sum_last_sum))) /\ forall fs_i_dst_last_sumnegative_body_steps. (exists fs_lt_dst_last_sumnegative_body_steps_bound. fs_lt_dst_last_sumnegative_body_steps_bound + S fs_i_dst_last_sumnegative_body_steps = S l) -> exists fs_a_dst_last_sumnegative_body_steps fs_r_dst_last_sumnegative_body_steps fs_s_dst_last_sumnegative_body_steps. ((((exists fs_h_dst_last_sumnegative_body_steps_summand. fs_h_dst_last_sumnegative_body_steps_summand + S (fs_a_dst_last_sumnegative_body_steps) = S ((S (fs_i_dst_last_sumnegative_body_steps)) * dst_negative_scale_last_sum)) /\ exists fs_q_dst_last_sumnegative_body_steps_summand. dst_negative_code_last_sum = fs_q_dst_last_sumnegative_body_steps_summand * S ((S (fs_i_dst_last_sumnegative_body_steps)) * dst_negative_scale_last_sum) + (fs_a_dst_last_sumnegative_body_steps))) /\ ((((exists fs_h_dst_last_sumnegative_body_steps_partial. fs_h_dst_last_sumnegative_body_steps_partial + S (fs_r_dst_last_sumnegative_body_steps) = S ((S (fs_i_dst_last_sumnegative_body_steps)) * fs_v_dst_last_sumnegative)) /\ exists fs_q_dst_last_sumnegative_body_steps_partial. fs_u_dst_last_sumnegative = fs_q_dst_last_sumnegative_body_steps_partial * S ((S (fs_i_dst_last_sumnegative_body_steps)) * fs_v_dst_last_sumnegative) + (fs_r_dst_last_sumnegative_body_steps))) /\ ((((exists fs_h_dst_last_sumnegative_body_steps_successor. fs_h_dst_last_sumnegative_body_steps_successor + S (fs_s_dst_last_sumnegative_body_steps) = S ((S (S fs_i_dst_last_sumnegative_body_steps)) * fs_v_dst_last_sumnegative)) /\ exists fs_q_dst_last_sumnegative_body_steps_successor. fs_u_dst_last_sumnegative = fs_q_dst_last_sumnegative_body_steps_successor * S ((S (S fs_i_dst_last_sumnegative_body_steps)) * fs_v_dst_last_sumnegative) + (fs_s_dst_last_sumnegative_body_steps))) /\ fs_s_dst_last_sumnegative_body_steps = fs_r_dst_last_sumnegative_body_steps + fs_a_dst_last_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_last_sumresult ge_balance_negative_last_sumresult. (((((z) = 2 * (ge_balance_positive_last_sumresult) /\ (ge_balance_negative_last_sumresult) = 0) \/ exists ge_signed_half_last_sumresultdecode. (((z) = 2 * ge_signed_half_last_sumresultdecode + 1 /\ (ge_balance_positive_last_sumresult) = 0) /\ (ge_balance_negative_last_sumresult) = S ge_signed_half_last_sumresultdecode))) /\ ((dst_positive_sum_last_sum) + ge_balance_negative_last_sumresult = (dst_negative_sum_last_sum) + ge_balance_positive_last_sumresult))))))))) -> z=a

Complete tactic proof in conservative notation

All 44 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

44 script commands · 7 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.

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)
signed prefix sum zero value
01Fix variables and assumptionsL1–7

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

  1. L1
    intro F
  2. L2
    intro l
  3. L3
    intro a
  4. L4
    intro z
  5. L5
    intro hz
  6. L6
    intro ha
  7. L7
    intro hs
02Establish hdL8–13

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

  1. L8
    have hd : ∃ u. ∃ v. SignedPrefixSum(F,l,u) ∧ (ArithAt(F,l,v) ∧ SignedAdd(u,v,z))Definitions: SignedPrefixSum(F,l,u)ArithAt(F,l,v)SignedAdd(u,v,z)Original native command in the exact edition
  2. L9
    specialize divisor_signed_sum_successor_decompose (F)
  3. L10
    specialize divisor_signed_sum_successor_decompose (l)
  4. L11
    specialize divisor_signed_sum_successor_decompose (z)
  5. L12
    apply divisor_signed_sum_successor_decompose
  6. L13
    exact hs
03Separate the logical casesL14–17

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

  1. L14
    cases hd
  2. L15
    cases hd_witness
  3. L16
    cases hd_witness_witness
  4. L17
    cases hd_witness_witness_right
04Establish hpL18–24

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

  1. L18
    have hp : x=0
  2. L19
    specialize signed_prefix_sum_zero_value (F)
  3. L20
    specialize signed_prefix_sum_zero_value (l)
  4. L21
    specialize signed_prefix_sum_zero_value (x)
  5. L22
    apply signed_prefix_sum_zero_value
  6. L23
    exact hz
  7. L24
    exact hd_witness_witness_left
05Establish heL25–34

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table at functional.

  1. L25
    have he : x1=a
  2. L26
    specialize divisor_signed_table_at_functional (F)
  3. L27
    specialize divisor_signed_table_at_functional (l)
  4. L28
    specialize divisor_signed_table_at_functional (x1)
  5. L29
    specialize divisor_signed_table_at_functional (a)
  6. L30
    apply divisor_signed_table_at_functional
  7. L31
    exact hd_witness_witness_right_left
  8. L32
    exact ha
  9. L33
    rewrite hp at hd_witness_witness_right_right
  10. L34
    rewrite hp at hd_witness_witness_right_right
06Calculate and transport equalitiesL35–36

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

  1. L35
    rewrite he at hd_witness_witness_right_right
  2. L36
    rewrite he at hd_witness_witness_right_right
07Use earlier factsL37–44

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

  1. L37
    specialize signed_add_functional (0)
  2. L38
    specialize signed_add_functional (a)
  3. L39
    specialize signed_add_functional (z)
  4. L40
    specialize signed_add_functional (a)
  5. L41
    apply signed_add_functional
  6. L42
    exact hd_witness_witness_right_right
  7. L43
    specialize signed_add_zero_left (a)
  8. L44
    apply signed_add_zero_left

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro F
  2. 0002intro l
  3. 0003intro a
  4. 0004intro z
  5. 0005intro hz
  6. 0006intro ha
  7. 0007intro hs
  8. 0008have hd : ∃ u. ∃ v. SignedPrefixSum(F,l,u) ∧ (ArithAt(F,l,v) ∧ SignedAdd(u,v,z))
  9. 0009specialize divisor_signed_sum_successor_decompose (F)
  10. 0010specialize divisor_signed_sum_successor_decompose (l)
  11. 0011specialize divisor_signed_sum_successor_decompose (z)
  12. 0012apply divisor_signed_sum_successor_decompose
  13. 0013exact hs
  14. 0014cases hd
  15. 0015cases hd_witness
  16. 0016cases hd_witness_witness
  17. 0017cases hd_witness_witness_right
  18. 0018have hp : x=0
  19. 0019specialize signed_prefix_sum_zero_value (F)
  20. 0020specialize signed_prefix_sum_zero_value (l)
  21. 0021specialize signed_prefix_sum_zero_value (x)
  22. 0022apply signed_prefix_sum_zero_value
  23. 0023exact hz
  24. 0024exact hd_witness_witness_left
  25. 0025have he : x1=a
  26. 0026specialize divisor_signed_table_at_functional (F)
  27. 0027specialize divisor_signed_table_at_functional (l)
  28. 0028specialize divisor_signed_table_at_functional (x1)
  29. 0029specialize divisor_signed_table_at_functional (a)
  30. 0030apply divisor_signed_table_at_functional
  31. 0031exact hd_witness_witness_right_left
  32. 0032exact ha
  33. 0033rewrite hp at hd_witness_witness_right_right
  34. 0034rewrite hp at hd_witness_witness_right_right
  35. 0035rewrite he at hd_witness_witness_right_right
  36. 0036rewrite he at hd_witness_witness_right_right
  37. 0037specialize signed_add_functional (0)
  38. 0038specialize signed_add_functional (a)
  39. 0039specialize signed_add_functional (z)
  40. 0040specialize signed_add_functional (a)
  41. 0041apply signed_add_functional
  42. 0042exact hd_witness_witness_right_right
  43. 0043specialize signed_add_zero_left (a)
  44. 0044apply signed_add_zero_left