MC000C

divisor_prime_toggle_prefix_exists

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

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

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 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)))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 4 declared prerequisites and contains 75 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 MC0008 divisor_prime_toggle_exists beta_prefix_extend Stable theorem; checked-use authorized finite_lt_succ_eq_or_lt Stable theorem; checked-use authorized

Direct dependents

MC000F divisor_prime_toggle_permutation_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

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.

Named ingredients (1)
divisor prime toggle 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–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
  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
  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: LtBetaAt
  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 \/ (exists pvs_gap_choice_cases. pvs_gap_choice_cases + S (i) = (l))
  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: DivisorPrimeToggleBetaAt
  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 exact 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 : 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)) /\ (((exists pvs_factor_choice_previousgraphdivisor. (n) = (dvi_index_choice_previous) * pvs_factor_choice_previousgraphdivisor) /\ ((((~(exists pvs_factor_choice_previousgraphtogglefresh_input. (dvi_index_choice_previous) = (p) * pvs_factor_choice_previousgraphtogglefresh_input)) /\ ((dvi_value_choice_previous)=(p)*(dvi_index_choice_previous)))) \/ (((((dvi_index_choice_previous)=(p)*(dvi_value_choice_previous)) /\ (~(exists pvs_factor_choice_previousgraphtogglefresh_output. (dvi_value_choice_previous) = (p) * pvs_factor_choice_previousgraphtogglefresh_output)))) \/ (((exists pvs_factor_choice_previousgraphtogglesquare. (dvi_index_choice_previous) = ((p)*(p)) * pvs_factor_choice_previousgraphtogglesquare) /\ ((dvi_value_choice_previous)=(dvi_index_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)))))))
  16. 0016apply IH
  17. 0017exact hp
  18. 0018cases hprev
  19. 0019cases hprev_witness
  20. 0020have hv : exists v. ((((~((l)=0)) /\ (((exists pvs_factor_choice_valuedivisor. (n) = (l) * pvs_factor_choice_valuedivisor) /\ ((((~(exists pvs_factor_choice_valuetogglefresh_input. (l) = (p) * pvs_factor_choice_valuetogglefresh_input)) /\ ((v)=(p)*(l)))) \/ (((((l)=(p)*(v)) /\ (~(exists pvs_factor_choice_valuetogglefresh_output. (v) = (p) * pvs_factor_choice_valuetogglefresh_output)))) \/ (((exists pvs_factor_choice_valuetogglesquare. (l) = ((p)*(p)) * pvs_factor_choice_valuetogglesquare) /\ ((v)=(l)))))))))) \/ ((((l)=0 \/ ~(exists pvs_factor_choice_valuenondivisor. (n) = (l) * pvs_factor_choice_valuenondivisor)) /\ ((v)=(l)))))
  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 : 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))))))
  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 \/ (exists pvs_gap_choice_cases. pvs_gap_choice_cases + S (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 : 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)) /\ (((exists pvs_factor_choice_old_graphdivisor. (n) = (i) * pvs_factor_choice_old_graphdivisor) /\ ((((~(exists pvs_factor_choice_old_graphtogglefresh_input. (i) = (p) * pvs_factor_choice_old_graphtogglefresh_input)) /\ ((v)=(p)*(i)))) \/ (((((i)=(p)*(v)) /\ (~(exists pvs_factor_choice_old_graphtogglefresh_output. (v) = (p) * pvs_factor_choice_old_graphtogglefresh_output)))) \/ (((exists pvs_factor_choice_old_graphtogglesquare. (i) = ((p)*(p)) * pvs_factor_choice_old_graphtogglesquare) /\ ((v)=(i)))))))))) \/ ((((i)=0 \/ ~(exists pvs_factor_choice_old_graphnondivisor. (n) = (i) * pvs_factor_choice_old_graphnondivisor)) /\ ((v)=(i)))))))
  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