MC000F

divisor_prime_toggle_permutation_exists

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

For every actual prime divisor of a positive input, construct the complete finite toggle permutation without supplying its code.

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. ~(n=0) -> (~((p) = 1) /\ forall pvs_left_constructed_prime pvs_right_constructed_prime. (p) = pvs_left_constructed_prime * pvs_right_constructed_prime -> pvs_left_constructed_prime = 1 \/ pvs_right_constructed_prime = 1) -> (exists pvs_factor_constructed_divisor. (n) = (p) * pvs_factor_constructed_divisor) -> exists b c. (forall dvi_index_constructed_prefix. (exists pvs_gap_constructed_prefixdomain. pvs_gap_constructed_prefixdomain + S (dvi_index_constructed_prefix) = (S n)) -> exists dvi_value_constructed_prefix. ((((exists ff_h_pvs_constructed_prefixentry. ff_h_pvs_constructed_prefixentry + S (dvi_value_constructed_prefix) = S ((S (dvi_index_constructed_prefix)) * c)) /\ exists ff_q_pvs_constructed_prefixentry. b = ff_q_pvs_constructed_prefixentry * S ((S (dvi_index_constructed_prefix)) * c) + (dvi_value_constructed_prefix))) /\ ((((~((dvi_index_constructed_prefix)=0)) /\ (((exists pvs_factor_constructed_prefixgraphdivisor. (n) = (dvi_index_constructed_prefix) * pvs_factor_constructed_prefixgraphdivisor) /\ ((((~(exists pvs_factor_constructed_prefixgraphtogglefresh_input. (dvi_index_constructed_prefix) = (p) * pvs_factor_constructed_prefixgraphtogglefresh_input)) /\ ((dvi_value_constructed_prefix)=(p)*(dvi_index_constructed_prefix)))) \/ (((((dvi_index_constructed_prefix)=(p)*(dvi_value_constructed_prefix)) /\ (~(exists pvs_factor_constructed_prefixgraphtogglefresh_output. (dvi_value_constructed_prefix) = (p) * pvs_factor_constructed_prefixgraphtogglefresh_output)))) \/ (((exists pvs_factor_constructed_prefixgraphtogglesquare. (dvi_index_constructed_prefix) = ((p)*(p)) * pvs_factor_constructed_prefixgraphtogglesquare) /\ ((dvi_value_constructed_prefix)=(dvi_index_constructed_prefix)))))))))) \/ ((((dvi_index_constructed_prefix)=0 \/ ~(exists pvs_factor_constructed_prefixgraphnondivisor. (n) = (dvi_index_constructed_prefix) * pvs_factor_constructed_prefixgraphnondivisor)) /\ ((dvi_value_constructed_prefix)=(dvi_index_constructed_prefix))))))) /\ (((forall pfp_i_constructed_permutationbounded. (exists pfp_gap_constructed_permutationboundedindex. pfp_gap_constructed_permutationboundedindex + S (pfp_i_constructed_permutationbounded) = (S n)) -> exists pfp_a_constructed_permutationbounded. (((exists ff_h_pfp_constructed_permutationboundedentry. ff_h_pfp_constructed_permutationboundedentry + S (pfp_a_constructed_permutationbounded) = S ((S (pfp_i_constructed_permutationbounded)) * c)) /\ exists ff_q_pfp_constructed_permutationboundedentry. b = ff_q_pfp_constructed_permutationboundedentry * S ((S (pfp_i_constructed_permutationbounded)) * c) + (pfp_a_constructed_permutationbounded))) /\ (exists pfp_gap_constructed_permutationboundedvalue. pfp_gap_constructed_permutationboundedvalue + S (pfp_a_constructed_permutationbounded) = (S n))) /\ (((forall pfp_i_constructed_permutationinjective pfp_j_constructed_permutationinjective pfp_a_constructed_permutationinjective. (exists pfp_gap_constructed_permutationinjectivefirst. pfp_gap_constructed_permutationinjectivefirst + S (pfp_i_constructed_permutationinjective) = (S n)) -> (exists pfp_gap_constructed_permutationinjectivesecond. pfp_gap_constructed_permutationinjectivesecond + S (pfp_j_constructed_permutationinjective) = (S n)) -> (((exists ff_h_pfp_constructed_permutationinjectiveleft. ff_h_pfp_constructed_permutationinjectiveleft + S (pfp_a_constructed_permutationinjective) = S ((S (pfp_i_constructed_permutationinjective)) * c)) /\ exists ff_q_pfp_constructed_permutationinjectiveleft. b = ff_q_pfp_constructed_permutationinjectiveleft * S ((S (pfp_i_constructed_permutationinjective)) * c) + (pfp_a_constructed_permutationinjective))) -> (((exists ff_h_pfp_constructed_permutationinjectiveright. ff_h_pfp_constructed_permutationinjectiveright + S (pfp_a_constructed_permutationinjective) = S ((S (pfp_j_constructed_permutationinjective)) * c)) /\ exists ff_q_pfp_constructed_permutationinjectiveright. b = ff_q_pfp_constructed_permutationinjectiveright * S ((S (pfp_j_constructed_permutationinjective)) * c) + (pfp_a_constructed_permutationinjective))) -> pfp_i_constructed_permutationinjective = pfp_j_constructed_permutationinjective) /\ (forall pfp_a_constructed_permutationsurjective. (exists pfp_gap_constructed_permutationsurjectivevalue. pfp_gap_constructed_permutationsurjectivevalue + S (pfp_a_constructed_permutationsurjective) = (S n)) -> exists pfp_i_constructed_permutationsurjective. (exists pfp_gap_constructed_permutationsurjectiveindex. pfp_gap_constructed_permutationsurjectiveindex + S (pfp_i_constructed_permutationsurjective) = (S n)) /\ (((exists ff_h_pfp_constructed_permutationsurjectiveentry. ff_h_pfp_constructed_permutationsurjectiveentry + S (pfp_a_constructed_permutationsurjective) = S ((S (pfp_i_constructed_permutationsurjective)) * c)) /\ exists ff_q_pfp_constructed_permutationsurjectiveentry. b = ff_q_pfp_constructed_permutationsurjectiveentry * S ((S (pfp_i_constructed_permutationsurjective)) * c) + (pfp_a_constructed_permutationsurjective))))))))

