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. ∀ F. ∀ G. KroneckerDeltaTable(N,F) → ArithTable(N,G) → ArithPositiveEqual(F,G,N) → KroneckerDeltaTable(N,G)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall N F G. (((exists dst_positive_code_kronecker_deltatransport_sourcetable dst_positive_scale_kronecker_deltatransport_sourcetable dst_negative_code_kronecker_deltatransport_sourcetable dst_negative_scale_kronecker_deltatransport_sourcetable. (((F) = (((((dst_positive_code_kronecker_deltatransport_sourcetable) + (dst_positive_scale_kronecker_deltatransport_sourcetable)) * S ((dst_positive_code_kronecker_deltatransport_sourcetable) + (dst_positive_scale_kronecker_deltatransport_sourcetable)) + ((dst_positive_scale_kronecker_deltatransport_sourcetable) + (dst_positive_scale_kronecker_deltatransport_sourcetable))) + (((dst_negative_code_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)) * S ((dst_negative_code_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)) + ((dst_negative_scale_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)))) * S ((((dst_positive_code_kronecker_deltatransport_sourcetable) + (dst_positive_scale_kronecker_deltatransport_sourcetable)) * S ((dst_positive_code_kronecker_deltatransport_sourcetable) + (dst_positive_scale_kronecker_deltatransport_sourcetable)) + ((dst_positive_scale_kronecker_deltatransport_sourcetable) + (dst_positive_scale_kronecker_deltatransport_sourcetable))) + (((dst_negative_code_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)) * S ((dst_negative_code_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)) + ((dst_negative_scale_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)))) + ((((dst_negative_code_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)) * S ((dst_negative_code_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)) + ((dst_negative_scale_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable))) + (((dst_negative_code_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)) * S ((dst_negative_code_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)) + ((dst_negative_scale_kronecker_deltatransport_sourcetable) + (dst_negative_scale_kronecker_deltatransport_sourcetable)))))) /\ (forall dst_index_kronecker_deltatransport_sourcetable. (exists pvs_le_gap_kronecker_deltatransport_sourcetabledomain. pvs_le_gap_kronecker_deltatransport_sourcetabledomain + (dst_index_kronecker_deltatransport_sourcetable) = (N)) -> exists dst_positive_kronecker_deltatransport_sourcetable dst_negative_kronecker_deltatransport_sourcetable dst_value_kronecker_deltatransport_sourcetable. ((((exists ff_h_pvs_kronecker_deltatransport_sourcetableentrypositive. ff_h_pvs_kronecker_deltatransport_sourcetableentrypositive + S (dst_positive_kronecker_deltatransport_sourcetable) = S ((S (dst_index_kronecker_deltatransport_sourcetable)) * dst_positive_scale_kronecker_deltatransport_sourcetable)) /\ exists ff_q_pvs_kronecker_deltatransport_sourcetableentrypositive. dst_positive_code_kronecker_deltatransport_sourcetable = ff_q_pvs_kronecker_deltatransport_sourcetableentrypositive * S ((S (dst_index_kronecker_deltatransport_sourcetable)) * dst_positive_scale_kronecker_deltatransport_sourcetable) + (dst_positive_kronecker_deltatransport_sourcetable))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_sourcetableentrynegative. ff_h_pvs_kronecker_deltatransport_sourcetableentrynegative + S (dst_negative_kronecker_deltatransport_sourcetable) = S ((S (dst_index_kronecker_deltatransport_sourcetable)) * dst_negative_scale_kronecker_deltatransport_sourcetable)) /\ exists ff_q_pvs_kronecker_deltatransport_sourcetableentrynegative. dst_negative_code_kronecker_deltatransport_sourcetable = ff_q_pvs_kronecker_deltatransport_sourcetableentrynegative * S ((S (dst_index_kronecker_deltatransport_sourcetable)) * dst_negative_scale_kronecker_deltatransport_sourcetable) + (dst_negative_kronecker_deltatransport_sourcetable))) /\ (exists ge_balance_positive_kronecker_deltatransport_sourcetableentryvalue ge_balance_negative_kronecker_deltatransport_sourcetableentryvalue. (((((dst_value_kronecker_deltatransport_sourcetable) = 2 * (ge_balance_positive_kronecker_deltatransport_sourcetableentryvalue) /\ (ge_balance_negative_kronecker_deltatransport_sourcetableentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltatransport_sourcetableentryvaluedecode. (((dst_value_kronecker_deltatransport_sourcetable) = 2 * ge_signed_half_kronecker_deltatransport_sourcetableentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltatransport_sourcetableentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltatransport_sourcetableentryvalue) = S ge_signed_half_kronecker_deltatransport_sourcetableentryvaluedecode))) /\ ((dst_positive_kronecker_deltatransport_sourcetable) + ge_balance_negative_kronecker_deltatransport_sourcetableentryvalue = (dst_negative_kronecker_deltatransport_sourcetable) + ge_balance_positive_kronecker_deltatransport_sourcetableentryvalue))))))))) /\ (forall du_index_kronecker_deltatransport_source du_value_kronecker_deltatransport_source. ~(du_index_kronecker_deltatransport_source=0) -> (exists pvs_le_gap_kronecker_deltatransport_sourcebound. pvs_le_gap_kronecker_deltatransport_sourcebound + (du_index_kronecker_deltatransport_source) = (N)) -> (exists dst_positive_code_kronecker_deltatransport_sourceentry dst_positive_scale_kronecker_deltatransport_sourceentry dst_negative_code_kronecker_deltatransport_sourceentry dst_negative_scale_kronecker_deltatransport_sourceentry dst_positive_kronecker_deltatransport_sourceentry dst_negative_kronecker_deltatransport_sourceentry. (((F) = (((((dst_positive_code_kronecker_deltatransport_sourceentry) + (dst_positive_scale_kronecker_deltatransport_sourceentry)) * S ((dst_positive_code_kronecker_deltatransport_sourceentry) + (dst_positive_scale_kronecker_deltatransport_sourceentry)) + ((dst_positive_scale_kronecker_deltatransport_sourceentry) + (dst_positive_scale_kronecker_deltatransport_sourceentry))) + (((dst_negative_code_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)) * S ((dst_negative_code_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)) + ((dst_negative_scale_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)))) * S ((((dst_positive_code_kronecker_deltatransport_sourceentry) + (dst_positive_scale_kronecker_deltatransport_sourceentry)) * S ((dst_positive_code_kronecker_deltatransport_sourceentry) + (dst_positive_scale_kronecker_deltatransport_sourceentry)) + ((dst_positive_scale_kronecker_deltatransport_sourceentry) + (dst_positive_scale_kronecker_deltatransport_sourceentry))) + (((dst_negative_code_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)) * S ((dst_negative_code_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)) + ((dst_negative_scale_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)))) + ((((dst_negative_code_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)) * S ((dst_negative_code_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)) + ((dst_negative_scale_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry))) + (((dst_negative_code_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)) * S ((dst_negative_code_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)) + ((dst_negative_scale_kronecker_deltatransport_sourceentry) + (dst_negative_scale_kronecker_deltatransport_sourceentry)))))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_sourceentrypositive. ff_h_pvs_kronecker_deltatransport_sourceentrypositive + S (dst_positive_kronecker_deltatransport_sourceentry) = S ((S (du_index_kronecker_deltatransport_source)) * dst_positive_scale_kronecker_deltatransport_sourceentry)) /\ exists ff_q_pvs_kronecker_deltatransport_sourceentrypositive. dst_positive_code_kronecker_deltatransport_sourceentry = ff_q_pvs_kronecker_deltatransport_sourceentrypositive * S ((S (du_index_kronecker_deltatransport_source)) * dst_positive_scale_kronecker_deltatransport_sourceentry) + (dst_positive_kronecker_deltatransport_sourceentry))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_sourceentrynegative. ff_h_pvs_kronecker_deltatransport_sourceentrynegative + S (dst_negative_kronecker_deltatransport_sourceentry) = S ((S (du_index_kronecker_deltatransport_source)) * dst_negative_scale_kronecker_deltatransport_sourceentry)) /\ exists ff_q_pvs_kronecker_deltatransport_sourceentrynegative. dst_negative_code_kronecker_deltatransport_sourceentry = ff_q_pvs_kronecker_deltatransport_sourceentrynegative * S ((S (du_index_kronecker_deltatransport_source)) * dst_negative_scale_kronecker_deltatransport_sourceentry) + (dst_negative_kronecker_deltatransport_sourceentry))) /\ (exists ge_balance_positive_kronecker_deltatransport_sourceentryvalue ge_balance_negative_kronecker_deltatransport_sourceentryvalue. (((((du_value_kronecker_deltatransport_source) = 2 * (ge_balance_positive_kronecker_deltatransport_sourceentryvalue) /\ (ge_balance_negative_kronecker_deltatransport_sourceentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltatransport_sourceentryvaluedecode. (((du_value_kronecker_deltatransport_source) = 2 * ge_signed_half_kronecker_deltatransport_sourceentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltatransport_sourceentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltatransport_sourceentryvalue) = S ge_signed_half_kronecker_deltatransport_sourceentryvaluedecode))) /\ ((dst_positive_kronecker_deltatransport_sourceentry) + ge_balance_negative_kronecker_deltatransport_sourceentryvalue = (dst_negative_kronecker_deltatransport_sourceentry) + ge_balance_positive_kronecker_deltatransport_sourceentryvalue))))))))) -> ((((du_index_kronecker_deltatransport_source)=1 -> (du_value_kronecker_deltatransport_source)=2) /\ (~((du_index_kronecker_deltatransport_source)=1) -> (du_value_kronecker_deltatransport_source)=0)))))) -> (exists dst_positive_code_kronecker_deltatransport_valid dst_positive_scale_kronecker_deltatransport_valid dst_negative_code_kronecker_deltatransport_valid dst_negative_scale_kronecker_deltatransport_valid. (((G) = (((((dst_positive_code_kronecker_deltatransport_valid) + (dst_positive_scale_kronecker_deltatransport_valid)) * S ((dst_positive_code_kronecker_deltatransport_valid) + (dst_positive_scale_kronecker_deltatransport_valid)) + ((dst_positive_scale_kronecker_deltatransport_valid) + (dst_positive_scale_kronecker_deltatransport_valid))) + (((dst_negative_code_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)) * S ((dst_negative_code_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)) + ((dst_negative_scale_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)))) * S ((((dst_positive_code_kronecker_deltatransport_valid) + (dst_positive_scale_kronecker_deltatransport_valid)) * S ((dst_positive_code_kronecker_deltatransport_valid) + (dst_positive_scale_kronecker_deltatransport_valid)) + ((dst_positive_scale_kronecker_deltatransport_valid) + (dst_positive_scale_kronecker_deltatransport_valid))) + (((dst_negative_code_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)) * S ((dst_negative_code_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)) + ((dst_negative_scale_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)))) + ((((dst_negative_code_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)) * S ((dst_negative_code_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)) + ((dst_negative_scale_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid))) + (((dst_negative_code_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)) * S ((dst_negative_code_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)) + ((dst_negative_scale_kronecker_deltatransport_valid) + (dst_negative_scale_kronecker_deltatransport_valid)))))) /\ (forall dst_index_kronecker_deltatransport_valid. (exists pvs_le_gap_kronecker_deltatransport_validdomain. pvs_le_gap_kronecker_deltatransport_validdomain + (dst_index_kronecker_deltatransport_valid) = (N)) -> exists dst_positive_kronecker_deltatransport_valid dst_negative_kronecker_deltatransport_valid dst_value_kronecker_deltatransport_valid. ((((exists ff_h_pvs_kronecker_deltatransport_validentrypositive. ff_h_pvs_kronecker_deltatransport_validentrypositive + S (dst_positive_kronecker_deltatransport_valid) = S ((S (dst_index_kronecker_deltatransport_valid)) * dst_positive_scale_kronecker_deltatransport_valid)) /\ exists ff_q_pvs_kronecker_deltatransport_validentrypositive. dst_positive_code_kronecker_deltatransport_valid = ff_q_pvs_kronecker_deltatransport_validentrypositive * S ((S (dst_index_kronecker_deltatransport_valid)) * dst_positive_scale_kronecker_deltatransport_valid) + (dst_positive_kronecker_deltatransport_valid))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_validentrynegative. ff_h_pvs_kronecker_deltatransport_validentrynegative + S (dst_negative_kronecker_deltatransport_valid) = S ((S (dst_index_kronecker_deltatransport_valid)) * dst_negative_scale_kronecker_deltatransport_valid)) /\ exists ff_q_pvs_kronecker_deltatransport_validentrynegative. dst_negative_code_kronecker_deltatransport_valid = ff_q_pvs_kronecker_deltatransport_validentrynegative * S ((S (dst_index_kronecker_deltatransport_valid)) * dst_negative_scale_kronecker_deltatransport_valid) + (dst_negative_kronecker_deltatransport_valid))) /\ (exists ge_balance_positive_kronecker_deltatransport_validentryvalue ge_balance_negative_kronecker_deltatransport_validentryvalue. (((((dst_value_kronecker_deltatransport_valid) = 2 * (ge_balance_positive_kronecker_deltatransport_validentryvalue) /\ (ge_balance_negative_kronecker_deltatransport_validentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltatransport_validentryvaluedecode. (((dst_value_kronecker_deltatransport_valid) = 2 * ge_signed_half_kronecker_deltatransport_validentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltatransport_validentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltatransport_validentryvalue) = S ge_signed_half_kronecker_deltatransport_validentryvaluedecode))) /\ ((dst_positive_kronecker_deltatransport_valid) + ge_balance_negative_kronecker_deltatransport_validentryvalue = (dst_negative_kronecker_deltatransport_valid) + ge_balance_positive_kronecker_deltatransport_validentryvalue))))))))) -> (forall dm_index_kronecker_deltatransport_equal dm_first_value_kronecker_deltatransport_equal dm_second_value_kronecker_deltatransport_equal. ~(dm_index_kronecker_deltatransport_equal=0) -> (exists pvs_le_gap_kronecker_deltatransport_equaldomain. pvs_le_gap_kronecker_deltatransport_equaldomain + (dm_index_kronecker_deltatransport_equal) = (N)) -> (exists dst_positive_code_kronecker_deltatransport_equalfirst dst_positive_scale_kronecker_deltatransport_equalfirst dst_negative_code_kronecker_deltatransport_equalfirst dst_negative_scale_kronecker_deltatransport_equalfirst dst_positive_kronecker_deltatransport_equalfirst dst_negative_kronecker_deltatransport_equalfirst. (((F) = (((((dst_positive_code_kronecker_deltatransport_equalfirst) + (dst_positive_scale_kronecker_deltatransport_equalfirst)) * S ((dst_positive_code_kronecker_deltatransport_equalfirst) + (dst_positive_scale_kronecker_deltatransport_equalfirst)) + ((dst_positive_scale_kronecker_deltatransport_equalfirst) + (dst_positive_scale_kronecker_deltatransport_equalfirst))) + (((dst_negative_code_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)) * S ((dst_negative_code_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)) + ((dst_negative_scale_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)))) * S ((((dst_positive_code_kronecker_deltatransport_equalfirst) + (dst_positive_scale_kronecker_deltatransport_equalfirst)) * S ((dst_positive_code_kronecker_deltatransport_equalfirst) + (dst_positive_scale_kronecker_deltatransport_equalfirst)) + ((dst_positive_scale_kronecker_deltatransport_equalfirst) + (dst_positive_scale_kronecker_deltatransport_equalfirst))) + (((dst_negative_code_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)) * S ((dst_negative_code_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)) + ((dst_negative_scale_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)))) + ((((dst_negative_code_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)) * S ((dst_negative_code_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)) + ((dst_negative_scale_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst))) + (((dst_negative_code_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)) * S ((dst_negative_code_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)) + ((dst_negative_scale_kronecker_deltatransport_equalfirst) + (dst_negative_scale_kronecker_deltatransport_equalfirst)))))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_equalfirstpositive. ff_h_pvs_kronecker_deltatransport_equalfirstpositive + S (dst_positive_kronecker_deltatransport_equalfirst) = S ((S (dm_index_kronecker_deltatransport_equal)) * dst_positive_scale_kronecker_deltatransport_equalfirst)) /\ exists ff_q_pvs_kronecker_deltatransport_equalfirstpositive. dst_positive_code_kronecker_deltatransport_equalfirst = ff_q_pvs_kronecker_deltatransport_equalfirstpositive * S ((S (dm_index_kronecker_deltatransport_equal)) * dst_positive_scale_kronecker_deltatransport_equalfirst) + (dst_positive_kronecker_deltatransport_equalfirst))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_equalfirstnegative. ff_h_pvs_kronecker_deltatransport_equalfirstnegative + S (dst_negative_kronecker_deltatransport_equalfirst) = S ((S (dm_index_kronecker_deltatransport_equal)) * dst_negative_scale_kronecker_deltatransport_equalfirst)) /\ exists ff_q_pvs_kronecker_deltatransport_equalfirstnegative. dst_negative_code_kronecker_deltatransport_equalfirst = ff_q_pvs_kronecker_deltatransport_equalfirstnegative * S ((S (dm_index_kronecker_deltatransport_equal)) * dst_negative_scale_kronecker_deltatransport_equalfirst) + (dst_negative_kronecker_deltatransport_equalfirst))) /\ (exists ge_balance_positive_kronecker_deltatransport_equalfirstvalue ge_balance_negative_kronecker_deltatransport_equalfirstvalue. (((((dm_first_value_kronecker_deltatransport_equal) = 2 * (ge_balance_positive_kronecker_deltatransport_equalfirstvalue) /\ (ge_balance_negative_kronecker_deltatransport_equalfirstvalue) = 0) \/ exists ge_signed_half_kronecker_deltatransport_equalfirstvaluedecode. (((dm_first_value_kronecker_deltatransport_equal) = 2 * ge_signed_half_kronecker_deltatransport_equalfirstvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltatransport_equalfirstvalue) = 0) /\ (ge_balance_negative_kronecker_deltatransport_equalfirstvalue) = S ge_signed_half_kronecker_deltatransport_equalfirstvaluedecode))) /\ ((dst_positive_kronecker_deltatransport_equalfirst) + ge_balance_negative_kronecker_deltatransport_equalfirstvalue = (dst_negative_kronecker_deltatransport_equalfirst) + ge_balance_positive_kronecker_deltatransport_equalfirstvalue))))))))) -> (exists dst_positive_code_kronecker_deltatransport_equalsecond dst_positive_scale_kronecker_deltatransport_equalsecond dst_negative_code_kronecker_deltatransport_equalsecond dst_negative_scale_kronecker_deltatransport_equalsecond dst_positive_kronecker_deltatransport_equalsecond dst_negative_kronecker_deltatransport_equalsecond. (((G) = (((((dst_positive_code_kronecker_deltatransport_equalsecond) + (dst_positive_scale_kronecker_deltatransport_equalsecond)) * S ((dst_positive_code_kronecker_deltatransport_equalsecond) + (dst_positive_scale_kronecker_deltatransport_equalsecond)) + ((dst_positive_scale_kronecker_deltatransport_equalsecond) + (dst_positive_scale_kronecker_deltatransport_equalsecond))) + (((dst_negative_code_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)) * S ((dst_negative_code_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)) + ((dst_negative_scale_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)))) * S ((((dst_positive_code_kronecker_deltatransport_equalsecond) + (dst_positive_scale_kronecker_deltatransport_equalsecond)) * S ((dst_positive_code_kronecker_deltatransport_equalsecond) + (dst_positive_scale_kronecker_deltatransport_equalsecond)) + ((dst_positive_scale_kronecker_deltatransport_equalsecond) + (dst_positive_scale_kronecker_deltatransport_equalsecond))) + (((dst_negative_code_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)) * S ((dst_negative_code_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)) + ((dst_negative_scale_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)))) + ((((dst_negative_code_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)) * S ((dst_negative_code_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)) + ((dst_negative_scale_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond))) + (((dst_negative_code_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)) * S ((dst_negative_code_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)) + ((dst_negative_scale_kronecker_deltatransport_equalsecond) + (dst_negative_scale_kronecker_deltatransport_equalsecond)))))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_equalsecondpositive. ff_h_pvs_kronecker_deltatransport_equalsecondpositive + S (dst_positive_kronecker_deltatransport_equalsecond) = S ((S (dm_index_kronecker_deltatransport_equal)) * dst_positive_scale_kronecker_deltatransport_equalsecond)) /\ exists ff_q_pvs_kronecker_deltatransport_equalsecondpositive. dst_positive_code_kronecker_deltatransport_equalsecond = ff_q_pvs_kronecker_deltatransport_equalsecondpositive * S ((S (dm_index_kronecker_deltatransport_equal)) * dst_positive_scale_kronecker_deltatransport_equalsecond) + (dst_positive_kronecker_deltatransport_equalsecond))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_equalsecondnegative. ff_h_pvs_kronecker_deltatransport_equalsecondnegative + S (dst_negative_kronecker_deltatransport_equalsecond) = S ((S (dm_index_kronecker_deltatransport_equal)) * dst_negative_scale_kronecker_deltatransport_equalsecond)) /\ exists ff_q_pvs_kronecker_deltatransport_equalsecondnegative. dst_negative_code_kronecker_deltatransport_equalsecond = ff_q_pvs_kronecker_deltatransport_equalsecondnegative * S ((S (dm_index_kronecker_deltatransport_equal)) * dst_negative_scale_kronecker_deltatransport_equalsecond) + (dst_negative_kronecker_deltatransport_equalsecond))) /\ (exists ge_balance_positive_kronecker_deltatransport_equalsecondvalue ge_balance_negative_kronecker_deltatransport_equalsecondvalue. (((((dm_second_value_kronecker_deltatransport_equal) = 2 * (ge_balance_positive_kronecker_deltatransport_equalsecondvalue) /\ (ge_balance_negative_kronecker_deltatransport_equalsecondvalue) = 0) \/ exists ge_signed_half_kronecker_deltatransport_equalsecondvaluedecode. (((dm_second_value_kronecker_deltatransport_equal) = 2 * ge_signed_half_kronecker_deltatransport_equalsecondvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltatransport_equalsecondvalue) = 0) /\ (ge_balance_negative_kronecker_deltatransport_equalsecondvalue) = S ge_signed_half_kronecker_deltatransport_equalsecondvaluedecode))) /\ ((dst_positive_kronecker_deltatransport_equalsecond) + ge_balance_negative_kronecker_deltatransport_equalsecondvalue = (dst_negative_kronecker_deltatransport_equalsecond) + ge_balance_positive_kronecker_deltatransport_equalsecondvalue))))))))) -> dm_first_value_kronecker_deltatransport_equal=dm_second_value_kronecker_deltatransport_equal) -> (((exists dst_positive_code_kronecker_deltatransport_resulttable dst_positive_scale_kronecker_deltatransport_resulttable dst_negative_code_kronecker_deltatransport_resulttable dst_negative_scale_kronecker_deltatransport_resulttable. (((G) = (((((dst_positive_code_kronecker_deltatransport_resulttable) + (dst_positive_scale_kronecker_deltatransport_resulttable)) * S ((dst_positive_code_kronecker_deltatransport_resulttable) + (dst_positive_scale_kronecker_deltatransport_resulttable)) + ((dst_positive_scale_kronecker_deltatransport_resulttable) + (dst_positive_scale_kronecker_deltatransport_resulttable))) + (((dst_negative_code_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)) * S ((dst_negative_code_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)) + ((dst_negative_scale_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)))) * S ((((dst_positive_code_kronecker_deltatransport_resulttable) + (dst_positive_scale_kronecker_deltatransport_resulttable)) * S ((dst_positive_code_kronecker_deltatransport_resulttable) + (dst_positive_scale_kronecker_deltatransport_resulttable)) + ((dst_positive_scale_kronecker_deltatransport_resulttable) + (dst_positive_scale_kronecker_deltatransport_resulttable))) + (((dst_negative_code_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)) * S ((dst_negative_code_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)) + ((dst_negative_scale_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)))) + ((((dst_negative_code_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)) * S ((dst_negative_code_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)) + ((dst_negative_scale_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable))) + (((dst_negative_code_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)) * S ((dst_negative_code_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)) + ((dst_negative_scale_kronecker_deltatransport_resulttable) + (dst_negative_scale_kronecker_deltatransport_resulttable)))))) /\ (forall dst_index_kronecker_deltatransport_resulttable. (exists pvs_le_gap_kronecker_deltatransport_resulttabledomain. pvs_le_gap_kronecker_deltatransport_resulttabledomain + (dst_index_kronecker_deltatransport_resulttable) = (N)) -> exists dst_positive_kronecker_deltatransport_resulttable dst_negative_kronecker_deltatransport_resulttable dst_value_kronecker_deltatransport_resulttable. ((((exists ff_h_pvs_kronecker_deltatransport_resulttableentrypositive. ff_h_pvs_kronecker_deltatransport_resulttableentrypositive + S (dst_positive_kronecker_deltatransport_resulttable) = S ((S (dst_index_kronecker_deltatransport_resulttable)) * dst_positive_scale_kronecker_deltatransport_resulttable)) /\ exists ff_q_pvs_kronecker_deltatransport_resulttableentrypositive. dst_positive_code_kronecker_deltatransport_resulttable = ff_q_pvs_kronecker_deltatransport_resulttableentrypositive * S ((S (dst_index_kronecker_deltatransport_resulttable)) * dst_positive_scale_kronecker_deltatransport_resulttable) + (dst_positive_kronecker_deltatransport_resulttable))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_resulttableentrynegative. ff_h_pvs_kronecker_deltatransport_resulttableentrynegative + S (dst_negative_kronecker_deltatransport_resulttable) = S ((S (dst_index_kronecker_deltatransport_resulttable)) * dst_negative_scale_kronecker_deltatransport_resulttable)) /\ exists ff_q_pvs_kronecker_deltatransport_resulttableentrynegative. dst_negative_code_kronecker_deltatransport_resulttable = ff_q_pvs_kronecker_deltatransport_resulttableentrynegative * S ((S (dst_index_kronecker_deltatransport_resulttable)) * dst_negative_scale_kronecker_deltatransport_resulttable) + (dst_negative_kronecker_deltatransport_resulttable))) /\ (exists ge_balance_positive_kronecker_deltatransport_resulttableentryvalue ge_balance_negative_kronecker_deltatransport_resulttableentryvalue. (((((dst_value_kronecker_deltatransport_resulttable) = 2 * (ge_balance_positive_kronecker_deltatransport_resulttableentryvalue) /\ (ge_balance_negative_kronecker_deltatransport_resulttableentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltatransport_resulttableentryvaluedecode. (((dst_value_kronecker_deltatransport_resulttable) = 2 * ge_signed_half_kronecker_deltatransport_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltatransport_resulttableentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltatransport_resulttableentryvalue) = S ge_signed_half_kronecker_deltatransport_resulttableentryvaluedecode))) /\ ((dst_positive_kronecker_deltatransport_resulttable) + ge_balance_negative_kronecker_deltatransport_resulttableentryvalue = (dst_negative_kronecker_deltatransport_resulttable) + ge_balance_positive_kronecker_deltatransport_resulttableentryvalue))))))))) /\ (forall du_index_kronecker_deltatransport_result du_value_kronecker_deltatransport_result. ~(du_index_kronecker_deltatransport_result=0) -> (exists pvs_le_gap_kronecker_deltatransport_resultbound. pvs_le_gap_kronecker_deltatransport_resultbound + (du_index_kronecker_deltatransport_result) = (N)) -> (exists dst_positive_code_kronecker_deltatransport_resultentry dst_positive_scale_kronecker_deltatransport_resultentry dst_negative_code_kronecker_deltatransport_resultentry dst_negative_scale_kronecker_deltatransport_resultentry dst_positive_kronecker_deltatransport_resultentry dst_negative_kronecker_deltatransport_resultentry. (((G) = (((((dst_positive_code_kronecker_deltatransport_resultentry) + (dst_positive_scale_kronecker_deltatransport_resultentry)) * S ((dst_positive_code_kronecker_deltatransport_resultentry) + (dst_positive_scale_kronecker_deltatransport_resultentry)) + ((dst_positive_scale_kronecker_deltatransport_resultentry) + (dst_positive_scale_kronecker_deltatransport_resultentry))) + (((dst_negative_code_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)) * S ((dst_negative_code_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)) + ((dst_negative_scale_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)))) * S ((((dst_positive_code_kronecker_deltatransport_resultentry) + (dst_positive_scale_kronecker_deltatransport_resultentry)) * S ((dst_positive_code_kronecker_deltatransport_resultentry) + (dst_positive_scale_kronecker_deltatransport_resultentry)) + ((dst_positive_scale_kronecker_deltatransport_resultentry) + (dst_positive_scale_kronecker_deltatransport_resultentry))) + (((dst_negative_code_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)) * S ((dst_negative_code_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)) + ((dst_negative_scale_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)))) + ((((dst_negative_code_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)) * S ((dst_negative_code_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)) + ((dst_negative_scale_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry))) + (((dst_negative_code_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)) * S ((dst_negative_code_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)) + ((dst_negative_scale_kronecker_deltatransport_resultentry) + (dst_negative_scale_kronecker_deltatransport_resultentry)))))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_resultentrypositive. ff_h_pvs_kronecker_deltatransport_resultentrypositive + S (dst_positive_kronecker_deltatransport_resultentry) = S ((S (du_index_kronecker_deltatransport_result)) * dst_positive_scale_kronecker_deltatransport_resultentry)) /\ exists ff_q_pvs_kronecker_deltatransport_resultentrypositive. dst_positive_code_kronecker_deltatransport_resultentry = ff_q_pvs_kronecker_deltatransport_resultentrypositive * S ((S (du_index_kronecker_deltatransport_result)) * dst_positive_scale_kronecker_deltatransport_resultentry) + (dst_positive_kronecker_deltatransport_resultentry))) /\ (((((exists ff_h_pvs_kronecker_deltatransport_resultentrynegative. ff_h_pvs_kronecker_deltatransport_resultentrynegative + S (dst_negative_kronecker_deltatransport_resultentry) = S ((S (du_index_kronecker_deltatransport_result)) * dst_negative_scale_kronecker_deltatransport_resultentry)) /\ exists ff_q_pvs_kronecker_deltatransport_resultentrynegative. dst_negative_code_kronecker_deltatransport_resultentry = ff_q_pvs_kronecker_deltatransport_resultentrynegative * S ((S (du_index_kronecker_deltatransport_result)) * dst_negative_scale_kronecker_deltatransport_resultentry) + (dst_negative_kronecker_deltatransport_resultentry))) /\ (exists ge_balance_positive_kronecker_deltatransport_resultentryvalue ge_balance_negative_kronecker_deltatransport_resultentryvalue. (((((du_value_kronecker_deltatransport_result) = 2 * (ge_balance_positive_kronecker_deltatransport_resultentryvalue) /\ (ge_balance_negative_kronecker_deltatransport_resultentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltatransport_resultentryvaluedecode. (((du_value_kronecker_deltatransport_result) = 2 * ge_signed_half_kronecker_deltatransport_resultentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltatransport_resultentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltatransport_resultentryvalue) = S ge_signed_half_kronecker_deltatransport_resultentryvaluedecode))) /\ ((dst_positive_kronecker_deltatransport_resultentry) + ge_balance_negative_kronecker_deltatransport_resultentryvalue = (dst_negative_kronecker_deltatransport_resultentry) + ge_balance_positive_kronecker_deltatransport_resultentryvalue))))))))) -> ((((du_index_kronecker_deltatransport_result)=1 -> (du_value_kronecker_deltatransport_result)=2) /\ (~((du_index_kronecker_deltatransport_result)=1) -> (du_value_kronecker_deltatransport_result)=0))))))Complete tactic proof in conservative notation
All 41 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
41 script commands · 8 reading checkpoints · 3 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
01Fix variables and assumptionsL1–6
02Separate the logical casesL7–8
03Use earlier factsL9–9
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
exact hg
04Fix variables and assumptionsL10–14
05Establish hvL15–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.
- L15
have hv : ∃ v. ArithAt(F,i,v)Definitions: ArithAt(F,i,v)Original native command in the exact edition - L16
specialize divisor_signed_table_lookup (N) - L17
specialize divisor_signed_table_lookup (F) - L18
specialize divisor_signed_table_lookup (i) - L19
apply divisor_signed_table_lookup - L20
exact hf_left - L21
exact hb
06Separate the logical casesL22–22
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L22
cases hv
07Establish heqL23–31
08Establish hdL32–41
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hf right.
Original defined command ledger · 41 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro hf - 0005
intro hg - 0006
intro he - 0007
cases hf - 0008
split - 0009
exact hg - 0010
intro i - 0011
intro z - 0012
intro hi - 0013
intro hb - 0014
intro hz - 0015
have hv : ∃ v. ArithAt(F,i,v) - 0016
specialize divisor_signed_table_lookup (N) - 0017
specialize divisor_signed_table_lookup (F) - 0018
specialize divisor_signed_table_lookup (i) - 0019
apply divisor_signed_table_lookup - 0020
exact hf_left - 0021
exact hb - 0022
cases hv - 0023
have heq : x=z - 0024
specialize he (i) - 0025
specialize he (x) - 0026
specialize he (z) - 0027
apply he - 0028
exact hi - 0029
exact hb - 0030
exact hv_witness - 0031
exact hz - 0032
have hd : (((i)=1 -> (x)=2) /\ (~((i)=1) -> (x)=0)) - 0033
specialize hf_right (i) - 0034
specialize hf_right (x) - 0035
apply hf_right - 0036
exact hi - 0037
exact hb - 0038
exact hv_witness - 0039
rewrite heq at hd - 0040
rewrite heq at hd - 0041
exact hd