MC000E

divisor_prime_toggle_prefix_permutation

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

The actual S n-entry prime toggle is a bounded, injective and constructively surjective permutation, including all fixed omitted indices.

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 b c. ~(n=0) -> (~((p) = 1) /\ forall pvs_left_permutation_prime pvs_right_permutation_prime. (p) = pvs_left_permutation_prime * pvs_right_permutation_prime -> pvs_left_permutation_prime = 1 \/ pvs_right_permutation_prime = 1) -> (exists pvs_factor_permutation_prime_divisor. (n) = (p) * pvs_factor_permutation_prime_divisor) -> (forall dvi_index_permutation_source. (exists pvs_gap_permutation_sourcedomain. pvs_gap_permutation_sourcedomain + S (dvi_index_permutation_source) = (S n)) -> exists dvi_value_permutation_source. ((((exists ff_h_pvs_permutation_sourceentry. ff_h_pvs_permutation_sourceentry + S (dvi_value_permutation_source) = S ((S (dvi_index_permutation_source)) * c)) /\ exists ff_q_pvs_permutation_sourceentry. b = ff_q_pvs_permutation_sourceentry * S ((S (dvi_index_permutation_source)) * c) + (dvi_value_permutation_source))) /\ ((((~((dvi_index_permutation_source)=0)) /\ (((exists pvs_factor_permutation_sourcegraphdivisor. (n) = (dvi_index_permutation_source) * pvs_factor_permutation_sourcegraphdivisor) /\ ((((~(exists pvs_factor_permutation_sourcegraphtogglefresh_input. (dvi_index_permutation_source) = (p) * pvs_factor_permutation_sourcegraphtogglefresh_input)) /\ ((dvi_value_permutation_source)=(p)*(dvi_index_permutation_source)))) \/ (((((dvi_index_permutation_source)=(p)*(dvi_value_permutation_source)) /\ (~(exists pvs_factor_permutation_sourcegraphtogglefresh_output. (dvi_value_permutation_source) = (p) * pvs_factor_permutation_sourcegraphtogglefresh_output)))) \/ (((exists pvs_factor_permutation_sourcegraphtogglesquare. (dvi_index_permutation_source) = ((p)*(p)) * pvs_factor_permutation_sourcegraphtogglesquare) /\ ((dvi_value_permutation_source)=(dvi_index_permutation_source)))))))))) \/ ((((dvi_index_permutation_source)=0 \/ ~(exists pvs_factor_permutation_sourcegraphnondivisor. (n) = (dvi_index_permutation_source) * pvs_factor_permutation_sourcegraphnondivisor)) /\ ((dvi_value_permutation_source)=(dvi_index_permutation_source))))))) -> (((forall pfp_i_permutation_targetbounded. (exists pfp_gap_permutation_targetboundedindex. pfp_gap_permutation_targetboundedindex + S (pfp_i_permutation_targetbounded) = (S n)) -> exists pfp_a_permutation_targetbounded. (((exists ff_h_pfp_permutation_targetboundedentry. ff_h_pfp_permutation_targetboundedentry + S (pfp_a_permutation_targetbounded) = S ((S (pfp_i_permutation_targetbounded)) * c)) /\ exists ff_q_pfp_permutation_targetboundedentry. b = ff_q_pfp_permutation_targetboundedentry * S ((S (pfp_i_permutation_targetbounded)) * c) + (pfp_a_permutation_targetbounded))) /\ (exists pfp_gap_permutation_targetboundedvalue. pfp_gap_permutation_targetboundedvalue + S (pfp_a_permutation_targetbounded) = (S n))) /\ (((forall pfp_i_permutation_targetinjective pfp_j_permutation_targetinjective pfp_a_permutation_targetinjective. (exists pfp_gap_permutation_targetinjectivefirst. pfp_gap_permutation_targetinjectivefirst + S (pfp_i_permutation_targetinjective) = (S n)) -> (exists pfp_gap_permutation_targetinjectivesecond. pfp_gap_permutation_targetinjectivesecond + S (pfp_j_permutation_targetinjective) = (S n)) -> (((exists ff_h_pfp_permutation_targetinjectiveleft. ff_h_pfp_permutation_targetinjectiveleft + S (pfp_a_permutation_targetinjective) = S ((S (pfp_i_permutation_targetinjective)) * c)) /\ exists ff_q_pfp_permutation_targetinjectiveleft. b = ff_q_pfp_permutation_targetinjectiveleft * S ((S (pfp_i_permutation_targetinjective)) * c) + (pfp_a_permutation_targetinjective))) -> (((exists ff_h_pfp_permutation_targetinjectiveright. ff_h_pfp_permutation_targetinjectiveright + S (pfp_a_permutation_targetinjective) = S ((S (pfp_j_permutation_targetinjective)) * c)) /\ exists ff_q_pfp_permutation_targetinjectiveright. b = ff_q_pfp_permutation_targetinjectiveright * S ((S (pfp_j_permutation_targetinjective)) * c) + (pfp_a_permutation_targetinjective))) -> pfp_i_permutation_targetinjective = pfp_j_permutation_targetinjective) /\ (forall pfp_a_permutation_targetsurjective. (exists pfp_gap_permutation_targetsurjectivevalue. pfp_gap_permutation_targetsurjectivevalue + S (pfp_a_permutation_targetsurjective) = (S n)) -> exists pfp_i_permutation_targetsurjective. (exists pfp_gap_permutation_targetsurjectiveindex. pfp_gap_permutation_targetsurjectiveindex + S (pfp_i_permutation_targetsurjective) = (S n)) /\ (((exists ff_h_pfp_permutation_targetsurjectiveentry. ff_h_pfp_permutation_targetsurjectiveentry + S (pfp_a_permutation_targetsurjective) = S ((S (pfp_i_permutation_targetsurjective)) * c)) /\ exists ff_q_pfp_permutation_targetsurjectiveentry. b = ff_q_pfp_permutation_targetsurjectiveentry * S ((S (pfp_i_permutation_targetsurjective)) * c) + (pfp_a_permutation_targetsurjective))))))))

