DU000C

dirichlet_kronecker_delta_table_positive_unique

All constructed representations agree at every positive in-domain entry; neither equality at zero nor equality of arbitrary table encodings is asserted.

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. ∀ F. ∀ G. KroneckerDeltaTable(N,F) → KroneckerDeltaTable(N,G) → ArithPositiveEqual(F,G,N)

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

Definition DAG

ArithPositiveEqual(F,G,N) · 1KroneckerDeltaTable(N,E) · 2

Actual proof prerequisites

eq_decidable · checked external prerequisite
Original expanded first-order statement 
forall N F G. (((exists dst_positive_code_kronecker_deltaunique_firsttable dst_positive_scale_kronecker_deltaunique_firsttable dst_negative_code_kronecker_deltaunique_firsttable dst_negative_scale_kronecker_deltaunique_firsttable. (((F) = (((((dst_positive_code_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable)) * S ((dst_positive_code_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable)) + ((dst_positive_scale_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable))) + (((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) * S ((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) + ((dst_negative_scale_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)))) * S ((((dst_positive_code_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable)) * S ((dst_positive_code_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable)) + ((dst_positive_scale_kronecker_deltaunique_firsttable) + (dst_positive_scale_kronecker_deltaunique_firsttable))) + (((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) * S ((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) + ((dst_negative_scale_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)))) + ((((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) * S ((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) + ((dst_negative_scale_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable))) + (((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) * S ((dst_negative_code_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)) + ((dst_negative_scale_kronecker_deltaunique_firsttable) + (dst_negative_scale_kronecker_deltaunique_firsttable)))))) /\ (forall dst_index_kronecker_deltaunique_firsttable. (exists pvs_le_gap_kronecker_deltaunique_firsttabledomain. pvs_le_gap_kronecker_deltaunique_firsttabledomain + (dst_index_kronecker_deltaunique_firsttable) = (N)) -> exists dst_positive_kronecker_deltaunique_firsttable dst_negative_kronecker_deltaunique_firsttable dst_value_kronecker_deltaunique_firsttable. ((((exists ff_h_pvs_kronecker_deltaunique_firsttableentrypositive. ff_h_pvs_kronecker_deltaunique_firsttableentrypositive + S (dst_positive_kronecker_deltaunique_firsttable) = S ((S (dst_index_kronecker_deltaunique_firsttable)) * dst_positive_scale_kronecker_deltaunique_firsttable)) /\ exists ff_q_pvs_kronecker_deltaunique_firsttableentrypositive. dst_positive_code_kronecker_deltaunique_firsttable = ff_q_pvs_kronecker_deltaunique_firsttableentrypositive * S ((S (dst_index_kronecker_deltaunique_firsttable)) * dst_positive_scale_kronecker_deltaunique_firsttable) + (dst_positive_kronecker_deltaunique_firsttable))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_firsttableentrynegative. ff_h_pvs_kronecker_deltaunique_firsttableentrynegative + S (dst_negative_kronecker_deltaunique_firsttable) = S ((S (dst_index_kronecker_deltaunique_firsttable)) * dst_negative_scale_kronecker_deltaunique_firsttable)) /\ exists ff_q_pvs_kronecker_deltaunique_firsttableentrynegative. dst_negative_code_kronecker_deltaunique_firsttable = ff_q_pvs_kronecker_deltaunique_firsttableentrynegative * S ((S (dst_index_kronecker_deltaunique_firsttable)) * dst_negative_scale_kronecker_deltaunique_firsttable) + (dst_negative_kronecker_deltaunique_firsttable))) /\ (exists ge_balance_positive_kronecker_deltaunique_firsttableentryvalue ge_balance_negative_kronecker_deltaunique_firsttableentryvalue. (((((dst_value_kronecker_deltaunique_firsttable) = 2 * (ge_balance_positive_kronecker_deltaunique_firsttableentryvalue) /\ (ge_balance_negative_kronecker_deltaunique_firsttableentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_firsttableentryvaluedecode. (((dst_value_kronecker_deltaunique_firsttable) = 2 * ge_signed_half_kronecker_deltaunique_firsttableentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_firsttableentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_firsttableentryvalue) = S ge_signed_half_kronecker_deltaunique_firsttableentryvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_firsttable) + ge_balance_negative_kronecker_deltaunique_firsttableentryvalue = (dst_negative_kronecker_deltaunique_firsttable) + ge_balance_positive_kronecker_deltaunique_firsttableentryvalue))))))))) /\ (forall du_index_kronecker_deltaunique_first du_value_kronecker_deltaunique_first. ~(du_index_kronecker_deltaunique_first=0) -> (exists pvs_le_gap_kronecker_deltaunique_firstbound. pvs_le_gap_kronecker_deltaunique_firstbound + (du_index_kronecker_deltaunique_first) = (N)) -> (exists dst_positive_code_kronecker_deltaunique_firstentry dst_positive_scale_kronecker_deltaunique_firstentry dst_negative_code_kronecker_deltaunique_firstentry dst_negative_scale_kronecker_deltaunique_firstentry dst_positive_kronecker_deltaunique_firstentry dst_negative_kronecker_deltaunique_firstentry. (((F) = (((((dst_positive_code_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry)) * S ((dst_positive_code_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry)) + ((dst_positive_scale_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry))) + (((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) * S ((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) + ((dst_negative_scale_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)))) * S ((((dst_positive_code_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry)) * S ((dst_positive_code_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry)) + ((dst_positive_scale_kronecker_deltaunique_firstentry) + (dst_positive_scale_kronecker_deltaunique_firstentry))) + (((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) * S ((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) + ((dst_negative_scale_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)))) + ((((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) * S ((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) + ((dst_negative_scale_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry))) + (((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) * S ((dst_negative_code_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)) + ((dst_negative_scale_kronecker_deltaunique_firstentry) + (dst_negative_scale_kronecker_deltaunique_firstentry)))))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_firstentrypositive. ff_h_pvs_kronecker_deltaunique_firstentrypositive + S (dst_positive_kronecker_deltaunique_firstentry) = S ((S (du_index_kronecker_deltaunique_first)) * dst_positive_scale_kronecker_deltaunique_firstentry)) /\ exists ff_q_pvs_kronecker_deltaunique_firstentrypositive. dst_positive_code_kronecker_deltaunique_firstentry = ff_q_pvs_kronecker_deltaunique_firstentrypositive * S ((S (du_index_kronecker_deltaunique_first)) * dst_positive_scale_kronecker_deltaunique_firstentry) + (dst_positive_kronecker_deltaunique_firstentry))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_firstentrynegative. ff_h_pvs_kronecker_deltaunique_firstentrynegative + S (dst_negative_kronecker_deltaunique_firstentry) = S ((S (du_index_kronecker_deltaunique_first)) * dst_negative_scale_kronecker_deltaunique_firstentry)) /\ exists ff_q_pvs_kronecker_deltaunique_firstentrynegative. dst_negative_code_kronecker_deltaunique_firstentry = ff_q_pvs_kronecker_deltaunique_firstentrynegative * S ((S (du_index_kronecker_deltaunique_first)) * dst_negative_scale_kronecker_deltaunique_firstentry) + (dst_negative_kronecker_deltaunique_firstentry))) /\ (exists ge_balance_positive_kronecker_deltaunique_firstentryvalue ge_balance_negative_kronecker_deltaunique_firstentryvalue. (((((du_value_kronecker_deltaunique_first) = 2 * (ge_balance_positive_kronecker_deltaunique_firstentryvalue) /\ (ge_balance_negative_kronecker_deltaunique_firstentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_firstentryvaluedecode. (((du_value_kronecker_deltaunique_first) = 2 * ge_signed_half_kronecker_deltaunique_firstentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_firstentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_firstentryvalue) = S ge_signed_half_kronecker_deltaunique_firstentryvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_firstentry) + ge_balance_negative_kronecker_deltaunique_firstentryvalue = (dst_negative_kronecker_deltaunique_firstentry) + ge_balance_positive_kronecker_deltaunique_firstentryvalue))))))))) -> ((((du_index_kronecker_deltaunique_first)=1 -> (du_value_kronecker_deltaunique_first)=2) /\ (~((du_index_kronecker_deltaunique_first)=1) -> (du_value_kronecker_deltaunique_first)=0)))))) -> (((exists dst_positive_code_kronecker_deltaunique_secondtable dst_positive_scale_kronecker_deltaunique_secondtable dst_negative_code_kronecker_deltaunique_secondtable dst_negative_scale_kronecker_deltaunique_secondtable. (((G) = (((((dst_positive_code_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable)) * S ((dst_positive_code_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable)) + ((dst_positive_scale_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable))) + (((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) * S ((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) + ((dst_negative_scale_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)))) * S ((((dst_positive_code_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable)) * S ((dst_positive_code_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable)) + ((dst_positive_scale_kronecker_deltaunique_secondtable) + (dst_positive_scale_kronecker_deltaunique_secondtable))) + (((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) * S ((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) + ((dst_negative_scale_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)))) + ((((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) * S ((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) + ((dst_negative_scale_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable))) + (((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) * S ((dst_negative_code_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)) + ((dst_negative_scale_kronecker_deltaunique_secondtable) + (dst_negative_scale_kronecker_deltaunique_secondtable)))))) /\ (forall dst_index_kronecker_deltaunique_secondtable. (exists pvs_le_gap_kronecker_deltaunique_secondtabledomain. pvs_le_gap_kronecker_deltaunique_secondtabledomain + (dst_index_kronecker_deltaunique_secondtable) = (N)) -> exists dst_positive_kronecker_deltaunique_secondtable dst_negative_kronecker_deltaunique_secondtable dst_value_kronecker_deltaunique_secondtable. ((((exists ff_h_pvs_kronecker_deltaunique_secondtableentrypositive. ff_h_pvs_kronecker_deltaunique_secondtableentrypositive + S (dst_positive_kronecker_deltaunique_secondtable) = S ((S (dst_index_kronecker_deltaunique_secondtable)) * dst_positive_scale_kronecker_deltaunique_secondtable)) /\ exists ff_q_pvs_kronecker_deltaunique_secondtableentrypositive. dst_positive_code_kronecker_deltaunique_secondtable = ff_q_pvs_kronecker_deltaunique_secondtableentrypositive * S ((S (dst_index_kronecker_deltaunique_secondtable)) * dst_positive_scale_kronecker_deltaunique_secondtable) + (dst_positive_kronecker_deltaunique_secondtable))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_secondtableentrynegative. ff_h_pvs_kronecker_deltaunique_secondtableentrynegative + S (dst_negative_kronecker_deltaunique_secondtable) = S ((S (dst_index_kronecker_deltaunique_secondtable)) * dst_negative_scale_kronecker_deltaunique_secondtable)) /\ exists ff_q_pvs_kronecker_deltaunique_secondtableentrynegative. dst_negative_code_kronecker_deltaunique_secondtable = ff_q_pvs_kronecker_deltaunique_secondtableentrynegative * S ((S (dst_index_kronecker_deltaunique_secondtable)) * dst_negative_scale_kronecker_deltaunique_secondtable) + (dst_negative_kronecker_deltaunique_secondtable))) /\ (exists ge_balance_positive_kronecker_deltaunique_secondtableentryvalue ge_balance_negative_kronecker_deltaunique_secondtableentryvalue. (((((dst_value_kronecker_deltaunique_secondtable) = 2 * (ge_balance_positive_kronecker_deltaunique_secondtableentryvalue) /\ (ge_balance_negative_kronecker_deltaunique_secondtableentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_secondtableentryvaluedecode. (((dst_value_kronecker_deltaunique_secondtable) = 2 * ge_signed_half_kronecker_deltaunique_secondtableentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_secondtableentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_secondtableentryvalue) = S ge_signed_half_kronecker_deltaunique_secondtableentryvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_secondtable) + ge_balance_negative_kronecker_deltaunique_secondtableentryvalue = (dst_negative_kronecker_deltaunique_secondtable) + ge_balance_positive_kronecker_deltaunique_secondtableentryvalue))))))))) /\ (forall du_index_kronecker_deltaunique_second du_value_kronecker_deltaunique_second. ~(du_index_kronecker_deltaunique_second=0) -> (exists pvs_le_gap_kronecker_deltaunique_secondbound. pvs_le_gap_kronecker_deltaunique_secondbound + (du_index_kronecker_deltaunique_second) = (N)) -> (exists dst_positive_code_kronecker_deltaunique_secondentry dst_positive_scale_kronecker_deltaunique_secondentry dst_negative_code_kronecker_deltaunique_secondentry dst_negative_scale_kronecker_deltaunique_secondentry dst_positive_kronecker_deltaunique_secondentry dst_negative_kronecker_deltaunique_secondentry. (((G) = (((((dst_positive_code_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry)) * S ((dst_positive_code_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry)) + ((dst_positive_scale_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry))) + (((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) * S ((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) + ((dst_negative_scale_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)))) * S ((((dst_positive_code_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry)) * S ((dst_positive_code_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry)) + ((dst_positive_scale_kronecker_deltaunique_secondentry) + (dst_positive_scale_kronecker_deltaunique_secondentry))) + (((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) * S ((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) + ((dst_negative_scale_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)))) + ((((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) * S ((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) + ((dst_negative_scale_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry))) + (((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) * S ((dst_negative_code_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)) + ((dst_negative_scale_kronecker_deltaunique_secondentry) + (dst_negative_scale_kronecker_deltaunique_secondentry)))))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_secondentrypositive. ff_h_pvs_kronecker_deltaunique_secondentrypositive + S (dst_positive_kronecker_deltaunique_secondentry) = S ((S (du_index_kronecker_deltaunique_second)) * dst_positive_scale_kronecker_deltaunique_secondentry)) /\ exists ff_q_pvs_kronecker_deltaunique_secondentrypositive. dst_positive_code_kronecker_deltaunique_secondentry = ff_q_pvs_kronecker_deltaunique_secondentrypositive * S ((S (du_index_kronecker_deltaunique_second)) * dst_positive_scale_kronecker_deltaunique_secondentry) + (dst_positive_kronecker_deltaunique_secondentry))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_secondentrynegative. ff_h_pvs_kronecker_deltaunique_secondentrynegative + S (dst_negative_kronecker_deltaunique_secondentry) = S ((S (du_index_kronecker_deltaunique_second)) * dst_negative_scale_kronecker_deltaunique_secondentry)) /\ exists ff_q_pvs_kronecker_deltaunique_secondentrynegative. dst_negative_code_kronecker_deltaunique_secondentry = ff_q_pvs_kronecker_deltaunique_secondentrynegative * S ((S (du_index_kronecker_deltaunique_second)) * dst_negative_scale_kronecker_deltaunique_secondentry) + (dst_negative_kronecker_deltaunique_secondentry))) /\ (exists ge_balance_positive_kronecker_deltaunique_secondentryvalue ge_balance_negative_kronecker_deltaunique_secondentryvalue. (((((du_value_kronecker_deltaunique_second) = 2 * (ge_balance_positive_kronecker_deltaunique_secondentryvalue) /\ (ge_balance_negative_kronecker_deltaunique_secondentryvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_secondentryvaluedecode. (((du_value_kronecker_deltaunique_second) = 2 * ge_signed_half_kronecker_deltaunique_secondentryvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_secondentryvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_secondentryvalue) = S ge_signed_half_kronecker_deltaunique_secondentryvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_secondentry) + ge_balance_negative_kronecker_deltaunique_secondentryvalue = (dst_negative_kronecker_deltaunique_secondentry) + ge_balance_positive_kronecker_deltaunique_secondentryvalue))))))))) -> ((((du_index_kronecker_deltaunique_second)=1 -> (du_value_kronecker_deltaunique_second)=2) /\ (~((du_index_kronecker_deltaunique_second)=1) -> (du_value_kronecker_deltaunique_second)=0)))))) -> (forall dm_index_kronecker_deltaunique_result dm_first_value_kronecker_deltaunique_result dm_second_value_kronecker_deltaunique_result. ~(dm_index_kronecker_deltaunique_result=0) -> (exists pvs_le_gap_kronecker_deltaunique_resultdomain. pvs_le_gap_kronecker_deltaunique_resultdomain + (dm_index_kronecker_deltaunique_result) = (N)) -> (exists dst_positive_code_kronecker_deltaunique_resultfirst dst_positive_scale_kronecker_deltaunique_resultfirst dst_negative_code_kronecker_deltaunique_resultfirst dst_negative_scale_kronecker_deltaunique_resultfirst dst_positive_kronecker_deltaunique_resultfirst dst_negative_kronecker_deltaunique_resultfirst. (((F) = (((((dst_positive_code_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst)) * S ((dst_positive_code_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst)) + ((dst_positive_scale_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst))) + (((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) * S ((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) + ((dst_negative_scale_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)))) * S ((((dst_positive_code_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst)) * S ((dst_positive_code_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst)) + ((dst_positive_scale_kronecker_deltaunique_resultfirst) + (dst_positive_scale_kronecker_deltaunique_resultfirst))) + (((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) * S ((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) + ((dst_negative_scale_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)))) + ((((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) * S ((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) + ((dst_negative_scale_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst))) + (((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) * S ((dst_negative_code_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)) + ((dst_negative_scale_kronecker_deltaunique_resultfirst) + (dst_negative_scale_kronecker_deltaunique_resultfirst)))))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_resultfirstpositive. ff_h_pvs_kronecker_deltaunique_resultfirstpositive + S (dst_positive_kronecker_deltaunique_resultfirst) = S ((S (dm_index_kronecker_deltaunique_result)) * dst_positive_scale_kronecker_deltaunique_resultfirst)) /\ exists ff_q_pvs_kronecker_deltaunique_resultfirstpositive. dst_positive_code_kronecker_deltaunique_resultfirst = ff_q_pvs_kronecker_deltaunique_resultfirstpositive * S ((S (dm_index_kronecker_deltaunique_result)) * dst_positive_scale_kronecker_deltaunique_resultfirst) + (dst_positive_kronecker_deltaunique_resultfirst))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_resultfirstnegative. ff_h_pvs_kronecker_deltaunique_resultfirstnegative + S (dst_negative_kronecker_deltaunique_resultfirst) = S ((S (dm_index_kronecker_deltaunique_result)) * dst_negative_scale_kronecker_deltaunique_resultfirst)) /\ exists ff_q_pvs_kronecker_deltaunique_resultfirstnegative. dst_negative_code_kronecker_deltaunique_resultfirst = ff_q_pvs_kronecker_deltaunique_resultfirstnegative * S ((S (dm_index_kronecker_deltaunique_result)) * dst_negative_scale_kronecker_deltaunique_resultfirst) + (dst_negative_kronecker_deltaunique_resultfirst))) /\ (exists ge_balance_positive_kronecker_deltaunique_resultfirstvalue ge_balance_negative_kronecker_deltaunique_resultfirstvalue. (((((dm_first_value_kronecker_deltaunique_result) = 2 * (ge_balance_positive_kronecker_deltaunique_resultfirstvalue) /\ (ge_balance_negative_kronecker_deltaunique_resultfirstvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_resultfirstvaluedecode. (((dm_first_value_kronecker_deltaunique_result) = 2 * ge_signed_half_kronecker_deltaunique_resultfirstvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_resultfirstvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_resultfirstvalue) = S ge_signed_half_kronecker_deltaunique_resultfirstvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_resultfirst) + ge_balance_negative_kronecker_deltaunique_resultfirstvalue = (dst_negative_kronecker_deltaunique_resultfirst) + ge_balance_positive_kronecker_deltaunique_resultfirstvalue))))))))) -> (exists dst_positive_code_kronecker_deltaunique_resultsecond dst_positive_scale_kronecker_deltaunique_resultsecond dst_negative_code_kronecker_deltaunique_resultsecond dst_negative_scale_kronecker_deltaunique_resultsecond dst_positive_kronecker_deltaunique_resultsecond dst_negative_kronecker_deltaunique_resultsecond. (((G) = (((((dst_positive_code_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond)) * S ((dst_positive_code_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond)) + ((dst_positive_scale_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond))) + (((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) * S ((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) + ((dst_negative_scale_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)))) * S ((((dst_positive_code_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond)) * S ((dst_positive_code_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond)) + ((dst_positive_scale_kronecker_deltaunique_resultsecond) + (dst_positive_scale_kronecker_deltaunique_resultsecond))) + (((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) * S ((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) + ((dst_negative_scale_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)))) + ((((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) * S ((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) + ((dst_negative_scale_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond))) + (((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) * S ((dst_negative_code_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)) + ((dst_negative_scale_kronecker_deltaunique_resultsecond) + (dst_negative_scale_kronecker_deltaunique_resultsecond)))))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_resultsecondpositive. ff_h_pvs_kronecker_deltaunique_resultsecondpositive + S (dst_positive_kronecker_deltaunique_resultsecond) = S ((S (dm_index_kronecker_deltaunique_result)) * dst_positive_scale_kronecker_deltaunique_resultsecond)) /\ exists ff_q_pvs_kronecker_deltaunique_resultsecondpositive. dst_positive_code_kronecker_deltaunique_resultsecond = ff_q_pvs_kronecker_deltaunique_resultsecondpositive * S ((S (dm_index_kronecker_deltaunique_result)) * dst_positive_scale_kronecker_deltaunique_resultsecond) + (dst_positive_kronecker_deltaunique_resultsecond))) /\ (((((exists ff_h_pvs_kronecker_deltaunique_resultsecondnegative. ff_h_pvs_kronecker_deltaunique_resultsecondnegative + S (dst_negative_kronecker_deltaunique_resultsecond) = S ((S (dm_index_kronecker_deltaunique_result)) * dst_negative_scale_kronecker_deltaunique_resultsecond)) /\ exists ff_q_pvs_kronecker_deltaunique_resultsecondnegative. dst_negative_code_kronecker_deltaunique_resultsecond = ff_q_pvs_kronecker_deltaunique_resultsecondnegative * S ((S (dm_index_kronecker_deltaunique_result)) * dst_negative_scale_kronecker_deltaunique_resultsecond) + (dst_negative_kronecker_deltaunique_resultsecond))) /\ (exists ge_balance_positive_kronecker_deltaunique_resultsecondvalue ge_balance_negative_kronecker_deltaunique_resultsecondvalue. (((((dm_second_value_kronecker_deltaunique_result) = 2 * (ge_balance_positive_kronecker_deltaunique_resultsecondvalue) /\ (ge_balance_negative_kronecker_deltaunique_resultsecondvalue) = 0) \/ exists ge_signed_half_kronecker_deltaunique_resultsecondvaluedecode. (((dm_second_value_kronecker_deltaunique_result) = 2 * ge_signed_half_kronecker_deltaunique_resultsecondvaluedecode + 1 /\ (ge_balance_positive_kronecker_deltaunique_resultsecondvalue) = 0) /\ (ge_balance_negative_kronecker_deltaunique_resultsecondvalue) = S ge_signed_half_kronecker_deltaunique_resultsecondvaluedecode))) /\ ((dst_positive_kronecker_deltaunique_resultsecond) + ge_balance_negative_kronecker_deltaunique_resultsecondvalue = (dst_negative_kronecker_deltaunique_resultsecond) + ge_balance_positive_kronecker_deltaunique_resultsecondvalue))))))))) -> dm_first_value_kronecker_deltaunique_result=dm_second_value_kronecker_deltaunique_result)

Complete tactic proof in conservative notation

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

47 script commands · 16 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–5

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro G
  4. L4
    intro hf
  5. L5
    intro hg
02Separate the logical casesL6–7

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

  1. L6
    cases hf
  2. L7
    cases hg
03Fix variables and assumptionsL8–14

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

  1. L8
    intro i
  2. L9
    intro a
  3. L10
    intro b
  4. L11
    intro hi
  5. L12
    intro hb
  6. L13
    intro ha
  7. L14
    intro hbv
04Establish hfaL15–21

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

  1. L15
    have hfa : (((i)=1 -> (a)=2) /\ (~((i)=1) -> (a)=0))
  2. L16
    specialize hf_right (i)
  3. L17
    specialize hf_right (a)
  4. L18
    apply hf_right
  5. L19
    exact hi
  6. L20
    exact hb
  7. L21
    exact ha
05Establish hgbL22–28

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

  1. L22
    have hgb : (((i)=1 -> (b)=2) /\ (~((i)=1) -> (b)=0))
  2. L23
    specialize hg_right (i)
  3. L24
    specialize hg_right (b)
  4. L25
    apply hg_right
  5. L26
    exact hi
  6. L27
    exact hb
  7. L28
    exact hbv
06Separate the logical casesL29–30

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

  1. L29
    cases hfa
  2. L30
    cases hgb
07Establish hcL31–34

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

  1. L31
    have hc : i=1 \/ ~(i=1)
  2. L32
    specialize eq_decidable (i)
  3. L33
    specialize eq_decidable (1)
  4. L34
    apply eq_decidable
08Separate the logical casesL35–35

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

  1. L35
    cases hc
09Calculate and transport equalitiesL36–36

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

  1. L36
    trans 2
10Use earlier factsL37–38

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

  1. L37
    apply hfa_left
  2. L38
    exact hc_left
11Calculate and transport equalitiesL39–39

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

  1. L39
    symm
12Use earlier factsL40–41

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

  1. L40
    apply hgb_left
  2. L41
    exact hc_left
13Calculate and transport equalitiesL42–42

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

  1. L42
    trans 0
14Use earlier factsL43–44

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

  1. L43
    apply hfa_right
  2. L44
    exact hc_right
15Calculate and transport equalitiesL45–45

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

  1. L45
    symm
16Use earlier factsL46–47

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

  1. L46
    apply hgb_right
  2. L47
    exact hc_right

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro G
  4. 0004intro hf
  5. 0005intro hg
  6. 0006cases hf
  7. 0007cases hg
  8. 0008intro i
  9. 0009intro a
  10. 0010intro b
  11. 0011intro hi
  12. 0012intro hb
  13. 0013intro ha
  14. 0014intro hbv
  15. 0015have hfa : (((i)=1 -> (a)=2) /\ (~((i)=1) -> (a)=0))
  16. 0016specialize hf_right (i)
  17. 0017specialize hf_right (a)
  18. 0018apply hf_right
  19. 0019exact hi
  20. 0020exact hb
  21. 0021exact ha
  22. 0022have hgb : (((i)=1 -> (b)=2) /\ (~((i)=1) -> (b)=0))
  23. 0023specialize hg_right (i)
  24. 0024specialize hg_right (b)
  25. 0025apply hg_right
  26. 0026exact hi
  27. 0027exact hb
  28. 0028exact hbv
  29. 0029cases hfa
  30. 0030cases hgb
  31. 0031have hc : i=1 \/ ~(i=1)
  32. 0032specialize eq_decidable (i)
  33. 0033specialize eq_decidable (1)
  34. 0034apply eq_decidable
  35. 0035cases hc
  36. 0036trans 2
  37. 0037apply hfa_left
  38. 0038exact hc_left
  39. 0039symm
  40. 0040apply hgb_left
  41. 0041exact hc_left
  42. 0042trans 0
  43. 0043apply hfa_right
  44. 0044exact hc_right
  45. 0045symm
  46. 0046apply hgb_right
  47. 0047exact hc_right