DV0014

divisor_mask_entry_functional

The kept and omitted alternatives are constructively exclusive, and actual signed input functionality makes the resulting code unique.

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. ∀ d. ∀ a. ∀ b. DivisorMaskEntry(F,n,d,a) → DivisorMaskEntry(F,n,d,b) → a = b

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

Definition DAG

DivisorMaskEntry(F,n,d,z) · 2

Actual proof prerequisites

divisor_signed_table_at_functional · checked external prerequisite
Original expanded first-order statement 
forall F n d a b. ((((~((d)=0)) /\ (exists dm_quotient_unique_first. (((n)=(d)*dm_quotient_unique_first) /\ (exists dst_positive_code_unique_firstinput dst_positive_scale_unique_firstinput dst_negative_code_unique_firstinput dst_negative_scale_unique_firstinput dst_positive_unique_firstinput dst_negative_unique_firstinput. (((F) = (((((dst_positive_code_unique_firstinput) + (dst_positive_scale_unique_firstinput)) * S ((dst_positive_code_unique_firstinput) + (dst_positive_scale_unique_firstinput)) + ((dst_positive_scale_unique_firstinput) + (dst_positive_scale_unique_firstinput))) + (((dst_negative_code_unique_firstinput) + (dst_negative_scale_unique_firstinput)) * S ((dst_negative_code_unique_firstinput) + (dst_negative_scale_unique_firstinput)) + ((dst_negative_scale_unique_firstinput) + (dst_negative_scale_unique_firstinput)))) * S ((((dst_positive_code_unique_firstinput) + (dst_positive_scale_unique_firstinput)) * S ((dst_positive_code_unique_firstinput) + (dst_positive_scale_unique_firstinput)) + ((dst_positive_scale_unique_firstinput) + (dst_positive_scale_unique_firstinput))) + (((dst_negative_code_unique_firstinput) + (dst_negative_scale_unique_firstinput)) * S ((dst_negative_code_unique_firstinput) + (dst_negative_scale_unique_firstinput)) + ((dst_negative_scale_unique_firstinput) + (dst_negative_scale_unique_firstinput)))) + ((((dst_negative_code_unique_firstinput) + (dst_negative_scale_unique_firstinput)) * S ((dst_negative_code_unique_firstinput) + (dst_negative_scale_unique_firstinput)) + ((dst_negative_scale_unique_firstinput) + (dst_negative_scale_unique_firstinput))) + (((dst_negative_code_unique_firstinput) + (dst_negative_scale_unique_firstinput)) * S ((dst_negative_code_unique_firstinput) + (dst_negative_scale_unique_firstinput)) + ((dst_negative_scale_unique_firstinput) + (dst_negative_scale_unique_firstinput)))))) /\ (((((exists ff_h_pvs_unique_firstinputpositive. ff_h_pvs_unique_firstinputpositive + S (dst_positive_unique_firstinput) = S ((S (d)) * dst_positive_scale_unique_firstinput)) /\ exists ff_q_pvs_unique_firstinputpositive. dst_positive_code_unique_firstinput = ff_q_pvs_unique_firstinputpositive * S ((S (d)) * dst_positive_scale_unique_firstinput) + (dst_positive_unique_firstinput))) /\ (((((exists ff_h_pvs_unique_firstinputnegative. ff_h_pvs_unique_firstinputnegative + S (dst_negative_unique_firstinput) = S ((S (d)) * dst_negative_scale_unique_firstinput)) /\ exists ff_q_pvs_unique_firstinputnegative. dst_negative_code_unique_firstinput = ff_q_pvs_unique_firstinputnegative * S ((S (d)) * dst_negative_scale_unique_firstinput) + (dst_negative_unique_firstinput))) /\ (exists ge_balance_positive_unique_firstinputvalue ge_balance_negative_unique_firstinputvalue. (((((a) = 2 * (ge_balance_positive_unique_firstinputvalue) /\ (ge_balance_negative_unique_firstinputvalue) = 0) \/ exists ge_signed_half_unique_firstinputvaluedecode. (((a) = 2 * ge_signed_half_unique_firstinputvaluedecode + 1 /\ (ge_balance_positive_unique_firstinputvalue) = 0) /\ (ge_balance_negative_unique_firstinputvalue) = S ge_signed_half_unique_firstinputvaluedecode))) /\ ((dst_positive_unique_firstinput) + ge_balance_negative_unique_firstinputvalue = (dst_negative_unique_firstinput) + ge_balance_positive_unique_firstinputvalue))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_unique_firstnondivisor. (n) = (d) * pvs_factor_unique_firstnondivisor)) /\ ((a)=0)))) -> ((((~((d)=0)) /\ (exists dm_quotient_unique_second. (((n)=(d)*dm_quotient_unique_second) /\ (exists dst_positive_code_unique_secondinput dst_positive_scale_unique_secondinput dst_negative_code_unique_secondinput dst_negative_scale_unique_secondinput dst_positive_unique_secondinput dst_negative_unique_secondinput. (((F) = (((((dst_positive_code_unique_secondinput) + (dst_positive_scale_unique_secondinput)) * S ((dst_positive_code_unique_secondinput) + (dst_positive_scale_unique_secondinput)) + ((dst_positive_scale_unique_secondinput) + (dst_positive_scale_unique_secondinput))) + (((dst_negative_code_unique_secondinput) + (dst_negative_scale_unique_secondinput)) * S ((dst_negative_code_unique_secondinput) + (dst_negative_scale_unique_secondinput)) + ((dst_negative_scale_unique_secondinput) + (dst_negative_scale_unique_secondinput)))) * S ((((dst_positive_code_unique_secondinput) + (dst_positive_scale_unique_secondinput)) * S ((dst_positive_code_unique_secondinput) + (dst_positive_scale_unique_secondinput)) + ((dst_positive_scale_unique_secondinput) + (dst_positive_scale_unique_secondinput))) + (((dst_negative_code_unique_secondinput) + (dst_negative_scale_unique_secondinput)) * S ((dst_negative_code_unique_secondinput) + (dst_negative_scale_unique_secondinput)) + ((dst_negative_scale_unique_secondinput) + (dst_negative_scale_unique_secondinput)))) + ((((dst_negative_code_unique_secondinput) + (dst_negative_scale_unique_secondinput)) * S ((dst_negative_code_unique_secondinput) + (dst_negative_scale_unique_secondinput)) + ((dst_negative_scale_unique_secondinput) + (dst_negative_scale_unique_secondinput))) + (((dst_negative_code_unique_secondinput) + (dst_negative_scale_unique_secondinput)) * S ((dst_negative_code_unique_secondinput) + (dst_negative_scale_unique_secondinput)) + ((dst_negative_scale_unique_secondinput) + (dst_negative_scale_unique_secondinput)))))) /\ (((((exists ff_h_pvs_unique_secondinputpositive. ff_h_pvs_unique_secondinputpositive + S (dst_positive_unique_secondinput) = S ((S (d)) * dst_positive_scale_unique_secondinput)) /\ exists ff_q_pvs_unique_secondinputpositive. dst_positive_code_unique_secondinput = ff_q_pvs_unique_secondinputpositive * S ((S (d)) * dst_positive_scale_unique_secondinput) + (dst_positive_unique_secondinput))) /\ (((((exists ff_h_pvs_unique_secondinputnegative. ff_h_pvs_unique_secondinputnegative + S (dst_negative_unique_secondinput) = S ((S (d)) * dst_negative_scale_unique_secondinput)) /\ exists ff_q_pvs_unique_secondinputnegative. dst_negative_code_unique_secondinput = ff_q_pvs_unique_secondinputnegative * S ((S (d)) * dst_negative_scale_unique_secondinput) + (dst_negative_unique_secondinput))) /\ (exists ge_balance_positive_unique_secondinputvalue ge_balance_negative_unique_secondinputvalue. (((((b) = 2 * (ge_balance_positive_unique_secondinputvalue) /\ (ge_balance_negative_unique_secondinputvalue) = 0) \/ exists ge_signed_half_unique_secondinputvaluedecode. (((b) = 2 * ge_signed_half_unique_secondinputvaluedecode + 1 /\ (ge_balance_positive_unique_secondinputvalue) = 0) /\ (ge_balance_negative_unique_secondinputvalue) = S ge_signed_half_unique_secondinputvaluedecode))) /\ ((dst_positive_unique_secondinput) + ge_balance_negative_unique_secondinputvalue = (dst_negative_unique_secondinput) + ge_balance_positive_unique_secondinputvalue))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_unique_secondnondivisor. (n) = (d) * pvs_factor_unique_secondnondivisor)) /\ ((b)=0)))) -> a=b

Complete tactic proof in conservative notation

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

47 script commands · 16 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–7

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

  1. L1
    intro F
  2. L2
    intro n
  3. L3
    intro d
  4. L4
    intro a
  5. L5
    intro b
  6. L6
    intro ha
  7. L7
    intro hb
02Separate the logical casesL8–15

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

  1. L8
    cases ha
  2. L9
    cases ha_left
  3. L10
    cases ha_left_right
  4. L11
    cases ha_left_right_witness
  5. L12
    cases hb
  6. L13
    cases hb_left
  7. L14
    cases hb_left_right
  8. L15
    cases hb_left_right_witness
03Use earlier factsL16–22

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

  1. L16
    specialize divisor_signed_table_at_functional (F)
  2. L17
    specialize divisor_signed_table_at_functional (d)
  3. L18
    specialize divisor_signed_table_at_functional (a)
  4. L19
    specialize divisor_signed_table_at_functional (b)
  5. L20
    apply divisor_signed_table_at_functional
  6. L21
    exact ha_left_right_witness_right
  7. L22
    exact hb_left_right_witness_right
04Separate the logical casesL23–25

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

  1. L23
    cases hb_right
  2. L24
    exfalso
  3. L25
    cases hb_right_left
05Use earlier factsL26–28

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

  1. L26
    apply ha_left_left
  2. L27
    exact hb_right_left_left
  3. L28
    apply hb_right_left_right
06Construct an explicit witnessL29–29

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

  1. L29
    exists x
07Use earlier factsL30–30

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

  1. L30
    exact ha_left_right_witness_left
08Separate the logical casesL31–37

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

  1. L31
    cases ha_right
  2. L32
    cases hb
  3. L33
    cases hb_left
  4. L34
    cases hb_left_right
  5. L35
    cases hb_left_right_witness
  6. L36
    exfalso
  7. L37
    cases ha_right_left
09Use earlier factsL38–40

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

  1. L38
    apply hb_left_left
  2. L39
    exact ha_right_left_left
  3. L40
    apply ha_right_left_right
10Construct an explicit witnessL41–41

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

  1. L41
    exists x
11Use earlier factsL42–42

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

  1. L42
    exact hb_left_right_witness_left
12Separate the logical casesL43–43

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

  1. L43
    cases hb_right
13Calculate and transport equalitiesL44–44

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

  1. L44
    trans 0
14Use earlier factsL45–45

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

  1. L45
    exact ha_right_right
15Calculate and transport equalitiesL46–46

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

  1. L46
    symm
16Use earlier factsL47–47

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

  1. L47
    exact hb_right_right

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro F
  2. 0002intro n
  3. 0003intro d
  4. 0004intro a
  5. 0005intro b
  6. 0006intro ha
  7. 0007intro hb
  8. 0008cases ha
  9. 0009cases ha_left
  10. 0010cases ha_left_right
  11. 0011cases ha_left_right_witness
  12. 0012cases hb
  13. 0013cases hb_left
  14. 0014cases hb_left_right
  15. 0015cases hb_left_right_witness
  16. 0016specialize divisor_signed_table_at_functional (F)
  17. 0017specialize divisor_signed_table_at_functional (d)
  18. 0018specialize divisor_signed_table_at_functional (a)
  19. 0019specialize divisor_signed_table_at_functional (b)
  20. 0020apply divisor_signed_table_at_functional
  21. 0021exact ha_left_right_witness_right
  22. 0022exact hb_left_right_witness_right
  23. 0023cases hb_right
  24. 0024exfalso
  25. 0025cases hb_right_left
  26. 0026apply ha_left_left
  27. 0027exact hb_right_left_left
  28. 0028apply hb_right_left_right
  29. 0029exists x
  30. 0030exact ha_left_right_witness_left
  31. 0031cases ha_right
  32. 0032cases hb
  33. 0033cases hb_left
  34. 0034cases hb_left_right
  35. 0035cases hb_left_right_witness
  36. 0036exfalso
  37. 0037cases ha_right_left
  38. 0038apply hb_left_left
  39. 0039exact ha_right_left_left
  40. 0040apply ha_right_left_right
  41. 0041exists x
  42. 0042exact hb_left_right_witness_left
  43. 0043cases hb_right
  44. 0044trans 0
  45. 0045exact ha_right_right
  46. 0046symm
  47. 0047exact hb_right_right