MC000C

divisor_prime_toggle_prefix_exists

Ordinary finite induction constructs the actual beta-coded prime toggle at every index in the requested window.

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 input n is positive. Signed code 2 denotes +1, so the actual sum is +1 at n=1 and zero for n>1. The positive-values result permits arbitrary F(0), which the divisor mask excludes. Prime-square multiples contribute zero. Full G007 inversion is established in its separate family.

Exact theorem in conservative defined notation

∀ n. ∀ p. ∀ l. Prime(p) → ∃ x. ∃ y. DivisorPrimeTogglePrefix(n,p,x,y,l)

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

Definition DAG

DivisorPrimeToggle(n,p,d,e) · 2DivisorPrimeTogglePrefix(n,p,b,c,l) · 2Lt(a,b) · 2Prime(p) · 1BetaAt(b,c,i,x) · 4

Actual proof prerequisites

factor_permutation_below_zero_impossible · checked external prerequisitedivisor_prime_toggle_existsbeta_prefix_extend · checked external prerequisitefinite_lt_succ_eq_or_lt · checked external prerequisite
Original expanded first-order statement 
forall n p l. (~((p) = 1) /\ forall pvs_left_prefix_prime pvs_right_prefix_prime. (p) = pvs_left_prefix_prime * pvs_right_prefix_prime -> pvs_left_prefix_prime = 1 \/ pvs_right_prefix_prime = 1) -> exists b c. (forall dvi_index_prefix_result. (exists pvs_gap_prefix_resultdomain. pvs_gap_prefix_resultdomain + S (dvi_index_prefix_result) = (l)) -> exists dvi_value_prefix_result. ((((exists ff_h_pvs_prefix_resultentry. ff_h_pvs_prefix_resultentry + S (dvi_value_prefix_result) = S ((S (dvi_index_prefix_result)) * c)) /\ exists ff_q_pvs_prefix_resultentry. b = ff_q_pvs_prefix_resultentry * S ((S (dvi_index_prefix_result)) * c) + (dvi_value_prefix_result))) /\ ((((~((dvi_index_prefix_result)=0)) /\ (((exists pvs_factor_prefix_resultgraphdivisor. (n) = (dvi_index_prefix_result) * pvs_factor_prefix_resultgraphdivisor) /\ ((((~(exists pvs_factor_prefix_resultgraphtogglefresh_input. (dvi_index_prefix_result) = (p) * pvs_factor_prefix_resultgraphtogglefresh_input)) /\ ((dvi_value_prefix_result)=(p)*(dvi_index_prefix_result)))) \/ (((((dvi_index_prefix_result)=(p)*(dvi_value_prefix_result)) /\ (~(exists pvs_factor_prefix_resultgraphtogglefresh_output. (dvi_value_prefix_result) = (p) * pvs_factor_prefix_resultgraphtogglefresh_output)))) \/ (((exists pvs_factor_prefix_resultgraphtogglesquare. (dvi_index_prefix_result) = ((p)*(p)) * pvs_factor_prefix_resultgraphtogglesquare) /\ ((dvi_value_prefix_result)=(dvi_index_prefix_result)))))))))) \/ ((((dvi_index_prefix_result)=0 \/ ~(exists pvs_factor_prefix_resultgraphnondivisor. (n) = (dvi_index_prefix_result) * pvs_factor_prefix_resultgraphnondivisor)) /\ ((dvi_value_prefix_result)=(dvi_index_prefix_result)))))))

Complete tactic proof in conservative notation

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

75 script commands · 27 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 prime toggle exists
01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro p
  3. L3
    intro l
02Induction on lL4–5

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

  1. L4
    induction l
  2. L5
    intro hp
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–9

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

  1. L8
    intro i
  2. L9
    intro hi
05Separate the logical casesL10–10

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

  1. L10
    exfalso
06Use earlier factsL11–13

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

  1. L11
    specialize factor_permutation_below_zero_impossible (i)
  2. L12
    apply factor_permutation_below_zero_impossible
  3. L13
    exact hi
