DI000C

divisor_complement_prefix_positive_quotient

The actual beta code at a positive divisor is precisely its witnessed quotient, not merely an unspecified bounded permutation image.

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.

The complementary quotient is witnessed by n=d*q at positive divisors. The actual permutation covers indices zero through n, fixing zero and nondivisors. This is the involution foundation for the separate cancellation and full G007 inversion proofs, not an assumed divisor bijection.

Exact theorem in conservative defined notation

∀ n. ∀ b. ∀ c. ∀ d. ∀ q. ¬n = 0 → DivisorComplementPrefix(n,b,c,S n) → ¬d = 0 → n = d · q → BetaAt(b,c,d,q)

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

Definition DAG

DivisorComplement(n,d,q) · 1DivisorComplementPrefix(n,b,c,l) · 1Lt(a,b) · 1BetaAt(b,c,i,x) · 2

Actual proof prerequisites

succ_le_succ · checked external prerequisitedivisor_le_nonzero · checked external prerequisitedivisor_complement_functional
Original expanded first-order statement 
forall n b c d q. ~(n=0) -> (forall dvi_index_decoded_quotient_prefix. (exists pvs_gap_decoded_quotient_prefixdomain. pvs_gap_decoded_quotient_prefixdomain + S (dvi_index_decoded_quotient_prefix) = (S n)) -> exists dvi_value_decoded_quotient_prefix. ((((exists ff_h_pvs_decoded_quotient_prefixentry. ff_h_pvs_decoded_quotient_prefixentry + S (dvi_value_decoded_quotient_prefix) = S ((S (dvi_index_decoded_quotient_prefix)) * c)) /\ exists ff_q_pvs_decoded_quotient_prefixentry. b = ff_q_pvs_decoded_quotient_prefixentry * S ((S (dvi_index_decoded_quotient_prefix)) * c) + (dvi_value_decoded_quotient_prefix))) /\ ((((~((dvi_index_decoded_quotient_prefix)=0)) /\ ((n)=(dvi_index_decoded_quotient_prefix)*(dvi_value_decoded_quotient_prefix)))) \/ ((((dvi_index_decoded_quotient_prefix)=0 \/ ~(exists pvs_factor_decoded_quotient_prefixgraphnondivisor. (n) = (dvi_index_decoded_quotient_prefix) * pvs_factor_decoded_quotient_prefixgraphnondivisor)) /\ ((dvi_value_decoded_quotient_prefix)=(dvi_index_decoded_quotient_prefix))))))) -> ~(d=0) -> n=d*q -> (((exists ff_h_pvs_decoded_quotient_result. ff_h_pvs_decoded_quotient_result + S (q) = S ((S (d)) * c)) /\ exists ff_q_pvs_decoded_quotient_result. b = ff_q_pvs_decoded_quotient_result * S ((S (d)) * c) + (q)))

Complete tactic proof in conservative notation

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

39 script commands · 11 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 (1)
divisor complement functional
01Fix variables and assumptionsL1–9

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

  1. L1
    intro n
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro q
  6. L6
    intro hn
  7. L7
    intro hp
  8. L8
    intro hd
  9. L9
    intro heq
02Establish hboundL10–17

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

  1. L10
    have hbound : Lt(d,S n)Definitions: Lt(d,S n)Original native command in the exact edition
  2. L11
    specialize succ_le_succ (d)
  3. L12
    specialize succ_le_succ (n)
  4. L13
    apply succ_le_succ
  5. L14
    specialize divisor_le_nonzero (d)
  6. L15
    specialize divisor_le_nonzero (n)
  7. L16
    apply divisor_le_nonzero
  8. L17
    exact hn
03Construct an explicit witnessL18–18

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

  1. L18
    exists q
04Use earlier factsL19–19

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

  1. L19
    exact heq
05Establish hvL20–23

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

  1. L20
    have hv : ∃ r. BetaAt(b,c,d,r) ∧ DivisorComplement(n,d,r)Definitions: BetaAt(b,c,d,r)DivisorComplement(n,d,r)Original native command in the exact edition
  2. L21
    specialize hp (d)
  3. L22
    apply hp
  4. L23
    exact hbound
06Separate the logical casesL24–25

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

  1. L24
    cases hv
  2. L25
    cases hv_witness
07Establish hvalueL26–32

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

  1. L26
    have hvalue : x=q
  2. L27
    specialize divisor_complement_functional (n)
  3. L28
    specialize divisor_complement_functional (d)
  4. L29
    specialize divisor_complement_functional (x)
  5. L30
    specialize divisor_complement_functional (q)
  6. L31
    apply divisor_complement_functional
  7. L32
    exact hv_witness_right
08Separate the logical casesL33–34

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

  1. L33
    left
  2. L34
    split
09Use earlier factsL35–36

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

  1. L35
    exact hd
  2. L36
    exact heq
10Calculate and transport equalitiesL37–38

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

  1. L37
    rewrite hvalue at hv_witness_left
  2. L38
    rewrite hvalue at hv_witness_left
11Use earlier factsL39–39

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

  1. L39
    exact hv_witness_left

Library-wide reading audit

Original defined command ledger · 39 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro q
  6. 0006intro hn
  7. 0007intro hp
  8. 0008intro hd
  9. 0009intro heq
  10. 0010have hbound : Lt(d,S n)
  11. 0011specialize succ_le_succ (d)
  12. 0012specialize succ_le_succ (n)
  13. 0013apply succ_le_succ
  14. 0014specialize divisor_le_nonzero (d)
  15. 0015specialize divisor_le_nonzero (n)
  16. 0016apply divisor_le_nonzero
  17. 0017exact hn
  18. 0018exists q
  19. 0019exact heq
  20. 0020have hv : ∃ r. BetaAt(b,c,d,r) ∧ DivisorComplement(n,d,r)
  21. 0021specialize hp (d)
  22. 0022apply hp
  23. 0023exact hbound
  24. 0024cases hv
  25. 0025cases hv_witness
  26. 0026have hvalue : x=q
  27. 0027specialize divisor_complement_functional (n)
  28. 0028specialize divisor_complement_functional (d)
  29. 0029specialize divisor_complement_functional (x)
  30. 0030specialize divisor_complement_functional (q)
  31. 0031apply divisor_complement_functional
  32. 0032exact hv_witness_right
  33. 0033left
  34. 0034split
  35. 0035exact hd
  36. 0036exact heq
  37. 0037rewrite hvalue at hv_witness_left
  38. 0038rewrite hvalue at hv_witness_left
  39. 0039exact hv_witness_left