DV001E

divisor_mask_entry_positive_source_extensional

Mask values depend only on positive input values: zero branches ignore F(0), while kept branches supply the positivity and quotient data needed for actual source equality.

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

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

Definition DAG

DivisorMaskEntry(F,n,d,z) · 2ArithPositiveEqual(F,G,N) · 1Le(a,b) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall F G n d a b. (forall dm_index_source_equal dm_first_value_source_equal dm_second_value_source_equal. ~(dm_index_source_equal=0) -> (exists pvs_le_gap_source_equaldomain. pvs_le_gap_source_equaldomain + (dm_index_source_equal) = (n)) -> (exists dst_positive_code_source_equalfirst dst_positive_scale_source_equalfirst dst_negative_code_source_equalfirst dst_negative_scale_source_equalfirst dst_positive_source_equalfirst dst_negative_source_equalfirst. (((F) = (((((dst_positive_code_source_equalfirst) + (dst_positive_scale_source_equalfirst)) * S ((dst_positive_code_source_equalfirst) + (dst_positive_scale_source_equalfirst)) + ((dst_positive_scale_source_equalfirst) + (dst_positive_scale_source_equalfirst))) + (((dst_negative_code_source_equalfirst) + (dst_negative_scale_source_equalfirst)) * S ((dst_negative_code_source_equalfirst) + (dst_negative_scale_source_equalfirst)) + ((dst_negative_scale_source_equalfirst) + (dst_negative_scale_source_equalfirst)))) * S ((((dst_positive_code_source_equalfirst) + (dst_positive_scale_source_equalfirst)) * S ((dst_positive_code_source_equalfirst) + (dst_positive_scale_source_equalfirst)) + ((dst_positive_scale_source_equalfirst) + (dst_positive_scale_source_equalfirst))) + (((dst_negative_code_source_equalfirst) + (dst_negative_scale_source_equalfirst)) * S ((dst_negative_code_source_equalfirst) + (dst_negative_scale_source_equalfirst)) + ((dst_negative_scale_source_equalfirst) + (dst_negative_scale_source_equalfirst)))) + ((((dst_negative_code_source_equalfirst) + (dst_negative_scale_source_equalfirst)) * S ((dst_negative_code_source_equalfirst) + (dst_negative_scale_source_equalfirst)) + ((dst_negative_scale_source_equalfirst) + (dst_negative_scale_source_equalfirst))) + (((dst_negative_code_source_equalfirst) + (dst_negative_scale_source_equalfirst)) * S ((dst_negative_code_source_equalfirst) + (dst_negative_scale_source_equalfirst)) + ((dst_negative_scale_source_equalfirst) + (dst_negative_scale_source_equalfirst)))))) /\ (((((exists ff_h_pvs_source_equalfirstpositive. ff_h_pvs_source_equalfirstpositive + S (dst_positive_source_equalfirst) = S ((S (dm_index_source_equal)) * dst_positive_scale_source_equalfirst)) /\ exists ff_q_pvs_source_equalfirstpositive. dst_positive_code_source_equalfirst = ff_q_pvs_source_equalfirstpositive * S ((S (dm_index_source_equal)) * dst_positive_scale_source_equalfirst) + (dst_positive_source_equalfirst))) /\ (((((exists ff_h_pvs_source_equalfirstnegative. ff_h_pvs_source_equalfirstnegative + S (dst_negative_source_equalfirst) = S ((S (dm_index_source_equal)) * dst_negative_scale_source_equalfirst)) /\ exists ff_q_pvs_source_equalfirstnegative. dst_negative_code_source_equalfirst = ff_q_pvs_source_equalfirstnegative * S ((S (dm_index_source_equal)) * dst_negative_scale_source_equalfirst) + (dst_negative_source_equalfirst))) /\ (exists ge_balance_positive_source_equalfirstvalue ge_balance_negative_source_equalfirstvalue. (((((dm_first_value_source_equal) = 2 * (ge_balance_positive_source_equalfirstvalue) /\ (ge_balance_negative_source_equalfirstvalue) = 0) \/ exists ge_signed_half_source_equalfirstvaluedecode. (((dm_first_value_source_equal) = 2 * ge_signed_half_source_equalfirstvaluedecode + 1 /\ (ge_balance_positive_source_equalfirstvalue) = 0) /\ (ge_balance_negative_source_equalfirstvalue) = S ge_signed_half_source_equalfirstvaluedecode))) /\ ((dst_positive_source_equalfirst) + ge_balance_negative_source_equalfirstvalue = (dst_negative_source_equalfirst) + ge_balance_positive_source_equalfirstvalue))))))))) -> (exists dst_positive_code_source_equalsecond dst_positive_scale_source_equalsecond dst_negative_code_source_equalsecond dst_negative_scale_source_equalsecond dst_positive_source_equalsecond dst_negative_source_equalsecond. (((G) = (((((dst_positive_code_source_equalsecond) + (dst_positive_scale_source_equalsecond)) * S ((dst_positive_code_source_equalsecond) + (dst_positive_scale_source_equalsecond)) + ((dst_positive_scale_source_equalsecond) + (dst_positive_scale_source_equalsecond))) + (((dst_negative_code_source_equalsecond) + (dst_negative_scale_source_equalsecond)) * S ((dst_negative_code_source_equalsecond) + (dst_negative_scale_source_equalsecond)) + ((dst_negative_scale_source_equalsecond) + (dst_negative_scale_source_equalsecond)))) * S ((((dst_positive_code_source_equalsecond) + (dst_positive_scale_source_equalsecond)) * S ((dst_positive_code_source_equalsecond) + (dst_positive_scale_source_equalsecond)) + ((dst_positive_scale_source_equalsecond) + (dst_positive_scale_source_equalsecond))) + (((dst_negative_code_source_equalsecond) + (dst_negative_scale_source_equalsecond)) * S ((dst_negative_code_source_equalsecond) + (dst_negative_scale_source_equalsecond)) + ((dst_negative_scale_source_equalsecond) + (dst_negative_scale_source_equalsecond)))) + ((((dst_negative_code_source_equalsecond) + (dst_negative_scale_source_equalsecond)) * S ((dst_negative_code_source_equalsecond) + (dst_negative_scale_source_equalsecond)) + ((dst_negative_scale_source_equalsecond) + (dst_negative_scale_source_equalsecond))) + (((dst_negative_code_source_equalsecond) + (dst_negative_scale_source_equalsecond)) * S ((dst_negative_code_source_equalsecond) + (dst_negative_scale_source_equalsecond)) + ((dst_negative_scale_source_equalsecond) + (dst_negative_scale_source_equalsecond)))))) /\ (((((exists ff_h_pvs_source_equalsecondpositive. ff_h_pvs_source_equalsecondpositive + S (dst_positive_source_equalsecond) = S ((S (dm_index_source_equal)) * dst_positive_scale_source_equalsecond)) /\ exists ff_q_pvs_source_equalsecondpositive. dst_positive_code_source_equalsecond = ff_q_pvs_source_equalsecondpositive * S ((S (dm_index_source_equal)) * dst_positive_scale_source_equalsecond) + (dst_positive_source_equalsecond))) /\ (((((exists ff_h_pvs_source_equalsecondnegative. ff_h_pvs_source_equalsecondnegative + S (dst_negative_source_equalsecond) = S ((S (dm_index_source_equal)) * dst_negative_scale_source_equalsecond)) /\ exists ff_q_pvs_source_equalsecondnegative. dst_negative_code_source_equalsecond = ff_q_pvs_source_equalsecondnegative * S ((S (dm_index_source_equal)) * dst_negative_scale_source_equalsecond) + (dst_negative_source_equalsecond))) /\ (exists ge_balance_positive_source_equalsecondvalue ge_balance_negative_source_equalsecondvalue. (((((dm_second_value_source_equal) = 2 * (ge_balance_positive_source_equalsecondvalue) /\ (ge_balance_negative_source_equalsecondvalue) = 0) \/ exists ge_signed_half_source_equalsecondvaluedecode. (((dm_second_value_source_equal) = 2 * ge_signed_half_source_equalsecondvaluedecode + 1 /\ (ge_balance_positive_source_equalsecondvalue) = 0) /\ (ge_balance_negative_source_equalsecondvalue) = S ge_signed_half_source_equalsecondvaluedecode))) /\ ((dst_positive_source_equalsecond) + ge_balance_negative_source_equalsecondvalue = (dst_negative_source_equalsecond) + ge_balance_positive_source_equalsecondvalue))))))))) -> dm_first_value_source_equal=dm_second_value_source_equal) -> (exists pvs_le_gap_source_bound. pvs_le_gap_source_bound + (d) = (n)) -> ((((~((d)=0)) /\ (exists dm_quotient_source_first. (((n)=(d)*dm_quotient_source_first) /\ (exists dst_positive_code_source_firstinput dst_positive_scale_source_firstinput dst_negative_code_source_firstinput dst_negative_scale_source_firstinput dst_positive_source_firstinput dst_negative_source_firstinput. (((F) = (((((dst_positive_code_source_firstinput) + (dst_positive_scale_source_firstinput)) * S ((dst_positive_code_source_firstinput) + (dst_positive_scale_source_firstinput)) + ((dst_positive_scale_source_firstinput) + (dst_positive_scale_source_firstinput))) + (((dst_negative_code_source_firstinput) + (dst_negative_scale_source_firstinput)) * S ((dst_negative_code_source_firstinput) + (dst_negative_scale_source_firstinput)) + ((dst_negative_scale_source_firstinput) + (dst_negative_scale_source_firstinput)))) * S ((((dst_positive_code_source_firstinput) + (dst_positive_scale_source_firstinput)) * S ((dst_positive_code_source_firstinput) + (dst_positive_scale_source_firstinput)) + ((dst_positive_scale_source_firstinput) + (dst_positive_scale_source_firstinput))) + (((dst_negative_code_source_firstinput) + (dst_negative_scale_source_firstinput)) * S ((dst_negative_code_source_firstinput) + (dst_negative_scale_source_firstinput)) + ((dst_negative_scale_source_firstinput) + (dst_negative_scale_source_firstinput)))) + ((((dst_negative_code_source_firstinput) + (dst_negative_scale_source_firstinput)) * S ((dst_negative_code_source_firstinput) + (dst_negative_scale_source_firstinput)) + ((dst_negative_scale_source_firstinput) + (dst_negative_scale_source_firstinput))) + (((dst_negative_code_source_firstinput) + (dst_negative_scale_source_firstinput)) * S ((dst_negative_code_source_firstinput) + (dst_negative_scale_source_firstinput)) + ((dst_negative_scale_source_firstinput) + (dst_negative_scale_source_firstinput)))))) /\ (((((exists ff_h_pvs_source_firstinputpositive. ff_h_pvs_source_firstinputpositive + S (dst_positive_source_firstinput) = S ((S (d)) * dst_positive_scale_source_firstinput)) /\ exists ff_q_pvs_source_firstinputpositive. dst_positive_code_source_firstinput = ff_q_pvs_source_firstinputpositive * S ((S (d)) * dst_positive_scale_source_firstinput) + (dst_positive_source_firstinput))) /\ (((((exists ff_h_pvs_source_firstinputnegative. ff_h_pvs_source_firstinputnegative + S (dst_negative_source_firstinput) = S ((S (d)) * dst_negative_scale_source_firstinput)) /\ exists ff_q_pvs_source_firstinputnegative. dst_negative_code_source_firstinput = ff_q_pvs_source_firstinputnegative * S ((S (d)) * dst_negative_scale_source_firstinput) + (dst_negative_source_firstinput))) /\ (exists ge_balance_positive_source_firstinputvalue ge_balance_negative_source_firstinputvalue. (((((a) = 2 * (ge_balance_positive_source_firstinputvalue) /\ (ge_balance_negative_source_firstinputvalue) = 0) \/ exists ge_signed_half_source_firstinputvaluedecode. (((a) = 2 * ge_signed_half_source_firstinputvaluedecode + 1 /\ (ge_balance_positive_source_firstinputvalue) = 0) /\ (ge_balance_negative_source_firstinputvalue) = S ge_signed_half_source_firstinputvaluedecode))) /\ ((dst_positive_source_firstinput) + ge_balance_negative_source_firstinputvalue = (dst_negative_source_firstinput) + ge_balance_positive_source_firstinputvalue))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_source_firstnondivisor. (n) = (d) * pvs_factor_source_firstnondivisor)) /\ ((a)=0)))) -> ((((~((d)=0)) /\ (exists dm_quotient_source_second. (((n)=(d)*dm_quotient_source_second) /\ (exists dst_positive_code_source_secondinput dst_positive_scale_source_secondinput dst_negative_code_source_secondinput dst_negative_scale_source_secondinput dst_positive_source_secondinput dst_negative_source_secondinput. (((G) = (((((dst_positive_code_source_secondinput) + (dst_positive_scale_source_secondinput)) * S ((dst_positive_code_source_secondinput) + (dst_positive_scale_source_secondinput)) + ((dst_positive_scale_source_secondinput) + (dst_positive_scale_source_secondinput))) + (((dst_negative_code_source_secondinput) + (dst_negative_scale_source_secondinput)) * S ((dst_negative_code_source_secondinput) + (dst_negative_scale_source_secondinput)) + ((dst_negative_scale_source_secondinput) + (dst_negative_scale_source_secondinput)))) * S ((((dst_positive_code_source_secondinput) + (dst_positive_scale_source_secondinput)) * S ((dst_positive_code_source_secondinput) + (dst_positive_scale_source_secondinput)) + ((dst_positive_scale_source_secondinput) + (dst_positive_scale_source_secondinput))) + (((dst_negative_code_source_secondinput) + (dst_negative_scale_source_secondinput)) * S ((dst_negative_code_source_secondinput) + (dst_negative_scale_source_secondinput)) + ((dst_negative_scale_source_secondinput) + (dst_negative_scale_source_secondinput)))) + ((((dst_negative_code_source_secondinput) + (dst_negative_scale_source_secondinput)) * S ((dst_negative_code_source_secondinput) + (dst_negative_scale_source_secondinput)) + ((dst_negative_scale_source_secondinput) + (dst_negative_scale_source_secondinput))) + (((dst_negative_code_source_secondinput) + (dst_negative_scale_source_secondinput)) * S ((dst_negative_code_source_secondinput) + (dst_negative_scale_source_secondinput)) + ((dst_negative_scale_source_secondinput) + (dst_negative_scale_source_secondinput)))))) /\ (((((exists ff_h_pvs_source_secondinputpositive. ff_h_pvs_source_secondinputpositive + S (dst_positive_source_secondinput) = S ((S (d)) * dst_positive_scale_source_secondinput)) /\ exists ff_q_pvs_source_secondinputpositive. dst_positive_code_source_secondinput = ff_q_pvs_source_secondinputpositive * S ((S (d)) * dst_positive_scale_source_secondinput) + (dst_positive_source_secondinput))) /\ (((((exists ff_h_pvs_source_secondinputnegative. ff_h_pvs_source_secondinputnegative + S (dst_negative_source_secondinput) = S ((S (d)) * dst_negative_scale_source_secondinput)) /\ exists ff_q_pvs_source_secondinputnegative. dst_negative_code_source_secondinput = ff_q_pvs_source_secondinputnegative * S ((S (d)) * dst_negative_scale_source_secondinput) + (dst_negative_source_secondinput))) /\ (exists ge_balance_positive_source_secondinputvalue ge_balance_negative_source_secondinputvalue. (((((b) = 2 * (ge_balance_positive_source_secondinputvalue) /\ (ge_balance_negative_source_secondinputvalue) = 0) \/ exists ge_signed_half_source_secondinputvaluedecode. (((b) = 2 * ge_signed_half_source_secondinputvaluedecode + 1 /\ (ge_balance_positive_source_secondinputvalue) = 0) /\ (ge_balance_negative_source_secondinputvalue) = S ge_signed_half_source_secondinputvaluedecode))) /\ ((dst_positive_source_secondinput) + ge_balance_negative_source_secondinputvalue = (dst_negative_source_secondinput) + ge_balance_positive_source_secondinputvalue))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_source_secondnondivisor. (n) = (d) * pvs_factor_source_secondnondivisor)) /\ ((b)=0)))) -> a=b

Complete tactic proof in conservative notation

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

51 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–10

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

  1. L1
    intro F
  2. L2
    intro G
  3. L3
    intro n
  4. L4
    intro d
  5. L5
    intro a
  6. L6
    intro b
  7. L7
    intro he
  8. L8
    intro hdn
  9. L9
    intro ha
  10. L10
    intro hb
02Separate the logical casesL11–18

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

  1. L11
    cases ha
  2. L12
    cases ha_left
  3. L13
    cases ha_left_right
  4. L14
    cases ha_left_right_witness
  5. L15
    cases hb
  6. L16
    cases hb_left
  7. L17
    cases hb_left_right
  8. L18
    cases hb_left_right_witness
03Use earlier factsL19–26

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

  1. L19
    specialize he (d)
  2. L20
    specialize he (a)
  3. L21
    specialize he (b)
  4. L22
    apply he
  5. L23
    exact ha_left_left
  6. L24
    exact hdn
  7. L25
    exact ha_left_right_witness_right
  8. L26
    exact hb_left_right_witness_right
04Separate the logical casesL27–29

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

  1. L27
    cases hb_right
  2. L28
    exfalso
  3. L29
    cases hb_right_left
05Use earlier factsL30–32

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

  1. L30
    apply ha_left_left
  2. L31
    exact hb_right_left_left
  3. L32
    apply hb_right_left_right
06Construct an explicit witnessL33–33

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

  1. L33
    exists x
07Use earlier factsL34–34

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

  1. L34
    exact ha_left_right_witness_left
08Separate the logical casesL35–41

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

  1. L35
    cases ha_right
  2. L36
    cases hb
  3. L37
    cases hb_left
  4. L38
    cases hb_left_right
  5. L39
    cases hb_left_right_witness
  6. L40
    exfalso
  7. L41
    cases ha_right_left
09Use earlier factsL42–44

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

  1. L42
    apply hb_left_left
  2. L43
    exact ha_right_left_left
  3. L44
    apply ha_right_left_right
10Construct an explicit witnessL45–45

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

  1. L45
    exists x
11Use earlier factsL46–46

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

  1. L46
    exact hb_left_right_witness_left
12Separate the logical casesL47–47

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

  1. L47
    cases hb_right
13Calculate and transport equalitiesL48–48

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

  1. L48
    trans 0
14Use earlier factsL49–49

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

  1. L49
    exact ha_right_right
15Calculate and transport equalitiesL50–50

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

  1. L50
    symm
16Use earlier factsL51–51

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

  1. L51
    exact hb_right_right

Library-wide reading audit

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