07Fix variables and assumptionsL14–14

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

  1. L14
    intro hp
08Establish hprevL15–17

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

  1. L15
    have hprev : ∃ b. ∃ c. DivisorPrimeTogglePrefix(n,p,b,c,l)Definitions: DivisorPrimeTogglePrefix(n,p,b,c,l)Original native command in the exact edition
  2. L16
    apply IH
  3. L17
    exact hp
09Separate the logical casesL18–19

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

  1. L18
    cases hprev
  2. L19
    cases hprev_witness
10Establish hvL20–25

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

  1. L20
    have hv : ∃ v. DivisorPrimeToggle(n,p,l,v)Definitions: DivisorPrimeToggle(n,p,l,v)Original native command in the exact edition
  2. L21
    specialize divisor_prime_toggle_exists (n)
  3. L22
    specialize divisor_prime_toggle_exists (p)
  4. L23
    specialize divisor_prime_toggle_exists (l)
  5. L24
    apply divisor_prime_toggle_exists
  6. L25
    exact hp
11Separate the logical casesL26–26

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

  1. L26
    cases hv
12Establish hextL27–32

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

  1. L27
    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. L28
    specialize beta_prefix_extend (l)
  3. L29
    specialize beta_prefix_extend (x)
  4. L30
    specialize beta_prefix_extend (x1)
  5. L31
    specialize beta_prefix_extend (x2)
  6. L32
    apply beta_prefix_extend
13Separate the logical casesL33–35

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

  1. L33
    cases hext
  2. L34
    cases hext_witness
  3. L35
    cases hext_witness_witness
14Construct an explicit witnessL36–37

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

  1. L36
    exists x3
  2. L37
    exists x4
15Fix variables and assumptionsL38–39

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

  1. L38
    intro i
  2. L39
    intro hi
16Establish hcL40–44

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. L40
    have hc : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L41
    specialize finite_lt_succ_eq_or_lt (l)
  3. L42
    specialize finite_lt_succ_eq_or_lt (i)
  4. L43
    apply finite_lt_succ_eq_or_lt
  5. L44
    exact hi
17Separate the logical casesL45–45

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

  1. L45
    cases hc
18Calculate and transport equalitiesL46–55

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

  1. L46
    rewrite hc_left
  2. L47
    rewrite hc_left
  3. L48
    rewrite hc_left
  4. L49
    rewrite hc_left
  5. L50
    rewrite hc_left
  6. L51
    rewrite hc_left
  7. L52
    rewrite hc_left
  8. L53
    rewrite hc_left
  9. L54
    rewrite hc_left
  10. L55
    rewrite hc_left
19Calculate and transport equalitiesL56–57

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

  1. L56
    rewrite hc_left
  2. L57
    rewrite hc_left
20Construct an explicit witnessL58–58

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

  1. L58
    exists x2
21Separate the logical casesL59–59

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

  1. L59
    split
22Use earlier factsL60–61

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

  1. L60
    exact hext_witness_witness_left
  2. L61
    exact hv_witness
23Establish holdL62–65

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

  1. L62
    have hold : ∃ v. BetaAt(x,x1,i,v) ∧ DivisorPrimeToggle(n,p,i,v)Definitions: BetaAt(x,x1,i,v)DivisorPrimeToggle(n,p,i,v)Original native command in the exact edition
  2. L63
    specialize hprev_witness_witness (i)
  3. L64
    apply hprev_witness_witness
  4. L65
    exact hc_right
24Separate the logical casesL66–67

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

  1. L66
    cases hold
  2. L67
    cases hold_witness
25Construct an explicit witnessL68–68

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

  1. L68
    exists x5
26Separate the logical casesL69–69

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

  1. L69
    split
27Use earlier factsL70–75

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

  1. L70
    specialize hext_witness_witness_right (i)
  2. L71
    specialize hext_witness_witness_right (x5)
  3. L72
    apply hext_witness_witness_right
  4. L73
    exact hc_right
  5. L74
    exact hold_witness_left
  6. L75
    exact hold_witness_right

Library-wide reading audit

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