ZS0006

signed_prefix_sum_zero_exists

Construct the actual sum of a valid all-zero prefix and prove its value, without postulating a sum oracle.

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

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

Definition DAG

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

Actual proof prerequisites

arithmetic_signed_sum_exists · checked external prerequisitesigned_prefix_sum_zero_value
Original expanded first-order statement 
forall F l. (exists dst_positive_code_zero_source dst_positive_scale_zero_source dst_negative_code_zero_source dst_negative_scale_zero_source. (((F) = (((((dst_positive_code_zero_source) + (dst_positive_scale_zero_source)) * S ((dst_positive_code_zero_source) + (dst_positive_scale_zero_source)) + ((dst_positive_scale_zero_source) + (dst_positive_scale_zero_source))) + (((dst_negative_code_zero_source) + (dst_negative_scale_zero_source)) * S ((dst_negative_code_zero_source) + (dst_negative_scale_zero_source)) + ((dst_negative_scale_zero_source) + (dst_negative_scale_zero_source)))) * S ((((dst_positive_code_zero_source) + (dst_positive_scale_zero_source)) * S ((dst_positive_code_zero_source) + (dst_positive_scale_zero_source)) + ((dst_positive_scale_zero_source) + (dst_positive_scale_zero_source))) + (((dst_negative_code_zero_source) + (dst_negative_scale_zero_source)) * S ((dst_negative_code_zero_source) + (dst_negative_scale_zero_source)) + ((dst_negative_scale_zero_source) + (dst_negative_scale_zero_source)))) + ((((dst_negative_code_zero_source) + (dst_negative_scale_zero_source)) * S ((dst_negative_code_zero_source) + (dst_negative_scale_zero_source)) + ((dst_negative_scale_zero_source) + (dst_negative_scale_zero_source))) + (((dst_negative_code_zero_source) + (dst_negative_scale_zero_source)) * S ((dst_negative_code_zero_source) + (dst_negative_scale_zero_source)) + ((dst_negative_scale_zero_source) + (dst_negative_scale_zero_source)))))) /\ (forall dst_index_zero_source. (exists pvs_le_gap_zero_sourcedomain. pvs_le_gap_zero_sourcedomain + (dst_index_zero_source) = (0)) -> exists dst_positive_zero_source dst_negative_zero_source dst_value_zero_source. ((((exists ff_h_pvs_zero_sourceentrypositive. ff_h_pvs_zero_sourceentrypositive + S (dst_positive_zero_source) = S ((S (dst_index_zero_source)) * dst_positive_scale_zero_source)) /\ exists ff_q_pvs_zero_sourceentrypositive. dst_positive_code_zero_source = ff_q_pvs_zero_sourceentrypositive * S ((S (dst_index_zero_source)) * dst_positive_scale_zero_source) + (dst_positive_zero_source))) /\ (((((exists ff_h_pvs_zero_sourceentrynegative. ff_h_pvs_zero_sourceentrynegative + S (dst_negative_zero_source) = S ((S (dst_index_zero_source)) * dst_negative_scale_zero_source)) /\ exists ff_q_pvs_zero_sourceentrynegative. dst_negative_code_zero_source = ff_q_pvs_zero_sourceentrynegative * S ((S (dst_index_zero_source)) * dst_negative_scale_zero_source) + (dst_negative_zero_source))) /\ (exists ge_balance_positive_zero_sourceentryvalue ge_balance_negative_zero_sourceentryvalue. (((((dst_value_zero_source) = 2 * (ge_balance_positive_zero_sourceentryvalue) /\ (ge_balance_negative_zero_sourceentryvalue) = 0) \/ exists ge_signed_half_zero_sourceentryvaluedecode. (((dst_value_zero_source) = 2 * ge_signed_half_zero_sourceentryvaluedecode + 1 /\ (ge_balance_positive_zero_sourceentryvalue) = 0) /\ (ge_balance_negative_zero_sourceentryvalue) = S ge_signed_half_zero_sourceentryvaluedecode))) /\ ((dst_positive_zero_source) + ge_balance_negative_zero_sourceentryvalue = (dst_negative_zero_source) + ge_balance_positive_zero_sourceentryvalue))))))))) -> (forall sfs_index_zero_window sfs_value_zero_window. (exists pvs_le_gap_zero_windowlower. pvs_le_gap_zero_windowlower + (0) = (sfs_index_zero_window)) -> (exists pvs_gap_zero_windowupper. pvs_gap_zero_windowupper + S (sfs_index_zero_window) = (l)) -> (exists dst_positive_code_zero_windowentry dst_positive_scale_zero_windowentry dst_negative_code_zero_windowentry dst_negative_scale_zero_windowentry dst_positive_zero_windowentry dst_negative_zero_windowentry. (((F) = (((((dst_positive_code_zero_windowentry) + (dst_positive_scale_zero_windowentry)) * S ((dst_positive_code_zero_windowentry) + (dst_positive_scale_zero_windowentry)) + ((dst_positive_scale_zero_windowentry) + (dst_positive_scale_zero_windowentry))) + (((dst_negative_code_zero_windowentry) + (dst_negative_scale_zero_windowentry)) * S ((dst_negative_code_zero_windowentry) + (dst_negative_scale_zero_windowentry)) + ((dst_negative_scale_zero_windowentry) + (dst_negative_scale_zero_windowentry)))) * S ((((dst_positive_code_zero_windowentry) + (dst_positive_scale_zero_windowentry)) * S ((dst_positive_code_zero_windowentry) + (dst_positive_scale_zero_windowentry)) + ((dst_positive_scale_zero_windowentry) + (dst_positive_scale_zero_windowentry))) + (((dst_negative_code_zero_windowentry) + (dst_negative_scale_zero_windowentry)) * S ((dst_negative_code_zero_windowentry) + (dst_negative_scale_zero_windowentry)) + ((dst_negative_scale_zero_windowentry) + (dst_negative_scale_zero_windowentry)))) + ((((dst_negative_code_zero_windowentry) + (dst_negative_scale_zero_windowentry)) * S ((dst_negative_code_zero_windowentry) + (dst_negative_scale_zero_windowentry)) + ((dst_negative_scale_zero_windowentry) + (dst_negative_scale_zero_windowentry))) + (((dst_negative_code_zero_windowentry) + (dst_negative_scale_zero_windowentry)) * S ((dst_negative_code_zero_windowentry) + (dst_negative_scale_zero_windowentry)) + ((dst_negative_scale_zero_windowentry) + (dst_negative_scale_zero_windowentry)))))) /\ (((((exists ff_h_pvs_zero_windowentrypositive. ff_h_pvs_zero_windowentrypositive + S (dst_positive_zero_windowentry) = S ((S (sfs_index_zero_window)) * dst_positive_scale_zero_windowentry)) /\ exists ff_q_pvs_zero_windowentrypositive. dst_positive_code_zero_windowentry = ff_q_pvs_zero_windowentrypositive * S ((S (sfs_index_zero_window)) * dst_positive_scale_zero_windowentry) + (dst_positive_zero_windowentry))) /\ (((((exists ff_h_pvs_zero_windowentrynegative. ff_h_pvs_zero_windowentrynegative + S (dst_negative_zero_windowentry) = S ((S (sfs_index_zero_window)) * dst_negative_scale_zero_windowentry)) /\ exists ff_q_pvs_zero_windowentrynegative. dst_negative_code_zero_windowentry = ff_q_pvs_zero_windowentrynegative * S ((S (sfs_index_zero_window)) * dst_negative_scale_zero_windowentry) + (dst_negative_zero_windowentry))) /\ (exists ge_balance_positive_zero_windowentryvalue ge_balance_negative_zero_windowentryvalue. (((((sfs_value_zero_window) = 2 * (ge_balance_positive_zero_windowentryvalue) /\ (ge_balance_negative_zero_windowentryvalue) = 0) \/ exists ge_signed_half_zero_windowentryvaluedecode. (((sfs_value_zero_window) = 2 * ge_signed_half_zero_windowentryvaluedecode + 1 /\ (ge_balance_positive_zero_windowentryvalue) = 0) /\ (ge_balance_negative_zero_windowentryvalue) = S ge_signed_half_zero_windowentryvaluedecode))) /\ ((dst_positive_zero_windowentry) + ge_balance_negative_zero_windowentryvalue = (dst_negative_zero_windowentry) + ge_balance_positive_zero_windowentryvalue))))))))) -> sfs_value_zero_window=0) -> (exists dst_positive_code_zero_result dst_positive_scale_zero_result dst_negative_code_zero_result dst_negative_scale_zero_result dst_positive_sum_zero_result dst_negative_sum_zero_result. (((F) = (((((dst_positive_code_zero_result) + (dst_positive_scale_zero_result)) * S ((dst_positive_code_zero_result) + (dst_positive_scale_zero_result)) + ((dst_positive_scale_zero_result) + (dst_positive_scale_zero_result))) + (((dst_negative_code_zero_result) + (dst_negative_scale_zero_result)) * S ((dst_negative_code_zero_result) + (dst_negative_scale_zero_result)) + ((dst_negative_scale_zero_result) + (dst_negative_scale_zero_result)))) * S ((((dst_positive_code_zero_result) + (dst_positive_scale_zero_result)) * S ((dst_positive_code_zero_result) + (dst_positive_scale_zero_result)) + ((dst_positive_scale_zero_result) + (dst_positive_scale_zero_result))) + (((dst_negative_code_zero_result) + (dst_negative_scale_zero_result)) * S ((dst_negative_code_zero_result) + (dst_negative_scale_zero_result)) + ((dst_negative_scale_zero_result) + (dst_negative_scale_zero_result)))) + ((((dst_negative_code_zero_result) + (dst_negative_scale_zero_result)) * S ((dst_negative_code_zero_result) + (dst_negative_scale_zero_result)) + ((dst_negative_scale_zero_result) + (dst_negative_scale_zero_result))) + (((dst_negative_code_zero_result) + (dst_negative_scale_zero_result)) * S ((dst_negative_code_zero_result) + (dst_negative_scale_zero_result)) + ((dst_negative_scale_zero_result) + (dst_negative_scale_zero_result)))))) /\ (((exists fs_u_dst_zero_resultpositive fs_v_dst_zero_resultpositive. ((((exists fs_h_dst_zero_resultpositive_body_start. fs_h_dst_zero_resultpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_resultpositive)) /\ exists fs_q_dst_zero_resultpositive_body_start. fs_u_dst_zero_resultpositive = fs_q_dst_zero_resultpositive_body_start * S ((S (0)) * fs_v_dst_zero_resultpositive) + (0))) /\ ((((exists fs_h_dst_zero_resultpositive_body_terminal. fs_h_dst_zero_resultpositive_body_terminal + S (dst_positive_sum_zero_result) = S ((S (l)) * fs_v_dst_zero_resultpositive)) /\ exists fs_q_dst_zero_resultpositive_body_terminal. fs_u_dst_zero_resultpositive = fs_q_dst_zero_resultpositive_body_terminal * S ((S (l)) * fs_v_dst_zero_resultpositive) + (dst_positive_sum_zero_result))) /\ forall fs_i_dst_zero_resultpositive_body_steps. (exists fs_lt_dst_zero_resultpositive_body_steps_bound. fs_lt_dst_zero_resultpositive_body_steps_bound + S fs_i_dst_zero_resultpositive_body_steps = l) -> exists fs_a_dst_zero_resultpositive_body_steps fs_r_dst_zero_resultpositive_body_steps fs_s_dst_zero_resultpositive_body_steps. ((((exists fs_h_dst_zero_resultpositive_body_steps_summand. fs_h_dst_zero_resultpositive_body_steps_summand + S (fs_a_dst_zero_resultpositive_body_steps) = S ((S (fs_i_dst_zero_resultpositive_body_steps)) * dst_positive_scale_zero_result)) /\ exists fs_q_dst_zero_resultpositive_body_steps_summand. dst_positive_code_zero_result = fs_q_dst_zero_resultpositive_body_steps_summand * S ((S (fs_i_dst_zero_resultpositive_body_steps)) * dst_positive_scale_zero_result) + (fs_a_dst_zero_resultpositive_body_steps))) /\ ((((exists fs_h_dst_zero_resultpositive_body_steps_partial. fs_h_dst_zero_resultpositive_body_steps_partial + S (fs_r_dst_zero_resultpositive_body_steps) = S ((S (fs_i_dst_zero_resultpositive_body_steps)) * fs_v_dst_zero_resultpositive)) /\ exists fs_q_dst_zero_resultpositive_body_steps_partial. fs_u_dst_zero_resultpositive = fs_q_dst_zero_resultpositive_body_steps_partial * S ((S (fs_i_dst_zero_resultpositive_body_steps)) * fs_v_dst_zero_resultpositive) + (fs_r_dst_zero_resultpositive_body_steps))) /\ ((((exists fs_h_dst_zero_resultpositive_body_steps_successor. fs_h_dst_zero_resultpositive_body_steps_successor + S (fs_s_dst_zero_resultpositive_body_steps) = S ((S (S fs_i_dst_zero_resultpositive_body_steps)) * fs_v_dst_zero_resultpositive)) /\ exists fs_q_dst_zero_resultpositive_body_steps_successor. fs_u_dst_zero_resultpositive = fs_q_dst_zero_resultpositive_body_steps_successor * S ((S (S fs_i_dst_zero_resultpositive_body_steps)) * fs_v_dst_zero_resultpositive) + (fs_s_dst_zero_resultpositive_body_steps))) /\ fs_s_dst_zero_resultpositive_body_steps = fs_r_dst_zero_resultpositive_body_steps + fs_a_dst_zero_resultpositive_body_steps)))))) /\ (((exists fs_u_dst_zero_resultnegative fs_v_dst_zero_resultnegative. ((((exists fs_h_dst_zero_resultnegative_body_start. fs_h_dst_zero_resultnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_zero_resultnegative)) /\ exists fs_q_dst_zero_resultnegative_body_start. fs_u_dst_zero_resultnegative = fs_q_dst_zero_resultnegative_body_start * S ((S (0)) * fs_v_dst_zero_resultnegative) + (0))) /\ ((((exists fs_h_dst_zero_resultnegative_body_terminal. fs_h_dst_zero_resultnegative_body_terminal + S (dst_negative_sum_zero_result) = S ((S (l)) * fs_v_dst_zero_resultnegative)) /\ exists fs_q_dst_zero_resultnegative_body_terminal. fs_u_dst_zero_resultnegative = fs_q_dst_zero_resultnegative_body_terminal * S ((S (l)) * fs_v_dst_zero_resultnegative) + (dst_negative_sum_zero_result))) /\ forall fs_i_dst_zero_resultnegative_body_steps. (exists fs_lt_dst_zero_resultnegative_body_steps_bound. fs_lt_dst_zero_resultnegative_body_steps_bound + S fs_i_dst_zero_resultnegative_body_steps = l) -> exists fs_a_dst_zero_resultnegative_body_steps fs_r_dst_zero_resultnegative_body_steps fs_s_dst_zero_resultnegative_body_steps. ((((exists fs_h_dst_zero_resultnegative_body_steps_summand. fs_h_dst_zero_resultnegative_body_steps_summand + S (fs_a_dst_zero_resultnegative_body_steps) = S ((S (fs_i_dst_zero_resultnegative_body_steps)) * dst_negative_scale_zero_result)) /\ exists fs_q_dst_zero_resultnegative_body_steps_summand. dst_negative_code_zero_result = fs_q_dst_zero_resultnegative_body_steps_summand * S ((S (fs_i_dst_zero_resultnegative_body_steps)) * dst_negative_scale_zero_result) + (fs_a_dst_zero_resultnegative_body_steps))) /\ ((((exists fs_h_dst_zero_resultnegative_body_steps_partial. fs_h_dst_zero_resultnegative_body_steps_partial + S (fs_r_dst_zero_resultnegative_body_steps) = S ((S (fs_i_dst_zero_resultnegative_body_steps)) * fs_v_dst_zero_resultnegative)) /\ exists fs_q_dst_zero_resultnegative_body_steps_partial. fs_u_dst_zero_resultnegative = fs_q_dst_zero_resultnegative_body_steps_partial * S ((S (fs_i_dst_zero_resultnegative_body_steps)) * fs_v_dst_zero_resultnegative) + (fs_r_dst_zero_resultnegative_body_steps))) /\ ((((exists fs_h_dst_zero_resultnegative_body_steps_successor. fs_h_dst_zero_resultnegative_body_steps_successor + S (fs_s_dst_zero_resultnegative_body_steps) = S ((S (S fs_i_dst_zero_resultnegative_body_steps)) * fs_v_dst_zero_resultnegative)) /\ exists fs_q_dst_zero_resultnegative_body_steps_successor. fs_u_dst_zero_resultnegative = fs_q_dst_zero_resultnegative_body_steps_successor * S ((S (S fs_i_dst_zero_resultnegative_body_steps)) * fs_v_dst_zero_resultnegative) + (fs_s_dst_zero_resultnegative_body_steps))) /\ fs_s_dst_zero_resultnegative_body_steps = fs_r_dst_zero_resultnegative_body_steps + fs_a_dst_zero_resultnegative_body_steps)))))) /\ (exists ge_balance_positive_zero_resultresult ge_balance_negative_zero_resultresult. (((((0) = 2 * (ge_balance_positive_zero_resultresult) /\ (ge_balance_negative_zero_resultresult) = 0) \/ exists ge_signed_half_zero_resultresultdecode. (((0) = 2 * ge_signed_half_zero_resultresultdecode + 1 /\ (ge_balance_positive_zero_resultresult) = 0) /\ (ge_balance_negative_zero_resultresult) = S ge_signed_half_zero_resultresultdecode))) /\ ((dst_positive_sum_zero_result) + ge_balance_negative_zero_resultresult = (dst_negative_sum_zero_result) + ge_balance_positive_zero_resultresult)))))))))

