DU0003

dirichlet_kronecker_delta_table_other_value

Every other positive in-domain delta entry is canonical zero; the omitted index-zero case remains unrestricted.

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. ∀ n. ∀ z. KroneckerDeltaTable(N,E) → ¬n = 0 → ¬n = 1 → Le(n,N) → ArithAt(E,n,z) → z = 0

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

Definition DAG

ArithAt(F,i,z) · 1KroneckerDeltaTable(N,E) · 1Le(a,b) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall N E n z. (((exists dst_positive_code_delta_other_tabletable dst_positive_scale_delta_other_tabletable dst_negative_code_delta_other_tabletable dst_negative_scale_delta_other_tabletable. (((E) = (((((dst_positive_code_delta_other_tabletable) + (dst_positive_scale_delta_other_tabletable)) * S ((dst_positive_code_delta_other_tabletable) + (dst_positive_scale_delta_other_tabletable)) + ((dst_positive_scale_delta_other_tabletable) + (dst_positive_scale_delta_other_tabletable))) + (((dst_negative_code_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)) * S ((dst_negative_code_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)) + ((dst_negative_scale_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)))) * S ((((dst_positive_code_delta_other_tabletable) + (dst_positive_scale_delta_other_tabletable)) * S ((dst_positive_code_delta_other_tabletable) + (dst_positive_scale_delta_other_tabletable)) + ((dst_positive_scale_delta_other_tabletable) + (dst_positive_scale_delta_other_tabletable))) + (((dst_negative_code_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)) * S ((dst_negative_code_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)) + ((dst_negative_scale_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)))) + ((((dst_negative_code_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)) * S ((dst_negative_code_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)) + ((dst_negative_scale_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable))) + (((dst_negative_code_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)) * S ((dst_negative_code_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)) + ((dst_negative_scale_delta_other_tabletable) + (dst_negative_scale_delta_other_tabletable)))))) /\ (forall dst_index_delta_other_tabletable. (exists pvs_le_gap_delta_other_tabletabledomain. pvs_le_gap_delta_other_tabletabledomain + (dst_index_delta_other_tabletable) = (N)) -> exists dst_positive_delta_other_tabletable dst_negative_delta_other_tabletable dst_value_delta_other_tabletable. ((((exists ff_h_pvs_delta_other_tabletableentrypositive. ff_h_pvs_delta_other_tabletableentrypositive + S (dst_positive_delta_other_tabletable) = S ((S (dst_index_delta_other_tabletable)) * dst_positive_scale_delta_other_tabletable)) /\ exists ff_q_pvs_delta_other_tabletableentrypositive. dst_positive_code_delta_other_tabletable = ff_q_pvs_delta_other_tabletableentrypositive * S ((S (dst_index_delta_other_tabletable)) * dst_positive_scale_delta_other_tabletable) + (dst_positive_delta_other_tabletable))) /\ (((((exists ff_h_pvs_delta_other_tabletableentrynegative. ff_h_pvs_delta_other_tabletableentrynegative + S (dst_negative_delta_other_tabletable) = S ((S (dst_index_delta_other_tabletable)) * dst_negative_scale_delta_other_tabletable)) /\ exists ff_q_pvs_delta_other_tabletableentrynegative. dst_negative_code_delta_other_tabletable = ff_q_pvs_delta_other_tabletableentrynegative * S ((S (dst_index_delta_other_tabletable)) * dst_negative_scale_delta_other_tabletable) + (dst_negative_delta_other_tabletable))) /\ (exists ge_balance_positive_delta_other_tabletableentryvalue ge_balance_negative_delta_other_tabletableentryvalue. (((((dst_value_delta_other_tabletable) = 2 * (ge_balance_positive_delta_other_tabletableentryvalue) /\ (ge_balance_negative_delta_other_tabletableentryvalue) = 0) \/ exists ge_signed_half_delta_other_tabletableentryvaluedecode. (((dst_value_delta_other_tabletable) = 2 * ge_signed_half_delta_other_tabletableentryvaluedecode + 1 /\ (ge_balance_positive_delta_other_tabletableentryvalue) = 0) /\ (ge_balance_negative_delta_other_tabletableentryvalue) = S ge_signed_half_delta_other_tabletableentryvaluedecode))) /\ ((dst_positive_delta_other_tabletable) + ge_balance_negative_delta_other_tabletableentryvalue = (dst_negative_delta_other_tabletable) + ge_balance_positive_delta_other_tabletableentryvalue))))))))) /\ (forall du_index_delta_other_table du_value_delta_other_table. ~(du_index_delta_other_table=0) -> (exists pvs_le_gap_delta_other_tablebound. pvs_le_gap_delta_other_tablebound + (du_index_delta_other_table) = (N)) -> (exists dst_positive_code_delta_other_tableentry dst_positive_scale_delta_other_tableentry dst_negative_code_delta_other_tableentry dst_negative_scale_delta_other_tableentry dst_positive_delta_other_tableentry dst_negative_delta_other_tableentry. (((E) = (((((dst_positive_code_delta_other_tableentry) + (dst_positive_scale_delta_other_tableentry)) * S ((dst_positive_code_delta_other_tableentry) + (dst_positive_scale_delta_other_tableentry)) + ((dst_positive_scale_delta_other_tableentry) + (dst_positive_scale_delta_other_tableentry))) + (((dst_negative_code_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)) * S ((dst_negative_code_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)) + ((dst_negative_scale_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)))) * S ((((dst_positive_code_delta_other_tableentry) + (dst_positive_scale_delta_other_tableentry)) * S ((dst_positive_code_delta_other_tableentry) + (dst_positive_scale_delta_other_tableentry)) + ((dst_positive_scale_delta_other_tableentry) + (dst_positive_scale_delta_other_tableentry))) + (((dst_negative_code_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)) * S ((dst_negative_code_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)) + ((dst_negative_scale_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)))) + ((((dst_negative_code_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)) * S ((dst_negative_code_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)) + ((dst_negative_scale_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry))) + (((dst_negative_code_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)) * S ((dst_negative_code_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)) + ((dst_negative_scale_delta_other_tableentry) + (dst_negative_scale_delta_other_tableentry)))))) /\ (((((exists ff_h_pvs_delta_other_tableentrypositive. ff_h_pvs_delta_other_tableentrypositive + S (dst_positive_delta_other_tableentry) = S ((S (du_index_delta_other_table)) * dst_positive_scale_delta_other_tableentry)) /\ exists ff_q_pvs_delta_other_tableentrypositive. dst_positive_code_delta_other_tableentry = ff_q_pvs_delta_other_tableentrypositive * S ((S (du_index_delta_other_table)) * dst_positive_scale_delta_other_tableentry) + (dst_positive_delta_other_tableentry))) /\ (((((exists ff_h_pvs_delta_other_tableentrynegative. ff_h_pvs_delta_other_tableentrynegative + S (dst_negative_delta_other_tableentry) = S ((S (du_index_delta_other_table)) * dst_negative_scale_delta_other_tableentry)) /\ exists ff_q_pvs_delta_other_tableentrynegative. dst_negative_code_delta_other_tableentry = ff_q_pvs_delta_other_tableentrynegative * S ((S (du_index_delta_other_table)) * dst_negative_scale_delta_other_tableentry) + (dst_negative_delta_other_tableentry))) /\ (exists ge_balance_positive_delta_other_tableentryvalue ge_balance_negative_delta_other_tableentryvalue. (((((du_value_delta_other_table) = 2 * (ge_balance_positive_delta_other_tableentryvalue) /\ (ge_balance_negative_delta_other_tableentryvalue) = 0) \/ exists ge_signed_half_delta_other_tableentryvaluedecode. (((du_value_delta_other_table) = 2 * ge_signed_half_delta_other_tableentryvaluedecode + 1 /\ (ge_balance_positive_delta_other_tableentryvalue) = 0) /\ (ge_balance_negative_delta_other_tableentryvalue) = S ge_signed_half_delta_other_tableentryvaluedecode))) /\ ((dst_positive_delta_other_tableentry) + ge_balance_negative_delta_other_tableentryvalue = (dst_negative_delta_other_tableentry) + ge_balance_positive_delta_other_tableentryvalue))))))))) -> ((((du_index_delta_other_table)=1 -> (du_value_delta_other_table)=2) /\ (~((du_index_delta_other_table)=1) -> (du_value_delta_other_table)=0)))))) -> ~(n=0) -> ~(n=1) -> (exists pvs_le_gap_delta_other_bound. pvs_le_gap_delta_other_bound + (n) = (N)) -> (exists dst_positive_code_delta_other_entry dst_positive_scale_delta_other_entry dst_negative_code_delta_other_entry dst_negative_scale_delta_other_entry dst_positive_delta_other_entry dst_negative_delta_other_entry. (((E) = (((((dst_positive_code_delta_other_entry) + (dst_positive_scale_delta_other_entry)) * S ((dst_positive_code_delta_other_entry) + (dst_positive_scale_delta_other_entry)) + ((dst_positive_scale_delta_other_entry) + (dst_positive_scale_delta_other_entry))) + (((dst_negative_code_delta_other_entry) + (dst_negative_scale_delta_other_entry)) * S ((dst_negative_code_delta_other_entry) + (dst_negative_scale_delta_other_entry)) + ((dst_negative_scale_delta_other_entry) + (dst_negative_scale_delta_other_entry)))) * S ((((dst_positive_code_delta_other_entry) + (dst_positive_scale_delta_other_entry)) * S ((dst_positive_code_delta_other_entry) + (dst_positive_scale_delta_other_entry)) + ((dst_positive_scale_delta_other_entry) + (dst_positive_scale_delta_other_entry))) + (((dst_negative_code_delta_other_entry) + (dst_negative_scale_delta_other_entry)) * S ((dst_negative_code_delta_other_entry) + (dst_negative_scale_delta_other_entry)) + ((dst_negative_scale_delta_other_entry) + (dst_negative_scale_delta_other_entry)))) + ((((dst_negative_code_delta_other_entry) + (dst_negative_scale_delta_other_entry)) * S ((dst_negative_code_delta_other_entry) + (dst_negative_scale_delta_other_entry)) + ((dst_negative_scale_delta_other_entry) + (dst_negative_scale_delta_other_entry))) + (((dst_negative_code_delta_other_entry) + (dst_negative_scale_delta_other_entry)) * S ((dst_negative_code_delta_other_entry) + (dst_negative_scale_delta_other_entry)) + ((dst_negative_scale_delta_other_entry) + (dst_negative_scale_delta_other_entry)))))) /\ (((((exists ff_h_pvs_delta_other_entrypositive. ff_h_pvs_delta_other_entrypositive + S (dst_positive_delta_other_entry) = S ((S (n)) * dst_positive_scale_delta_other_entry)) /\ exists ff_q_pvs_delta_other_entrypositive. dst_positive_code_delta_other_entry = ff_q_pvs_delta_other_entrypositive * S ((S (n)) * dst_positive_scale_delta_other_entry) + (dst_positive_delta_other_entry))) /\ (((((exists ff_h_pvs_delta_other_entrynegative. ff_h_pvs_delta_other_entrynegative + S (dst_negative_delta_other_entry) = S ((S (n)) * dst_negative_scale_delta_other_entry)) /\ exists ff_q_pvs_delta_other_entrynegative. dst_negative_code_delta_other_entry = ff_q_pvs_delta_other_entrynegative * S ((S (n)) * dst_negative_scale_delta_other_entry) + (dst_negative_delta_other_entry))) /\ (exists ge_balance_positive_delta_other_entryvalue ge_balance_negative_delta_other_entryvalue. (((((z) = 2 * (ge_balance_positive_delta_other_entryvalue) /\ (ge_balance_negative_delta_other_entryvalue) = 0) \/ exists ge_signed_half_delta_other_entryvaluedecode. (((z) = 2 * ge_signed_half_delta_other_entryvaluedecode + 1 /\ (ge_balance_positive_delta_other_entryvalue) = 0) /\ (ge_balance_negative_delta_other_entryvalue) = S ge_signed_half_delta_other_entryvaluedecode))) /\ ((dst_positive_delta_other_entry) + ge_balance_negative_delta_other_entryvalue = (dst_negative_delta_other_entry) + ge_balance_positive_delta_other_entryvalue))))))))) -> z=0

