SS0015

divisor_signed_sum_negation_transport

Swapping the actual positive/negative beta streams negates their signed sum, using the same genuine natural traces.

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.

These are actual signed-table and finite-sum foundations. Equality compares represented signed values, not arbitrary encodings. MatrixMinorFourCode is reused solely as generic nested pairing, without a matrix hypothesis. Full finite signed G007 is established separately in the Möbius-inversion family.

Exact theorem in conservative defined notation

∀ F. ∀ G. ∀ pb. ∀ pc. ∀ nb. ∀ nc. ∀ l. ∀ a. ∀ b. MatrixMinorFourCode(F,pb,pc,nb,nc) → MatrixMinorFourCode(G,nb,nc,pb,pc) → SignedPrefixSum(F,l,a) → (∃ x. ∃ y. SignedDecode(a,x,y) ∧ SignedDecode(b,y,x)) → SignedPrefixSum(G,l,b)

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

Definition DAG

MatrixMinorFourCode(z,up,us,un,ut) · 2SignedDecode(z,p,n) · 2SignedBalance(z,p,n) · 1SignedPrefixSum(F,l,z) · 2Sum(b,c,l,z) · 2

Actual proof prerequisites

divisor_signed_sum_to_componentsdivisor_signed_sum_from_componentsdivisor_signed_balance_negate
Original expanded first-order statement 
forall F G pb pc nb nc l a b. ((F) = (((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) * S ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))) + ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc)))))) -> ((G) = (((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc)))) * S ((((nb) + (nc)) * S ((nb) + (nc)) + ((nc) + (nc))) + (((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc)))) + ((((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc))) + (((pb) + (pc)) * S ((pb) + (pc)) + ((pc) + (pc)))))) -> (exists dst_positive_code_negation_source_sum dst_positive_scale_negation_source_sum dst_negative_code_negation_source_sum dst_negative_scale_negation_source_sum dst_positive_sum_negation_source_sum dst_negative_sum_negation_source_sum. (((F) = (((((dst_positive_code_negation_source_sum) + (dst_positive_scale_negation_source_sum)) * S ((dst_positive_code_negation_source_sum) + (dst_positive_scale_negation_source_sum)) + ((dst_positive_scale_negation_source_sum) + (dst_positive_scale_negation_source_sum))) + (((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) * S ((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) + ((dst_negative_scale_negation_source_sum) + (dst_negative_scale_negation_source_sum)))) * S ((((dst_positive_code_negation_source_sum) + (dst_positive_scale_negation_source_sum)) * S ((dst_positive_code_negation_source_sum) + (dst_positive_scale_negation_source_sum)) + ((dst_positive_scale_negation_source_sum) + (dst_positive_scale_negation_source_sum))) + (((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) * S ((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) + ((dst_negative_scale_negation_source_sum) + (dst_negative_scale_negation_source_sum)))) + ((((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) * S ((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) + ((dst_negative_scale_negation_source_sum) + (dst_negative_scale_negation_source_sum))) + (((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) * S ((dst_negative_code_negation_source_sum) + (dst_negative_scale_negation_source_sum)) + ((dst_negative_scale_negation_source_sum) + (dst_negative_scale_negation_source_sum)))))) /\ (((exists fs_u_dst_negation_source_sumpositive fs_v_dst_negation_source_sumpositive. ((((exists fs_h_dst_negation_source_sumpositive_body_start. fs_h_dst_negation_source_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_negation_source_sumpositive)) /\ exists fs_q_dst_negation_source_sumpositive_body_start. fs_u_dst_negation_source_sumpositive = fs_q_dst_negation_source_sumpositive_body_start * S ((S (0)) * fs_v_dst_negation_source_sumpositive) + (0))) /\ ((((exists fs_h_dst_negation_source_sumpositive_body_terminal. fs_h_dst_negation_source_sumpositive_body_terminal + S (dst_positive_sum_negation_source_sum) = S ((S (l)) * fs_v_dst_negation_source_sumpositive)) /\ exists fs_q_dst_negation_source_sumpositive_body_terminal. fs_u_dst_negation_source_sumpositive = fs_q_dst_negation_source_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_negation_source_sumpositive) + (dst_positive_sum_negation_source_sum))) /\ forall fs_i_dst_negation_source_sumpositive_body_steps. (exists fs_lt_dst_negation_source_sumpositive_body_steps_bound. fs_lt_dst_negation_source_sumpositive_body_steps_bound + S fs_i_dst_negation_source_sumpositive_body_steps = l) -> exists fs_a_dst_negation_source_sumpositive_body_steps fs_r_dst_negation_source_sumpositive_body_steps fs_s_dst_negation_source_sumpositive_body_steps. ((((exists fs_h_dst_negation_source_sumpositive_body_steps_summand. fs_h_dst_negation_source_sumpositive_body_steps_summand + S (fs_a_dst_negation_source_sumpositive_body_steps) = S ((S (fs_i_dst_negation_source_sumpositive_body_steps)) * dst_positive_scale_negation_source_sum)) /\ exists fs_q_dst_negation_source_sumpositive_body_steps_summand. dst_positive_code_negation_source_sum = fs_q_dst_negation_source_sumpositive_body_steps_summand * S ((S (fs_i_dst_negation_source_sumpositive_body_steps)) * dst_positive_scale_negation_source_sum) + (fs_a_dst_negation_source_sumpositive_body_steps))) /\ ((((exists fs_h_dst_negation_source_sumpositive_body_steps_partial. fs_h_dst_negation_source_sumpositive_body_steps_partial + S (fs_r_dst_negation_source_sumpositive_body_steps) = S ((S (fs_i_dst_negation_source_sumpositive_body_steps)) * fs_v_dst_negation_source_sumpositive)) /\ exists fs_q_dst_negation_source_sumpositive_body_steps_partial. fs_u_dst_negation_source_sumpositive = fs_q_dst_negation_source_sumpositive_body_steps_partial * S ((S (fs_i_dst_negation_source_sumpositive_body_steps)) * fs_v_dst_negation_source_sumpositive) + (fs_r_dst_negation_source_sumpositive_body_steps))) /\ ((((exists fs_h_dst_negation_source_sumpositive_body_steps_successor. fs_h_dst_negation_source_sumpositive_body_steps_successor + S (fs_s_dst_negation_source_sumpositive_body_steps) = S ((S (S fs_i_dst_negation_source_sumpositive_body_steps)) * fs_v_dst_negation_source_sumpositive)) /\ exists fs_q_dst_negation_source_sumpositive_body_steps_successor. fs_u_dst_negation_source_sumpositive = fs_q_dst_negation_source_sumpositive_body_steps_successor * S ((S (S fs_i_dst_negation_source_sumpositive_body_steps)) * fs_v_dst_negation_source_sumpositive) + (fs_s_dst_negation_source_sumpositive_body_steps))) /\ fs_s_dst_negation_source_sumpositive_body_steps = fs_r_dst_negation_source_sumpositive_body_steps + fs_a_dst_negation_source_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_negation_source_sumnegative fs_v_dst_negation_source_sumnegative. ((((exists fs_h_dst_negation_source_sumnegative_body_start. fs_h_dst_negation_source_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_negation_source_sumnegative)) /\ exists fs_q_dst_negation_source_sumnegative_body_start. fs_u_dst_negation_source_sumnegative = fs_q_dst_negation_source_sumnegative_body_start * S ((S (0)) * fs_v_dst_negation_source_sumnegative) + (0))) /\ ((((exists fs_h_dst_negation_source_sumnegative_body_terminal. fs_h_dst_negation_source_sumnegative_body_terminal + S (dst_negative_sum_negation_source_sum) = S ((S (l)) * fs_v_dst_negation_source_sumnegative)) /\ exists fs_q_dst_negation_source_sumnegative_body_terminal. fs_u_dst_negation_source_sumnegative = fs_q_dst_negation_source_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_negation_source_sumnegative) + (dst_negative_sum_negation_source_sum))) /\ forall fs_i_dst_negation_source_sumnegative_body_steps. (exists fs_lt_dst_negation_source_sumnegative_body_steps_bound. fs_lt_dst_negation_source_sumnegative_body_steps_bound + S fs_i_dst_negation_source_sumnegative_body_steps = l) -> exists fs_a_dst_negation_source_sumnegative_body_steps fs_r_dst_negation_source_sumnegative_body_steps fs_s_dst_negation_source_sumnegative_body_steps. ((((exists fs_h_dst_negation_source_sumnegative_body_steps_summand. fs_h_dst_negation_source_sumnegative_body_steps_summand + S (fs_a_dst_negation_source_sumnegative_body_steps) = S ((S (fs_i_dst_negation_source_sumnegative_body_steps)) * dst_negative_scale_negation_source_sum)) /\ exists fs_q_dst_negation_source_sumnegative_body_steps_summand. dst_negative_code_negation_source_sum = fs_q_dst_negation_source_sumnegative_body_steps_summand * S ((S (fs_i_dst_negation_source_sumnegative_body_steps)) * dst_negative_scale_negation_source_sum) + (fs_a_dst_negation_source_sumnegative_body_steps))) /\ ((((exists fs_h_dst_negation_source_sumnegative_body_steps_partial. fs_h_dst_negation_source_sumnegative_body_steps_partial + S (fs_r_dst_negation_source_sumnegative_body_steps) = S ((S (fs_i_dst_negation_source_sumnegative_body_steps)) * fs_v_dst_negation_source_sumnegative)) /\ exists fs_q_dst_negation_source_sumnegative_body_steps_partial. fs_u_dst_negation_source_sumnegative = fs_q_dst_negation_source_sumnegative_body_steps_partial * S ((S (fs_i_dst_negation_source_sumnegative_body_steps)) * fs_v_dst_negation_source_sumnegative) + (fs_r_dst_negation_source_sumnegative_body_steps))) /\ ((((exists fs_h_dst_negation_source_sumnegative_body_steps_successor. fs_h_dst_negation_source_sumnegative_body_steps_successor + S (fs_s_dst_negation_source_sumnegative_body_steps) = S ((S (S fs_i_dst_negation_source_sumnegative_body_steps)) * fs_v_dst_negation_source_sumnegative)) /\ exists fs_q_dst_negation_source_sumnegative_body_steps_successor. fs_u_dst_negation_source_sumnegative = fs_q_dst_negation_source_sumnegative_body_steps_successor * S ((S (S fs_i_dst_negation_source_sumnegative_body_steps)) * fs_v_dst_negation_source_sumnegative) + (fs_s_dst_negation_source_sumnegative_body_steps))) /\ fs_s_dst_negation_source_sumnegative_body_steps = fs_r_dst_negation_source_sumnegative_body_steps + fs_a_dst_negation_source_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_negation_source_sumresult ge_balance_negative_negation_source_sumresult. (((((a) = 2 * (ge_balance_positive_negation_source_sumresult) /\ (ge_balance_negative_negation_source_sumresult) = 0) \/ exists ge_signed_half_negation_source_sumresultdecode. (((a) = 2 * ge_signed_half_negation_source_sumresultdecode + 1 /\ (ge_balance_positive_negation_source_sumresult) = 0) /\ (ge_balance_negative_negation_source_sumresult) = S ge_signed_half_negation_source_sumresultdecode))) /\ ((dst_positive_sum_negation_source_sum) + ge_balance_negative_negation_source_sumresult = (dst_negative_sum_negation_source_sum) + ge_balance_positive_negation_source_sumresult))))))))) -> (exists mps_positive_negation_relation mps_negative_negation_relation. (((((a) = 2 * (mps_positive_negation_relation) /\ (mps_negative_negation_relation) = 0) \/ exists ge_signed_half_negation_relationsource. (((a) = 2 * ge_signed_half_negation_relationsource + 1 /\ (mps_positive_negation_relation) = 0) /\ (mps_negative_negation_relation) = S ge_signed_half_negation_relationsource))) /\ ((((b) = 2 * (mps_negative_negation_relation) /\ (mps_positive_negation_relation) = 0) \/ exists ge_signed_half_negation_relationtarget. (((b) = 2 * ge_signed_half_negation_relationtarget + 1 /\ (mps_negative_negation_relation) = 0) /\ (mps_positive_negation_relation) = S ge_signed_half_negation_relationtarget))))) -> (exists dst_positive_code_negation_target_sum dst_positive_scale_negation_target_sum dst_negative_code_negation_target_sum dst_negative_scale_negation_target_sum dst_positive_sum_negation_target_sum dst_negative_sum_negation_target_sum. (((G) = (((((dst_positive_code_negation_target_sum) + (dst_positive_scale_negation_target_sum)) * S ((dst_positive_code_negation_target_sum) + (dst_positive_scale_negation_target_sum)) + ((dst_positive_scale_negation_target_sum) + (dst_positive_scale_negation_target_sum))) + (((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) * S ((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) + ((dst_negative_scale_negation_target_sum) + (dst_negative_scale_negation_target_sum)))) * S ((((dst_positive_code_negation_target_sum) + (dst_positive_scale_negation_target_sum)) * S ((dst_positive_code_negation_target_sum) + (dst_positive_scale_negation_target_sum)) + ((dst_positive_scale_negation_target_sum) + (dst_positive_scale_negation_target_sum))) + (((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) * S ((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) + ((dst_negative_scale_negation_target_sum) + (dst_negative_scale_negation_target_sum)))) + ((((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) * S ((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) + ((dst_negative_scale_negation_target_sum) + (dst_negative_scale_negation_target_sum))) + (((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) * S ((dst_negative_code_negation_target_sum) + (dst_negative_scale_negation_target_sum)) + ((dst_negative_scale_negation_target_sum) + (dst_negative_scale_negation_target_sum)))))) /\ (((exists fs_u_dst_negation_target_sumpositive fs_v_dst_negation_target_sumpositive. ((((exists fs_h_dst_negation_target_sumpositive_body_start. fs_h_dst_negation_target_sumpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_negation_target_sumpositive)) /\ exists fs_q_dst_negation_target_sumpositive_body_start. fs_u_dst_negation_target_sumpositive = fs_q_dst_negation_target_sumpositive_body_start * S ((S (0)) * fs_v_dst_negation_target_sumpositive) + (0))) /\ ((((exists fs_h_dst_negation_target_sumpositive_body_terminal. fs_h_dst_negation_target_sumpositive_body_terminal + S (dst_positive_sum_negation_target_sum) = S ((S (l)) * fs_v_dst_negation_target_sumpositive)) /\ exists fs_q_dst_negation_target_sumpositive_body_terminal. fs_u_dst_negation_target_sumpositive = fs_q_dst_negation_target_sumpositive_body_terminal * S ((S (l)) * fs_v_dst_negation_target_sumpositive) + (dst_positive_sum_negation_target_sum))) /\ forall fs_i_dst_negation_target_sumpositive_body_steps. (exists fs_lt_dst_negation_target_sumpositive_body_steps_bound. fs_lt_dst_negation_target_sumpositive_body_steps_bound + S fs_i_dst_negation_target_sumpositive_body_steps = l) -> exists fs_a_dst_negation_target_sumpositive_body_steps fs_r_dst_negation_target_sumpositive_body_steps fs_s_dst_negation_target_sumpositive_body_steps. ((((exists fs_h_dst_negation_target_sumpositive_body_steps_summand. fs_h_dst_negation_target_sumpositive_body_steps_summand + S (fs_a_dst_negation_target_sumpositive_body_steps) = S ((S (fs_i_dst_negation_target_sumpositive_body_steps)) * dst_positive_scale_negation_target_sum)) /\ exists fs_q_dst_negation_target_sumpositive_body_steps_summand. dst_positive_code_negation_target_sum = fs_q_dst_negation_target_sumpositive_body_steps_summand * S ((S (fs_i_dst_negation_target_sumpositive_body_steps)) * dst_positive_scale_negation_target_sum) + (fs_a_dst_negation_target_sumpositive_body_steps))) /\ ((((exists fs_h_dst_negation_target_sumpositive_body_steps_partial. fs_h_dst_negation_target_sumpositive_body_steps_partial + S (fs_r_dst_negation_target_sumpositive_body_steps) = S ((S (fs_i_dst_negation_target_sumpositive_body_steps)) * fs_v_dst_negation_target_sumpositive)) /\ exists fs_q_dst_negation_target_sumpositive_body_steps_partial. fs_u_dst_negation_target_sumpositive = fs_q_dst_negation_target_sumpositive_body_steps_partial * S ((S (fs_i_dst_negation_target_sumpositive_body_steps)) * fs_v_dst_negation_target_sumpositive) + (fs_r_dst_negation_target_sumpositive_body_steps))) /\ ((((exists fs_h_dst_negation_target_sumpositive_body_steps_successor. fs_h_dst_negation_target_sumpositive_body_steps_successor + S (fs_s_dst_negation_target_sumpositive_body_steps) = S ((S (S fs_i_dst_negation_target_sumpositive_body_steps)) * fs_v_dst_negation_target_sumpositive)) /\ exists fs_q_dst_negation_target_sumpositive_body_steps_successor. fs_u_dst_negation_target_sumpositive = fs_q_dst_negation_target_sumpositive_body_steps_successor * S ((S (S fs_i_dst_negation_target_sumpositive_body_steps)) * fs_v_dst_negation_target_sumpositive) + (fs_s_dst_negation_target_sumpositive_body_steps))) /\ fs_s_dst_negation_target_sumpositive_body_steps = fs_r_dst_negation_target_sumpositive_body_steps + fs_a_dst_negation_target_sumpositive_body_steps)))))) /\ (((exists fs_u_dst_negation_target_sumnegative fs_v_dst_negation_target_sumnegative. ((((exists fs_h_dst_negation_target_sumnegative_body_start. fs_h_dst_negation_target_sumnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_negation_target_sumnegative)) /\ exists fs_q_dst_negation_target_sumnegative_body_start. fs_u_dst_negation_target_sumnegative = fs_q_dst_negation_target_sumnegative_body_start * S ((S (0)) * fs_v_dst_negation_target_sumnegative) + (0))) /\ ((((exists fs_h_dst_negation_target_sumnegative_body_terminal. fs_h_dst_negation_target_sumnegative_body_terminal + S (dst_negative_sum_negation_target_sum) = S ((S (l)) * fs_v_dst_negation_target_sumnegative)) /\ exists fs_q_dst_negation_target_sumnegative_body_terminal. fs_u_dst_negation_target_sumnegative = fs_q_dst_negation_target_sumnegative_body_terminal * S ((S (l)) * fs_v_dst_negation_target_sumnegative) + (dst_negative_sum_negation_target_sum))) /\ forall fs_i_dst_negation_target_sumnegative_body_steps. (exists fs_lt_dst_negation_target_sumnegative_body_steps_bound. fs_lt_dst_negation_target_sumnegative_body_steps_bound + S fs_i_dst_negation_target_sumnegative_body_steps = l) -> exists fs_a_dst_negation_target_sumnegative_body_steps fs_r_dst_negation_target_sumnegative_body_steps fs_s_dst_negation_target_sumnegative_body_steps. ((((exists fs_h_dst_negation_target_sumnegative_body_steps_summand. fs_h_dst_negation_target_sumnegative_body_steps_summand + S (fs_a_dst_negation_target_sumnegative_body_steps) = S ((S (fs_i_dst_negation_target_sumnegative_body_steps)) * dst_negative_scale_negation_target_sum)) /\ exists fs_q_dst_negation_target_sumnegative_body_steps_summand. dst_negative_code_negation_target_sum = fs_q_dst_negation_target_sumnegative_body_steps_summand * S ((S (fs_i_dst_negation_target_sumnegative_body_steps)) * dst_negative_scale_negation_target_sum) + (fs_a_dst_negation_target_sumnegative_body_steps))) /\ ((((exists fs_h_dst_negation_target_sumnegative_body_steps_partial. fs_h_dst_negation_target_sumnegative_body_steps_partial + S (fs_r_dst_negation_target_sumnegative_body_steps) = S ((S (fs_i_dst_negation_target_sumnegative_body_steps)) * fs_v_dst_negation_target_sumnegative)) /\ exists fs_q_dst_negation_target_sumnegative_body_steps_partial. fs_u_dst_negation_target_sumnegative = fs_q_dst_negation_target_sumnegative_body_steps_partial * S ((S (fs_i_dst_negation_target_sumnegative_body_steps)) * fs_v_dst_negation_target_sumnegative) + (fs_r_dst_negation_target_sumnegative_body_steps))) /\ ((((exists fs_h_dst_negation_target_sumnegative_body_steps_successor. fs_h_dst_negation_target_sumnegative_body_steps_successor + S (fs_s_dst_negation_target_sumnegative_body_steps) = S ((S (S fs_i_dst_negation_target_sumnegative_body_steps)) * fs_v_dst_negation_target_sumnegative)) /\ exists fs_q_dst_negation_target_sumnegative_body_steps_successor. fs_u_dst_negation_target_sumnegative = fs_q_dst_negation_target_sumnegative_body_steps_successor * S ((S (S fs_i_dst_negation_target_sumnegative_body_steps)) * fs_v_dst_negation_target_sumnegative) + (fs_s_dst_negation_target_sumnegative_body_steps))) /\ fs_s_dst_negation_target_sumnegative_body_steps = fs_r_dst_negation_target_sumnegative_body_steps + fs_a_dst_negation_target_sumnegative_body_steps)))))) /\ (exists ge_balance_positive_negation_target_sumresult ge_balance_negative_negation_target_sumresult. (((((b) = 2 * (ge_balance_positive_negation_target_sumresult) /\ (ge_balance_negative_negation_target_sumresult) = 0) \/ exists ge_signed_half_negation_target_sumresultdecode. (((b) = 2 * ge_signed_half_negation_target_sumresultdecode + 1 /\ (ge_balance_positive_negation_target_sumresult) = 0) /\ (ge_balance_negative_negation_target_sumresult) = S ge_signed_half_negation_target_sumresultdecode))) /\ ((dst_positive_sum_negation_target_sum) + ge_balance_negative_negation_target_sumresult = (dst_negative_sum_negation_target_sum) + ge_balance_positive_negation_target_sumresult)))))))))

Complete tactic proof in conservative notation

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

48 script commands · 7 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

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

Named ingredients (3)
divisor signed sum to componentsdivisor signed sum from componentsdivisor signed balance negate
01Fix variables and assumptionsL1–10

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro pb
  4. L4
    intro pc
  5. L5
    intro nb
  6. L6
    intro nc
  7. L7
    intro l
  8. L8
    intro a
  9. L9
    intro b
  10. L10
    intro hF
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hG
  2. L12
    intro hs
  3. L13
    intro hn
03Establish hpartsL14–23

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

  1. L14
    have hparts : ∃ p. ∃ n. Sum(pb,pc,l,p) ∧ (Sum(nb,nc,l,n) ∧ SignedBalance(a,p,n))Definitions: Sum(pb,pc,l,p)Sum(nb,nc,l,n)SignedBalance(a,p,n)Original native command in the exact edition
  2. L15
    specialize divisor_signed_sum_to_components (F)
  3. L16
    specialize divisor_signed_sum_to_components (pb)
  4. L17
    specialize divisor_signed_sum_to_components (pc)
  5. L18
    specialize divisor_signed_sum_to_components (nb)
  6. L19
    specialize divisor_signed_sum_to_components (nc)
  7. L20
    specialize divisor_signed_sum_to_components (l)
  8. L21
    specialize divisor_signed_sum_to_components (a)
  9. L22
    apply divisor_signed_sum_to_components
  10. L23
    exact hF
04Use earlier factsL24–24

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

  1. L24
    exact hs
05Separate the logical casesL25–28

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

  1. L25
    cases hparts
  2. L26
    cases hparts_witness
  3. L27
    cases hparts_witness_witness
  4. L28
    cases hparts_witness_witness_right
06Use earlier factsL29–38

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

  1. L29
    specialize divisor_signed_sum_from_components (G)
  2. L30
    specialize divisor_signed_sum_from_components (nb)
  3. L31
    specialize divisor_signed_sum_from_components (nc)
  4. L32
    specialize divisor_signed_sum_from_components (pb)
  5. L33
    specialize divisor_signed_sum_from_components (pc)
  6. L34
    specialize divisor_signed_sum_from_components (l)
  7. L35
    specialize divisor_signed_sum_from_components (x1)
  8. L36
    specialize divisor_signed_sum_from_components (x)
  9. L37
    specialize divisor_signed_sum_from_components (b)
  10. L38
    apply divisor_signed_sum_from_components
07Use earlier factsL39–48

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

  1. L39
    exact hG
  2. L40
    exact hparts_witness_witness_right_left
  3. L41
    exact hparts_witness_witness_left
  4. L42
    specialize divisor_signed_balance_negate (a)
  5. L43
    specialize divisor_signed_balance_negate (b)
  6. L44
    specialize divisor_signed_balance_negate (x)
  7. L45
    specialize divisor_signed_balance_negate (x1)
  8. L46
    apply divisor_signed_balance_negate
  9. L47
    exact hparts_witness_witness_right_right
  10. L48
    exact hn

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro F
  2. 0002intro G
  3. 0003intro pb
  4. 0004intro pc
  5. 0005intro nb
  6. 0006intro nc
  7. 0007intro l
  8. 0008intro a
  9. 0009intro b
  10. 0010intro hF
  11. 0011intro hG
  12. 0012intro hs
  13. 0013intro hn
  14. 0014have hparts : ∃ p. ∃ n. Sum(pb,pc,l,p) ∧ (Sum(nb,nc,l,n) ∧ SignedBalance(a,p,n))
  15. 0015specialize divisor_signed_sum_to_components (F)
  16. 0016specialize divisor_signed_sum_to_components (pb)
  17. 0017specialize divisor_signed_sum_to_components (pc)
  18. 0018specialize divisor_signed_sum_to_components (nb)
  19. 0019specialize divisor_signed_sum_to_components (nc)
  20. 0020specialize divisor_signed_sum_to_components (l)
  21. 0021specialize divisor_signed_sum_to_components (a)
  22. 0022apply divisor_signed_sum_to_components
  23. 0023exact hF
  24. 0024exact hs
  25. 0025cases hparts
  26. 0026cases hparts_witness
  27. 0027cases hparts_witness_witness
  28. 0028cases hparts_witness_witness_right
  29. 0029specialize divisor_signed_sum_from_components (G)
  30. 0030specialize divisor_signed_sum_from_components (nb)
  31. 0031specialize divisor_signed_sum_from_components (nc)
  32. 0032specialize divisor_signed_sum_from_components (pb)
  33. 0033specialize divisor_signed_sum_from_components (pc)
  34. 0034specialize divisor_signed_sum_from_components (l)
  35. 0035specialize divisor_signed_sum_from_components (x1)
  36. 0036specialize divisor_signed_sum_from_components (x)
  37. 0037specialize divisor_signed_sum_from_components (b)
  38. 0038apply divisor_signed_sum_from_components
  39. 0039exact hG
  40. 0040exact hparts_witness_witness_right_left
  41. 0041exact hparts_witness_witness_left
  42. 0042specialize divisor_signed_balance_negate (a)
  43. 0043specialize divisor_signed_balance_negate (b)
  44. 0044specialize divisor_signed_balance_negate (x)
  45. 0045specialize divisor_signed_balance_negate (x1)
  46. 0046apply divisor_signed_balance_negate
  47. 0047exact hparts_witness_witness_right_right
  48. 0048exact hn