Constructive proof overview

Generated structural guide

The actual S n-entry prime toggle is a bounded, injective and constructively surjective permutation, including all fixed omitted indices.

The unchanged tactic script uses 7 declared prerequisites and contains 99 exact native proof lines.

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

Proof neighborhood

Direct dependencies

succ_le_succ Stable theorem; checked-use authorized MC000B divisor_prime_toggle_bounded le_of_succ_le_succ Stable theorem; checked-use authorized MC0009 divisor_prime_toggle_functional MC000A divisor_prime_toggle_symmetric MC000D divisor_prime_toggle_prefix_lookup finite_bounded_injective_surjective 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

99 script commands · 18 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.

Named ingredients (4)
divisor prime toggle boundeddivisor prime toggle functionaldivisor prime toggle symmetricdivisor prime toggle prefix lookup

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–8

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

  1. L1
    intro n
  2. L2
    intro p
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro hn
  6. L6
    intro hp
  7. L7
    intro hpn
  8. L8
    intro hprefix
02Establish hbL9–11

Establish this local claim before using it. It is not an additional assumption.

  1. L9
    have hb : BoundedPrefix(b,c,S n)Definitions: BoundedPrefix
  2. L10
    intro i
  3. L11
    intro hi
03Establish hvL12–15

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

  1. L12
    have hv : ∃ e. BetaAt(b,c,i,e) ∧ DivisorPrimeToggle(n,p,i,e)Definitions: DivisorPrimeToggleBetaAt
  2. L13
    specialize hprefix (i)
  3. L14
    apply hprefix
  4. L15
    exact hi
04Separate the logical casesL16–17

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

  1. L16
    cases hv
  2. L17
    cases hv_witness
05Construct an explicit witnessL18–18

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

  1. L18
    exists x
06Separate the logical casesL19–19

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

  1. L19
    split
07Use earlier factsL20–29

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

  1. L20
    exact hv_witness_left
  2. L21
    specialize succ_le_succ (x)
  3. L22
    specialize succ_le_succ (n)
  4. L23
    apply succ_le_succ
  5. L24
    specialize divisor_prime_toggle_bounded (n)
  6. L25
    specialize divisor_prime_toggle_bounded (p)
  7. L26
    specialize divisor_prime_toggle_bounded (i)
  8. L27
    specialize divisor_prime_toggle_bounded (x)
  9. L28
    apply divisor_prime_toggle_bounded
  10. L29
    exact hn
