DU0006

dirichlet_kronecker_delta_table_append

Append the separately chosen actual delta value, preserving every earlier signed entry rather than assuming a table oracle.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Signed one is code 2. Positive-only table graphs preserve arbitrary zeroth values, including N=0. The unit and divisor-sum identities are proved, never embedded in definitions. The separate inverse family proves the general unit-at-one criterion; multiplicative-function closure remains open.

Exact theorem in conservative defined notation

∀ N. ∀ E. ∀ z. KroneckerDeltaTable(N,E) → (S N = 1 → z = 2) ∧ (¬S N = 1 → z = 0) → ∃ x. KroneckerDeltaTable(S N,x) ∧ (∀ y. ∀ n. ∀ m. Lt(y,S N) → ArithAt(E,y,n) → ArithAt(x,y,m) → n = m)

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

Definition DAG

ArithTable(N,F) · 1ArithAt(F,i,z) · 6KroneckerDeltaTable(N,E) · 2Le(a,b) · 1Lt(a,b) · 3

Actual proof prerequisites

arithmetic_signed_table_append · checked external prerequisitele_eq_or_lt · checked external prerequisitedivisor_signed_table_at_functional · checked external prerequisitele_of_succ_le_succ · checked external prerequisitedivisor_signed_table_lookup · checked external prerequisite
Original expanded first-order statement 
forall N E z. (((exists dst_positive_code_delta_append_inputtable dst_positive_scale_delta_append_inputtable dst_negative_code_delta_append_inputtable dst_negative_scale_delta_append_inputtable. (((E) = (((((dst_positive_code_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable)) * S ((dst_positive_code_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable)) + ((dst_positive_scale_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable))) + (((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) * S ((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) + ((dst_negative_scale_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)))) * S ((((dst_positive_code_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable)) * S ((dst_positive_code_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable)) + ((dst_positive_scale_delta_append_inputtable) + (dst_positive_scale_delta_append_inputtable))) + (((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) * S ((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) + ((dst_negative_scale_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)))) + ((((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) * S ((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) + ((dst_negative_scale_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable))) + (((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) * S ((dst_negative_code_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)) + ((dst_negative_scale_delta_append_inputtable) + (dst_negative_scale_delta_append_inputtable)))))) /\ (forall dst_index_delta_append_inputtable. (exists pvs_le_gap_delta_append_inputtabledomain. pvs_le_gap_delta_append_inputtabledomain + (dst_index_delta_append_inputtable) = (N)) -> exists dst_positive_delta_append_inputtable dst_negative_delta_append_inputtable dst_value_delta_append_inputtable. ((((exists ff_h_pvs_delta_append_inputtableentrypositive. ff_h_pvs_delta_append_inputtableentrypositive + S (dst_positive_delta_append_inputtable) = S ((S (dst_index_delta_append_inputtable)) * dst_positive_scale_delta_append_inputtable)) /\ exists ff_q_pvs_delta_append_inputtableentrypositive. dst_positive_code_delta_append_inputtable = ff_q_pvs_delta_append_inputtableentrypositive * S ((S (dst_index_delta_append_inputtable)) * dst_positive_scale_delta_append_inputtable) + (dst_positive_delta_append_inputtable))) /\ (((((exists ff_h_pvs_delta_append_inputtableentrynegative. ff_h_pvs_delta_append_inputtableentrynegative + S (dst_negative_delta_append_inputtable) = S ((S (dst_index_delta_append_inputtable)) * dst_negative_scale_delta_append_inputtable)) /\ exists ff_q_pvs_delta_append_inputtableentrynegative. dst_negative_code_delta_append_inputtable = ff_q_pvs_delta_append_inputtableentrynegative * S ((S (dst_index_delta_append_inputtable)) * dst_negative_scale_delta_append_inputtable) + (dst_negative_delta_append_inputtable))) /\ (exists ge_balance_positive_delta_append_inputtableentryvalue ge_balance_negative_delta_append_inputtableentryvalue. (((((dst_value_delta_append_inputtable) = 2 * (ge_balance_positive_delta_append_inputtableentryvalue) /\ (ge_balance_negative_delta_append_inputtableentryvalue) = 0) \/ exists ge_signed_half_delta_append_inputtableentryvaluedecode. (((dst_value_delta_append_inputtable) = 2 * ge_signed_half_delta_append_inputtableentryvaluedecode + 1 /\ (ge_balance_positive_delta_append_inputtableentryvalue) = 0) /\ (ge_balance_negative_delta_append_inputtableentryvalue) = S ge_signed_half_delta_append_inputtableentryvaluedecode))) /\ ((dst_positive_delta_append_inputtable) + ge_balance_negative_delta_append_inputtableentryvalue = (dst_negative_delta_append_inputtable) + ge_balance_positive_delta_append_inputtableentryvalue))))))))) /\ (forall du_index_delta_append_input du_value_delta_append_input. ~(du_index_delta_append_input=0) -> (exists pvs_le_gap_delta_append_inputbound. pvs_le_gap_delta_append_inputbound + (du_index_delta_append_input) = (N)) -> (exists dst_positive_code_delta_append_inputentry dst_positive_scale_delta_append_inputentry dst_negative_code_delta_append_inputentry dst_negative_scale_delta_append_inputentry dst_positive_delta_append_inputentry dst_negative_delta_append_inputentry. (((E) = (((((dst_positive_code_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry)) * S ((dst_positive_code_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry)) + ((dst_positive_scale_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry))) + (((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) * S ((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) + ((dst_negative_scale_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)))) * S ((((dst_positive_code_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry)) * S ((dst_positive_code_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry)) + ((dst_positive_scale_delta_append_inputentry) + (dst_positive_scale_delta_append_inputentry))) + (((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) * S ((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) + ((dst_negative_scale_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)))) + ((((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) * S ((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) + ((dst_negative_scale_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry))) + (((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) * S ((dst_negative_code_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)) + ((dst_negative_scale_delta_append_inputentry) + (dst_negative_scale_delta_append_inputentry)))))) /\ (((((exists ff_h_pvs_delta_append_inputentrypositive. ff_h_pvs_delta_append_inputentrypositive + S (dst_positive_delta_append_inputentry) = S ((S (du_index_delta_append_input)) * dst_positive_scale_delta_append_inputentry)) /\ exists ff_q_pvs_delta_append_inputentrypositive. dst_positive_code_delta_append_inputentry = ff_q_pvs_delta_append_inputentrypositive * S ((S (du_index_delta_append_input)) * dst_positive_scale_delta_append_inputentry) + (dst_positive_delta_append_inputentry))) /\ (((((exists ff_h_pvs_delta_append_inputentrynegative. ff_h_pvs_delta_append_inputentrynegative + S (dst_negative_delta_append_inputentry) = S ((S (du_index_delta_append_input)) * dst_negative_scale_delta_append_inputentry)) /\ exists ff_q_pvs_delta_append_inputentrynegative. dst_negative_code_delta_append_inputentry = ff_q_pvs_delta_append_inputentrynegative * S ((S (du_index_delta_append_input)) * dst_negative_scale_delta_append_inputentry) + (dst_negative_delta_append_inputentry))) /\ (exists ge_balance_positive_delta_append_inputentryvalue ge_balance_negative_delta_append_inputentryvalue. (((((du_value_delta_append_input) = 2 * (ge_balance_positive_delta_append_inputentryvalue) /\ (ge_balance_negative_delta_append_inputentryvalue) = 0) \/ exists ge_signed_half_delta_append_inputentryvaluedecode. (((du_value_delta_append_input) = 2 * ge_signed_half_delta_append_inputentryvaluedecode + 1 /\ (ge_balance_positive_delta_append_inputentryvalue) = 0) /\ (ge_balance_negative_delta_append_inputentryvalue) = S ge_signed_half_delta_append_inputentryvaluedecode))) /\ ((dst_positive_delta_append_inputentry) + ge_balance_negative_delta_append_inputentryvalue = (dst_negative_delta_append_inputentry) + ge_balance_positive_delta_append_inputentryvalue))))))))) -> ((((du_index_delta_append_input)=1 -> (du_value_delta_append_input)=2) /\ (~((du_index_delta_append_input)=1) -> (du_value_delta_append_input)=0)))))) -> ((((S N)=1 -> (z)=2) /\ (~((S N)=1) -> (z)=0))) -> exists D. (((exists dst_positive_code_delta_append_outputtable dst_positive_scale_delta_append_outputtable dst_negative_code_delta_append_outputtable dst_negative_scale_delta_append_outputtable. (((D) = (((((dst_positive_code_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable)) * S ((dst_positive_code_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable)) + ((dst_positive_scale_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable))) + (((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) * S ((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) + ((dst_negative_scale_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)))) * S ((((dst_positive_code_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable)) * S ((dst_positive_code_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable)) + ((dst_positive_scale_delta_append_outputtable) + (dst_positive_scale_delta_append_outputtable))) + (((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) * S ((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) + ((dst_negative_scale_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)))) + ((((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) * S ((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) + ((dst_negative_scale_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable))) + (((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) * S ((dst_negative_code_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)) + ((dst_negative_scale_delta_append_outputtable) + (dst_negative_scale_delta_append_outputtable)))))) /\ (forall dst_index_delta_append_outputtable. (exists pvs_le_gap_delta_append_outputtabledomain. pvs_le_gap_delta_append_outputtabledomain + (dst_index_delta_append_outputtable) = (S N)) -> exists dst_positive_delta_append_outputtable dst_negative_delta_append_outputtable dst_value_delta_append_outputtable. ((((exists ff_h_pvs_delta_append_outputtableentrypositive. ff_h_pvs_delta_append_outputtableentrypositive + S (dst_positive_delta_append_outputtable) = S ((S (dst_index_delta_append_outputtable)) * dst_positive_scale_delta_append_outputtable)) /\ exists ff_q_pvs_delta_append_outputtableentrypositive. dst_positive_code_delta_append_outputtable = ff_q_pvs_delta_append_outputtableentrypositive * S ((S (dst_index_delta_append_outputtable)) * dst_positive_scale_delta_append_outputtable) + (dst_positive_delta_append_outputtable))) /\ (((((exists ff_h_pvs_delta_append_outputtableentrynegative. ff_h_pvs_delta_append_outputtableentrynegative + S (dst_negative_delta_append_outputtable) = S ((S (dst_index_delta_append_outputtable)) * dst_negative_scale_delta_append_outputtable)) /\ exists ff_q_pvs_delta_append_outputtableentrynegative. dst_negative_code_delta_append_outputtable = ff_q_pvs_delta_append_outputtableentrynegative * S ((S (dst_index_delta_append_outputtable)) * dst_negative_scale_delta_append_outputtable) + (dst_negative_delta_append_outputtable))) /\ (exists ge_balance_positive_delta_append_outputtableentryvalue ge_balance_negative_delta_append_outputtableentryvalue. (((((dst_value_delta_append_outputtable) = 2 * (ge_balance_positive_delta_append_outputtableentryvalue) /\ (ge_balance_negative_delta_append_outputtableentryvalue) = 0) \/ exists ge_signed_half_delta_append_outputtableentryvaluedecode. (((dst_value_delta_append_outputtable) = 2 * ge_signed_half_delta_append_outputtableentryvaluedecode + 1 /\ (ge_balance_positive_delta_append_outputtableentryvalue) = 0) /\ (ge_balance_negative_delta_append_outputtableentryvalue) = S ge_signed_half_delta_append_outputtableentryvaluedecode))) /\ ((dst_positive_delta_append_outputtable) + ge_balance_negative_delta_append_outputtableentryvalue = (dst_negative_delta_append_outputtable) + ge_balance_positive_delta_append_outputtableentryvalue))))))))) /\ (forall du_index_delta_append_output du_value_delta_append_output. ~(du_index_delta_append_output=0) -> (exists pvs_le_gap_delta_append_outputbound. pvs_le_gap_delta_append_outputbound + (du_index_delta_append_output) = (S N)) -> (exists dst_positive_code_delta_append_outputentry dst_positive_scale_delta_append_outputentry dst_negative_code_delta_append_outputentry dst_negative_scale_delta_append_outputentry dst_positive_delta_append_outputentry dst_negative_delta_append_outputentry. (((D) = (((((dst_positive_code_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry)) * S ((dst_positive_code_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry)) + ((dst_positive_scale_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry))) + (((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) * S ((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) + ((dst_negative_scale_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)))) * S ((((dst_positive_code_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry)) * S ((dst_positive_code_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry)) + ((dst_positive_scale_delta_append_outputentry) + (dst_positive_scale_delta_append_outputentry))) + (((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) * S ((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) + ((dst_negative_scale_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)))) + ((((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) * S ((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) + ((dst_negative_scale_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry))) + (((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) * S ((dst_negative_code_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)) + ((dst_negative_scale_delta_append_outputentry) + (dst_negative_scale_delta_append_outputentry)))))) /\ (((((exists ff_h_pvs_delta_append_outputentrypositive. ff_h_pvs_delta_append_outputentrypositive + S (dst_positive_delta_append_outputentry) = S ((S (du_index_delta_append_output)) * dst_positive_scale_delta_append_outputentry)) /\ exists ff_q_pvs_delta_append_outputentrypositive. dst_positive_code_delta_append_outputentry = ff_q_pvs_delta_append_outputentrypositive * S ((S (du_index_delta_append_output)) * dst_positive_scale_delta_append_outputentry) + (dst_positive_delta_append_outputentry))) /\ (((((exists ff_h_pvs_delta_append_outputentrynegative. ff_h_pvs_delta_append_outputentrynegative + S (dst_negative_delta_append_outputentry) = S ((S (du_index_delta_append_output)) * dst_negative_scale_delta_append_outputentry)) /\ exists ff_q_pvs_delta_append_outputentrynegative. dst_negative_code_delta_append_outputentry = ff_q_pvs_delta_append_outputentrynegative * S ((S (du_index_delta_append_output)) * dst_negative_scale_delta_append_outputentry) + (dst_negative_delta_append_outputentry))) /\ (exists ge_balance_positive_delta_append_outputentryvalue ge_balance_negative_delta_append_outputentryvalue. (((((du_value_delta_append_output) = 2 * (ge_balance_positive_delta_append_outputentryvalue) /\ (ge_balance_negative_delta_append_outputentryvalue) = 0) \/ exists ge_signed_half_delta_append_outputentryvaluedecode. (((du_value_delta_append_output) = 2 * ge_signed_half_delta_append_outputentryvaluedecode + 1 /\ (ge_balance_positive_delta_append_outputentryvalue) = 0) /\ (ge_balance_negative_delta_append_outputentryvalue) = S ge_signed_half_delta_append_outputentryvaluedecode))) /\ ((dst_positive_delta_append_outputentry) + ge_balance_negative_delta_append_outputentryvalue = (dst_negative_delta_append_outputentry) + ge_balance_positive_delta_append_outputentryvalue))))))))) -> ((((du_index_delta_append_output)=1 -> (du_value_delta_append_output)=2) /\ (~((du_index_delta_append_output)=1) -> (du_value_delta_append_output)=0)))))) /\ (forall dst_index_delta_append_prefix dst_first_delta_append_prefix dst_second_delta_append_prefix. (exists pvs_gap_delta_append_prefixbound. pvs_gap_delta_append_prefixbound + S (dst_index_delta_append_prefix) = (S N)) -> (exists dst_positive_code_delta_append_prefixfirst dst_positive_scale_delta_append_prefixfirst dst_negative_code_delta_append_prefixfirst dst_negative_scale_delta_append_prefixfirst dst_positive_delta_append_prefixfirst dst_negative_delta_append_prefixfirst. (((E) = (((((dst_positive_code_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst)) * S ((dst_positive_code_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst)) + ((dst_positive_scale_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst))) + (((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) * S ((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) + ((dst_negative_scale_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)))) * S ((((dst_positive_code_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst)) * S ((dst_positive_code_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst)) + ((dst_positive_scale_delta_append_prefixfirst) + (dst_positive_scale_delta_append_prefixfirst))) + (((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) * S ((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) + ((dst_negative_scale_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)))) + ((((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) * S ((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) + ((dst_negative_scale_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst))) + (((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) * S ((dst_negative_code_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)) + ((dst_negative_scale_delta_append_prefixfirst) + (dst_negative_scale_delta_append_prefixfirst)))))) /\ (((((exists ff_h_pvs_delta_append_prefixfirstpositive. ff_h_pvs_delta_append_prefixfirstpositive + S (dst_positive_delta_append_prefixfirst) = S ((S (dst_index_delta_append_prefix)) * dst_positive_scale_delta_append_prefixfirst)) /\ exists ff_q_pvs_delta_append_prefixfirstpositive. dst_positive_code_delta_append_prefixfirst = ff_q_pvs_delta_append_prefixfirstpositive * S ((S (dst_index_delta_append_prefix)) * dst_positive_scale_delta_append_prefixfirst) + (dst_positive_delta_append_prefixfirst))) /\ (((((exists ff_h_pvs_delta_append_prefixfirstnegative. ff_h_pvs_delta_append_prefixfirstnegative + S (dst_negative_delta_append_prefixfirst) = S ((S (dst_index_delta_append_prefix)) * dst_negative_scale_delta_append_prefixfirst)) /\ exists ff_q_pvs_delta_append_prefixfirstnegative. dst_negative_code_delta_append_prefixfirst = ff_q_pvs_delta_append_prefixfirstnegative * S ((S (dst_index_delta_append_prefix)) * dst_negative_scale_delta_append_prefixfirst) + (dst_negative_delta_append_prefixfirst))) /\ (exists ge_balance_positive_delta_append_prefixfirstvalue ge_balance_negative_delta_append_prefixfirstvalue. (((((dst_first_delta_append_prefix) = 2 * (ge_balance_positive_delta_append_prefixfirstvalue) /\ (ge_balance_negative_delta_append_prefixfirstvalue) = 0) \/ exists ge_signed_half_delta_append_prefixfirstvaluedecode. (((dst_first_delta_append_prefix) = 2 * ge_signed_half_delta_append_prefixfirstvaluedecode + 1 /\ (ge_balance_positive_delta_append_prefixfirstvalue) = 0) /\ (ge_balance_negative_delta_append_prefixfirstvalue) = S ge_signed_half_delta_append_prefixfirstvaluedecode))) /\ ((dst_positive_delta_append_prefixfirst) + ge_balance_negative_delta_append_prefixfirstvalue = (dst_negative_delta_append_prefixfirst) + ge_balance_positive_delta_append_prefixfirstvalue))))))))) -> (exists dst_positive_code_delta_append_prefixsecond dst_positive_scale_delta_append_prefixsecond dst_negative_code_delta_append_prefixsecond dst_negative_scale_delta_append_prefixsecond dst_positive_delta_append_prefixsecond dst_negative_delta_append_prefixsecond. (((D) = (((((dst_positive_code_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond)) * S ((dst_positive_code_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond)) + ((dst_positive_scale_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond))) + (((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) * S ((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) + ((dst_negative_scale_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)))) * S ((((dst_positive_code_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond)) * S ((dst_positive_code_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond)) + ((dst_positive_scale_delta_append_prefixsecond) + (dst_positive_scale_delta_append_prefixsecond))) + (((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) * S ((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) + ((dst_negative_scale_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)))) + ((((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) * S ((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) + ((dst_negative_scale_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond))) + (((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) * S ((dst_negative_code_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)) + ((dst_negative_scale_delta_append_prefixsecond) + (dst_negative_scale_delta_append_prefixsecond)))))) /\ (((((exists ff_h_pvs_delta_append_prefixsecondpositive. ff_h_pvs_delta_append_prefixsecondpositive + S (dst_positive_delta_append_prefixsecond) = S ((S (dst_index_delta_append_prefix)) * dst_positive_scale_delta_append_prefixsecond)) /\ exists ff_q_pvs_delta_append_prefixsecondpositive. dst_positive_code_delta_append_prefixsecond = ff_q_pvs_delta_append_prefixsecondpositive * S ((S (dst_index_delta_append_prefix)) * dst_positive_scale_delta_append_prefixsecond) + (dst_positive_delta_append_prefixsecond))) /\ (((((exists ff_h_pvs_delta_append_prefixsecondnegative. ff_h_pvs_delta_append_prefixsecondnegative + S (dst_negative_delta_append_prefixsecond) = S ((S (dst_index_delta_append_prefix)) * dst_negative_scale_delta_append_prefixsecond)) /\ exists ff_q_pvs_delta_append_prefixsecondnegative. dst_negative_code_delta_append_prefixsecond = ff_q_pvs_delta_append_prefixsecondnegative * S ((S (dst_index_delta_append_prefix)) * dst_negative_scale_delta_append_prefixsecond) + (dst_negative_delta_append_prefixsecond))) /\ (exists ge_balance_positive_delta_append_prefixsecondvalue ge_balance_negative_delta_append_prefixsecondvalue. (((((dst_second_delta_append_prefix) = 2 * (ge_balance_positive_delta_append_prefixsecondvalue) /\ (ge_balance_negative_delta_append_prefixsecondvalue) = 0) \/ exists ge_signed_half_delta_append_prefixsecondvaluedecode. (((dst_second_delta_append_prefix) = 2 * ge_signed_half_delta_append_prefixsecondvaluedecode + 1 /\ (ge_balance_positive_delta_append_prefixsecondvalue) = 0) /\ (ge_balance_negative_delta_append_prefixsecondvalue) = S ge_signed_half_delta_append_prefixsecondvaluedecode))) /\ ((dst_positive_delta_append_prefixsecond) + ge_balance_negative_delta_append_prefixsecondvalue = (dst_negative_delta_append_prefixsecond) + ge_balance_positive_delta_append_prefixsecondvalue))))))))) -> dst_first_delta_append_prefix = dst_second_delta_append_prefix)

Complete tactic proof in conservative notation

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

77 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.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro z
  4. L4
    intro hf
  5. L5
    intro hz
02Separate the logical casesL6–6

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

  1. L6
    cases hf
03Establish hxL7–12

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

  1. L7
    have hx : ∃ G. ArithTable(S N,G) ∧ ((∀ x. ∀ y. ∀ n. Lt(x,S N) → ArithAt(F,x,y) → ArithAt(G,x,n) → y = n) ∧ ArithAt(G,S N,z))Definitions: ArithTable(S N,G)Lt(x,S N)ArithAt(F,x,y)ArithAt(G,x,n)ArithAt(G,S N,z)Original native command in the exact edition
  2. L8
    specialize arithmetic_signed_table_append (N)
  3. L9
    specialize arithmetic_signed_table_append (F)
  4. L10
    specialize arithmetic_signed_table_append (z)
  5. L11
    apply arithmetic_signed_table_append
  6. L12
    exact hf_left
04Separate the logical casesL13–15

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

  1. L13
    cases hx
  2. L14
    cases hx_witness
  3. L15
    cases hx_witness_right
05Construct an explicit witnessL16–16

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

  1. L16
    exists x
06Separate the logical casesL17–18

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

  1. L17
    split
  2. L18
    split
07Use earlier factsL19–19

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

  1. L19
    exact hx_witness_left
08Fix variables and assumptionsL20–24

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

  1. L20
    intro i
  2. L21
    intro a
  3. L22
    intro hi
  4. L23
    intro hb
  5. L24
    intro ha
09Establish hcL25–29

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

  1. L25
    have hc : i = S N ∨ Lt(i,S N)Definitions: Lt(i,S N)Original native command in the exact edition
  2. L26
    specialize le_eq_or_lt (i)
  3. L27
    specialize le_eq_or_lt (S N)
  4. L28
    apply le_eq_or_lt
  5. L29
    exact hb
10Separate the logical casesL30–30

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

  1. L30
    cases hc
11Calculate and transport equalitiesL31–34

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

  1. L31
    rewrite hc_left at ha
  2. L32
    rewrite hc_left at ha
  3. L33
    rewrite hc_left at ha
  4. L34
    rewrite hc_left at ha
12Establish hvL35–44

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table at functional.

  1. L35
    have hv : a=z
  2. L36
    specialize divisor_signed_table_at_functional (x)
  3. L37
    specialize divisor_signed_table_at_functional (S N)
  4. L38
    specialize divisor_signed_table_at_functional (a)
  5. L39
    specialize divisor_signed_table_at_functional (z)
  6. L40
    apply divisor_signed_table_at_functional
  7. L41
    exact ha
  8. L42
    exact hx_witness_right_right
  9. L43
    rewrite hc_left
  10. L44
    rewrite hc_left
13Calculate and transport equalitiesL45–46

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

  1. L45
    rewrite hv
  2. L46
    rewrite hv
14Use earlier factsL47–47

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

  1. L47
    exact hz
15Establish hibL48–52

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

  1. L48
  2. L49
    specialize le_of_succ_le_succ (i)
  3. L50
    specialize le_of_succ_le_succ (N)
  4. L51
    apply le_of_succ_le_succ
  5. L52
    exact hc_right
16Establish hvL53–59

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

  1. L53
    have hv : ∃ v. ArithAt(F,i,v)Definitions: ArithAt(F,i,v)Original native command in the exact edition
  2. L54
    specialize divisor_signed_table_lookup (N)
  3. L55
    specialize divisor_signed_table_lookup (F)
  4. L56
    specialize divisor_signed_table_lookup (i)
  5. L57
    apply divisor_signed_table_lookup
  6. L58
    exact hf_left
  7. L59
    exact hib
17Separate the logical casesL60–60

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

  1. L60
    cases hv
18Establish heqL61–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hx witness right left.

  1. L61
    have heq : x1=a
  2. L62
    specialize hx_witness_right_left (i)
  3. L63
    specialize hx_witness_right_left (x1)
  4. L64
    specialize hx_witness_right_left (a)
  5. L65
    apply hx_witness_right_left
  6. L66
    exact hc_right
  7. L67
    exact hv_witness
  8. L68
    exact ha
  9. L69
    rewrite heq at hv_witness
  10. L70
    rewrite heq at hv_witness
19Use earlier factsL71–77

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

  1. L71
    specialize hf_right (i)
  2. L72
    specialize hf_right (a)
  3. L73
    apply hf_right
  4. L74
    exact hi
  5. L75
    exact hib
  6. L76
    exact hv_witness
  7. L77
    exact hx_witness_right_left

Library-wide reading audit

Original defined command ledger · 77 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro z
  4. 0004intro hf
  5. 0005intro hz
  6. 0006cases hf
  7. 0007have hx : ∃ G. ArithTable(S N,G) ∧ ((∀ x. ∀ y. ∀ n. Lt(x,S N) → ArithAt(F,x,y) → ArithAt(G,x,n) → y = n) ∧ ArithAt(G,S N,z))
  8. 0008specialize arithmetic_signed_table_append (N)
  9. 0009specialize arithmetic_signed_table_append (F)
  10. 0010specialize arithmetic_signed_table_append (z)
  11. 0011apply arithmetic_signed_table_append
  12. 0012exact hf_left
  13. 0013cases hx
  14. 0014cases hx_witness
  15. 0015cases hx_witness_right
  16. 0016exists x
  17. 0017split
  18. 0018split
  19. 0019exact hx_witness_left
  20. 0020intro i
  21. 0021intro a
  22. 0022intro hi
  23. 0023intro hb
  24. 0024intro ha
  25. 0025have hc : i = S N ∨ Lt(i,S N)
  26. 0026specialize le_eq_or_lt (i)
  27. 0027specialize le_eq_or_lt (S N)
  28. 0028apply le_eq_or_lt
  29. 0029exact hb
  30. 0030cases hc
  31. 0031rewrite hc_left at ha
  32. 0032rewrite hc_left at ha
  33. 0033rewrite hc_left at ha
  34. 0034rewrite hc_left at ha
  35. 0035have hv : a=z
  36. 0036specialize divisor_signed_table_at_functional (x)
  37. 0037specialize divisor_signed_table_at_functional (S N)
  38. 0038specialize divisor_signed_table_at_functional (a)
  39. 0039specialize divisor_signed_table_at_functional (z)
  40. 0040apply divisor_signed_table_at_functional
  41. 0041exact ha
  42. 0042exact hx_witness_right_right
  43. 0043rewrite hc_left
  44. 0044rewrite hc_left
  45. 0045rewrite hv
  46. 0046rewrite hv
  47. 0047exact hz
  48. 0048have hib : Le(i,N)
  49. 0049specialize le_of_succ_le_succ (i)
  50. 0050specialize le_of_succ_le_succ (N)
  51. 0051apply le_of_succ_le_succ
  52. 0052exact hc_right
  53. 0053have hv : ∃ v. ArithAt(F,i,v)
  54. 0054specialize divisor_signed_table_lookup (N)
  55. 0055specialize divisor_signed_table_lookup (F)
  56. 0056specialize divisor_signed_table_lookup (i)
  57. 0057apply divisor_signed_table_lookup
  58. 0058exact hf_left
  59. 0059exact hib
  60. 0060cases hv
  61. 0061have heq : x1=a
  62. 0062specialize hx_witness_right_left (i)
  63. 0063specialize hx_witness_right_left (x1)
  64. 0064specialize hx_witness_right_left (a)
  65. 0065apply hx_witness_right_left
  66. 0066exact hc_right
  67. 0067exact hv_witness
  68. 0068exact ha
  69. 0069rewrite heq at hv_witness
  70. 0070rewrite heq at hv_witness
  71. 0071specialize hf_right (i)
  72. 0072specialize hf_right (a)
  73. 0073apply hf_right
  74. 0074exact hi
  75. 0075exact hib
  76. 0076exact hv_witness
  77. 0077exact hx_witness_right_left