Constructive proof overview

Generated structural guide

For every actual prime divisor of a positive input, construct the complete finite toggle permutation without supplying its code.

The unchanged tactic script uses 2 declared prerequisites and contains 26 exact native proof lines.

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

Proof neighborhood

Direct dependencies

MC000C divisor_prime_toggle_prefix_exists MC000E divisor_prime_toggle_prefix_permutation

Direct dependents

MC0016 mobius_divisor_mask_prime_factor_sum_zero

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

26 script commands · 6 reading checkpoints · 1 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 (2)
divisor prime toggle prefix existsdivisor prime toggle prefix permutation

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

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

  1. L1
    intro n
  2. L2
    intro p
  3. L3
    intro hn
  4. L4
    intro hp
  5. L5
    intro hpn
02Establish htL6–11

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

  1. L6
    have ht : ∃ b. ∃ c. DivisorPrimeTogglePrefix(n,p,b,c,S n)Definitions: DivisorPrimeTogglePrefix
  2. L7
    specialize divisor_prime_toggle_prefix_exists (n)
  3. L8
    specialize divisor_prime_toggle_prefix_exists (p)
  4. L9
    specialize divisor_prime_toggle_prefix_exists (S n)
  5. L10
    apply divisor_prime_toggle_prefix_exists
  6. L11
    exact hp
03Separate the logical casesL12–13

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

  1. L12
    cases ht
  2. L13
    cases ht_witness
04Construct an explicit witnessL14–15

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

  1. L14
    exists x
  2. L15
    exists x1
