DU0001

dirichlet_constant_one_table_value

Every actual positive in-domain lookup in a constant-one table is canonical signed one, independently of its zero entry.

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. ∀ U. ∀ n. ∀ z. ConstantOneTable(N,U) → ¬n = 0 → Le(n,N) → ArithAt(U,n,z) → z = 2

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

Definition DAG

ArithAt(F,i,z) · 1ConstantOneTable(N,U) · 1Le(a,b) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall N U n z. (((exists dst_positive_code_one_lookup_tabletable dst_positive_scale_one_lookup_tabletable dst_negative_code_one_lookup_tabletable dst_negative_scale_one_lookup_tabletable. (((U) = (((((dst_positive_code_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable)) * S ((dst_positive_code_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable)) + ((dst_positive_scale_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable))) + (((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) * S ((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) + ((dst_negative_scale_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)))) * S ((((dst_positive_code_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable)) * S ((dst_positive_code_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable)) + ((dst_positive_scale_one_lookup_tabletable) + (dst_positive_scale_one_lookup_tabletable))) + (((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) * S ((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) + ((dst_negative_scale_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)))) + ((((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) * S ((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) + ((dst_negative_scale_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable))) + (((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) * S ((dst_negative_code_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)) + ((dst_negative_scale_one_lookup_tabletable) + (dst_negative_scale_one_lookup_tabletable)))))) /\ (forall dst_index_one_lookup_tabletable. (exists pvs_le_gap_one_lookup_tabletabledomain. pvs_le_gap_one_lookup_tabletabledomain + (dst_index_one_lookup_tabletable) = (N)) -> exists dst_positive_one_lookup_tabletable dst_negative_one_lookup_tabletable dst_value_one_lookup_tabletable. ((((exists ff_h_pvs_one_lookup_tabletableentrypositive. ff_h_pvs_one_lookup_tabletableentrypositive + S (dst_positive_one_lookup_tabletable) = S ((S (dst_index_one_lookup_tabletable)) * dst_positive_scale_one_lookup_tabletable)) /\ exists ff_q_pvs_one_lookup_tabletableentrypositive. dst_positive_code_one_lookup_tabletable = ff_q_pvs_one_lookup_tabletableentrypositive * S ((S (dst_index_one_lookup_tabletable)) * dst_positive_scale_one_lookup_tabletable) + (dst_positive_one_lookup_tabletable))) /\ (((((exists ff_h_pvs_one_lookup_tabletableentrynegative. ff_h_pvs_one_lookup_tabletableentrynegative + S (dst_negative_one_lookup_tabletable) = S ((S (dst_index_one_lookup_tabletable)) * dst_negative_scale_one_lookup_tabletable)) /\ exists ff_q_pvs_one_lookup_tabletableentrynegative. dst_negative_code_one_lookup_tabletable = ff_q_pvs_one_lookup_tabletableentrynegative * S ((S (dst_index_one_lookup_tabletable)) * dst_negative_scale_one_lookup_tabletable) + (dst_negative_one_lookup_tabletable))) /\ (exists ge_balance_positive_one_lookup_tabletableentryvalue ge_balance_negative_one_lookup_tabletableentryvalue. (((((dst_value_one_lookup_tabletable) = 2 * (ge_balance_positive_one_lookup_tabletableentryvalue) /\ (ge_balance_negative_one_lookup_tabletableentryvalue) = 0) \/ exists ge_signed_half_one_lookup_tabletableentryvaluedecode. (((dst_value_one_lookup_tabletable) = 2 * ge_signed_half_one_lookup_tabletableentryvaluedecode + 1 /\ (ge_balance_positive_one_lookup_tabletableentryvalue) = 0) /\ (ge_balance_negative_one_lookup_tabletableentryvalue) = S ge_signed_half_one_lookup_tabletableentryvaluedecode))) /\ ((dst_positive_one_lookup_tabletable) + ge_balance_negative_one_lookup_tabletableentryvalue = (dst_negative_one_lookup_tabletable) + ge_balance_positive_one_lookup_tabletableentryvalue))))))))) /\ (forall du_index_one_lookup_table du_value_one_lookup_table. ~(du_index_one_lookup_table=0) -> (exists pvs_le_gap_one_lookup_tablebound. pvs_le_gap_one_lookup_tablebound + (du_index_one_lookup_table) = (N)) -> (exists dst_positive_code_one_lookup_tableentry dst_positive_scale_one_lookup_tableentry dst_negative_code_one_lookup_tableentry dst_negative_scale_one_lookup_tableentry dst_positive_one_lookup_tableentry dst_negative_one_lookup_tableentry. (((U) = (((((dst_positive_code_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry)) * S ((dst_positive_code_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry)) + ((dst_positive_scale_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry))) + (((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) * S ((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) + ((dst_negative_scale_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)))) * S ((((dst_positive_code_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry)) * S ((dst_positive_code_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry)) + ((dst_positive_scale_one_lookup_tableentry) + (dst_positive_scale_one_lookup_tableentry))) + (((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) * S ((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) + ((dst_negative_scale_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)))) + ((((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) * S ((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) + ((dst_negative_scale_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry))) + (((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) * S ((dst_negative_code_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)) + ((dst_negative_scale_one_lookup_tableentry) + (dst_negative_scale_one_lookup_tableentry)))))) /\ (((((exists ff_h_pvs_one_lookup_tableentrypositive. ff_h_pvs_one_lookup_tableentrypositive + S (dst_positive_one_lookup_tableentry) = S ((S (du_index_one_lookup_table)) * dst_positive_scale_one_lookup_tableentry)) /\ exists ff_q_pvs_one_lookup_tableentrypositive. dst_positive_code_one_lookup_tableentry = ff_q_pvs_one_lookup_tableentrypositive * S ((S (du_index_one_lookup_table)) * dst_positive_scale_one_lookup_tableentry) + (dst_positive_one_lookup_tableentry))) /\ (((((exists ff_h_pvs_one_lookup_tableentrynegative. ff_h_pvs_one_lookup_tableentrynegative + S (dst_negative_one_lookup_tableentry) = S ((S (du_index_one_lookup_table)) * dst_negative_scale_one_lookup_tableentry)) /\ exists ff_q_pvs_one_lookup_tableentrynegative. dst_negative_code_one_lookup_tableentry = ff_q_pvs_one_lookup_tableentrynegative * S ((S (du_index_one_lookup_table)) * dst_negative_scale_one_lookup_tableentry) + (dst_negative_one_lookup_tableentry))) /\ (exists ge_balance_positive_one_lookup_tableentryvalue ge_balance_negative_one_lookup_tableentryvalue. (((((du_value_one_lookup_table) = 2 * (ge_balance_positive_one_lookup_tableentryvalue) /\ (ge_balance_negative_one_lookup_tableentryvalue) = 0) \/ exists ge_signed_half_one_lookup_tableentryvaluedecode. (((du_value_one_lookup_table) = 2 * ge_signed_half_one_lookup_tableentryvaluedecode + 1 /\ (ge_balance_positive_one_lookup_tableentryvalue) = 0) /\ (ge_balance_negative_one_lookup_tableentryvalue) = S ge_signed_half_one_lookup_tableentryvaluedecode))) /\ ((dst_positive_one_lookup_tableentry) + ge_balance_negative_one_lookup_tableentryvalue = (dst_negative_one_lookup_tableentry) + ge_balance_positive_one_lookup_tableentryvalue))))))))) -> du_value_one_lookup_table=2))) -> ~(n=0) -> (exists pvs_le_gap_one_lookup_bound. pvs_le_gap_one_lookup_bound + (n) = (N)) -> (exists dst_positive_code_one_lookup_entry dst_positive_scale_one_lookup_entry dst_negative_code_one_lookup_entry dst_negative_scale_one_lookup_entry dst_positive_one_lookup_entry dst_negative_one_lookup_entry. (((U) = (((((dst_positive_code_one_lookup_entry) + (dst_positive_scale_one_lookup_entry)) * S ((dst_positive_code_one_lookup_entry) + (dst_positive_scale_one_lookup_entry)) + ((dst_positive_scale_one_lookup_entry) + (dst_positive_scale_one_lookup_entry))) + (((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) * S ((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) + ((dst_negative_scale_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)))) * S ((((dst_positive_code_one_lookup_entry) + (dst_positive_scale_one_lookup_entry)) * S ((dst_positive_code_one_lookup_entry) + (dst_positive_scale_one_lookup_entry)) + ((dst_positive_scale_one_lookup_entry) + (dst_positive_scale_one_lookup_entry))) + (((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) * S ((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) + ((dst_negative_scale_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)))) + ((((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) * S ((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) + ((dst_negative_scale_one_lookup_entry) + (dst_negative_scale_one_lookup_entry))) + (((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) * S ((dst_negative_code_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)) + ((dst_negative_scale_one_lookup_entry) + (dst_negative_scale_one_lookup_entry)))))) /\ (((((exists ff_h_pvs_one_lookup_entrypositive. ff_h_pvs_one_lookup_entrypositive + S (dst_positive_one_lookup_entry) = S ((S (n)) * dst_positive_scale_one_lookup_entry)) /\ exists ff_q_pvs_one_lookup_entrypositive. dst_positive_code_one_lookup_entry = ff_q_pvs_one_lookup_entrypositive * S ((S (n)) * dst_positive_scale_one_lookup_entry) + (dst_positive_one_lookup_entry))) /\ (((((exists ff_h_pvs_one_lookup_entrynegative. ff_h_pvs_one_lookup_entrynegative + S (dst_negative_one_lookup_entry) = S ((S (n)) * dst_negative_scale_one_lookup_entry)) /\ exists ff_q_pvs_one_lookup_entrynegative. dst_negative_code_one_lookup_entry = ff_q_pvs_one_lookup_entrynegative * S ((S (n)) * dst_negative_scale_one_lookup_entry) + (dst_negative_one_lookup_entry))) /\ (exists ge_balance_positive_one_lookup_entryvalue ge_balance_negative_one_lookup_entryvalue. (((((z) = 2 * (ge_balance_positive_one_lookup_entryvalue) /\ (ge_balance_negative_one_lookup_entryvalue) = 0) \/ exists ge_signed_half_one_lookup_entryvaluedecode. (((z) = 2 * ge_signed_half_one_lookup_entryvaluedecode + 1 /\ (ge_balance_positive_one_lookup_entryvalue) = 0) /\ (ge_balance_negative_one_lookup_entryvalue) = S ge_signed_half_one_lookup_entryvaluedecode))) /\ ((dst_positive_one_lookup_entry) + ge_balance_negative_one_lookup_entryvalue = (dst_negative_one_lookup_entry) + ge_balance_positive_one_lookup_entryvalue))))))))) -> z=2

Complete tactic proof in conservative notation

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

15 script commands · 3 reading checkpoints · 0 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–8

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

  1. L1
    intro N
  2. L2
    intro U
  3. L3
    intro n
  4. L4
    intro z
  5. L5
    intro hu
  6. L6
    intro hn
  7. L7
    intro hb
  8. L8
    intro hz
02Separate the logical casesL9–9

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

  1. L9
    cases hu
03Use earlier factsL10–15

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

  1. L10
    specialize hu_right (n)
  2. L11
    specialize hu_right (z)
  3. L12
    apply hu_right
  4. L13
    exact hn
  5. L14
    exact hb
  6. L15
    exact hz

Library-wide reading audit

Original defined command ledger · 15 lines
  1. 0001intro N
  2. 0002intro U
  3. 0003intro n
  4. 0004intro z
  5. 0005intro hu
  6. 0006intro hn
  7. 0007intro hb
  8. 0008intro hz
  9. 0009cases hu
  10. 0010specialize hu_right (n)
  11. 0011specialize hu_right (z)
  12. 0012apply hu_right
  13. 0013exact hn
  14. 0014exact hb
  15. 0015exact hz