DI0007

divisor_complement_prefix_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic 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)))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 68 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

factor_permutation_below_zero_impossible Alpha theorem; checked-use authorized DI0002 divisor_complement_exists beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

Direct dependents

DI000A positive_divisor_involution_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

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.

Named ingredients (1)
divisor complement exists

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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
  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 : exists v. ((((~((l)=0)) /\ ((n)=(l)*(v)))) \/ ((((l)=0 \/ ~(exists pvs_factor_choice_valuenondivisor. (n) = (l) * pvs_factor_choice_valuenondivisor)) /\ ((v)=(l)))))
  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: LtBetaAt
  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 \/ (exists pvs_gap_choice_cases. pvs_gap_choice_cases + S (i) = (l))
  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 : exists v. (((((exists ff_h_pvs_choice_old_entry. ff_h_pvs_choice_old_entry + S (v) = S ((S (i)) * x1)) /\ exists ff_q_pvs_choice_old_entry. x = ff_q_pvs_choice_old_entry * S ((S (i)) * x1) + (v))) /\ ((((~((i)=0)) /\ ((n)=(i)*(v)))) \/ ((((i)=0 \/ ~(exists pvs_factor_choice_old_graphnondivisor. (n) = (i) * pvs_factor_choice_old_graphnondivisor)) /\ ((v)=(i)))))))
  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 exact 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 : exists b c. (forall dvi_index_choice_previous. (exists pvs_gap_choice_previousdomain. pvs_gap_choice_previousdomain + S (dvi_index_choice_previous) = (l)) -> exists dvi_value_choice_previous. ((((exists ff_h_pvs_choice_previousentry. ff_h_pvs_choice_previousentry + S (dvi_value_choice_previous) = S ((S (dvi_index_choice_previous)) * c)) /\ exists ff_q_pvs_choice_previousentry. b = ff_q_pvs_choice_previousentry * S ((S (dvi_index_choice_previous)) * c) + (dvi_value_choice_previous))) /\ ((((~((dvi_index_choice_previous)=0)) /\ ((n)=(dvi_index_choice_previous)*(dvi_value_choice_previous)))) \/ ((((dvi_index_choice_previous)=0 \/ ~(exists pvs_factor_choice_previousgraphnondivisor. (n) = (dvi_index_choice_previous) * pvs_factor_choice_previousgraphnondivisor)) /\ ((dvi_value_choice_previous)=(dvi_index_choice_previous)))))))
  15. 0015apply IH
  16. 0016exact hn
  17. 0017cases hprev
  18. 0018cases hprev_witness
  19. 0019have hv : exists v. ((((~((l)=0)) /\ ((n)=(l)*(v)))) \/ ((((l)=0 \/ ~(exists pvs_factor_choice_valuenondivisor. (n) = (l) * pvs_factor_choice_valuenondivisor)) /\ ((v)=(l)))))
  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 : exists b c. (((((exists ff_h_pvs_choice_last. ff_h_pvs_choice_last + S (x2) = S ((S (l)) * c)) /\ exists ff_q_pvs_choice_last. b = ff_q_pvs_choice_last * S ((S (l)) * c) + (x2))) /\ (forall pfp_i_choice_preserve pfp_a_choice_preserve. (exists pfp_gap_choice_preservebound. pfp_gap_choice_preservebound + S (pfp_i_choice_preserve) = (l)) -> (((exists ff_h_pfp_choice_preserveold. ff_h_pfp_choice_preserveold + S (pfp_a_choice_preserve) = S ((S (pfp_i_choice_preserve)) * x1)) /\ exists ff_q_pfp_choice_preserveold. x = ff_q_pfp_choice_preserveold * S ((S (pfp_i_choice_preserve)) * x1) + (pfp_a_choice_preserve))) -> (((exists ff_h_pfp_choice_preservenew. ff_h_pfp_choice_preservenew + S (pfp_a_choice_preserve) = S ((S (pfp_i_choice_preserve)) * c)) /\ exists ff_q_pfp_choice_preservenew. b = ff_q_pfp_choice_preservenew * S ((S (pfp_i_choice_preserve)) * c) + (pfp_a_choice_preserve))))))
  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 \/ (exists pvs_gap_choice_cases. pvs_gap_choice_cases + S (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 : exists v. (((((exists ff_h_pvs_choice_old_entry. ff_h_pvs_choice_old_entry + S (v) = S ((S (i)) * x1)) /\ exists ff_q_pvs_choice_old_entry. x = ff_q_pvs_choice_old_entry * S ((S (i)) * x1) + (v))) /\ ((((~((i)=0)) /\ ((n)=(i)*(v)))) \/ ((((i)=0 \/ ~(exists pvs_factor_choice_old_graphnondivisor. (n) = (i) * pvs_factor_choice_old_graphnondivisor)) /\ ((v)=(i)))))))
  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