DV0017

divisor_mask_prefix_zero_constructor

The genuine singleton zero table is the base mask prefix for any fixed divisibility target.

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.

A genuine divisor mask has S n entries, indexed zero through n, and forces its zeroth entry to zero regardless of F(0). Möbius values remain positive-domain only. This family constructs divisor sums and Möbius tables; cancellation and the full G007 endpoint are separately proved later in the same release.

Exact theorem in conservative defined notation

∀ F. ∀ n. ∀ M. ArithTable(0,M) → ArithAt(M,0,0) → DivisorMask(F,n,0,M)

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

Definition DAG

ArithTable(N,F) · 1ArithAt(F,i,z) · 1DivisorMask(F,n,l,M) · 1

Actual proof prerequisites

le_zero · checked external prerequisitedivisor_signed_table_at_functional · checked external prerequisite
Original expanded first-order statement 
forall F n M. (exists dst_positive_code_base_table dst_positive_scale_base_table dst_negative_code_base_table dst_negative_scale_base_table. (((M) = (((((dst_positive_code_base_table) + (dst_positive_scale_base_table)) * S ((dst_positive_code_base_table) + (dst_positive_scale_base_table)) + ((dst_positive_scale_base_table) + (dst_positive_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))) * S ((((dst_positive_code_base_table) + (dst_positive_scale_base_table)) * S ((dst_positive_code_base_table) + (dst_positive_scale_base_table)) + ((dst_positive_scale_base_table) + (dst_positive_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))) + ((((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table))) + (((dst_negative_code_base_table) + (dst_negative_scale_base_table)) * S ((dst_negative_code_base_table) + (dst_negative_scale_base_table)) + ((dst_negative_scale_base_table) + (dst_negative_scale_base_table)))))) /\ (forall dst_index_base_table. (exists pvs_le_gap_base_tabledomain. pvs_le_gap_base_tabledomain + (dst_index_base_table) = (0)) -> exists dst_positive_base_table dst_negative_base_table dst_value_base_table. ((((exists ff_h_pvs_base_tableentrypositive. ff_h_pvs_base_tableentrypositive + S (dst_positive_base_table) = S ((S (dst_index_base_table)) * dst_positive_scale_base_table)) /\ exists ff_q_pvs_base_tableentrypositive. dst_positive_code_base_table = ff_q_pvs_base_tableentrypositive * S ((S (dst_index_base_table)) * dst_positive_scale_base_table) + (dst_positive_base_table))) /\ (((((exists ff_h_pvs_base_tableentrynegative. ff_h_pvs_base_tableentrynegative + S (dst_negative_base_table) = S ((S (dst_index_base_table)) * dst_negative_scale_base_table)) /\ exists ff_q_pvs_base_tableentrynegative. dst_negative_code_base_table = ff_q_pvs_base_tableentrynegative * S ((S (dst_index_base_table)) * dst_negative_scale_base_table) + (dst_negative_base_table))) /\ (exists ge_balance_positive_base_tableentryvalue ge_balance_negative_base_tableentryvalue. (((((dst_value_base_table) = 2 * (ge_balance_positive_base_tableentryvalue) /\ (ge_balance_negative_base_tableentryvalue) = 0) \/ exists ge_signed_half_base_tableentryvaluedecode. (((dst_value_base_table) = 2 * ge_signed_half_base_tableentryvaluedecode + 1 /\ (ge_balance_positive_base_tableentryvalue) = 0) /\ (ge_balance_negative_base_tableentryvalue) = S ge_signed_half_base_tableentryvaluedecode))) /\ ((dst_positive_base_table) + ge_balance_negative_base_tableentryvalue = (dst_negative_base_table) + ge_balance_positive_base_tableentryvalue))))))))) -> (exists dst_positive_code_base_entry dst_positive_scale_base_entry dst_negative_code_base_entry dst_negative_scale_base_entry dst_positive_base_entry dst_negative_base_entry. (((M) = (((((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) * S ((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) + ((dst_positive_scale_base_entry) + (dst_positive_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))) * S ((((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) * S ((dst_positive_code_base_entry) + (dst_positive_scale_base_entry)) + ((dst_positive_scale_base_entry) + (dst_positive_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))) + ((((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry))) + (((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) * S ((dst_negative_code_base_entry) + (dst_negative_scale_base_entry)) + ((dst_negative_scale_base_entry) + (dst_negative_scale_base_entry)))))) /\ (((((exists ff_h_pvs_base_entrypositive. ff_h_pvs_base_entrypositive + S (dst_positive_base_entry) = S ((S (0)) * dst_positive_scale_base_entry)) /\ exists ff_q_pvs_base_entrypositive. dst_positive_code_base_entry = ff_q_pvs_base_entrypositive * S ((S (0)) * dst_positive_scale_base_entry) + (dst_positive_base_entry))) /\ (((((exists ff_h_pvs_base_entrynegative. ff_h_pvs_base_entrynegative + S (dst_negative_base_entry) = S ((S (0)) * dst_negative_scale_base_entry)) /\ exists ff_q_pvs_base_entrynegative. dst_negative_code_base_entry = ff_q_pvs_base_entrynegative * S ((S (0)) * dst_negative_scale_base_entry) + (dst_negative_base_entry))) /\ (exists ge_balance_positive_base_entryvalue ge_balance_negative_base_entryvalue. (((((0) = 2 * (ge_balance_positive_base_entryvalue) /\ (ge_balance_negative_base_entryvalue) = 0) \/ exists ge_signed_half_base_entryvaluedecode. (((0) = 2 * ge_signed_half_base_entryvaluedecode + 1 /\ (ge_balance_positive_base_entryvalue) = 0) /\ (ge_balance_negative_base_entryvalue) = S ge_signed_half_base_entryvaluedecode))) /\ ((dst_positive_base_entry) + ge_balance_negative_base_entryvalue = (dst_negative_base_entry) + ge_balance_positive_base_entryvalue))))))))) -> (((exists dst_positive_code_base_resulttable dst_positive_scale_base_resulttable dst_negative_code_base_resulttable dst_negative_scale_base_resulttable. (((M) = (((((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) * S ((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) + ((dst_positive_scale_base_resulttable) + (dst_positive_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))) * S ((((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) * S ((dst_positive_code_base_resulttable) + (dst_positive_scale_base_resulttable)) + ((dst_positive_scale_base_resulttable) + (dst_positive_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))) + ((((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable))) + (((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) * S ((dst_negative_code_base_resulttable) + (dst_negative_scale_base_resulttable)) + ((dst_negative_scale_base_resulttable) + (dst_negative_scale_base_resulttable)))))) /\ (forall dst_index_base_resulttable. (exists pvs_le_gap_base_resulttabledomain. pvs_le_gap_base_resulttabledomain + (dst_index_base_resulttable) = (0)) -> exists dst_positive_base_resulttable dst_negative_base_resulttable dst_value_base_resulttable. ((((exists ff_h_pvs_base_resulttableentrypositive. ff_h_pvs_base_resulttableentrypositive + S (dst_positive_base_resulttable) = S ((S (dst_index_base_resulttable)) * dst_positive_scale_base_resulttable)) /\ exists ff_q_pvs_base_resulttableentrypositive. dst_positive_code_base_resulttable = ff_q_pvs_base_resulttableentrypositive * S ((S (dst_index_base_resulttable)) * dst_positive_scale_base_resulttable) + (dst_positive_base_resulttable))) /\ (((((exists ff_h_pvs_base_resulttableentrynegative. ff_h_pvs_base_resulttableentrynegative + S (dst_negative_base_resulttable) = S ((S (dst_index_base_resulttable)) * dst_negative_scale_base_resulttable)) /\ exists ff_q_pvs_base_resulttableentrynegative. dst_negative_code_base_resulttable = ff_q_pvs_base_resulttableentrynegative * S ((S (dst_index_base_resulttable)) * dst_negative_scale_base_resulttable) + (dst_negative_base_resulttable))) /\ (exists ge_balance_positive_base_resulttableentryvalue ge_balance_negative_base_resulttableentryvalue. (((((dst_value_base_resulttable) = 2 * (ge_balance_positive_base_resulttableentryvalue) /\ (ge_balance_negative_base_resulttableentryvalue) = 0) \/ exists ge_signed_half_base_resulttableentryvaluedecode. (((dst_value_base_resulttable) = 2 * ge_signed_half_base_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_base_resulttableentryvalue) = 0) /\ (ge_balance_negative_base_resulttableentryvalue) = S ge_signed_half_base_resulttableentryvaluedecode))) /\ ((dst_positive_base_resulttable) + ge_balance_negative_base_resulttableentryvalue = (dst_negative_base_resulttable) + ge_balance_positive_base_resulttableentryvalue))))))))) /\ (forall dm_index_base_result dm_value_base_result. (exists pvs_le_gap_base_resultdomain. pvs_le_gap_base_resultdomain + (dm_index_base_result) = (0)) -> (exists dst_positive_code_base_resultlookup dst_positive_scale_base_resultlookup dst_negative_code_base_resultlookup dst_negative_scale_base_resultlookup dst_positive_base_resultlookup dst_negative_base_resultlookup. (((M) = (((((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) * S ((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) + ((dst_positive_scale_base_resultlookup) + (dst_positive_scale_base_resultlookup))) + (((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup)))) * S ((((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) * S ((dst_positive_code_base_resultlookup) + (dst_positive_scale_base_resultlookup)) + ((dst_positive_scale_base_resultlookup) + (dst_positive_scale_base_resultlookup))) + (((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup)))) + ((((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup))) + (((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) * S ((dst_negative_code_base_resultlookup) + (dst_negative_scale_base_resultlookup)) + ((dst_negative_scale_base_resultlookup) + (dst_negative_scale_base_resultlookup)))))) /\ (((((exists ff_h_pvs_base_resultlookuppositive. ff_h_pvs_base_resultlookuppositive + S (dst_positive_base_resultlookup) = S ((S (dm_index_base_result)) * dst_positive_scale_base_resultlookup)) /\ exists ff_q_pvs_base_resultlookuppositive. dst_positive_code_base_resultlookup = ff_q_pvs_base_resultlookuppositive * S ((S (dm_index_base_result)) * dst_positive_scale_base_resultlookup) + (dst_positive_base_resultlookup))) /\ (((((exists ff_h_pvs_base_resultlookupnegative. ff_h_pvs_base_resultlookupnegative + S (dst_negative_base_resultlookup) = S ((S (dm_index_base_result)) * dst_negative_scale_base_resultlookup)) /\ exists ff_q_pvs_base_resultlookupnegative. dst_negative_code_base_resultlookup = ff_q_pvs_base_resultlookupnegative * S ((S (dm_index_base_result)) * dst_negative_scale_base_resultlookup) + (dst_negative_base_resultlookup))) /\ (exists ge_balance_positive_base_resultlookupvalue ge_balance_negative_base_resultlookupvalue. (((((dm_value_base_result) = 2 * (ge_balance_positive_base_resultlookupvalue) /\ (ge_balance_negative_base_resultlookupvalue) = 0) \/ exists ge_signed_half_base_resultlookupvaluedecode. (((dm_value_base_result) = 2 * ge_signed_half_base_resultlookupvaluedecode + 1 /\ (ge_balance_positive_base_resultlookupvalue) = 0) /\ (ge_balance_negative_base_resultlookupvalue) = S ge_signed_half_base_resultlookupvaluedecode))) /\ ((dst_positive_base_resultlookup) + ge_balance_negative_base_resultlookupvalue = (dst_negative_base_resultlookup) + ge_balance_positive_base_resultlookupvalue))))))))) -> ((((~((dm_index_base_result)=0)) /\ (exists dm_quotient_base_resultentry. (((n)=(dm_index_base_result)*dm_quotient_base_resultentry) /\ (exists dst_positive_code_base_resultentryinput dst_positive_scale_base_resultentryinput dst_negative_code_base_resultentryinput dst_negative_scale_base_resultentryinput dst_positive_base_resultentryinput dst_negative_base_resultentryinput. (((F) = (((((dst_positive_code_base_resultentryinput) + (dst_positive_scale_base_resultentryinput)) * S ((dst_positive_code_base_resultentryinput) + (dst_positive_scale_base_resultentryinput)) + ((dst_positive_scale_base_resultentryinput) + (dst_positive_scale_base_resultentryinput))) + (((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) * S ((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) + ((dst_negative_scale_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)))) * S ((((dst_positive_code_base_resultentryinput) + (dst_positive_scale_base_resultentryinput)) * S ((dst_positive_code_base_resultentryinput) + (dst_positive_scale_base_resultentryinput)) + ((dst_positive_scale_base_resultentryinput) + (dst_positive_scale_base_resultentryinput))) + (((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) * S ((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) + ((dst_negative_scale_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)))) + ((((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) * S ((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) + ((dst_negative_scale_base_resultentryinput) + (dst_negative_scale_base_resultentryinput))) + (((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) * S ((dst_negative_code_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)) + ((dst_negative_scale_base_resultentryinput) + (dst_negative_scale_base_resultentryinput)))))) /\ (((((exists ff_h_pvs_base_resultentryinputpositive. ff_h_pvs_base_resultentryinputpositive + S (dst_positive_base_resultentryinput) = S ((S (dm_index_base_result)) * dst_positive_scale_base_resultentryinput)) /\ exists ff_q_pvs_base_resultentryinputpositive. dst_positive_code_base_resultentryinput = ff_q_pvs_base_resultentryinputpositive * S ((S (dm_index_base_result)) * dst_positive_scale_base_resultentryinput) + (dst_positive_base_resultentryinput))) /\ (((((exists ff_h_pvs_base_resultentryinputnegative. ff_h_pvs_base_resultentryinputnegative + S (dst_negative_base_resultentryinput) = S ((S (dm_index_base_result)) * dst_negative_scale_base_resultentryinput)) /\ exists ff_q_pvs_base_resultentryinputnegative. dst_negative_code_base_resultentryinput = ff_q_pvs_base_resultentryinputnegative * S ((S (dm_index_base_result)) * dst_negative_scale_base_resultentryinput) + (dst_negative_base_resultentryinput))) /\ (exists ge_balance_positive_base_resultentryinputvalue ge_balance_negative_base_resultentryinputvalue. (((((dm_value_base_result) = 2 * (ge_balance_positive_base_resultentryinputvalue) /\ (ge_balance_negative_base_resultentryinputvalue) = 0) \/ exists ge_signed_half_base_resultentryinputvaluedecode. (((dm_value_base_result) = 2 * ge_signed_half_base_resultentryinputvaluedecode + 1 /\ (ge_balance_positive_base_resultentryinputvalue) = 0) /\ (ge_balance_negative_base_resultentryinputvalue) = S ge_signed_half_base_resultentryinputvaluedecode))) /\ ((dst_positive_base_resultentryinput) + ge_balance_negative_base_resultentryinputvalue = (dst_negative_base_resultentryinput) + ge_balance_positive_base_resultentryinputvalue))))))))))))) \/ ((((dm_index_base_result)=0 \/ ~(exists pvs_factor_base_resultentrynondivisor. (n) = (dm_index_base_result) * pvs_factor_base_resultentrynondivisor)) /\ ((dm_value_base_result)=0)))))))

Complete tactic proof in conservative notation

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

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

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

  1. L1
    intro F
  2. L2
    intro n
  3. L3
    intro M
  4. L4
    intro ht
  5. L5
    intro hz
02Separate the logical casesL6–6

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

  1. L6
    split
03Use earlier factsL7–7

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

  1. L7
    exact ht
04Fix variables and assumptionsL8–11

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

  1. L8
    intro d
  2. L9
    intro z
  3. L10
    intro hd
  4. L11
    intro he
05Establish hd0L12–19

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

  1. L12
    have hd0 : d=0
  2. L13
    specialize le_zero (d)
  3. L14
    apply le_zero
  4. L15
    exact hd
  5. L16
    rewrite hd0 at he
  6. L17
    rewrite hd0 at he
  7. L18
    rewrite hd0 at he
  8. L19
    rewrite hd0 at he
06Separate the logical casesL20–22

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

  1. L20
    right
  2. L21
    split
  3. L22
    left
07Use earlier factsL23–30

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

  1. L23
    exact hd0
  2. L24
    specialize divisor_signed_table_at_functional (M)
  3. L25
    specialize divisor_signed_table_at_functional (0)
  4. L26
    specialize divisor_signed_table_at_functional (z)
  5. L27
    specialize divisor_signed_table_at_functional (0)
  6. L28
    apply divisor_signed_table_at_functional
  7. L29
    exact he
  8. L30
    exact hz

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro F
  2. 0002intro n
  3. 0003intro M
  4. 0004intro ht
  5. 0005intro hz
  6. 0006split
  7. 0007exact ht
  8. 0008intro d
  9. 0009intro z
  10. 0010intro hd
  11. 0011intro he
  12. 0012have hd0 : d=0
  13. 0013specialize le_zero (d)
  14. 0014apply le_zero
  15. 0015exact hd
  16. 0016rewrite hd0 at he
  17. 0017rewrite hd0 at he
  18. 0018rewrite hd0 at he
  19. 0019rewrite hd0 at he
  20. 0020right
  21. 0021split
  22. 0022left
  23. 0023exact hd0
  24. 0024specialize divisor_signed_table_at_functional (M)
  25. 0025specialize divisor_signed_table_at_functional (0)
  26. 0026specialize divisor_signed_table_at_functional (z)
  27. 0027specialize divisor_signed_table_at_functional (0)
  28. 0028apply divisor_signed_table_at_functional
  29. 0029exact he
  30. 0030exact hz