ZS0005

signed_prefix_sum_zero_value

A genuinely all-zero represented prefix has canonical signed sum zero; the proof retains actual fold witnesses.

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. ∀ z. SignedZeroWindow(F,0,l) → SignedPrefixSum(F,l,z) → z = 0

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

Definition DAG

SignedPrefixSum(F,l,z) · 2SignedZeroWindow(F,k,l) · 1

Actual proof prerequisites

divisor_signed_sum_empty_exists · checked external prerequisitesigned_prefix_sum_zero_tailzero_le · checked external prerequisite
Original expanded first-order statement 
forall F l z. (forall sfs_index_zero_values sfs_value_zero_values. (exists pvs_le_gap_zero_valueslower. pvs_le_gap_zero_valueslower + (0) = (sfs_index_zero_values)) -> (exists pvs_gap_zero_valuesupper. pvs_gap_zero_valuesupper + S (sfs_index_zero_values) = (l)) -> (exists dst_positive_code_zero_valuesentry dst_positive_scale_zero_valuesentry dst_negative_code_zero_valuesentry dst_negative_scale_zero_valuesentry dst_positive_zero_valuesentry dst_negative_zero_valuesentry. (((F) = (((((dst_positive_code_zero_valuesentry) + (dst_positive_scale_zero_valuesentry)) * S ((dst_positive_code_zero_valuesentry) + (dst_positive_scale_zero_valuesentry)) + ((dst_positive_scale_zero_valuesentry) + (dst_positive_scale_zero_valuesentry))) + (((dst_negative_code_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)) * S ((dst_negative_code_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)) + ((dst_negative_scale_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)))) * S ((((dst_positive_code_zero_valuesentry) + (dst_positive_scale_zero_valuesentry)) * S ((dst_positive_code_zero_valuesentry) + (dst_positive_scale_zero_valuesentry)) + ((dst_positive_scale_zero_valuesentry) + (dst_positive_scale_zero_valuesentry))) + (((dst_negative_code_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)) * S ((dst_negative_code_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)) + ((dst_negative_scale_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)))) + ((((dst_negative_code_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)) * S ((dst_negative_code_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)) + ((dst_negative_scale_zero_valuesentry) + (dst_negative_scale_zero_valuesentry))) + (((dst_negative_code_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)) * S ((dst_negative_code_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)) + ((dst_negative_scale_zero_valuesentry) + (dst_negative_scale_zero_valuesentry)))))) /\ (((((exists ff_h_pvs_zero_valuesentrypositive. ff_h_pvs_zero_valuesentrypositive + S (dst_positive_zero_valuesentry) = S ((S (sfs_index_zero_values)) * dst_positive_scale_zero_valuesentry)) /\ exists ff_q_pvs_zero_valuesentrypositive. dst_positive_code_zero_valuesentry = ff_q_pvs_zero_valuesentrypositive * S ((S (sfs_index_zero_values)) * dst_positive_scale_zero_valuesentry) + (dst_positive_zero_valuesentry))) /\ (((((exists ff_h_pvs_zero_valuesentrynegative. ff_h_pvs_zero_valuesentrynegative + S (dst_negative_zero_valuesentry) = S ((S (sfs_index_zero_values)) * dst_negative_scale_zero_valuesentry)) /\ exists ff_q_pvs_zero_valuesentrynegative. dst_negative_code_zero_valuesentry = ff_q_pvs_zero_valuesentrynegative * S ((S (sfs_index_zero_values)) * dst_negative_scale_zero_valuesentry) + (dst_negative_zero_valuesentry))) /\ (exists ge_balance_positive_zero_valuesentryvalue ge_balance_negative_zero_valuesentryvalue. (((((sfs_value_zero_values) = 2 * (ge_balance_positive_zero_valuesentryvalue) /\ (ge_balance_negative_zero_valuesentryvalue) = 0) \/ exists ge_signed_half_zero_valuesentryvaluedecode. (((sfs_value_zero_values) = 2 * ge_signed_half_zero_valuesentryvaluedecode + 1 /\ (ge_balance_positive_zero_valuesentryvalue) = 0) /\ (ge_balance_negative_zero_valuesentryvalue) = S ge_signed_half_zero_valuesentryvaluedecode))) /\ ((dst_positive_zero_valuesentry) + ge_balance_negative_zero_valuesentryvalue = (dst_negative_zero_valuesentry) + ge_balance_positive_zero_valuesentryvalue))))))))) -> sfs_value_zero_values=0) -> (exists dst_positive_code_zero_sum dst_positive_scale_zero_sum dst_negative_code_zero_sum dst_negative_scale_zero_sum dst_positive_sum_zero_sum dst_negative_sum_zero_sum. (((F) = (((((dst_positive_code_zero_sum) + (dst_positive_scale_zero_sum)) * S ((dst_positive_code_zero_sum) + (dst_positive_scale_zero_sum)) + ((dst_positive_scale_zero_sum) + (dst_positive_scale_zero_sum))) + (((dst_negative_code_zero_sum) + (dst_negative_scale_zero_sum)) * S ((dst_negative_code_zero_sum) + (dst_negative_scale_zero_sum)) + ((dst_negative_scale_zero_sum) + (dst_negative_scale_zero_sum)))) * S ((((dst_positive_code_zero_sum) + (dst_positive_scale_zero_sum)) * S ((dst_positive_code_zero_sum) + (dst_positive_scale_zero_sum)) + ((dst_positive_scale_zero_sum) + (dst_positive_scale_zero_sum))) + (((dst_negative_code_zero_sum) + (dst_negative_scale_zero_sum)) * S ((dst_negative_code_zero_sum) + (dst_negative_scale_zero_sum)) + ((dst_negative_scale_zero_sum) + (dst_negative_scale_zero_sum)))) + ((((dst_negative_code_zero_sum) + (dst_negative_scale_zero_sum)) * S ((dst_negative_code_zero_sum) + (dst_negative_scale_zero_sum)) + ((dst_negative_scale_zero_sum) + (dst_negative_scale_zero_sum))) + (((dst_negative_code_zero_sum) + (dst_negative_scale_zero_sum)) * S ((dst_negative_code_zero_sum) + (dst_negative_scale_zero_sum)) + ((dst_negative_scale_zero_sum) + (dst_negative_scale_zero_sum)))))) /\ (((exists fs_u_dst_zero_sumpositive fs_v_dst_zero_sumpositive. ((((exists fs_h_dst_zero_sumpositive_body_start. fs_h_dst_zero_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_sumpositive)) /\ exists fs_q_dst_zero_sumpositive_body_start. fs_u_dst_zero_sumpositive = fs_q_dst_zero_sumpositive_body_start * S ((S (0)) * fs_v_dst_zero_sumpositive) + (0))) /\ ((((exists fs_h_dst_zero_sumpositive_body_terminal. fs_h_dst_zero_sumpositive_body_terminal + S (dst_positive_sum_zero_sum) = S ((S (l)) * fs_v_dst_zero_sumpositive)) /\ exists fs_q_dst_zero_sumpositive_body_terminal. fs_u_dst_zero_sumpositive = fs_q_dst_zero_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_zero_sumpositive) + (dst_positive_sum_zero_sum))) /\ forall fs_i_dst_zero_sumpositive_body_steps. (exists fs_lt_dst_zero_sumpositive_body_steps_bound. fs_lt_dst_zero_sumpositive_body_steps_bound + S fs_i_dst_zero_sumpositive_body_steps = l) -> exists fs_a_dst_zero_sumpositive_body_steps fs_r_dst_zero_sumpositive_body_steps fs_s_dst_zero_sumpositive_body_steps. ((((exists fs_h_dst_zero_sumpositive_body_steps_summand. fs_h_dst_zero_sumpositive_body_steps_summand + S (fs_a_dst_zero_sumpositive_body_steps) = S ((S (fs_i_dst_zero_sumpositive_body_steps)) * dst_positive_scale_zero_sum)) /\ exists fs_q_dst_zero_sumpositive_body_steps_summand. dst_positive_code_zero_sum = fs_q_dst_zero_sumpositive_body_steps_summand * S ((S (fs_i_dst_zero_sumpositive_body_steps)) * dst_positive_scale_zero_sum) + (fs_a_dst_zero_sumpositive_body_steps))) /\ ((((exists fs_h_dst_zero_sumpositive_body_steps_partial. fs_h_dst_zero_sumpositive_body_steps_partial + S (fs_r_dst_zero_sumpositive_body_steps) = S ((S (fs_i_dst_zero_sumpositive_body_steps)) * fs_v_dst_zero_sumpositive)) /\ exists fs_q_dst_zero_sumpositive_body_steps_partial. fs_u_dst_zero_sumpositive = fs_q_dst_zero_sumpositive_body_steps_partial * S ((S (fs_i_dst_zero_sumpositive_body_steps)) * fs_v_dst_zero_sumpositive) + (fs_r_dst_zero_sumpositive_body_steps))) /\ ((((exists fs_h_dst_zero_sumpositive_body_steps_successor. fs_h_dst_zero_sumpositive_body_steps_successor + S (fs_s_dst_zero_sumpositive_body_steps) = S ((S (S fs_i_dst_zero_sumpositive_body_steps)) * fs_v_dst_zero_sumpositive)) /\ exists fs_q_dst_zero_sumpositive_body_steps_successor. fs_u_dst_zero_sumpositive = fs_q_dst_zero_sumpositive_body_steps_successor * S ((S (S fs_i_dst_zero_sumpositive_body_steps)) * fs_v_dst_zero_sumpositive) + (fs_s_dst_zero_sumpositive_body_steps))) /\ fs_s_dst_zero_sumpositive_body_steps = fs_r_dst_zero_sumpositive_body_steps + fs_a_dst_zero_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_zero_sumnegative fs_v_dst_zero_sumnegative. ((((exists fs_h_dst_zero_sumnegative_body_start. fs_h_dst_zero_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_sumnegative)) /\ exists fs_q_dst_zero_sumnegative_body_start. fs_u_dst_zero_sumnegative = fs_q_dst_zero_sumnegative_body_start * S ((S (0)) * fs_v_dst_zero_sumnegative) + (0))) /\ ((((exists fs_h_dst_zero_sumnegative_body_terminal. fs_h_dst_zero_sumnegative_body_terminal + S (dst_negative_sum_zero_sum) = S ((S (l)) * fs_v_dst_zero_sumnegative)) /\ exists fs_q_dst_zero_sumnegative_body_terminal. fs_u_dst_zero_sumnegative = fs_q_dst_zero_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_zero_sumnegative) + (dst_negative_sum_zero_sum))) /\ forall fs_i_dst_zero_sumnegative_body_steps. (exists fs_lt_dst_zero_sumnegative_body_steps_bound. fs_lt_dst_zero_sumnegative_body_steps_bound + S fs_i_dst_zero_sumnegative_body_steps = l) -> exists fs_a_dst_zero_sumnegative_body_steps fs_r_dst_zero_sumnegative_body_steps fs_s_dst_zero_sumnegative_body_steps. ((((exists fs_h_dst_zero_sumnegative_body_steps_summand. fs_h_dst_zero_sumnegative_body_steps_summand + S (fs_a_dst_zero_sumnegative_body_steps) = S ((S (fs_i_dst_zero_sumnegative_body_steps)) * dst_negative_scale_zero_sum)) /\ exists fs_q_dst_zero_sumnegative_body_steps_summand. dst_negative_code_zero_sum = fs_q_dst_zero_sumnegative_body_steps_summand * S ((S (fs_i_dst_zero_sumnegative_body_steps)) * dst_negative_scale_zero_sum) + (fs_a_dst_zero_sumnegative_body_steps))) /\ ((((exists fs_h_dst_zero_sumnegative_body_steps_partial. fs_h_dst_zero_sumnegative_body_steps_partial + S (fs_r_dst_zero_sumnegative_body_steps) = S ((S (fs_i_dst_zero_sumnegative_body_steps)) * fs_v_dst_zero_sumnegative)) /\ exists fs_q_dst_zero_sumnegative_body_steps_partial. fs_u_dst_zero_sumnegative = fs_q_dst_zero_sumnegative_body_steps_partial * S ((S (fs_i_dst_zero_sumnegative_body_steps)) * fs_v_dst_zero_sumnegative) + (fs_r_dst_zero_sumnegative_body_steps))) /\ ((((exists fs_h_dst_zero_sumnegative_body_steps_successor. fs_h_dst_zero_sumnegative_body_steps_successor + S (fs_s_dst_zero_sumnegative_body_steps) = S ((S (S fs_i_dst_zero_sumnegative_body_steps)) * fs_v_dst_zero_sumnegative)) /\ exists fs_q_dst_zero_sumnegative_body_steps_successor. fs_u_dst_zero_sumnegative = fs_q_dst_zero_sumnegative_body_steps_successor * S ((S (S fs_i_dst_zero_sumnegative_body_steps)) * fs_v_dst_zero_sumnegative) + (fs_s_dst_zero_sumnegative_body_steps))) /\ fs_s_dst_zero_sumnegative_body_steps = fs_r_dst_zero_sumnegative_body_steps + fs_a_dst_zero_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_zero_sumresult ge_balance_negative_zero_sumresult. (((((z) = 2 * (ge_balance_positive_zero_sumresult) /\ (ge_balance_negative_zero_sumresult) = 0) \/ exists ge_signed_half_zero_sumresultdecode. (((z) = 2 * ge_signed_half_zero_sumresultdecode + 1 /\ (ge_balance_positive_zero_sumresult) = 0) /\ (ge_balance_negative_zero_sumresult) = S ge_signed_half_zero_sumresultdecode))) /\ ((dst_positive_sum_zero_sum) + ge_balance_negative_zero_sumresult = (dst_negative_sum_zero_sum) + ge_balance_positive_zero_sumresult))))))))) -> z=0

Complete tactic proof in conservative notation

All 34 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

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

Named ingredients (1)
signed prefix sum zero tail
01Fix variables and assumptionsL1–5

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

  1. L1
    intro F
  2. L2
    intro l
  3. L3
    intro z
  4. L4
    intro hz
  5. L5
    intro hs
02Separate the logical casesL6–14

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

  1. L6
    cases hs
  2. L7
    cases hs_witness
  3. L8
    cases hs_witness_witness
  4. L9
    cases hs_witness_witness_witness
  5. L10
    cases hs_witness_witness_witness_witness
  6. L11
    cases hs_witness_witness_witness_witness_witness
  7. L12
    cases hs_witness_witness_witness_witness_witness_witness
  8. L13
    cases hs_witness_witness_witness_witness_witness_witness_right
  9. L14
    cases hs_witness_witness_witness_witness_witness_witness_right_right
03Establish hzeroL15–24

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

  1. L15
    have hzero : SignedPrefixSum(F,0,0)Definitions: SignedPrefixSum(F,0,0)Original native command in the exact edition
  2. L16
    specialize divisor_signed_sum_empty_exists (F)
  3. L17
    specialize divisor_signed_sum_empty_exists (x)
  4. L18
    specialize divisor_signed_sum_empty_exists (x1)
  5. L19
    specialize divisor_signed_sum_empty_exists (x2)
  6. L20
    specialize divisor_signed_sum_empty_exists (x3)
  7. L21
    apply divisor_signed_sum_empty_exists
  8. L22
    exact hs_witness_witness_witness_witness_witness_witness_left
  9. L23
    symm
  10. L24
    specialize signed_prefix_sum_zero_tail (F)
04Use earlier factsL25–34

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

  1. L25
    specialize signed_prefix_sum_zero_tail (0)
  2. L26
    specialize signed_prefix_sum_zero_tail (l)
  3. L27
    specialize signed_prefix_sum_zero_tail (0)
  4. L28
    specialize signed_prefix_sum_zero_tail (z)
  5. L29
    apply signed_prefix_sum_zero_tail
  6. L30
    specialize zero_le (l)
  7. L31
    apply zero_le
  8. L32
    exact hz
  9. L33
    exact hzero
  10. L34
    exact hs

Library-wide reading audit

Original defined command ledger · 34 lines
  1. 0001intro F
  2. 0002intro l
  3. 0003intro z
  4. 0004intro hz
  5. 0005intro hs
  6. 0006cases hs
  7. 0007cases hs_witness
  8. 0008cases hs_witness_witness
  9. 0009cases hs_witness_witness_witness
  10. 0010cases hs_witness_witness_witness_witness
  11. 0011cases hs_witness_witness_witness_witness_witness
  12. 0012cases hs_witness_witness_witness_witness_witness_witness
  13. 0013cases hs_witness_witness_witness_witness_witness_witness_right
  14. 0014cases hs_witness_witness_witness_witness_witness_witness_right_right
  15. 0015have hzero : SignedPrefixSum(F,0,0)
  16. 0016specialize divisor_signed_sum_empty_exists (F)
  17. 0017specialize divisor_signed_sum_empty_exists (x)
  18. 0018specialize divisor_signed_sum_empty_exists (x1)
  19. 0019specialize divisor_signed_sum_empty_exists (x2)
  20. 0020specialize divisor_signed_sum_empty_exists (x3)
  21. 0021apply divisor_signed_sum_empty_exists
  22. 0022exact hs_witness_witness_witness_witness_witness_witness_left
  23. 0023symm
  24. 0024specialize signed_prefix_sum_zero_tail (F)
  25. 0025specialize signed_prefix_sum_zero_tail (0)
  26. 0026specialize signed_prefix_sum_zero_tail (l)
  27. 0027specialize signed_prefix_sum_zero_tail (0)
  28. 0028specialize signed_prefix_sum_zero_tail (z)
  29. 0029apply signed_prefix_sum_zero_tail
  30. 0030specialize zero_le (l)
  31. 0031apply zero_le
  32. 0032exact hz
  33. 0033exact hzero
  34. 0034exact hs