MC000F

divisor_prime_toggle_permutation_exists

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

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. ¬n = 0 → Prime(p) → Dvd(p,n) → ∃ x. ∃ y. DivisorPrimeTogglePrefix(n,p,x,y,S n) ∧ PermutationPrefix(x,y,S n)

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

Definition DAG

PermutationPrefix(b,c,l) · 1DivisorPrimeTogglePrefix(n,p,b,c,l) · 2Dvd(d,n) · 1Prime(p) · 1

Actual proof prerequisites

divisor_prime_toggle_prefix_existsdivisor_prime_toggle_prefix_permutation
Original expanded first-order 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))))))))

Complete tactic proof in conservative notation

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

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.

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 (2)
divisor prime toggle prefix existsdivisor prime toggle prefix permutation
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(n,p,b,c,S n)Original native command in the exact edition
  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 defined command ledger · 26 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro hn
  4. 0004intro hp
  5. 0005intro hpn
  6. 0006have ht : ∃ b. ∃ c. DivisorPrimeTogglePrefix(n,p,b,c,S n)
  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