ZS0004

signed_prefix_sum_zero_tail

Ordinary finite induction proves that a genuinely zero tail changes no actual canonical signed prefix sum.

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. ∀ k. ∀ l. ∀ a. ∀ b. Le(k,l) → SignedZeroWindow(F,k,l) → SignedPrefixSum(F,k,a) → SignedPrefixSum(F,l,b) → a = b

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

Definition DAG

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

Actual proof prerequisites

le_zero · checked external prerequisitedivisor_signed_sum_functional · checked external prerequisitele_eq_or_lt · checked external prerequisitele_of_succ_le_succ · checked external prerequisitedivisor_signed_sum_successor_decompose · checked external prerequisitesigned_zero_window_restrictle_succ_self · checked external prerequisitele_refl · checked external prerequisitesigned_add_functional · checked external prerequisitesigned_add_zero_right · checked external prerequisite
Original expanded first-order statement 
forall F k l a b. (exists pvs_le_gap_tail_order. pvs_le_gap_tail_order + (k) = (l)) -> (forall sfs_index_tail_window sfs_value_tail_window. (exists pvs_le_gap_tail_windowlower. pvs_le_gap_tail_windowlower + (k) = (sfs_index_tail_window)) -> (exists pvs_gap_tail_windowupper. pvs_gap_tail_windowupper + S (sfs_index_tail_window) = (l)) -> (exists dst_positive_code_tail_windowentry dst_positive_scale_tail_windowentry dst_negative_code_tail_windowentry dst_negative_scale_tail_windowentry dst_positive_tail_windowentry dst_negative_tail_windowentry. (((F) = (((((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) * S ((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) + ((dst_positive_scale_tail_windowentry) + (dst_positive_scale_tail_windowentry))) + (((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry)))) * S ((((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) * S ((dst_positive_code_tail_windowentry) + (dst_positive_scale_tail_windowentry)) + ((dst_positive_scale_tail_windowentry) + (dst_positive_scale_tail_windowentry))) + (((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry)))) + ((((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry))) + (((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) * S ((dst_negative_code_tail_windowentry) + (dst_negative_scale_tail_windowentry)) + ((dst_negative_scale_tail_windowentry) + (dst_negative_scale_tail_windowentry)))))) /\ (((((exists ff_h_pvs_tail_windowentrypositive. ff_h_pvs_tail_windowentrypositive + S (dst_positive_tail_windowentry) = S ((S (sfs_index_tail_window)) * dst_positive_scale_tail_windowentry)) /\ exists ff_q_pvs_tail_windowentrypositive. dst_positive_code_tail_windowentry = ff_q_pvs_tail_windowentrypositive * S ((S (sfs_index_tail_window)) * dst_positive_scale_tail_windowentry) + (dst_positive_tail_windowentry))) /\ (((((exists ff_h_pvs_tail_windowentrynegative. ff_h_pvs_tail_windowentrynegative + S (dst_negative_tail_windowentry) = S ((S (sfs_index_tail_window)) * dst_negative_scale_tail_windowentry)) /\ exists ff_q_pvs_tail_windowentrynegative. dst_negative_code_tail_windowentry = ff_q_pvs_tail_windowentrynegative * S ((S (sfs_index_tail_window)) * dst_negative_scale_tail_windowentry) + (dst_negative_tail_windowentry))) /\ (exists ge_balance_positive_tail_windowentryvalue ge_balance_negative_tail_windowentryvalue. (((((sfs_value_tail_window) = 2 * (ge_balance_positive_tail_windowentryvalue) /\ (ge_balance_negative_tail_windowentryvalue) = 0) \/ exists ge_signed_half_tail_windowentryvaluedecode. (((sfs_value_tail_window) = 2 * ge_signed_half_tail_windowentryvaluedecode + 1 /\ (ge_balance_positive_tail_windowentryvalue) = 0) /\ (ge_balance_negative_tail_windowentryvalue) = S ge_signed_half_tail_windowentryvaluedecode))) /\ ((dst_positive_tail_windowentry) + ge_balance_negative_tail_windowentryvalue = (dst_negative_tail_windowentry) + ge_balance_positive_tail_windowentryvalue))))))))) -> sfs_value_tail_window=0) -> (exists dst_positive_code_tail_short dst_positive_scale_tail_short dst_negative_code_tail_short dst_negative_scale_tail_short dst_positive_sum_tail_short dst_negative_sum_tail_short. (((F) = (((((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) * S ((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) + ((dst_positive_scale_tail_short) + (dst_positive_scale_tail_short))) + (((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short)))) * S ((((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) * S ((dst_positive_code_tail_short) + (dst_positive_scale_tail_short)) + ((dst_positive_scale_tail_short) + (dst_positive_scale_tail_short))) + (((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short)))) + ((((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short))) + (((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) * S ((dst_negative_code_tail_short) + (dst_negative_scale_tail_short)) + ((dst_negative_scale_tail_short) + (dst_negative_scale_tail_short)))))) /\ (((exists fs_u_dst_tail_shortpositive fs_v_dst_tail_shortpositive. ((((exists fs_h_dst_tail_shortpositive_body_start. fs_h_dst_tail_shortpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_start. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_start * S ((S (0)) * fs_v_dst_tail_shortpositive) + (0))) /\ ((((exists fs_h_dst_tail_shortpositive_body_terminal. fs_h_dst_tail_shortpositive_body_terminal + S (dst_positive_sum_tail_short) = S ((S (k)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_terminal. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_terminal * S ((S (k)) * fs_v_dst_tail_shortpositive) + (dst_positive_sum_tail_short))) /\ forall fs_i_dst_tail_shortpositive_body_steps. (exists fs_lt_dst_tail_shortpositive_body_steps_bound. fs_lt_dst_tail_shortpositive_body_steps_bound + S fs_i_dst_tail_shortpositive_body_steps = k) -> exists fs_a_dst_tail_shortpositive_body_steps fs_r_dst_tail_shortpositive_body_steps fs_s_dst_tail_shortpositive_body_steps. ((((exists fs_h_dst_tail_shortpositive_body_steps_summand. fs_h_dst_tail_shortpositive_body_steps_summand + S (fs_a_dst_tail_shortpositive_body_steps) = S ((S (fs_i_dst_tail_shortpositive_body_steps)) * dst_positive_scale_tail_short)) /\ exists fs_q_dst_tail_shortpositive_body_steps_summand. dst_positive_code_tail_short = fs_q_dst_tail_shortpositive_body_steps_summand * S ((S (fs_i_dst_tail_shortpositive_body_steps)) * dst_positive_scale_tail_short) + (fs_a_dst_tail_shortpositive_body_steps))) /\ ((((exists fs_h_dst_tail_shortpositive_body_steps_partial. fs_h_dst_tail_shortpositive_body_steps_partial + S (fs_r_dst_tail_shortpositive_body_steps) = S ((S (fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_steps_partial. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_steps_partial * S ((S (fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive) + (fs_r_dst_tail_shortpositive_body_steps))) /\ ((((exists fs_h_dst_tail_shortpositive_body_steps_successor. fs_h_dst_tail_shortpositive_body_steps_successor + S (fs_s_dst_tail_shortpositive_body_steps) = S ((S (S fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive)) /\ exists fs_q_dst_tail_shortpositive_body_steps_successor. fs_u_dst_tail_shortpositive = fs_q_dst_tail_shortpositive_body_steps_successor * S ((S (S fs_i_dst_tail_shortpositive_body_steps)) * fs_v_dst_tail_shortpositive) + (fs_s_dst_tail_shortpositive_body_steps))) /\ fs_s_dst_tail_shortpositive_body_steps = fs_r_dst_tail_shortpositive_body_steps + fs_a_dst_tail_shortpositive_body_steps)))))) /\ (((exists fs_u_dst_tail_shortnegative fs_v_dst_tail_shortnegative. ((((exists fs_h_dst_tail_shortnegative_body_start. fs_h_dst_tail_shortnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_start. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_start * S ((S (0)) * fs_v_dst_tail_shortnegative) + (0))) /\ ((((exists fs_h_dst_tail_shortnegative_body_terminal. fs_h_dst_tail_shortnegative_body_terminal + S (dst_negative_sum_tail_short) = S ((S (k)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_terminal. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_terminal * S ((S (k)) * fs_v_dst_tail_shortnegative) + (dst_negative_sum_tail_short))) /\ forall fs_i_dst_tail_shortnegative_body_steps. (exists fs_lt_dst_tail_shortnegative_body_steps_bound. fs_lt_dst_tail_shortnegative_body_steps_bound + S fs_i_dst_tail_shortnegative_body_steps = k) -> exists fs_a_dst_tail_shortnegative_body_steps fs_r_dst_tail_shortnegative_body_steps fs_s_dst_tail_shortnegative_body_steps. ((((exists fs_h_dst_tail_shortnegative_body_steps_summand. fs_h_dst_tail_shortnegative_body_steps_summand + S (fs_a_dst_tail_shortnegative_body_steps) = S ((S (fs_i_dst_tail_shortnegative_body_steps)) * dst_negative_scale_tail_short)) /\ exists fs_q_dst_tail_shortnegative_body_steps_summand. dst_negative_code_tail_short = fs_q_dst_tail_shortnegative_body_steps_summand * S ((S (fs_i_dst_tail_shortnegative_body_steps)) * dst_negative_scale_tail_short) + (fs_a_dst_tail_shortnegative_body_steps))) /\ ((((exists fs_h_dst_tail_shortnegative_body_steps_partial. fs_h_dst_tail_shortnegative_body_steps_partial + S (fs_r_dst_tail_shortnegative_body_steps) = S ((S (fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_steps_partial. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_steps_partial * S ((S (fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative) + (fs_r_dst_tail_shortnegative_body_steps))) /\ ((((exists fs_h_dst_tail_shortnegative_body_steps_successor. fs_h_dst_tail_shortnegative_body_steps_successor + S (fs_s_dst_tail_shortnegative_body_steps) = S ((S (S fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative)) /\ exists fs_q_dst_tail_shortnegative_body_steps_successor. fs_u_dst_tail_shortnegative = fs_q_dst_tail_shortnegative_body_steps_successor * S ((S (S fs_i_dst_tail_shortnegative_body_steps)) * fs_v_dst_tail_shortnegative) + (fs_s_dst_tail_shortnegative_body_steps))) /\ fs_s_dst_tail_shortnegative_body_steps = fs_r_dst_tail_shortnegative_body_steps + fs_a_dst_tail_shortnegative_body_steps)))))) /\ (exists ge_balance_positive_tail_shortresult ge_balance_negative_tail_shortresult. (((((a) = 2 * (ge_balance_positive_tail_shortresult) /\ (ge_balance_negative_tail_shortresult) = 0) \/ exists ge_signed_half_tail_shortresultdecode. (((a) = 2 * ge_signed_half_tail_shortresultdecode + 1 /\ (ge_balance_positive_tail_shortresult) = 0) /\ (ge_balance_negative_tail_shortresult) = S ge_signed_half_tail_shortresultdecode))) /\ ((dst_positive_sum_tail_short) + ge_balance_negative_tail_shortresult = (dst_negative_sum_tail_short) + ge_balance_positive_tail_shortresult))))))))) -> (exists dst_positive_code_tail_long dst_positive_scale_tail_long dst_negative_code_tail_long dst_negative_scale_tail_long dst_positive_sum_tail_long dst_negative_sum_tail_long. (((F) = (((((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) * S ((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) + ((dst_positive_scale_tail_long) + (dst_positive_scale_tail_long))) + (((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long)))) * S ((((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) * S ((dst_positive_code_tail_long) + (dst_positive_scale_tail_long)) + ((dst_positive_scale_tail_long) + (dst_positive_scale_tail_long))) + (((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long)))) + ((((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long))) + (((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) * S ((dst_negative_code_tail_long) + (dst_negative_scale_tail_long)) + ((dst_negative_scale_tail_long) + (dst_negative_scale_tail_long)))))) /\ (((exists fs_u_dst_tail_longpositive fs_v_dst_tail_longpositive. ((((exists fs_h_dst_tail_longpositive_body_start. fs_h_dst_tail_longpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_start. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_start * S ((S (0)) * fs_v_dst_tail_longpositive) + (0))) /\ ((((exists fs_h_dst_tail_longpositive_body_terminal. fs_h_dst_tail_longpositive_body_terminal + S (dst_positive_sum_tail_long) = S ((S (l)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_terminal. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_terminal * S ((S (l)) * fs_v_dst_tail_longpositive) + (dst_positive_sum_tail_long))) /\ forall fs_i_dst_tail_longpositive_body_steps. (exists fs_lt_dst_tail_longpositive_body_steps_bound. fs_lt_dst_tail_longpositive_body_steps_bound + S fs_i_dst_tail_longpositive_body_steps = l) -> exists fs_a_dst_tail_longpositive_body_steps fs_r_dst_tail_longpositive_body_steps fs_s_dst_tail_longpositive_body_steps. ((((exists fs_h_dst_tail_longpositive_body_steps_summand. fs_h_dst_tail_longpositive_body_steps_summand + S (fs_a_dst_tail_longpositive_body_steps) = S ((S (fs_i_dst_tail_longpositive_body_steps)) * dst_positive_scale_tail_long)) /\ exists fs_q_dst_tail_longpositive_body_steps_summand. dst_positive_code_tail_long = fs_q_dst_tail_longpositive_body_steps_summand * S ((S (fs_i_dst_tail_longpositive_body_steps)) * dst_positive_scale_tail_long) + (fs_a_dst_tail_longpositive_body_steps))) /\ ((((exists fs_h_dst_tail_longpositive_body_steps_partial. fs_h_dst_tail_longpositive_body_steps_partial + S (fs_r_dst_tail_longpositive_body_steps) = S ((S (fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_steps_partial. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_steps_partial * S ((S (fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive) + (fs_r_dst_tail_longpositive_body_steps))) /\ ((((exists fs_h_dst_tail_longpositive_body_steps_successor. fs_h_dst_tail_longpositive_body_steps_successor + S (fs_s_dst_tail_longpositive_body_steps) = S ((S (S fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive)) /\ exists fs_q_dst_tail_longpositive_body_steps_successor. fs_u_dst_tail_longpositive = fs_q_dst_tail_longpositive_body_steps_successor * S ((S (S fs_i_dst_tail_longpositive_body_steps)) * fs_v_dst_tail_longpositive) + (fs_s_dst_tail_longpositive_body_steps))) /\ fs_s_dst_tail_longpositive_body_steps = fs_r_dst_tail_longpositive_body_steps + fs_a_dst_tail_longpositive_body_steps)))))) /\ (((exists fs_u_dst_tail_longnegative fs_v_dst_tail_longnegative. ((((exists fs_h_dst_tail_longnegative_body_start. fs_h_dst_tail_longnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_start. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_start * S ((S (0)) * fs_v_dst_tail_longnegative) + (0))) /\ ((((exists fs_h_dst_tail_longnegative_body_terminal. fs_h_dst_tail_longnegative_body_terminal + S (dst_negative_sum_tail_long) = S ((S (l)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_terminal. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_terminal * S ((S (l)) * fs_v_dst_tail_longnegative) + (dst_negative_sum_tail_long))) /\ forall fs_i_dst_tail_longnegative_body_steps. (exists fs_lt_dst_tail_longnegative_body_steps_bound. fs_lt_dst_tail_longnegative_body_steps_bound + S fs_i_dst_tail_longnegative_body_steps = l) -> exists fs_a_dst_tail_longnegative_body_steps fs_r_dst_tail_longnegative_body_steps fs_s_dst_tail_longnegative_body_steps. ((((exists fs_h_dst_tail_longnegative_body_steps_summand. fs_h_dst_tail_longnegative_body_steps_summand + S (fs_a_dst_tail_longnegative_body_steps) = S ((S (fs_i_dst_tail_longnegative_body_steps)) * dst_negative_scale_tail_long)) /\ exists fs_q_dst_tail_longnegative_body_steps_summand. dst_negative_code_tail_long = fs_q_dst_tail_longnegative_body_steps_summand * S ((S (fs_i_dst_tail_longnegative_body_steps)) * dst_negative_scale_tail_long) + (fs_a_dst_tail_longnegative_body_steps))) /\ ((((exists fs_h_dst_tail_longnegative_body_steps_partial. fs_h_dst_tail_longnegative_body_steps_partial + S (fs_r_dst_tail_longnegative_body_steps) = S ((S (fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_steps_partial. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_steps_partial * S ((S (fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative) + (fs_r_dst_tail_longnegative_body_steps))) /\ ((((exists fs_h_dst_tail_longnegative_body_steps_successor. fs_h_dst_tail_longnegative_body_steps_successor + S (fs_s_dst_tail_longnegative_body_steps) = S ((S (S fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative)) /\ exists fs_q_dst_tail_longnegative_body_steps_successor. fs_u_dst_tail_longnegative = fs_q_dst_tail_longnegative_body_steps_successor * S ((S (S fs_i_dst_tail_longnegative_body_steps)) * fs_v_dst_tail_longnegative) + (fs_s_dst_tail_longnegative_body_steps))) /\ fs_s_dst_tail_longnegative_body_steps = fs_r_dst_tail_longnegative_body_steps + fs_a_dst_tail_longnegative_body_steps)))))) /\ (exists ge_balance_positive_tail_longresult ge_balance_negative_tail_longresult. (((((b) = 2 * (ge_balance_positive_tail_longresult) /\ (ge_balance_negative_tail_longresult) = 0) \/ exists ge_signed_half_tail_longresultdecode. (((b) = 2 * ge_signed_half_tail_longresultdecode + 1 /\ (ge_balance_positive_tail_longresult) = 0) /\ (ge_balance_negative_tail_longresult) = S ge_signed_half_tail_longresultdecode))) /\ ((dst_positive_sum_tail_long) + ge_balance_negative_tail_longresult = (dst_negative_sum_tail_long) + ge_balance_positive_tail_longresult))))))))) -> a=b

Complete tactic proof in conservative notation

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

103 script commands · 19 reading checkpoints · 6 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 zero window restrict
01Fix variables and assumptionsL1–3

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

  1. L1
    intro F
  2. L2
    intro k
  3. L3
    intro l
02Induction on lL4–10

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L4
    induction l
  2. L5
    intro a
  3. L6
    intro b
  4. L7
    intro hkl
  5. L8
    intro hz
  6. L9
    intro ha
  7. L10
    intro hb
03Establish hkL11–20

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

  1. L11
    have hk : k=0
  2. L12
    specialize le_zero (k)
  3. L13
    apply le_zero
  4. L14
    exact hkl
  5. L15
    rewrite hk at ha
  6. L16
    rewrite hk at ha
  7. L17
    rewrite hk at ha
  8. L18
    rewrite hk at ha
  9. L19
    rewrite hk at ha
  10. L20
    rewrite hk at ha
04Use earlier factsL21–27

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

  1. L21
    specialize divisor_signed_sum_functional (F)
  2. L22
    specialize divisor_signed_sum_functional (0)
  3. L23
    specialize divisor_signed_sum_functional (a)
  4. L24
    specialize divisor_signed_sum_functional (b)
  5. L25
    apply divisor_signed_sum_functional
  6. L26
    exact ha
  7. L27
    exact hb
05Fix variables and assumptionsL28–33

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

  1. L28
    intro a
  2. L29
    intro b
  3. L30
    intro hkl
  4. L31
    intro hz
  5. L32
    intro ha
  6. L33
    intro hb
06Establish hcL34–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L34
    have hc : k = S l ∨ Lt(k,S l)Definitions: Lt(k,S l)Original native command in the exact edition
  2. L35
    specialize le_eq_or_lt (k)
  3. L36
    specialize le_eq_or_lt (S l)
  4. L37
    apply le_eq_or_lt
  5. L38
    exact hkl
07Separate the logical casesL39–39

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

  1. L39
    cases hc
08Calculate and transport equalitiesL40–45

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

  1. L40
    rewrite hc_left at ha
  2. L41
    rewrite hc_left at ha
  3. L42
    rewrite hc_left at ha
  4. L43
    rewrite hc_left at ha
  5. L44
    rewrite hc_left at ha
  6. L45
    rewrite hc_left at ha
09Use earlier factsL46–52

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

  1. L46
    specialize divisor_signed_sum_functional (F)
  2. L47
    specialize divisor_signed_sum_functional (S l)
  3. L48
    specialize divisor_signed_sum_functional (a)
  4. L49
    specialize divisor_signed_sum_functional (b)
  5. L50
    apply divisor_signed_sum_functional
  6. L51
    exact ha
  7. L52
    exact hb
10Establish hsmallL53–57

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L53
    have hsmall : Le(k,l)Definitions: Le(k,l)Original native command in the exact edition
  2. L54
    specialize le_of_succ_le_succ (k)
  3. L55
    specialize le_of_succ_le_succ (l)
  4. L56
    apply le_of_succ_le_succ
  5. L57
    exact hc_right
11Establish hdL58–63

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

  1. L58
    have hd : ∃ u. ∃ v. SignedPrefixSum(F,l,u) ∧ (ArithAt(F,l,v) ∧ SignedAdd(u,v,b))Definitions: SignedPrefixSum(F,l,u)ArithAt(F,l,v)SignedAdd(u,v,b)Original native command in the exact edition
  2. L59
    specialize divisor_signed_sum_successor_decompose (F)
  3. L60
    specialize divisor_signed_sum_successor_decompose (l)
  4. L61
    specialize divisor_signed_sum_successor_decompose (b)
  5. L62
    apply divisor_signed_sum_successor_decompose
  6. L63
    exact hb
12Separate the logical casesL64–67

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

  1. L64
    cases hd
  2. L65
    cases hd_witness
  3. L66
    cases hd_witness_witness
  4. L67
    cases hd_witness_witness_right
13Establish hpL68–77

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

  1. L68
    have hp : a=x
  2. L69
    specialize IH (a)
  3. L70
    specialize IH (x)
  4. L71
    apply IH
  5. L72
    exact hsmall
  6. L73
    specialize signed_zero_window_restrict (F)
  7. L74
    specialize signed_zero_window_restrict (k)
  8. L75
    specialize signed_zero_window_restrict (l)
  9. L76
    specialize signed_zero_window_restrict (S l)
  10. L77
    apply signed_zero_window_restrict
14Use earlier factsL78–82

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

  1. L78
    specialize le_succ_self (l)
  2. L79
    apply le_succ_self
  3. L80
    exact hz
  4. L81
    exact ha
  5. L82
    exact hd_witness_witness_left
15Establish hlastL83–92

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

  1. L83
    have hlast : x1=0
  2. L84
    specialize hz (l)
  3. L85
    specialize hz (x1)
  4. L86
    apply hz
  5. L87
    exact hsmall
  6. L88
    specialize le_refl (S l)
  7. L89
    apply le_refl
  8. L90
    exact hd_witness_witness_right_left
  9. L91
    rewrite hlast at hd_witness_witness_right_right
  10. L92
    rewrite hlast at hd_witness_witness_right_right
16Calculate and transport equalitiesL93–93

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

  1. L93
    trans x
17Use earlier factsL94–94

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

  1. L94
    exact hp
18Calculate and transport equalitiesL95–95

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

  1. L95
    symm
19Use earlier factsL96–103

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

  1. L96
    specialize signed_add_functional (x)
  2. L97
    specialize signed_add_functional (0)
  3. L98
    specialize signed_add_functional (b)
  4. L99
    specialize signed_add_functional (x)
  5. L100
    apply signed_add_functional
  6. L101
    exact hd_witness_witness_right_right
  7. L102
    specialize signed_add_zero_right (x)
  8. L103
    apply signed_add_zero_right

Library-wide reading audit

Original defined command ledger · 103 lines
  1. 0001intro F
  2. 0002intro k
  3. 0003intro l
  4. 0004induction l
  5. 0005intro a
  6. 0006intro b
  7. 0007intro hkl
  8. 0008intro hz
  9. 0009intro ha
  10. 0010intro hb
  11. 0011have hk : k=0
  12. 0012specialize le_zero (k)
  13. 0013apply le_zero
  14. 0014exact hkl
  15. 0015rewrite hk at ha
  16. 0016rewrite hk at ha
  17. 0017rewrite hk at ha
  18. 0018rewrite hk at ha
  19. 0019rewrite hk at ha
  20. 0020rewrite hk at ha
  21. 0021specialize divisor_signed_sum_functional (F)
  22. 0022specialize divisor_signed_sum_functional (0)
  23. 0023specialize divisor_signed_sum_functional (a)
  24. 0024specialize divisor_signed_sum_functional (b)
  25. 0025apply divisor_signed_sum_functional
  26. 0026exact ha
  27. 0027exact hb
  28. 0028intro a
  29. 0029intro b
  30. 0030intro hkl
  31. 0031intro hz
  32. 0032intro ha
  33. 0033intro hb
  34. 0034have hc : k = S l ∨ Lt(k,S l)
  35. 0035specialize le_eq_or_lt (k)
  36. 0036specialize le_eq_or_lt (S l)
  37. 0037apply le_eq_or_lt
  38. 0038exact hkl
  39. 0039cases hc
  40. 0040rewrite hc_left at ha
  41. 0041rewrite hc_left at ha
  42. 0042rewrite hc_left at ha
  43. 0043rewrite hc_left at ha
  44. 0044rewrite hc_left at ha
  45. 0045rewrite hc_left at ha
  46. 0046specialize divisor_signed_sum_functional (F)
  47. 0047specialize divisor_signed_sum_functional (S l)
  48. 0048specialize divisor_signed_sum_functional (a)
  49. 0049specialize divisor_signed_sum_functional (b)
  50. 0050apply divisor_signed_sum_functional
  51. 0051exact ha
  52. 0052exact hb
  53. 0053have hsmall : Le(k,l)
  54. 0054specialize le_of_succ_le_succ (k)
  55. 0055specialize le_of_succ_le_succ (l)
  56. 0056apply le_of_succ_le_succ
  57. 0057exact hc_right
  58. 0058have hd : ∃ u. ∃ v. SignedPrefixSum(F,l,u) ∧ (ArithAt(F,l,v) ∧ SignedAdd(u,v,b))
  59. 0059specialize divisor_signed_sum_successor_decompose (F)
  60. 0060specialize divisor_signed_sum_successor_decompose (l)
  61. 0061specialize divisor_signed_sum_successor_decompose (b)
  62. 0062apply divisor_signed_sum_successor_decompose
  63. 0063exact hb
  64. 0064cases hd
  65. 0065cases hd_witness
  66. 0066cases hd_witness_witness
  67. 0067cases hd_witness_witness_right
  68. 0068have hp : a=x
  69. 0069specialize IH (a)
  70. 0070specialize IH (x)
  71. 0071apply IH
  72. 0072exact hsmall
  73. 0073specialize signed_zero_window_restrict (F)
  74. 0074specialize signed_zero_window_restrict (k)
  75. 0075specialize signed_zero_window_restrict (l)
  76. 0076specialize signed_zero_window_restrict (S l)
  77. 0077apply signed_zero_window_restrict
  78. 0078specialize le_succ_self (l)
  79. 0079apply le_succ_self
  80. 0080exact hz
  81. 0081exact ha
  82. 0082exact hd_witness_witness_left
  83. 0083have hlast : x1=0
  84. 0084specialize hz (l)
  85. 0085specialize hz (x1)
  86. 0086apply hz
  87. 0087exact hsmall
  88. 0088specialize le_refl (S l)
  89. 0089apply le_refl
  90. 0090exact hd_witness_witness_right_left
  91. 0091rewrite hlast at hd_witness_witness_right_right
  92. 0092rewrite hlast at hd_witness_witness_right_right
  93. 0093trans x
  94. 0094exact hp
  95. 0095symm
  96. 0096specialize signed_add_functional (x)
  97. 0097specialize signed_add_functional (0)
  98. 0098specialize signed_add_functional (b)
  99. 0099specialize signed_add_functional (x)
  100. 0100apply signed_add_functional
  101. 0101exact hd_witness_witness_right_right
  102. 0102specialize signed_add_zero_right (x)
  103. 0103apply signed_add_zero_right