DI0007

divisor_complement_prefix_exists

Finite HA induction constructs a genuine beta prefix of quotient values, rather than assuming a finite-choice or coding oracle.

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. ∀ l. ¬n = 0 → ∃ x. ∃ y. DivisorComplementPrefix(n,x,y,l)

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

Definition DAG

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

Actual proof prerequisites

factor_permutation_below_zero_impossible · checked external prerequisitedivisor_complement_existsbeta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall n l. ~(n=0) -> exists b c. (forall dvi_index_prefix_exists. (exists pvs_gap_prefix_existsdomain. pvs_gap_prefix_existsdomain + S (dvi_index_prefix_exists) = (l)) -> exists dvi_value_prefix_exists. ((((exists ff_h_pvs_prefix_existsentry. ff_h_pvs_prefix_existsentry + S (dvi_value_prefix_exists) = S ((S (dvi_index_prefix_exists)) * c)) /\ exists ff_q_pvs_prefix_existsentry. b = ff_q_pvs_prefix_existsentry * S ((S (dvi_index_prefix_exists)) * c) + (dvi_value_prefix_exists))) /\ ((((~((dvi_index_prefix_exists)=0)) /\ ((n)=(dvi_index_prefix_exists)*(dvi_value_prefix_exists)))) \/ ((((dvi_index_prefix_exists)=0 \/ ~(exists pvs_factor_prefix_existsgraphnondivisor. (n) = (dvi_index_prefix_exists) * pvs_factor_prefix_existsgraphnondivisor)) /\ ((dvi_value_prefix_exists)=(dvi_index_prefix_exists)))))))

Complete tactic proof in conservative notation

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

68 script commands · 26 reading checkpoints · 5 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 exists
01Fix variables and assumptionsL1–2

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

  1. L1
    intro n
  2. L2
    intro l
02Induction on lL3–4

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction l
  2. L4
    intro hn
03Construct an explicit witnessL5–6

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

  1. L5
    exists 0
  2. L6
    exists 0
04Fix variables and assumptionsL7–8

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

  1. L7
    intro i
  2. L8
    intro hi
05Separate the logical casesL9–9

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

  1. L9
    exfalso
06Use earlier factsL10–12

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

  1. L10
    specialize factor_permutation_below_zero_impossible (i)
  2. L11
    apply factor_permutation_below_zero_impossible
  3. L12
    exact hi
07Fix variables and assumptionsL13–13

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

  1. L13
    intro hn
08Establish hprevL14–16

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

  1. L14
    have hprev : ∃ b. ∃ c. DivisorComplementPrefix(n,b,c,l)Definitions: DivisorComplementPrefix(n,b,c,l)Original native command in the exact edition
  2. L15
    apply IH
  3. L16
    exact hn
09Separate the logical casesL17–18

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

  1. L17
    cases hprev
  2. L18
    cases hprev_witness
10Establish hvL19–23

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

  1. L19
    have hv : ∃ v. DivisorComplement(n,l,v)Definitions: DivisorComplement(n,l,v)Original native command in the exact edition
  2. L20
    specialize divisor_complement_exists (n)
  3. L21
    specialize divisor_complement_exists (l)
  4. L22
    apply divisor_complement_exists
  5. L23
    exact hn
11Separate the logical casesL24–24

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

  1. L24
    cases hv
12Establish hextL25–30

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

  1. L25
    have hext : ∃ b. ∃ c. BetaAt(b,c,l,x2) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(b,c,y,z))Definitions: BetaAt(b,c,l,x2)Lt(y,l)BetaAt(x,x1,y,z)BetaAt(b,c,y,z)Original native command in the exact edition
  2. L26
    specialize beta_prefix_extend (l)
  3. L27
    specialize beta_prefix_extend (x)
  4. L28
    specialize beta_prefix_extend (x1)
  5. L29
    specialize beta_prefix_extend (x2)
  6. L30
    apply beta_prefix_extend
13Separate the logical casesL31–33

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

  1. L31
    cases hext
  2. L32
    cases hext_witness
  3. L33
    cases hext_witness_witness
14Construct an explicit witnessL34–35

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

  1. L34
    exists x3
  2. L35
    exists x4
15Fix variables and assumptionsL36–37

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

  1. L36
    intro i
  2. L37
    intro hi
16Establish hcL38–42

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

  1. L38
    have hc : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L39
    specialize finite_lt_succ_eq_or_lt (l)
  3. L40
    specialize finite_lt_succ_eq_or_lt (i)
  4. L41
    apply finite_lt_succ_eq_or_lt
  5. L42
    exact hi
17Separate the logical casesL43–43

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

  1. L43
    cases hc
