DI000A

positive_divisor_involution_exists

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

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

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. ~(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))))))))

Constructive proof overview

Generated structural guide

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

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

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

Proof neighborhood

Direct dependencies

DI0007 divisor_complement_prefix_exists DI0009 divisor_complement_prefix_permutation

Direct dependents

none

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

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.

Named ingredients (2)
divisor complement prefix existsdivisor complement 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–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
  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 exact command ledger · 19 lines
  1. 0001intro n
  2. 0002intro hn
  3. 0003have hp : exists b c. (forall dvi_index_involution_construct. (exists pvs_gap_involution_constructdomain. pvs_gap_involution_constructdomain + S (dvi_index_involution_construct) = (S n)) -> exists dvi_value_involution_construct. ((((exists ff_h_pvs_involution_constructentry. ff_h_pvs_involution_constructentry + S (dvi_value_involution_construct) = S ((S (dvi_index_involution_construct)) * c)) /\ exists ff_q_pvs_involution_constructentry. b = ff_q_pvs_involution_constructentry * S ((S (dvi_index_involution_construct)) * c) + (dvi_value_involution_construct))) /\ ((((~((dvi_index_involution_construct)=0)) /\ ((n)=(dvi_index_involution_construct)*(dvi_value_involution_construct)))) \/ ((((dvi_index_involution_construct)=0 \/ ~(exists pvs_factor_involution_constructgraphnondivisor. (n) = (dvi_index_involution_construct) * pvs_factor_involution_constructgraphnondivisor)) /\ ((dvi_value_involution_construct)=(dvi_index_involution_construct)))))))
  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