08Use earlier factsL30–36

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

  1. L30
    exact hp
  2. L31
    exact hpn
  3. L32
    specialize le_of_succ_le_succ (i)
  4. L33
    specialize le_of_succ_le_succ (n)
  5. L34
    apply le_of_succ_le_succ
  6. L35
    exact hi
  7. L36
    exact hv_witness_right
09Establish hinjL37–46

Establish this local claim before using it. It is not an additional assumption.

  1. L37
    have hinj : InjectivePrefix(b,c,S n)Definitions: InjectivePrefix
  2. L38
    intro i
  3. L39
    intro j
  4. L40
    intro a
  5. L41
    intro hi
  6. L42
    intro hj
  7. L43
    intro hia
  8. L44
    intro hja
  9. L45
    specialize divisor_prime_toggle_functional (n)
  10. L46
    specialize divisor_prime_toggle_functional (p)
10Use earlier factsL47–56

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

  1. L47
    specialize divisor_prime_toggle_functional (a)
  2. L48
    specialize divisor_prime_toggle_functional (i)
  3. L49
    specialize divisor_prime_toggle_functional (j)
  4. L50
    apply divisor_prime_toggle_functional
  5. L51
    exact hp
  6. L52
    specialize divisor_prime_toggle_symmetric (n)
  7. L53
    specialize divisor_prime_toggle_symmetric (p)
  8. L54
    specialize divisor_prime_toggle_symmetric (i)
  9. L55
    specialize divisor_prime_toggle_symmetric (a)
  10. L56
    apply divisor_prime_toggle_symmetric
11Use earlier factsL57–66

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

  1. L57
    exact hn
  2. L58
    exact hp
  3. L59
    exact hpn
  4. L60
    specialize divisor_prime_toggle_prefix_lookup (n)
  5. L61
    specialize divisor_prime_toggle_prefix_lookup (p)
  6. L62
    specialize divisor_prime_toggle_prefix_lookup (b)
  7. L63
    specialize divisor_prime_toggle_prefix_lookup (c)
  8. L64
    specialize divisor_prime_toggle_prefix_lookup (S n)
  9. L65
    specialize divisor_prime_toggle_prefix_lookup (i)
  10. L66
    specialize divisor_prime_toggle_prefix_lookup (a)
12Use earlier factsL67–76

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

  1. L67
    apply divisor_prime_toggle_prefix_lookup
  2. L68
    exact hprefix
  3. L69
    exact hi
  4. L70
    exact hia
  5. L71
    specialize divisor_prime_toggle_symmetric (n)
  6. L72
    specialize divisor_prime_toggle_symmetric (p)
  7. L73
    specialize divisor_prime_toggle_symmetric (j)
  8. L74
    specialize divisor_prime_toggle_symmetric (a)
  9. L75
    apply divisor_prime_toggle_symmetric
  10. L76
    exact hn
13Use earlier factsL77–86

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

  1. L77
    exact hp
  2. L78
    exact hpn
  3. L79
    specialize divisor_prime_toggle_prefix_lookup (n)
  4. L80
    specialize divisor_prime_toggle_prefix_lookup (p)
  5. L81
    specialize divisor_prime_toggle_prefix_lookup (b)
  6. L82
    specialize divisor_prime_toggle_prefix_lookup (c)
  7. L83
    specialize divisor_prime_toggle_prefix_lookup (S n)
  8. L84
    specialize divisor_prime_toggle_prefix_lookup (j)
  9. L85
    specialize divisor_prime_toggle_prefix_lookup (a)
  10. L86
    apply divisor_prime_toggle_prefix_lookup
14Use earlier factsL87–89

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

  1. L87
    exact hprefix
  2. L88
    exact hj
  3. L89
    exact hja
15Separate the logical casesL90–90

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

  1. L90
    split
16Use earlier factsL91–91

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

  1. L91
    exact hb
17Separate the logical casesL92–92

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

  1. L92
    split
18Use earlier factsL93–99

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

  1. L93
    exact hinj
  2. L94
    specialize finite_bounded_injective_surjective (S n)
  3. L95
    specialize finite_bounded_injective_surjective (b)
  4. L96
    specialize finite_bounded_injective_surjective (c)
  5. L97
    apply finite_bounded_injective_surjective
  6. L98
    exact hb
  7. L99
    exact hinj

