DV0013

divisor_mask_entry_exists

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

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

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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 6 declared prerequisites and contains 54 exact native proof lines.

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

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized multiple_decidable_nonzero Stable theorem; checked-use authorized divisor_signed_table_lookup Alpha theorem; checked-use authorized DV0010 divisor_mask_entry_zero DV0011 divisor_mask_entry_from_quotient DV0012 divisor_mask_entry_from_nondivisor

Direct dependents

DV0019 divisor_mask_prefix_exists

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

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.

Named ingredients (3)
divisor mask entry zerodivisor mask entry from quotientdivisor mask entry from nondivisor

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 : (exists pvs_factor_choice_yes. (n) = (d) * pvs_factor_choice_yes) \/ ~(exists pvs_factor_choice_no. (n) = (d) * pvs_factor_choice_no)
  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
  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 exact 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 : (exists pvs_factor_choice_yes. (n) = (d) * pvs_factor_choice_yes) \/ ~(exists pvs_factor_choice_no. (n) = (d) * pvs_factor_choice_no)
  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 : exists z. (exists dst_positive_code_choice_actual_input dst_positive_scale_choice_actual_input dst_negative_code_choice_actual_input dst_negative_scale_choice_actual_input dst_positive_choice_actual_input dst_negative_choice_actual_input. (((F) = (((((dst_positive_code_choice_actual_input) + (dst_positive_scale_choice_actual_input)) * S ((dst_positive_code_choice_actual_input) + (dst_positive_scale_choice_actual_input)) + ((dst_positive_scale_choice_actual_input) + (dst_positive_scale_choice_actual_input))) + (((dst_negative_code_choice_actual_input) + (dst_negative_scale_choice_actual_input)) * S ((dst_negative_code_choice_actual_input) + (dst_negative_scale_choice_actual_input)) + ((dst_negative_scale_choice_actual_input) + (dst_negative_scale_choice_actual_input)))) * S ((((dst_positive_code_choice_actual_input) + (dst_positive_scale_choice_actual_input)) * S ((dst_positive_code_choice_actual_input) + (dst_positive_scale_choice_actual_input)) + ((dst_positive_scale_choice_actual_input) + (dst_positive_scale_choice_actual_input))) + (((dst_negative_code_choice_actual_input) + (dst_negative_scale_choice_actual_input)) * S ((dst_negative_code_choice_actual_input) + (dst_negative_scale_choice_actual_input)) + ((dst_negative_scale_choice_actual_input) + (dst_negative_scale_choice_actual_input)))) + ((((dst_negative_code_choice_actual_input) + (dst_negative_scale_choice_actual_input)) * S ((dst_negative_code_choice_actual_input) + (dst_negative_scale_choice_actual_input)) + ((dst_negative_scale_choice_actual_input) + (dst_negative_scale_choice_actual_input))) + (((dst_negative_code_choice_actual_input) + (dst_negative_scale_choice_actual_input)) * S ((dst_negative_code_choice_actual_input) + (dst_negative_scale_choice_actual_input)) + ((dst_negative_scale_choice_actual_input) + (dst_negative_scale_choice_actual_input)))))) /\ (((((exists ff_h_pvs_choice_actual_inputpositive. ff_h_pvs_choice_actual_inputpositive + S (dst_positive_choice_actual_input) = S ((S (d)) * dst_positive_scale_choice_actual_input)) /\ exists ff_q_pvs_choice_actual_inputpositive. dst_positive_code_choice_actual_input = ff_q_pvs_choice_actual_inputpositive * S ((S (d)) * dst_positive_scale_choice_actual_input) + (dst_positive_choice_actual_input))) /\ (((((exists ff_h_pvs_choice_actual_inputnegative. ff_h_pvs_choice_actual_inputnegative + S (dst_negative_choice_actual_input) = S ((S (d)) * dst_negative_scale_choice_actual_input)) /\ exists ff_q_pvs_choice_actual_inputnegative. dst_negative_code_choice_actual_input = ff_q_pvs_choice_actual_inputnegative * S ((S (d)) * dst_negative_scale_choice_actual_input) + (dst_negative_choice_actual_input))) /\ (exists ge_balance_positive_choice_actual_inputvalue ge_balance_negative_choice_actual_inputvalue. (((((z) = 2 * (ge_balance_positive_choice_actual_inputvalue) /\ (ge_balance_negative_choice_actual_inputvalue) = 0) \/ exists ge_signed_half_choice_actual_inputvaluedecode. (((z) = 2 * ge_signed_half_choice_actual_inputvaluedecode + 1 /\ (ge_balance_positive_choice_actual_inputvalue) = 0) /\ (ge_balance_negative_choice_actual_inputvalue) = S ge_signed_half_choice_actual_inputvaluedecode))) /\ ((dst_positive_choice_actual_input) + ge_balance_negative_choice_actual_inputvalue = (dst_negative_choice_actual_input) + ge_balance_positive_choice_actual_inputvalue)))))))))
  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