SS000D

divisor_signed_sum_empty_value

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

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

Public research checkpoint: original HA and independently compiled Lean verified; not Alpha-enrolled, no Alpha checked-use authority; not Stable

These are genuine signed-table and finite-sum foundations, not full divisor-sum cancellation or Möbius inversion. G007 remains open. The historical MatrixMinorFourCode definition is reused solely as generic nested pairing of four beta parameters; no matrix-specific hypothesis is imported. Equality is equality of represented signed values, not equality of arbitrary component codes.

Exact theorem in conservative defined notation

∀ F. ∀ z. SignedPrefixSum(F,0,z) → z = 0

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

Definition DAG

SignedPrefixSum(F,l,z) · 1

Actual proof prerequisites

beta_sum_zero · checked external prerequisitesigned_balance_zero_iff · checked external prerequisite
Original expanded first-order 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

Complete tactic proof in conservative notation

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

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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