Library-wide reading audit

Original exact command ledger · 99 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro b
  4. 0004intro c
  5. 0005intro hn
  6. 0006intro hp
  7. 0007intro hpn
  8. 0008intro hprefix
  9. 0009have hb : forall pfp_i_toggle_permutation_bound. (exists pfp_gap_toggle_permutation_boundindex. pfp_gap_toggle_permutation_boundindex + S (pfp_i_toggle_permutation_bound) = (S n)) -> exists pfp_a_toggle_permutation_bound. (((exists ff_h_pfp_toggle_permutation_boundentry. ff_h_pfp_toggle_permutation_boundentry + S (pfp_a_toggle_permutation_bound) = S ((S (pfp_i_toggle_permutation_bound)) * c)) /\ exists ff_q_pfp_toggle_permutation_boundentry. b = ff_q_pfp_toggle_permutation_boundentry * S ((S (pfp_i_toggle_permutation_bound)) * c) + (pfp_a_toggle_permutation_bound))) /\ (exists pfp_gap_toggle_permutation_boundvalue. pfp_gap_toggle_permutation_boundvalue + S (pfp_a_toggle_permutation_bound) = (S n))
  10. 0010intro i
  11. 0011intro hi
  12. 0012have hv : exists e. (((((exists ff_h_pvs_toggle_permutation_entry. ff_h_pvs_toggle_permutation_entry + S (e) = S ((S (i)) * c)) /\ exists ff_q_pvs_toggle_permutation_entry. b = ff_q_pvs_toggle_permutation_entry * S ((S (i)) * c) + (e))) /\ ((((~((i)=0)) /\ (((exists pvs_factor_toggle_permutation_graphdivisor. (n) = (i) * pvs_factor_toggle_permutation_graphdivisor) /\ ((((~(exists pvs_factor_toggle_permutation_graphtogglefresh_input. (i) = (p) * pvs_factor_toggle_permutation_graphtogglefresh_input)) /\ ((e)=(p)*(i)))) \/ (((((i)=(p)*(e)) /\ (~(exists pvs_factor_toggle_permutation_graphtogglefresh_output. (e) = (p) * pvs_factor_toggle_permutation_graphtogglefresh_output)))) \/ (((exists pvs_factor_toggle_permutation_graphtogglesquare. (i) = ((p)*(p)) * pvs_factor_toggle_permutation_graphtogglesquare) /\ ((e)=(i)))))))))) \/ ((((i)=0 \/ ~(exists pvs_factor_toggle_permutation_graphnondivisor. (n) = (i) * pvs_factor_toggle_permutation_graphnondivisor)) /\ ((e)=(i)))))))
  13. 0013specialize hprefix (i)
  14. 0014apply hprefix
  15. 0015exact hi
  16. 0016cases hv
  17. 0017cases hv_witness
  18. 0018exists x
  19. 0019split
  20. 0020exact hv_witness_left
  21. 0021specialize succ_le_succ (x)
  22. 0022specialize succ_le_succ (n)
  23. 0023apply succ_le_succ
  24. 0024specialize divisor_prime_toggle_bounded (n)
  25. 0025specialize divisor_prime_toggle_bounded (p)
  26. 0026specialize divisor_prime_toggle_bounded (i)
  27. 0027specialize divisor_prime_toggle_bounded (x)
  28. 0028apply divisor_prime_toggle_bounded
  29. 0029exact hn
  30. 0030exact hp
  31. 0031exact hpn
  32. 0032specialize le_of_succ_le_succ (i)
  33. 0033specialize le_of_succ_le_succ (n)
  34. 0034apply le_of_succ_le_succ
  35. 0035exact hi
  36. 0036exact hv_witness_right
  37. 0037have hinj : forall pfp_i_toggle_permutation_injective pfp_j_toggle_permutation_injective pfp_a_toggle_permutation_injective. (exists pfp_gap_toggle_permutation_injectivefirst. pfp_gap_toggle_permutation_injectivefirst + S (pfp_i_toggle_permutation_injective) = (S n)) -> (exists pfp_gap_toggle_permutation_injectivesecond. pfp_gap_toggle_permutation_injectivesecond + S (pfp_j_toggle_permutation_injective) = (S n)) -> (((exists ff_h_pfp_toggle_permutation_injectiveleft. ff_h_pfp_toggle_permutation_injectiveleft + S (pfp_a_toggle_permutation_injective) = S ((S (pfp_i_toggle_permutation_injective)) * c)) /\ exists ff_q_pfp_toggle_permutation_injectiveleft. b = ff_q_pfp_toggle_permutation_injectiveleft * S ((S (pfp_i_toggle_permutation_injective)) * c) + (pfp_a_toggle_permutation_injective))) -> (((exists ff_h_pfp_toggle_permutation_injectiveright. ff_h_pfp_toggle_permutation_injectiveright + S (pfp_a_toggle_permutation_injective) = S ((S (pfp_j_toggle_permutation_injective)) * c)) /\ exists ff_q_pfp_toggle_permutation_injectiveright. b = ff_q_pfp_toggle_permutation_injectiveright * S ((S (pfp_j_toggle_permutation_injective)) * c) + (pfp_a_toggle_permutation_injective))) -> pfp_i_toggle_permutation_injective = pfp_j_toggle_permutation_injective
  38. 0038intro i
  39. 0039intro j
  40. 0040intro a
  41. 0041intro hi
  42. 0042intro hj
  43. 0043intro hia
  44. 0044intro hja
  45. 0045specialize divisor_prime_toggle_functional (n)
  46. 0046specialize divisor_prime_toggle_functional (p)
  47. 0047specialize divisor_prime_toggle_functional (a)
  48. 0048specialize divisor_prime_toggle_functional (i)
  49. 0049specialize divisor_prime_toggle_functional (j)
  50. 0050apply divisor_prime_toggle_functional
  51. 0051exact hp
  52. 0052specialize divisor_prime_toggle_symmetric (n)
  53. 0053specialize divisor_prime_toggle_symmetric (p)
  54. 0054specialize divisor_prime_toggle_symmetric (i)
  55. 0055specialize divisor_prime_toggle_symmetric (a)
  56. 0056apply divisor_prime_toggle_symmetric
  57. 0057exact hn
  58. 0058exact hp
  59. 0059exact hpn
  60. 0060specialize divisor_prime_toggle_prefix_lookup (n)
  61. 0061specialize divisor_prime_toggle_prefix_lookup (p)
  62. 0062specialize divisor_prime_toggle_prefix_lookup (b)
  63. 0063specialize divisor_prime_toggle_prefix_lookup (c)
  64. 0064specialize divisor_prime_toggle_prefix_lookup (S n)
  65. 0065specialize divisor_prime_toggle_prefix_lookup (i)
  66. 0066specialize divisor_prime_toggle_prefix_lookup (a)
  67. 0067apply divisor_prime_toggle_prefix_lookup
  68. 0068exact hprefix
  69. 0069exact hi
  70. 0070exact hia
  71. 0071specialize divisor_prime_toggle_symmetric (n)
  72. 0072specialize divisor_prime_toggle_symmetric (p)
  73. 0073specialize divisor_prime_toggle_symmetric (j)
  74. 0074specialize divisor_prime_toggle_symmetric (a)
  75. 0075apply divisor_prime_toggle_symmetric
  76. 0076exact hn
  77. 0077exact hp
  78. 0078exact hpn
  79. 0079specialize divisor_prime_toggle_prefix_lookup (n)
  80. 0080specialize divisor_prime_toggle_prefix_lookup (p)
  81. 0081specialize divisor_prime_toggle_prefix_lookup (b)
  82. 0082specialize divisor_prime_toggle_prefix_lookup (c)
  83. 0083specialize divisor_prime_toggle_prefix_lookup (S n)
  84. 0084specialize divisor_prime_toggle_prefix_lookup (j)
  85. 0085specialize divisor_prime_toggle_prefix_lookup (a)
  86. 0086apply divisor_prime_toggle_prefix_lookup
  87. 0087exact hprefix
  88. 0088exact hj
  89. 0089exact hja
  90. 0090split
  91. 0091exact hb
  92. 0092split
  93. 0093exact hinj
  94. 0094specialize finite_bounded_injective_surjective (S n)
  95. 0095specialize finite_bounded_injective_surjective (b)
  96. 0096specialize finite_bounded_injective_surjective (c)
  97. 0097apply finite_bounded_injective_surjective
  98. 0098exact hb
  99. 0099exact hinj