DV0013

divisor_mask_entry_exists

Constructively decide zero and divisibility, then construct the actual retained lookup or zero code; no quotient or choice oracle is assumed.

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

∀ N. ∀ F. ∀ n. ∀ d. ArithTable(N,F) → Le(d,N) → ∃ x. DivisorMaskEntry(F,n,d,x)

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

Definition DAG

ArithTable(N,F) · 1ArithAt(F,i,z) · 1DivisorMaskEntry(F,n,d,z) · 1Le(a,b) · 1Dvd(d,n) · 2

Actual proof prerequisites

eq_decidable · checked external prerequisitemultiple_decidable_nonzero · checked external prerequisitedivisor_signed_table_lookup · checked external prerequisitedivisor_mask_entry_zerodivisor_mask_entry_from_quotientdivisor_mask_entry_from_nondivisor
Original expanded first-order statement 
forall N F n d. (exists dst_positive_code_choice_table dst_positive_scale_choice_table dst_negative_code_choice_table dst_negative_scale_choice_table. (((F) = (((((dst_positive_code_choice_table) + (dst_positive_scale_choice_table)) * S ((dst_positive_code_choice_table) + (dst_positive_scale_choice_table)) + ((dst_positive_scale_choice_table) + (dst_positive_scale_choice_table))) + (((dst_negative_code_choice_table) + (dst_negative_scale_choice_table)) * S ((dst_negative_code_choice_table) + (dst_negative_scale_choice_table)) + ((dst_negative_scale_choice_table) + (dst_negative_scale_choice_table)))) * S ((((dst_positive_code_choice_table) + (dst_positive_scale_choice_table)) * S ((dst_positive_code_choice_table) + (dst_positive_scale_choice_table)) + ((dst_positive_scale_choice_table) + (dst_positive_scale_choice_table))) + (((dst_negative_code_choice_table) + (dst_negative_scale_choice_table)) * S ((dst_negative_code_choice_table) + (dst_negative_scale_choice_table)) + ((dst_negative_scale_choice_table) + (dst_negative_scale_choice_table)))) + ((((dst_negative_code_choice_table) + (dst_negative_scale_choice_table)) * S ((dst_negative_code_choice_table) + (dst_negative_scale_choice_table)) + ((dst_negative_scale_choice_table) + (dst_negative_scale_choice_table))) + (((dst_negative_code_choice_table) + (dst_negative_scale_choice_table)) * S ((dst_negative_code_choice_table) + (dst_negative_scale_choice_table)) + ((dst_negative_scale_choice_table) + (dst_negative_scale_choice_table)))))) /\ (forall dst_index_choice_table. (exists pvs_le_gap_choice_tabledomain. pvs_le_gap_choice_tabledomain + (dst_index_choice_table) = (N)) -> exists dst_positive_choice_table dst_negative_choice_table dst_value_choice_table. ((((exists ff_h_pvs_choice_tableentrypositive. ff_h_pvs_choice_tableentrypositive + S (dst_positive_choice_table) = S ((S (dst_index_choice_table)) * dst_positive_scale_choice_table)) /\ exists ff_q_pvs_choice_tableentrypositive. dst_positive_code_choice_table = ff_q_pvs_choice_tableentrypositive * S ((S (dst_index_choice_table)) * dst_positive_scale_choice_table) + (dst_positive_choice_table))) /\ (((((exists ff_h_pvs_choice_tableentrynegative. ff_h_pvs_choice_tableentrynegative + S (dst_negative_choice_table) = S ((S (dst_index_choice_table)) * dst_negative_scale_choice_table)) /\ exists ff_q_pvs_choice_tableentrynegative. dst_negative_code_choice_table = ff_q_pvs_choice_tableentrynegative * S ((S (dst_index_choice_table)) * dst_negative_scale_choice_table) + (dst_negative_choice_table))) /\ (exists ge_balance_positive_choice_tableentryvalue ge_balance_negative_choice_tableentryvalue. (((((dst_value_choice_table) = 2 * (ge_balance_positive_choice_tableentryvalue) /\ (ge_balance_negative_choice_tableentryvalue) = 0) \/ exists ge_signed_half_choice_tableentryvaluedecode. (((dst_value_choice_table) = 2 * ge_signed_half_choice_tableentryvaluedecode + 1 /\ (ge_balance_positive_choice_tableentryvalue) = 0) /\ (ge_balance_negative_choice_tableentryvalue) = S ge_signed_half_choice_tableentryvaluedecode))) /\ ((dst_positive_choice_table) + ge_balance_negative_choice_tableentryvalue = (dst_negative_choice_table) + ge_balance_positive_choice_tableentryvalue))))))))) -> (exists pvs_le_gap_choice_bound. pvs_le_gap_choice_bound + (d) = (N)) -> exists z. ((((~((d)=0)) /\ (exists dm_quotient_choice_result. (((n)=(d)*dm_quotient_choice_result) /\ (exists dst_positive_code_choice_resultinput dst_positive_scale_choice_resultinput dst_negative_code_choice_resultinput dst_negative_scale_choice_resultinput dst_positive_choice_resultinput dst_negative_choice_resultinput. (((F) = (((((dst_positive_code_choice_resultinput) + (dst_positive_scale_choice_resultinput)) * S ((dst_positive_code_choice_resultinput) + (dst_positive_scale_choice_resultinput)) + ((dst_positive_scale_choice_resultinput) + (dst_positive_scale_choice_resultinput))) + (((dst_negative_code_choice_resultinput) + (dst_negative_scale_choice_resultinput)) * S ((dst_negative_code_choice_resultinput) + (dst_negative_scale_choice_resultinput)) + ((dst_negative_scale_choice_resultinput) + (dst_negative_scale_choice_resultinput)))) * S ((((dst_positive_code_choice_resultinput) + (dst_positive_scale_choice_resultinput)) * S ((dst_positive_code_choice_resultinput) + (dst_positive_scale_choice_resultinput)) + ((dst_positive_scale_choice_resultinput) + (dst_positive_scale_choice_resultinput))) + (((dst_negative_code_choice_resultinput) + (dst_negative_scale_choice_resultinput)) * S ((dst_negative_code_choice_resultinput) + (dst_negative_scale_choice_resultinput)) + ((dst_negative_scale_choice_resultinput) + (dst_negative_scale_choice_resultinput)))) + ((((dst_negative_code_choice_resultinput) + (dst_negative_scale_choice_resultinput)) * S ((dst_negative_code_choice_resultinput) + (dst_negative_scale_choice_resultinput)) + ((dst_negative_scale_choice_resultinput) + (dst_negative_scale_choice_resultinput))) + (((dst_negative_code_choice_resultinput) + (dst_negative_scale_choice_resultinput)) * S ((dst_negative_code_choice_resultinput) + (dst_negative_scale_choice_resultinput)) + ((dst_negative_scale_choice_resultinput) + (dst_negative_scale_choice_resultinput)))))) /\ (((((exists ff_h_pvs_choice_resultinputpositive. ff_h_pvs_choice_resultinputpositive + S (dst_positive_choice_resultinput) = S ((S (d)) * dst_positive_scale_choice_resultinput)) /\ exists ff_q_pvs_choice_resultinputpositive. dst_positive_code_choice_resultinput = ff_q_pvs_choice_resultinputpositive * S ((S (d)) * dst_positive_scale_choice_resultinput) + (dst_positive_choice_resultinput))) /\ (((((exists ff_h_pvs_choice_resultinputnegative. ff_h_pvs_choice_resultinputnegative + S (dst_negative_choice_resultinput) = S ((S (d)) * dst_negative_scale_choice_resultinput)) /\ exists ff_q_pvs_choice_resultinputnegative. dst_negative_code_choice_resultinput = ff_q_pvs_choice_resultinputnegative * S ((S (d)) * dst_negative_scale_choice_resultinput) + (dst_negative_choice_resultinput))) /\ (exists ge_balance_positive_choice_resultinputvalue ge_balance_negative_choice_resultinputvalue. (((((z) = 2 * (ge_balance_positive_choice_resultinputvalue) /\ (ge_balance_negative_choice_resultinputvalue) = 0) \/ exists ge_signed_half_choice_resultinputvaluedecode. (((z) = 2 * ge_signed_half_choice_resultinputvaluedecode + 1 /\ (ge_balance_positive_choice_resultinputvalue) = 0) /\ (ge_balance_negative_choice_resultinputvalue) = S ge_signed_half_choice_resultinputvaluedecode))) /\ ((dst_positive_choice_resultinput) + ge_balance_negative_choice_resultinputvalue = (dst_negative_choice_resultinput) + ge_balance_positive_choice_resultinputvalue))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_choice_resultnondivisor. (n) = (d) * pvs_factor_choice_resultnondivisor)) /\ ((z)=0))))

Complete tactic proof in conservative notation

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

54 script commands · 14 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.

Named ingredients (3)
divisor mask entry zerodivisor mask entry from quotientdivisor mask entry from nondivisor
01Fix variables and assumptionsL1–6

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

  1. L1
    intro N
  2. L2
    intro F
  3. L3
    intro n
  4. L4
    intro d
  5. L5
    intro ht
  6. L6
    intro hbound
02Establish hcL7–10

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

  1. L7
    have hc : d=0 \/ ~(d=0)
  2. L8
    specialize eq_decidable (d)
  3. L9
    specialize eq_decidable (0)
  4. L10
    apply eq_decidable
03Separate the logical casesL11–11

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

  1. L11
    cases hc
04Construct an explicit witnessL12–12

Supply the displayed value, then prove that it has the required property.

  1. L12
    exists 0
05Calculate and transport equalitiesL13–20

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

  1. L13
    rewrite hc_left
  2. L14
    rewrite hc_left
  3. L15
    rewrite hc_left
  4. L16
    rewrite hc_left
  5. L17
    rewrite hc_left
  6. L18
    rewrite hc_left
  7. L19
    rewrite hc_left
  8. L20
    rewrite hc_left
06Use earlier factsL21–23

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

  1. L21
    specialize divisor_mask_entry_zero (F)
  2. L22
    specialize divisor_mask_entry_zero (n)
  3. L23
    apply divisor_mask_entry_zero
07Establish hdivL24–28

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

  1. L24
    have hdiv : Dvd(d,n) ∨ ¬Dvd(d,n)Definitions: Dvd(d,n)Original native command in the exact edition
  2. L25
    specialize multiple_decidable_nonzero (d)
  3. L26
    specialize multiple_decidable_nonzero (n)
  4. L27
    apply multiple_decidable_nonzero
  5. L28
    exact hc_right
08Separate the logical casesL29–30

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

  1. L29
    cases hdiv
  2. L30
    cases hdiv_left
09Establish hzL31–37

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.

  1. L31
    have hz : ∃ z. ArithAt(F,d,z)Definitions: ArithAt(F,d,z)Original native command in the exact edition
  2. L32
    specialize divisor_signed_table_lookup (N)
  3. L33
    specialize divisor_signed_table_lookup (F)
  4. L34
    specialize divisor_signed_table_lookup (d)
  5. L35
    apply divisor_signed_table_lookup
  6. L36
    exact ht
  7. L37
    exact hbound
10Separate the logical casesL38–38

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

  1. L38
    cases hz
11Construct an explicit witnessL39–39

Supply the displayed value, then prove that it has the required property.

  1. L39
    exists x1
12Use earlier factsL40–48

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

  1. L40
    specialize divisor_mask_entry_from_quotient (F)
  2. L41
    specialize divisor_mask_entry_from_quotient (n)
  3. L42
    specialize divisor_mask_entry_from_quotient (d)
  4. L43
    specialize divisor_mask_entry_from_quotient (x)
  5. L44
    specialize divisor_mask_entry_from_quotient (x1)
  6. L45
    apply divisor_mask_entry_from_quotient
  7. L46
    exact hc_right
  8. L47
    exact hdiv_left_witness
  9. L48
    exact hz_witness
13Construct an explicit witnessL49–49

Supply the displayed value, then prove that it has the required property.

  1. L49
    exists 0
14Use earlier factsL50–54

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

  1. L50
    specialize divisor_mask_entry_from_nondivisor (F)
  2. L51
    specialize divisor_mask_entry_from_nondivisor (n)
  3. L52
    specialize divisor_mask_entry_from_nondivisor (d)
  4. L53
    apply divisor_mask_entry_from_nondivisor
  5. L54
    exact hdiv_right

Library-wide reading audit

Original defined command ledger · 54 lines
  1. 0001intro N
  2. 0002intro F
  3. 0003intro n
  4. 0004intro d
  5. 0005intro ht
  6. 0006intro hbound
  7. 0007have hc : d=0 \/ ~(d=0)
  8. 0008specialize eq_decidable (d)
  9. 0009specialize eq_decidable (0)
  10. 0010apply eq_decidable
  11. 0011cases hc
  12. 0012exists 0
  13. 0013rewrite hc_left
  14. 0014rewrite hc_left
  15. 0015rewrite hc_left
  16. 0016rewrite hc_left
  17. 0017rewrite hc_left
  18. 0018rewrite hc_left
  19. 0019rewrite hc_left
  20. 0020rewrite hc_left
  21. 0021specialize divisor_mask_entry_zero (F)
  22. 0022specialize divisor_mask_entry_zero (n)
  23. 0023apply divisor_mask_entry_zero
  24. 0024have hdiv : Dvd(d,n) ∨ ¬Dvd(d,n)
  25. 0025specialize multiple_decidable_nonzero (d)
  26. 0026specialize multiple_decidable_nonzero (n)
  27. 0027apply multiple_decidable_nonzero
  28. 0028exact hc_right
  29. 0029cases hdiv
  30. 0030cases hdiv_left
  31. 0031have hz : ∃ z. ArithAt(F,d,z)
  32. 0032specialize divisor_signed_table_lookup (N)
  33. 0033specialize divisor_signed_table_lookup (F)
  34. 0034specialize divisor_signed_table_lookup (d)
  35. 0035apply divisor_signed_table_lookup
  36. 0036exact ht
  37. 0037exact hbound
  38. 0038cases hz
  39. 0039exists x1
  40. 0040specialize divisor_mask_entry_from_quotient (F)
  41. 0041specialize divisor_mask_entry_from_quotient (n)
  42. 0042specialize divisor_mask_entry_from_quotient (d)
  43. 0043specialize divisor_mask_entry_from_quotient (x)
  44. 0044specialize divisor_mask_entry_from_quotient (x1)
  45. 0045apply divisor_mask_entry_from_quotient
  46. 0046exact hc_right
  47. 0047exact hdiv_left_witness
  48. 0048exact hz_witness
  49. 0049exists 0
  50. 0050specialize divisor_mask_entry_from_nondivisor (F)
  51. 0051specialize divisor_mask_entry_from_nondivisor (n)
  52. 0052specialize divisor_mask_entry_from_nondivisor (d)
  53. 0053apply divisor_mask_entry_from_nondivisor
  54. 0054exact hdiv_right