05Separate the logical casesL16–16

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

  1. L16
    split
06Use earlier factsL17–26

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

  1. L17
    exact ht_witness_witness
  2. L18
    specialize divisor_prime_toggle_prefix_permutation (n)
  3. L19
    specialize divisor_prime_toggle_prefix_permutation (p)
  4. L20
    specialize divisor_prime_toggle_prefix_permutation (x)
  5. L21
    specialize divisor_prime_toggle_prefix_permutation (x1)
  6. L22
    apply divisor_prime_toggle_prefix_permutation
  7. L23
    exact hn
  8. L24
    exact hp
  9. L25
    exact hpn
  10. L26
    exact ht_witness_witness

Library-wide reading audit

Original exact command ledger · 26 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro hn
  4. 0004intro hp
  5. 0005intro hpn
  6. 0006have ht : exists b c. (forall dvi_index_constructed_map. (exists pvs_gap_constructed_mapdomain. pvs_gap_constructed_mapdomain + S (dvi_index_constructed_map) = (S n)) -> exists dvi_value_constructed_map. ((((exists ff_h_pvs_constructed_mapentry. ff_h_pvs_constructed_mapentry + S (dvi_value_constructed_map) = S ((S (dvi_index_constructed_map)) * c)) /\ exists ff_q_pvs_constructed_mapentry. b = ff_q_pvs_constructed_mapentry * S ((S (dvi_index_constructed_map)) * c) + (dvi_value_constructed_map))) /\ ((((~((dvi_index_constructed_map)=0)) /\ (((exists pvs_factor_constructed_mapgraphdivisor. (n) = (dvi_index_constructed_map) * pvs_factor_constructed_mapgraphdivisor) /\ ((((~(exists pvs_factor_constructed_mapgraphtogglefresh_input. (dvi_index_constructed_map) = (p) * pvs_factor_constructed_mapgraphtogglefresh_input)) /\ ((dvi_value_constructed_map)=(p)*(dvi_index_constructed_map)))) \/ (((((dvi_index_constructed_map)=(p)*(dvi_value_constructed_map)) /\ (~(exists pvs_factor_constructed_mapgraphtogglefresh_output. (dvi_value_constructed_map) = (p) * pvs_factor_constructed_mapgraphtogglefresh_output)))) \/ (((exists pvs_factor_constructed_mapgraphtogglesquare. (dvi_index_constructed_map) = ((p)*(p)) * pvs_factor_constructed_mapgraphtogglesquare) /\ ((dvi_value_constructed_map)=(dvi_index_constructed_map)))))))))) \/ ((((dvi_index_constructed_map)=0 \/ ~(exists pvs_factor_constructed_mapgraphnondivisor. (n) = (dvi_index_constructed_map) * pvs_factor_constructed_mapgraphnondivisor)) /\ ((dvi_value_constructed_map)=(dvi_index_constructed_map)))))))
  7. 0007specialize divisor_prime_toggle_prefix_exists (n)
  8. 0008specialize divisor_prime_toggle_prefix_exists (p)
  9. 0009specialize divisor_prime_toggle_prefix_exists (S n)
  10. 0010apply divisor_prime_toggle_prefix_exists
  11. 0011exact hp
  12. 0012cases ht
  13. 0013cases ht_witness
  14. 0014exists x
  15. 0015exists x1
  16. 0016split
  17. 0017exact ht_witness_witness
  18. 0018specialize divisor_prime_toggle_prefix_permutation (n)
  19. 0019specialize divisor_prime_toggle_prefix_permutation (p)
  20. 0020specialize divisor_prime_toggle_prefix_permutation (x)
  21. 0021specialize divisor_prime_toggle_prefix_permutation (x1)
  22. 0022apply divisor_prime_toggle_prefix_permutation
  23. 0023exact hn
  24. 0024exact hp
  25. 0025exact hpn
  26. 0026exact ht_witness_witness