18Calculate and transport equalitiesL44–50

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

  1. L44
    rewrite hc_left
  2. L45
    rewrite hc_left
  3. L46
    rewrite hc_left
  4. L47
    rewrite hc_left
  5. L48
    rewrite hc_left
  6. L49
    rewrite hc_left
  7. L50
    rewrite hc_left
19Construct an explicit witnessL51–51

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

  1. L51
    exists x2
20Separate the logical casesL52–52

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

  1. L52
    split
21Use earlier factsL53–54

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

  1. L53
    exact hext_witness_witness_left
  2. L54
    exact hv_witness
22Establish holdL55–58

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

  1. L55
    have hold : ∃ v. BetaAt(x,x1,i,v) ∧ DivisorComplement(n,i,v)Definitions: BetaAt(x,x1,i,v)DivisorComplement(n,i,v)Original native command in the exact edition
  2. L56
    specialize hprev_witness_witness (i)
  3. L57
    apply hprev_witness_witness
  4. L58
    exact hc_right
23Separate the logical casesL59–60

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

  1. L59
    cases hold
  2. L60
    cases hold_witness
24Construct an explicit witnessL61–61

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

  1. L61
    exists x5
25Separate the logical casesL62–62

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

  1. L62
    split
26Use earlier factsL63–68

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

  1. L63
    specialize hext_witness_witness_right (i)
  2. L64
    specialize hext_witness_witness_right (x5)
  3. L65
    apply hext_witness_witness_right
  4. L66
    exact hc_right
  5. L67
    exact hold_witness_left
  6. L68
    exact hold_witness_right

Library-wide reading audit

Original defined command ledger · 68 lines
  1. 0001intro n
  2. 0002intro l
  3. 0003induction l
  4. 0004intro hn
  5. 0005exists 0
  6. 0006exists 0
  7. 0007intro i
  8. 0008intro hi
  9. 0009exfalso
  10. 0010specialize factor_permutation_below_zero_impossible (i)
  11. 0011apply factor_permutation_below_zero_impossible
  12. 0012exact hi
  13. 0013intro hn
  14. 0014have hprev : ∃ b. ∃ c. DivisorComplementPrefix(n,b,c,l)
  15. 0015apply IH
  16. 0016exact hn
  17. 0017cases hprev
  18. 0018cases hprev_witness
  19. 0019have hv : ∃ v. DivisorComplement(n,l,v)
  20. 0020specialize divisor_complement_exists (n)
  21. 0021specialize divisor_complement_exists (l)
  22. 0022apply divisor_complement_exists
  23. 0023exact hn
  24. 0024cases hv
  25. 0025have hext : ∃ b. ∃ c. BetaAt(b,c,l,x2) ∧ (∀ y. ∀ z. Lt(y,l) → BetaAt(x,x1,y,z) → BetaAt(b,c,y,z))
  26. 0026specialize beta_prefix_extend (l)
  27. 0027specialize beta_prefix_extend (x)
  28. 0028specialize beta_prefix_extend (x1)
  29. 0029specialize beta_prefix_extend (x2)
  30. 0030apply beta_prefix_extend
  31. 0031cases hext
  32. 0032cases hext_witness
  33. 0033cases hext_witness_witness
  34. 0034exists x3
  35. 0035exists x4
  36. 0036intro i
  37. 0037intro hi
  38. 0038have hc : i = l ∨ Lt(i,l)
  39. 0039specialize finite_lt_succ_eq_or_lt (l)
  40. 0040specialize finite_lt_succ_eq_or_lt (i)
  41. 0041apply finite_lt_succ_eq_or_lt
  42. 0042exact hi
  43. 0043cases hc
  44. 0044rewrite hc_left
  45. 0045rewrite hc_left
  46. 0046rewrite hc_left
  47. 0047rewrite hc_left
  48. 0048rewrite hc_left
  49. 0049rewrite hc_left
  50. 0050rewrite hc_left
  51. 0051exists x2
  52. 0052split
  53. 0053exact hext_witness_witness_left
  54. 0054exact hv_witness
  55. 0055have hold : ∃ v. BetaAt(x,x1,i,v) ∧ DivisorComplement(n,i,v)
  56. 0056specialize hprev_witness_witness (i)
  57. 0057apply hprev_witness_witness
  58. 0058exact hc_right
  59. 0059cases hold
  60. 0060cases hold_witness
  61. 0061exists x5
  62. 0062split
  63. 0063specialize hext_witness_witness_right (i)
  64. 0064specialize hext_witness_witness_right (x5)
  65. 0065apply hext_witness_witness_right
  66. 0066exact hc_right
  67. 0067exact hold_witness_left
  68. 0068exact hold_witness_right