DI000A

positive_divisor_involution_exists

Every positive natural has an actually constructed finite divisor-complement permutation, with exact quotient equations on positive divisors.

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 complementary quotient is witnessed by n=d*q at positive divisors. The actual permutation covers indices zero through n, fixing zero and nondivisors. This is the involution foundation for the separate cancellation and full G007 inversion proofs, not an assumed divisor bijection.

Exact theorem in conservative defined notation

∀ n. ¬n = 0 → ∃ x. ∃ y. DivisorComplementPrefix(n,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) · 1DivisorComplementPrefix(n,b,c,l) · 2

Actual proof prerequisites

divisor_complement_prefix_existsdivisor_complement_prefix_permutation
Original expanded first-order statement 
forall n. ~(n=0) -> exists b c. (forall dvi_index_involution_prefix. (exists pvs_gap_involution_prefixdomain. pvs_gap_involution_prefixdomain + S (dvi_index_involution_prefix) = (S n)) -> exists dvi_value_involution_prefix. ((((exists ff_h_pvs_involution_prefixentry. ff_h_pvs_involution_prefixentry + S (dvi_value_involution_prefix) = S ((S (dvi_index_involution_prefix)) * c)) /\ exists ff_q_pvs_involution_prefixentry. b = ff_q_pvs_involution_prefixentry * S ((S (dvi_index_involution_prefix)) * c) + (dvi_value_involution_prefix))) /\ ((((~((dvi_index_involution_prefix)=0)) /\ ((n)=(dvi_index_involution_prefix)*(dvi_value_involution_prefix)))) \/ ((((dvi_index_involution_prefix)=0 \/ ~(exists pvs_factor_involution_prefixgraphnondivisor. (n) = (dvi_index_involution_prefix) * pvs_factor_involution_prefixgraphnondivisor)) /\ ((dvi_value_involution_prefix)=(dvi_index_involution_prefix))))))) /\ (((forall pfp_i_involution_permutationbounded. (exists pfp_gap_involution_permutationboundedindex. pfp_gap_involution_permutationboundedindex + S (pfp_i_involution_permutationbounded) = (S n)) -> exists pfp_a_involution_permutationbounded. (((exists ff_h_pfp_involution_permutationboundedentry. ff_h_pfp_involution_permutationboundedentry + S (pfp_a_involution_permutationbounded) = S ((S (pfp_i_involution_permutationbounded)) * c)) /\ exists ff_q_pfp_involution_permutationboundedentry. b = ff_q_pfp_involution_permutationboundedentry * S ((S (pfp_i_involution_permutationbounded)) * c) + (pfp_a_involution_permutationbounded))) /\ (exists pfp_gap_involution_permutationboundedvalue. pfp_gap_involution_permutationboundedvalue + S (pfp_a_involution_permutationbounded) = (S n))) /\ (((forall pfp_i_involution_permutationinjective pfp_j_involution_permutationinjective pfp_a_involution_permutationinjective. (exists pfp_gap_involution_permutationinjectivefirst. pfp_gap_involution_permutationinjectivefirst + S (pfp_i_involution_permutationinjective) = (S n)) -> (exists pfp_gap_involution_permutationinjectivesecond. pfp_gap_involution_permutationinjectivesecond + S (pfp_j_involution_permutationinjective) = (S n)) -> (((exists ff_h_pfp_involution_permutationinjectiveleft. ff_h_pfp_involution_permutationinjectiveleft + S (pfp_a_involution_permutationinjective) = S ((S (pfp_i_involution_permutationinjective)) * c)) /\ exists ff_q_pfp_involution_permutationinjectiveleft. b = ff_q_pfp_involution_permutationinjectiveleft * S ((S (pfp_i_involution_permutationinjective)) * c) + (pfp_a_involution_permutationinjective))) -> (((exists ff_h_pfp_involution_permutationinjectiveright. ff_h_pfp_involution_permutationinjectiveright + S (pfp_a_involution_permutationinjective) = S ((S (pfp_j_involution_permutationinjective)) * c)) /\ exists ff_q_pfp_involution_permutationinjectiveright. b = ff_q_pfp_involution_permutationinjectiveright * S ((S (pfp_j_involution_permutationinjective)) * c) + (pfp_a_involution_permutationinjective))) -> pfp_i_involution_permutationinjective = pfp_j_involution_permutationinjective) /\ (forall pfp_a_involution_permutationsurjective. (exists pfp_gap_involution_permutationsurjectivevalue. pfp_gap_involution_permutationsurjectivevalue + S (pfp_a_involution_permutationsurjective) = (S n)) -> exists pfp_i_involution_permutationsurjective. (exists pfp_gap_involution_permutationsurjectiveindex. pfp_gap_involution_permutationsurjectiveindex + S (pfp_i_involution_permutationsurjective) = (S n)) /\ (((exists ff_h_pfp_involution_permutationsurjectiveentry. ff_h_pfp_involution_permutationsurjectiveentry + S (pfp_a_involution_permutationsurjective) = S ((S (pfp_i_involution_permutationsurjective)) * c)) /\ exists ff_q_pfp_involution_permutationsurjectiveentry. b = ff_q_pfp_involution_permutationsurjectiveentry * S ((S (pfp_i_involution_permutationsurjective)) * c) + (pfp_a_involution_permutationsurjective))))))))

Complete tactic proof in conservative notation

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

19 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 complement prefix existsdivisor complement prefix permutation
01Fix variables and assumptionsL1–2

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

  1. L1
    intro n
  2. L2
    intro hn
02Establish hpL3–7

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

  1. L3
    have hp : ∃ b. ∃ c. DivisorComplementPrefix(n,b,c,S n)Definitions: DivisorComplementPrefix(n,b,c,S n)Original native command in the exact edition
  2. L4
    specialize divisor_complement_prefix_exists (n)
  3. L5
    specialize divisor_complement_prefix_exists (S n)
  4. L6
    apply divisor_complement_prefix_exists
  5. L7
    exact hn
03Separate the logical casesL8–9

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

  1. L8
    cases hp
  2. L9
    cases hp_witness
04Construct an explicit witnessL10–11

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

  1. L10
    exists x
  2. L11
    exists x1
05Separate the logical casesL12–12

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

  1. L12
    split
06Use earlier factsL13–19

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

  1. L13
    exact hp_witness_witness
  2. L14
    specialize divisor_complement_prefix_permutation (n)
  3. L15
    specialize divisor_complement_prefix_permutation (x)
  4. L16
    specialize divisor_complement_prefix_permutation (x1)
  5. L17
    apply divisor_complement_prefix_permutation
  6. L18
    exact hn
  7. L19
    exact hp_witness_witness

Library-wide reading audit

Original defined command ledger · 19 lines
  1. 0001intro n
  2. 0002intro hn
  3. 0003have hp : ∃ b. ∃ c. DivisorComplementPrefix(n,b,c,S n)
  4. 0004specialize divisor_complement_prefix_exists (n)
  5. 0005specialize divisor_complement_prefix_exists (S n)
  6. 0006apply divisor_complement_prefix_exists
  7. 0007exact hn
  8. 0008cases hp
  9. 0009cases hp_witness
  10. 0010exists x
  11. 0011exists x1
  12. 0012split
  13. 0013exact hp_witness_witness
  14. 0014specialize divisor_complement_prefix_permutation (n)
  15. 0015specialize divisor_complement_prefix_permutation (x)
  16. 0016specialize divisor_complement_prefix_permutation (x1)
  17. 0017apply divisor_complement_prefix_permutation
  18. 0018exact hn
  19. 0019exact hp_witness_witness