Complete tactic proof in conservative notation

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

21 script commands · 4 reading checkpoints · 2 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–4

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

  1. L1
    intro F
  2. L2
    intro l
  3. L3
    intro hF
  4. L4
    intro hz
02Establish hsL5–10

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

  1. L5
    have hs : ∃ z. SignedPrefixSum(F,l,z)Definitions: SignedPrefixSum(F,l,z)Original native command in the exact edition
  2. L6
    specialize arithmetic_signed_sum_exists (0)
  3. L7
    specialize arithmetic_signed_sum_exists (F)
  4. L8
    specialize arithmetic_signed_sum_exists (l)
  5. L9
    apply arithmetic_signed_sum_exists
  6. L10
    exact hF
03Separate the logical casesL11–11

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

  1. L11
    cases hs
04Establish hvL12–21

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

  1. L12
    have hv : x=0
  2. L13
    specialize signed_prefix_sum_zero_value (F)
  3. L14
    specialize signed_prefix_sum_zero_value (l)
  4. L15
    specialize signed_prefix_sum_zero_value (x)
  5. L16
    apply signed_prefix_sum_zero_value
  6. L17
    exact hz
  7. L18
    exact hs_witness
  8. L19
    rewrite hv at hs_witness
  9. L20
    rewrite hv at hs_witness
  10. L21
    exact hs_witness

Library-wide reading audit

Original defined command ledger · 21 lines
  1. 0001intro F
  2. 0002intro l
  3. 0003intro hF
  4. 0004intro hz
  5. 0005have hs : ∃ z. SignedPrefixSum(F,l,z)
  6. 0006specialize arithmetic_signed_sum_exists (0)
  7. 0007specialize arithmetic_signed_sum_exists (F)
  8. 0008specialize arithmetic_signed_sum_exists (l)
  9. 0009apply arithmetic_signed_sum_exists
  10. 0010exact hF
  11. 0011cases hs
  12. 0012have hv : x=0
  13. 0013specialize signed_prefix_sum_zero_value (F)
  14. 0014specialize signed_prefix_sum_zero_value (l)
  15. 0015specialize signed_prefix_sum_zero_value (x)
  16. 0016apply signed_prefix_sum_zero_value
  17. 0017exact hz
  18. 0018exact hs_witness
  19. 0019rewrite hv at hs_witness
  20. 0020rewrite hv at hs_witness
  21. 0021exact hs_witness