DU0003

dirichlet_kronecker_delta_table_other_value

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

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

Exact expanded first-order arithmetic 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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 0 declared prerequisites and contains 20 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

DU000D dirichlet_delta_right_entry_before_input

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

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 exact 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