Complete tactic proof in conservative notation

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

20 script commands · 5 reading checkpoints · 1 local claims

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

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

01Fix variables and assumptionsL1–9

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

  1. L1
    intro N
  2. L2
    intro E
  3. L3
    intro n
  4. L4
    intro z
  5. L5
    intro he
  6. L6
    intro hn
  7. L7
    intro hnotone
  8. L8
    intro hb
  9. L9
    intro hz
02Separate the logical casesL10–10

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

  1. L10
    cases he
03Establish hvL11–17

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

  1. L11
    have hv : (((n)=1 -> (z)=2) /\ (~((n)=1) -> (z)=0))
  2. L12
    specialize he_right (n)
  3. L13
    specialize he_right (z)
  4. L14
    apply he_right
  5. L15
    exact hn
  6. L16
    exact hb
  7. L17
    exact hz
04Separate the logical casesL18–18

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

  1. L18
    cases hv
05Use earlier factsL19–20

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

  1. L19
    apply hv_right
  2. L20
    exact hnotone

Library-wide reading audit

Original defined command ledger · 20 lines
  1. 0001intro N
  2. 0002intro E
  3. 0003intro n
  4. 0004intro z
  5. 0005intro he
  6. 0006intro hn
  7. 0007intro hnotone
  8. 0008intro hb
  9. 0009intro hz
  10. 0010cases he
  11. 0011have hv : (((n)=1 -> (z)=2) /\ (~((n)=1) -> (z)=0))
  12. 0012specialize he_right (n)
  13. 0013specialize he_right (z)
  14. 0014apply he_right
  15. 0015exact hn
  16. 0016exact hb
  17. 0017exact hz
  18. 0018cases hv
  19. 0019apply hv_right
  20. 0020exact hnotone