DV0011

divisor_mask_entry_from_quotient

A real quotient and a positive divisor justify retaining its actual signed input entry.

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. ∀ q. ∀ z. ¬d = 0 → n = d · q → ArithAt(F,d,z) → DivisorMaskEntry(F,n,d,z)

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

Definition DAG

ArithAt(F,i,z) · 1DivisorMaskEntry(F,n,d,z) · 1

Actual proof prerequisites

none
Original expanded first-order statement 
forall F n d q z. ~(d=0) -> n=d*q -> (exists dst_positive_code_keep_input dst_positive_scale_keep_input dst_negative_code_keep_input dst_negative_scale_keep_input dst_positive_keep_input dst_negative_keep_input. (((F) = (((((dst_positive_code_keep_input) + (dst_positive_scale_keep_input)) * S ((dst_positive_code_keep_input) + (dst_positive_scale_keep_input)) + ((dst_positive_scale_keep_input) + (dst_positive_scale_keep_input))) + (((dst_negative_code_keep_input) + (dst_negative_scale_keep_input)) * S ((dst_negative_code_keep_input) + (dst_negative_scale_keep_input)) + ((dst_negative_scale_keep_input) + (dst_negative_scale_keep_input)))) * S ((((dst_positive_code_keep_input) + (dst_positive_scale_keep_input)) * S ((dst_positive_code_keep_input) + (dst_positive_scale_keep_input)) + ((dst_positive_scale_keep_input) + (dst_positive_scale_keep_input))) + (((dst_negative_code_keep_input) + (dst_negative_scale_keep_input)) * S ((dst_negative_code_keep_input) + (dst_negative_scale_keep_input)) + ((dst_negative_scale_keep_input) + (dst_negative_scale_keep_input)))) + ((((dst_negative_code_keep_input) + (dst_negative_scale_keep_input)) * S ((dst_negative_code_keep_input) + (dst_negative_scale_keep_input)) + ((dst_negative_scale_keep_input) + (dst_negative_scale_keep_input))) + (((dst_negative_code_keep_input) + (dst_negative_scale_keep_input)) * S ((dst_negative_code_keep_input) + (dst_negative_scale_keep_input)) + ((dst_negative_scale_keep_input) + (dst_negative_scale_keep_input)))))) /\ (((((exists ff_h_pvs_keep_inputpositive. ff_h_pvs_keep_inputpositive + S (dst_positive_keep_input) = S ((S (d)) * dst_positive_scale_keep_input)) /\ exists ff_q_pvs_keep_inputpositive. dst_positive_code_keep_input = ff_q_pvs_keep_inputpositive * S ((S (d)) * dst_positive_scale_keep_input) + (dst_positive_keep_input))) /\ (((((exists ff_h_pvs_keep_inputnegative. ff_h_pvs_keep_inputnegative + S (dst_negative_keep_input) = S ((S (d)) * dst_negative_scale_keep_input)) /\ exists ff_q_pvs_keep_inputnegative. dst_negative_code_keep_input = ff_q_pvs_keep_inputnegative * S ((S (d)) * dst_negative_scale_keep_input) + (dst_negative_keep_input))) /\ (exists ge_balance_positive_keep_inputvalue ge_balance_negative_keep_inputvalue. (((((z) = 2 * (ge_balance_positive_keep_inputvalue) /\ (ge_balance_negative_keep_inputvalue) = 0) \/ exists ge_signed_half_keep_inputvaluedecode. (((z) = 2 * ge_signed_half_keep_inputvaluedecode + 1 /\ (ge_balance_positive_keep_inputvalue) = 0) /\ (ge_balance_negative_keep_inputvalue) = S ge_signed_half_keep_inputvaluedecode))) /\ ((dst_positive_keep_input) + ge_balance_negative_keep_inputvalue = (dst_negative_keep_input) + ge_balance_positive_keep_inputvalue))))))))) -> ((((~((d)=0)) /\ (exists dm_quotient_keep_result. (((n)=(d)*dm_quotient_keep_result) /\ (exists dst_positive_code_keep_resultinput dst_positive_scale_keep_resultinput dst_negative_code_keep_resultinput dst_negative_scale_keep_resultinput dst_positive_keep_resultinput dst_negative_keep_resultinput. (((F) = (((((dst_positive_code_keep_resultinput) + (dst_positive_scale_keep_resultinput)) * S ((dst_positive_code_keep_resultinput) + (dst_positive_scale_keep_resultinput)) + ((dst_positive_scale_keep_resultinput) + (dst_positive_scale_keep_resultinput))) + (((dst_negative_code_keep_resultinput) + (dst_negative_scale_keep_resultinput)) * S ((dst_negative_code_keep_resultinput) + (dst_negative_scale_keep_resultinput)) + ((dst_negative_scale_keep_resultinput) + (dst_negative_scale_keep_resultinput)))) * S ((((dst_positive_code_keep_resultinput) + (dst_positive_scale_keep_resultinput)) * S ((dst_positive_code_keep_resultinput) + (dst_positive_scale_keep_resultinput)) + ((dst_positive_scale_keep_resultinput) + (dst_positive_scale_keep_resultinput))) + (((dst_negative_code_keep_resultinput) + (dst_negative_scale_keep_resultinput)) * S ((dst_negative_code_keep_resultinput) + (dst_negative_scale_keep_resultinput)) + ((dst_negative_scale_keep_resultinput) + (dst_negative_scale_keep_resultinput)))) + ((((dst_negative_code_keep_resultinput) + (dst_negative_scale_keep_resultinput)) * S ((dst_negative_code_keep_resultinput) + (dst_negative_scale_keep_resultinput)) + ((dst_negative_scale_keep_resultinput) + (dst_negative_scale_keep_resultinput))) + (((dst_negative_code_keep_resultinput) + (dst_negative_scale_keep_resultinput)) * S ((dst_negative_code_keep_resultinput) + (dst_negative_scale_keep_resultinput)) + ((dst_negative_scale_keep_resultinput) + (dst_negative_scale_keep_resultinput)))))) /\ (((((exists ff_h_pvs_keep_resultinputpositive. ff_h_pvs_keep_resultinputpositive + S (dst_positive_keep_resultinput) = S ((S (d)) * dst_positive_scale_keep_resultinput)) /\ exists ff_q_pvs_keep_resultinputpositive. dst_positive_code_keep_resultinput = ff_q_pvs_keep_resultinputpositive * S ((S (d)) * dst_positive_scale_keep_resultinput) + (dst_positive_keep_resultinput))) /\ (((((exists ff_h_pvs_keep_resultinputnegative. ff_h_pvs_keep_resultinputnegative + S (dst_negative_keep_resultinput) = S ((S (d)) * dst_negative_scale_keep_resultinput)) /\ exists ff_q_pvs_keep_resultinputnegative. dst_negative_code_keep_resultinput = ff_q_pvs_keep_resultinputnegative * S ((S (d)) * dst_negative_scale_keep_resultinput) + (dst_negative_keep_resultinput))) /\ (exists ge_balance_positive_keep_resultinputvalue ge_balance_negative_keep_resultinputvalue. (((((z) = 2 * (ge_balance_positive_keep_resultinputvalue) /\ (ge_balance_negative_keep_resultinputvalue) = 0) \/ exists ge_signed_half_keep_resultinputvaluedecode. (((z) = 2 * ge_signed_half_keep_resultinputvaluedecode + 1 /\ (ge_balance_positive_keep_resultinputvalue) = 0) /\ (ge_balance_negative_keep_resultinputvalue) = S ge_signed_half_keep_resultinputvaluedecode))) /\ ((dst_positive_keep_resultinput) + ge_balance_negative_keep_resultinputvalue = (dst_negative_keep_resultinput) + ge_balance_positive_keep_resultinputvalue))))))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_keep_resultnondivisor. (n) = (d) * pvs_factor_keep_resultnondivisor)) /\ ((z)=0))))

Complete tactic proof in conservative notation

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

15 script commands · 6 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–8

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 q
  5. L5
    intro z
  6. L6
    intro hd
  7. L7
    intro hq
  8. L8
    intro hz
02Separate the logical casesL9–10

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

  1. L9
    left
  2. L10
    split
03Use earlier factsL11–11

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

  1. L11
    exact hd
04Construct an explicit witnessL12–12

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

  1. L12
    exists q
05Separate the logical casesL13–13

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

  1. L13
    split
06Use earlier factsL14–15

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

  1. L14
    exact hq
  2. L15
    exact hz

Library-wide reading audit

Original defined command ledger · 15 lines
  1. 0001intro F
  2. 0002intro n
  3. 0003intro d
  4. 0004intro q
  5. 0005intro z
  6. 0006intro hd
  7. 0007intro hq
  8. 0008intro hz
  9. 0009left
  10. 0010split
  11. 0011exact hd
  12. 0012exists q
  13. 0013split
  14. 0014exact hq
  15. 0015exact hz