DV0020

signed_divisor_sum_exists

For every positive n within the finite source domain, construct a real divisor mask and its S n-entry signed fold.

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.

A genuine divisor mask has S n entries, indexed zero through n, and forces its zeroth entry to zero regardless of F(0). Möbius values remain positive-domain only. This family constructs divisor sums and Möbius tables; cancellation and the full G007 endpoint are separately proved later in the same release.

Exact theorem in conservative defined notation

∀ N. ∀ F. ∀ n. ArithTable(N,F) → ¬n = 0 → Le(n,N) → ∃ x. DivisorSum(F,n,x)

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

Definition DAG

ArithTable(N,F) · 1SignedPrefixSum(F,l,z) · 1DivisorMask(F,n,l,M) · 1DivisorSum(F,n,z) · 1Le(a,b) · 1

Actual proof prerequisites

divisor_mask_prefix_existsarithmetic_signed_sum_exists
Original expanded first-order statement 
forall N F n. (exists dst_positive_code_sum_total_input dst_positive_scale_sum_total_input dst_negative_code_sum_total_input dst_negative_scale_sum_total_input. (((F) = (((((dst_positive_code_sum_total_input) + (dst_positive_scale_sum_total_input)) * S ((dst_positive_code_sum_total_input) + (dst_positive_scale_sum_total_input)) + ((dst_positive_scale_sum_total_input) + (dst_positive_scale_sum_total_input))) + (((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) * S ((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) + ((dst_negative_scale_sum_total_input) + (dst_negative_scale_sum_total_input)))) * S ((((dst_positive_code_sum_total_input) + (dst_positive_scale_sum_total_input)) * S ((dst_positive_code_sum_total_input) + (dst_positive_scale_sum_total_input)) + ((dst_positive_scale_sum_total_input) + (dst_positive_scale_sum_total_input))) + (((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) * S ((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) + ((dst_negative_scale_sum_total_input) + (dst_negative_scale_sum_total_input)))) + ((((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) * S ((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) + ((dst_negative_scale_sum_total_input) + (dst_negative_scale_sum_total_input))) + (((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) * S ((dst_negative_code_sum_total_input) + (dst_negative_scale_sum_total_input)) + ((dst_negative_scale_sum_total_input) + (dst_negative_scale_sum_total_input)))))) /\ (forall dst_index_sum_total_input. (exists pvs_le_gap_sum_total_inputdomain. pvs_le_gap_sum_total_inputdomain + (dst_index_sum_total_input) = (N)) -> exists dst_positive_sum_total_input dst_negative_sum_total_input dst_value_sum_total_input. ((((exists ff_h_pvs_sum_total_inputentrypositive. ff_h_pvs_sum_total_inputentrypositive + S (dst_positive_sum_total_input) = S ((S (dst_index_sum_total_input)) * dst_positive_scale_sum_total_input)) /\ exists ff_q_pvs_sum_total_inputentrypositive. dst_positive_code_sum_total_input = ff_q_pvs_sum_total_inputentrypositive * S ((S (dst_index_sum_total_input)) * dst_positive_scale_sum_total_input) + (dst_positive_sum_total_input))) /\ (((((exists ff_h_pvs_sum_total_inputentrynegative. ff_h_pvs_sum_total_inputentrynegative + S (dst_negative_sum_total_input) = S ((S (dst_index_sum_total_input)) * dst_negative_scale_sum_total_input)) /\ exists ff_q_pvs_sum_total_inputentrynegative. dst_negative_code_sum_total_input = ff_q_pvs_sum_total_inputentrynegative * S ((S (dst_index_sum_total_input)) * dst_negative_scale_sum_total_input) + (dst_negative_sum_total_input))) /\ (exists ge_balance_positive_sum_total_inputentryvalue ge_balance_negative_sum_total_inputentryvalue. (((((dst_value_sum_total_input) = 2 * (ge_balance_positive_sum_total_inputentryvalue) /\ (ge_balance_negative_sum_total_inputentryvalue) = 0) \/ exists ge_signed_half_sum_total_inputentryvaluedecode. (((dst_value_sum_total_input) = 2 * ge_signed_half_sum_total_inputentryvaluedecode + 1 /\ (ge_balance_positive_sum_total_inputentryvalue) = 0) /\ (ge_balance_negative_sum_total_inputentryvalue) = S ge_signed_half_sum_total_inputentryvaluedecode))) /\ ((dst_positive_sum_total_input) + ge_balance_negative_sum_total_inputentryvalue = (dst_negative_sum_total_input) + ge_balance_positive_sum_total_inputentryvalue))))))))) -> ~(n=0) -> (exists pvs_le_gap_sum_total_bound. pvs_le_gap_sum_total_bound + (n) = (N)) -> exists z. (((~((n)=0)) /\ (exists dm_mask_table_sum_total_result. ((((exists dst_positive_code_sum_total_resultmasktable dst_positive_scale_sum_total_resultmasktable dst_negative_code_sum_total_resultmasktable dst_negative_scale_sum_total_resultmasktable. (((dm_mask_table_sum_total_result) = (((((dst_positive_code_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable)) * S ((dst_positive_code_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable)) + ((dst_positive_scale_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable))) + (((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) * S ((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) + ((dst_negative_scale_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)))) * S ((((dst_positive_code_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable)) * S ((dst_positive_code_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable)) + ((dst_positive_scale_sum_total_resultmasktable) + (dst_positive_scale_sum_total_resultmasktable))) + (((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) * S ((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) + ((dst_negative_scale_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)))) + ((((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) * S ((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) + ((dst_negative_scale_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable))) + (((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) * S ((dst_negative_code_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)) + ((dst_negative_scale_sum_total_resultmasktable) + (dst_negative_scale_sum_total_resultmasktable)))))) /\ (forall dst_index_sum_total_resultmasktable. (exists pvs_le_gap_sum_total_resultmasktabledomain. pvs_le_gap_sum_total_resultmasktabledomain + (dst_index_sum_total_resultmasktable) = (n)) -> exists dst_positive_sum_total_resultmasktable dst_negative_sum_total_resultmasktable dst_value_sum_total_resultmasktable. ((((exists ff_h_pvs_sum_total_resultmasktableentrypositive. ff_h_pvs_sum_total_resultmasktableentrypositive + S (dst_positive_sum_total_resultmasktable) = S ((S (dst_index_sum_total_resultmasktable)) * dst_positive_scale_sum_total_resultmasktable)) /\ exists ff_q_pvs_sum_total_resultmasktableentrypositive. dst_positive_code_sum_total_resultmasktable = ff_q_pvs_sum_total_resultmasktableentrypositive * S ((S (dst_index_sum_total_resultmasktable)) * dst_positive_scale_sum_total_resultmasktable) + (dst_positive_sum_total_resultmasktable))) /\ (((((exists ff_h_pvs_sum_total_resultmasktableentrynegative. ff_h_pvs_sum_total_resultmasktableentrynegative + S (dst_negative_sum_total_resultmasktable) = S ((S (dst_index_sum_total_resultmasktable)) * dst_negative_scale_sum_total_resultmasktable)) /\ exists ff_q_pvs_sum_total_resultmasktableentrynegative. dst_negative_code_sum_total_resultmasktable = ff_q_pvs_sum_total_resultmasktableentrynegative * S ((S (dst_index_sum_total_resultmasktable)) * dst_negative_scale_sum_total_resultmasktable) + (dst_negative_sum_total_resultmasktable))) /\ (exists ge_balance_positive_sum_total_resultmasktableentryvalue ge_balance_negative_sum_total_resultmasktableentryvalue. (((((dst_value_sum_total_resultmasktable) = 2 * (ge_balance_positive_sum_total_resultmasktableentryvalue) /\ (ge_balance_negative_sum_total_resultmasktableentryvalue) = 0) \/ exists ge_signed_half_sum_total_resultmasktableentryvaluedecode. (((dst_value_sum_total_resultmasktable) = 2 * ge_signed_half_sum_total_resultmasktableentryvaluedecode + 1 /\ (ge_balance_positive_sum_total_resultmasktableentryvalue) = 0) /\ (ge_balance_negative_sum_total_resultmasktableentryvalue) = S ge_signed_half_sum_total_resultmasktableentryvaluedecode))) /\ ((dst_positive_sum_total_resultmasktable) + ge_balance_negative_sum_total_resultmasktableentryvalue = (dst_negative_sum_total_resultmasktable) + ge_balance_positive_sum_total_resultmasktableentryvalue))))))))) /\ (forall dm_index_sum_total_resultmask dm_value_sum_total_resultmask. (exists pvs_le_gap_sum_total_resultmaskdomain. pvs_le_gap_sum_total_resultmaskdomain + (dm_index_sum_total_resultmask) = (n)) -> (exists dst_positive_code_sum_total_resultmasklookup dst_positive_scale_sum_total_resultmasklookup dst_negative_code_sum_total_resultmasklookup dst_negative_scale_sum_total_resultmasklookup dst_positive_sum_total_resultmasklookup dst_negative_sum_total_resultmasklookup. (((dm_mask_table_sum_total_result) = (((((dst_positive_code_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup)) * S ((dst_positive_code_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup)) + ((dst_positive_scale_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup))) + (((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) * S ((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) + ((dst_negative_scale_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)))) * S ((((dst_positive_code_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup)) * S ((dst_positive_code_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup)) + ((dst_positive_scale_sum_total_resultmasklookup) + (dst_positive_scale_sum_total_resultmasklookup))) + (((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) * S ((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) + ((dst_negative_scale_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)))) + ((((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) * S ((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) + ((dst_negative_scale_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup))) + (((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) * S ((dst_negative_code_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)) + ((dst_negative_scale_sum_total_resultmasklookup) + (dst_negative_scale_sum_total_resultmasklookup)))))) /\ (((((exists ff_h_pvs_sum_total_resultmasklookuppositive. ff_h_pvs_sum_total_resultmasklookuppositive + S (dst_positive_sum_total_resultmasklookup) = S ((S (dm_index_sum_total_resultmask)) * dst_positive_scale_sum_total_resultmasklookup)) /\ exists ff_q_pvs_sum_total_resultmasklookuppositive. dst_positive_code_sum_total_resultmasklookup = ff_q_pvs_sum_total_resultmasklookuppositive * S ((S (dm_index_sum_total_resultmask)) * dst_positive_scale_sum_total_resultmasklookup) + (dst_positive_sum_total_resultmasklookup))) /\ (((((exists ff_h_pvs_sum_total_resultmasklookupnegative. ff_h_pvs_sum_total_resultmasklookupnegative + S (dst_negative_sum_total_resultmasklookup) = S ((S (dm_index_sum_total_resultmask)) * dst_negative_scale_sum_total_resultmasklookup)) /\ exists ff_q_pvs_sum_total_resultmasklookupnegative. dst_negative_code_sum_total_resultmasklookup = ff_q_pvs_sum_total_resultmasklookupnegative * S ((S (dm_index_sum_total_resultmask)) * dst_negative_scale_sum_total_resultmasklookup) + (dst_negative_sum_total_resultmasklookup))) /\ (exists ge_balance_positive_sum_total_resultmasklookupvalue ge_balance_negative_sum_total_resultmasklookupvalue. (((((dm_value_sum_total_resultmask) = 2 * (ge_balance_positive_sum_total_resultmasklookupvalue) /\ (ge_balance_negative_sum_total_resultmasklookupvalue) = 0) \/ exists ge_signed_half_sum_total_resultmasklookupvaluedecode. (((dm_value_sum_total_resultmask) = 2 * ge_signed_half_sum_total_resultmasklookupvaluedecode + 1 /\ (ge_balance_positive_sum_total_resultmasklookupvalue) = 0) /\ (ge_balance_negative_sum_total_resultmasklookupvalue) = S ge_signed_half_sum_total_resultmasklookupvaluedecode))) /\ ((dst_positive_sum_total_resultmasklookup) + ge_balance_negative_sum_total_resultmasklookupvalue = (dst_negative_sum_total_resultmasklookup) + ge_balance_positive_sum_total_resultmasklookupvalue))))))))) -> ((((~((dm_index_sum_total_resultmask)=0)) /\ (exists dm_quotient_sum_total_resultmaskentry. (((n)=(dm_index_sum_total_resultmask)*dm_quotient_sum_total_resultmaskentry) /\ (exists dst_positive_code_sum_total_resultmaskentryinput dst_positive_scale_sum_total_resultmaskentryinput dst_negative_code_sum_total_resultmaskentryinput dst_negative_scale_sum_total_resultmaskentryinput dst_positive_sum_total_resultmaskentryinput dst_negative_sum_total_resultmaskentryinput. (((F) = (((((dst_positive_code_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput)) * S ((dst_positive_code_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput)) + ((dst_positive_scale_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput))) + (((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) * S ((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) + ((dst_negative_scale_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)))) * S ((((dst_positive_code_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput)) * S ((dst_positive_code_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput)) + ((dst_positive_scale_sum_total_resultmaskentryinput) + (dst_positive_scale_sum_total_resultmaskentryinput))) + (((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) * S ((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) + ((dst_negative_scale_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)))) + ((((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) * S ((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) + ((dst_negative_scale_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput))) + (((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) * S ((dst_negative_code_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)) + ((dst_negative_scale_sum_total_resultmaskentryinput) + (dst_negative_scale_sum_total_resultmaskentryinput)))))) /\ (((((exists ff_h_pvs_sum_total_resultmaskentryinputpositive. ff_h_pvs_sum_total_resultmaskentryinputpositive + S (dst_positive_sum_total_resultmaskentryinput) = S ((S (dm_index_sum_total_resultmask)) * dst_positive_scale_sum_total_resultmaskentryinput)) /\ exists ff_q_pvs_sum_total_resultmaskentryinputpositive. dst_positive_code_sum_total_resultmaskentryinput = ff_q_pvs_sum_total_resultmaskentryinputpositive * S ((S (dm_index_sum_total_resultmask)) * dst_positive_scale_sum_total_resultmaskentryinput) + (dst_positive_sum_total_resultmaskentryinput))) /\ (((((exists ff_h_pvs_sum_total_resultmaskentryinputnegative. ff_h_pvs_sum_total_resultmaskentryinputnegative + S (dst_negative_sum_total_resultmaskentryinput) = S ((S (dm_index_sum_total_resultmask)) * dst_negative_scale_sum_total_resultmaskentryinput)) /\ exists ff_q_pvs_sum_total_resultmaskentryinputnegative. dst_negative_code_sum_total_resultmaskentryinput = ff_q_pvs_sum_total_resultmaskentryinputnegative * S ((S (dm_index_sum_total_resultmask)) * dst_negative_scale_sum_total_resultmaskentryinput) + (dst_negative_sum_total_resultmaskentryinput))) /\ (exists ge_balance_positive_sum_total_resultmaskentryinputvalue ge_balance_negative_sum_total_resultmaskentryinputvalue. (((((dm_value_sum_total_resultmask) = 2 * (ge_balance_positive_sum_total_resultmaskentryinputvalue) /\ (ge_balance_negative_sum_total_resultmaskentryinputvalue) = 0) \/ exists ge_signed_half_sum_total_resultmaskentryinputvaluedecode. (((dm_value_sum_total_resultmask) = 2 * ge_signed_half_sum_total_resultmaskentryinputvaluedecode + 1 /\ (ge_balance_positive_sum_total_resultmaskentryinputvalue) = 0) /\ (ge_balance_negative_sum_total_resultmaskentryinputvalue) = S ge_signed_half_sum_total_resultmaskentryinputvaluedecode))) /\ ((dst_positive_sum_total_resultmaskentryinput) + ge_balance_negative_sum_total_resultmaskentryinputvalue = (dst_negative_sum_total_resultmaskentryinput) + ge_balance_positive_sum_total_resultmaskentryinputvalue))))))))))))) \/ ((((dm_index_sum_total_resultmask)=0 \/ ~(exists pvs_factor_sum_total_resultmaskentrynondivisor. (n) = (dm_index_sum_total_resultmask) * pvs_factor_sum_total_resultmaskentrynondivisor)) /\ ((dm_value_sum_total_resultmask)=0))))))) /\ (exists dst_positive_code_sum_total_resultfold dst_positive_scale_sum_total_resultfold dst_negative_code_sum_total_resultfold dst_negative_scale_sum_total_resultfold dst_positive_sum_sum_total_resultfold dst_negative_sum_sum_total_resultfold. (((dm_mask_table_sum_total_result) = (((((dst_positive_code_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold)) * S ((dst_positive_code_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold)) + ((dst_positive_scale_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold))) + (((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) * S ((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) + ((dst_negative_scale_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)))) * S ((((dst_positive_code_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold)) * S ((dst_positive_code_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold)) + ((dst_positive_scale_sum_total_resultfold) + (dst_positive_scale_sum_total_resultfold))) + (((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) * S ((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) + ((dst_negative_scale_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)))) + ((((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) * S ((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) + ((dst_negative_scale_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold))) + (((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) * S ((dst_negative_code_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)) + ((dst_negative_scale_sum_total_resultfold) + (dst_negative_scale_sum_total_resultfold)))))) /\ (((exists fs_u_dst_sum_total_resultfoldpositive fs_v_dst_sum_total_resultfoldpositive. ((((exists fs_h_dst_sum_total_resultfoldpositive_body_start. fs_h_dst_sum_total_resultfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_total_resultfoldpositive)) /\ exists fs_q_dst_sum_total_resultfoldpositive_body_start. fs_u_dst_sum_total_resultfoldpositive = fs_q_dst_sum_total_resultfoldpositive_body_start * S ((S (0)) * fs_v_dst_sum_total_resultfoldpositive) + (0))) /\ ((((exists fs_h_dst_sum_total_resultfoldpositive_body_terminal. fs_h_dst_sum_total_resultfoldpositive_body_terminal + S (dst_positive_sum_sum_total_resultfold) = S ((S (S (n))) * fs_v_dst_sum_total_resultfoldpositive)) /\ exists fs_q_dst_sum_total_resultfoldpositive_body_terminal. fs_u_dst_sum_total_resultfoldpositive = fs_q_dst_sum_total_resultfoldpositive_body_terminal * S ((S (S (n))) * fs_v_dst_sum_total_resultfoldpositive) + (dst_positive_sum_sum_total_resultfold))) /\ forall fs_i_dst_sum_total_resultfoldpositive_body_steps. (exists fs_lt_dst_sum_total_resultfoldpositive_body_steps_bound. fs_lt_dst_sum_total_resultfoldpositive_body_steps_bound + S fs_i_dst_sum_total_resultfoldpositive_body_steps = S (n)) -> exists fs_a_dst_sum_total_resultfoldpositive_body_steps fs_r_dst_sum_total_resultfoldpositive_body_steps fs_s_dst_sum_total_resultfoldpositive_body_steps. ((((exists fs_h_dst_sum_total_resultfoldpositive_body_steps_summand. fs_h_dst_sum_total_resultfoldpositive_body_steps_summand + S (fs_a_dst_sum_total_resultfoldpositive_body_steps) = S ((S (fs_i_dst_sum_total_resultfoldpositive_body_steps)) * dst_positive_scale_sum_total_resultfold)) /\ exists fs_q_dst_sum_total_resultfoldpositive_body_steps_summand. dst_positive_code_sum_total_resultfold = fs_q_dst_sum_total_resultfoldpositive_body_steps_summand * S ((S (fs_i_dst_sum_total_resultfoldpositive_body_steps)) * dst_positive_scale_sum_total_resultfold) + (fs_a_dst_sum_total_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_total_resultfoldpositive_body_steps_partial. fs_h_dst_sum_total_resultfoldpositive_body_steps_partial + S (fs_r_dst_sum_total_resultfoldpositive_body_steps) = S ((S (fs_i_dst_sum_total_resultfoldpositive_body_steps)) * fs_v_dst_sum_total_resultfoldpositive)) /\ exists fs_q_dst_sum_total_resultfoldpositive_body_steps_partial. fs_u_dst_sum_total_resultfoldpositive = fs_q_dst_sum_total_resultfoldpositive_body_steps_partial * S ((S (fs_i_dst_sum_total_resultfoldpositive_body_steps)) * fs_v_dst_sum_total_resultfoldpositive) + (fs_r_dst_sum_total_resultfoldpositive_body_steps))) /\ ((((exists fs_h_dst_sum_total_resultfoldpositive_body_steps_successor. fs_h_dst_sum_total_resultfoldpositive_body_steps_successor + S (fs_s_dst_sum_total_resultfoldpositive_body_steps) = S ((S (S fs_i_dst_sum_total_resultfoldpositive_body_steps)) * fs_v_dst_sum_total_resultfoldpositive)) /\ exists fs_q_dst_sum_total_resultfoldpositive_body_steps_successor. fs_u_dst_sum_total_resultfoldpositive = fs_q_dst_sum_total_resultfoldpositive_body_steps_successor * S ((S (S fs_i_dst_sum_total_resultfoldpositive_body_steps)) * fs_v_dst_sum_total_resultfoldpositive) + (fs_s_dst_sum_total_resultfoldpositive_body_steps))) /\ fs_s_dst_sum_total_resultfoldpositive_body_steps = fs_r_dst_sum_total_resultfoldpositive_body_steps + fs_a_dst_sum_total_resultfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_sum_total_resultfoldnegative fs_v_dst_sum_total_resultfoldnegative. ((((exists fs_h_dst_sum_total_resultfoldnegative_body_start. fs_h_dst_sum_total_resultfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_sum_total_resultfoldnegative)) /\ exists fs_q_dst_sum_total_resultfoldnegative_body_start. fs_u_dst_sum_total_resultfoldnegative = fs_q_dst_sum_total_resultfoldnegative_body_start * S ((S (0)) * fs_v_dst_sum_total_resultfoldnegative) + (0))) /\ ((((exists fs_h_dst_sum_total_resultfoldnegative_body_terminal. fs_h_dst_sum_total_resultfoldnegative_body_terminal + S (dst_negative_sum_sum_total_resultfold) = S ((S (S (n))) * fs_v_dst_sum_total_resultfoldnegative)) /\ exists fs_q_dst_sum_total_resultfoldnegative_body_terminal. fs_u_dst_sum_total_resultfoldnegative = fs_q_dst_sum_total_resultfoldnegative_body_terminal * S ((S (S (n))) * fs_v_dst_sum_total_resultfoldnegative) + (dst_negative_sum_sum_total_resultfold))) /\ forall fs_i_dst_sum_total_resultfoldnegative_body_steps. (exists fs_lt_dst_sum_total_resultfoldnegative_body_steps_bound. fs_lt_dst_sum_total_resultfoldnegative_body_steps_bound + S fs_i_dst_sum_total_resultfoldnegative_body_steps = S (n)) -> exists fs_a_dst_sum_total_resultfoldnegative_body_steps fs_r_dst_sum_total_resultfoldnegative_body_steps fs_s_dst_sum_total_resultfoldnegative_body_steps. ((((exists fs_h_dst_sum_total_resultfoldnegative_body_steps_summand. fs_h_dst_sum_total_resultfoldnegative_body_steps_summand + S (fs_a_dst_sum_total_resultfoldnegative_body_steps) = S ((S (fs_i_dst_sum_total_resultfoldnegative_body_steps)) * dst_negative_scale_sum_total_resultfold)) /\ exists fs_q_dst_sum_total_resultfoldnegative_body_steps_summand. dst_negative_code_sum_total_resultfold = fs_q_dst_sum_total_resultfoldnegative_body_steps_summand * S ((S (fs_i_dst_sum_total_resultfoldnegative_body_steps)) * dst_negative_scale_sum_total_resultfold) + (fs_a_dst_sum_total_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_total_resultfoldnegative_body_steps_partial. fs_h_dst_sum_total_resultfoldnegative_body_steps_partial + S (fs_r_dst_sum_total_resultfoldnegative_body_steps) = S ((S (fs_i_dst_sum_total_resultfoldnegative_body_steps)) * fs_v_dst_sum_total_resultfoldnegative)) /\ exists fs_q_dst_sum_total_resultfoldnegative_body_steps_partial. fs_u_dst_sum_total_resultfoldnegative = fs_q_dst_sum_total_resultfoldnegative_body_steps_partial * S ((S (fs_i_dst_sum_total_resultfoldnegative_body_steps)) * fs_v_dst_sum_total_resultfoldnegative) + (fs_r_dst_sum_total_resultfoldnegative_body_steps))) /\ ((((exists fs_h_dst_sum_total_resultfoldnegative_body_steps_successor. fs_h_dst_sum_total_resultfoldnegative_body_steps_successor + S (fs_s_dst_sum_total_resultfoldnegative_body_steps) = S ((S (S fs_i_dst_sum_total_resultfoldnegative_body_steps)) * fs_v_dst_sum_total_resultfoldnegative)) /\ exists fs_q_dst_sum_total_resultfoldnegative_body_steps_successor. fs_u_dst_sum_total_resultfoldnegative = fs_q_dst_sum_total_resultfoldnegative_body_steps_successor * S ((S (S fs_i_dst_sum_total_resultfoldnegative_body_steps)) * fs_v_dst_sum_total_resultfoldnegative) + (fs_s_dst_sum_total_resultfoldnegative_body_steps))) /\ fs_s_dst_sum_total_resultfoldnegative_body_steps = fs_r_dst_sum_total_resultfoldnegative_body_steps + fs_a_dst_sum_total_resultfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_sum_total_resultfoldresult ge_balance_negative_sum_total_resultfoldresult. (((((z) = 2 * (ge_balance_positive_sum_total_resultfoldresult) /\ (ge_balance_negative_sum_total_resultfoldresult) = 0) \/ exists ge_signed_half_sum_total_resultfoldresultdecode. (((z) = 2 * ge_signed_half_sum_total_resultfoldresultdecode + 1 /\ (ge_balance_positive_sum_total_resultfoldresult) = 0) /\ (ge_balance_negative_sum_total_resultfoldresult) = S ge_signed_half_sum_total_resultfoldresultdecode))) /\ ((dst_positive_sum_sum_total_resultfold) + ge_balance_negative_sum_total_resultfoldresult = (dst_negative_sum_sum_total_resultfold) + ge_balance_positive_sum_total_resultfoldresult)))))))))))))

Complete tactic proof in conservative notation

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

30 script commands · 11 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 (2)
divisor mask prefix existsarithmetic signed sum exists
01Fix variables and assumptionsL1–6

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro n
  4. L4
    intro ht
  5. L5
    intro hn
  6. L6
    intro hbound
02Establish hmL7–14

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

  1. L7
    have hm : ∃ M. DivisorMask(F,n,n,M)Definitions: DivisorMask(F,n,n,M)Original native command in the exact edition
  2. L8
    specialize divisor_mask_prefix_exists (N)
  3. L9
    specialize divisor_mask_prefix_exists (F)
  4. L10
    specialize divisor_mask_prefix_exists (n)
  5. L11
    specialize divisor_mask_prefix_exists (n)
  6. L12
    apply divisor_mask_prefix_exists
  7. L13
    exact ht
  8. L14
    exact hbound
03Separate the logical casesL15–16

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

  1. L15
    cases hm
  2. L16
    cases hm_witness
04Establish hzL17–22

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

  1. L17
    have hz : ∃ z. SignedPrefixSum(x,S n,z)Definitions: SignedPrefixSum(x,S n,z)Original native command in the exact edition
  2. L18
    specialize arithmetic_signed_sum_exists (n)
  3. L19
    specialize arithmetic_signed_sum_exists (x)
  4. L20
    specialize arithmetic_signed_sum_exists (S n)
  5. L21
    apply arithmetic_signed_sum_exists
  6. L22
    exact hm_witness_left
05Separate the logical casesL23–23

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

  1. L23
    cases hz
06Construct an explicit witnessL24–24

Supply the displayed value, then prove that it has the required property.

  1. L24
    exists x1
07Separate the logical casesL25–25

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

  1. L25
    split
08Use earlier factsL26–26

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

  1. L26
    exact hn
09Construct an explicit witnessL27–27

Supply the displayed value, then prove that it has the required property.

  1. L27
    exists x
10Separate the logical casesL28–28

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

  1. L28
    split
11Use earlier factsL29–30

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

  1. L29
    exact hm_witness
  2. L30
    exact hz_witness

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro n
  4. 0004intro ht
  5. 0005intro hn
  6. 0006intro hbound
  7. 0007have hm : ∃ M. DivisorMask(F,n,n,M)
  8. 0008specialize divisor_mask_prefix_exists (N)
  9. 0009specialize divisor_mask_prefix_exists (F)
  10. 0010specialize divisor_mask_prefix_exists (n)
  11. 0011specialize divisor_mask_prefix_exists (n)
  12. 0012apply divisor_mask_prefix_exists
  13. 0013exact ht
  14. 0014exact hbound
  15. 0015cases hm
  16. 0016cases hm_witness
  17. 0017have hz : ∃ z. SignedPrefixSum(x,S n,z)
  18. 0018specialize arithmetic_signed_sum_exists (n)
  19. 0019specialize arithmetic_signed_sum_exists (x)
  20. 0020specialize arithmetic_signed_sum_exists (S n)
  21. 0021apply arithmetic_signed_sum_exists
  22. 0022exact hm_witness_left
  23. 0023cases hz
  24. 0024exists x1
  25. 0025split
  26. 0026exact hn
  27. 0027exists x
  28. 0028split
  29. 0029exact hm_witness
  30. 0030exact hz_witness