DI0009 — divisor_complement_prefix_permutation

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. ∀ b. ∀ c. ¬n = 0 → DivisorComplementPrefix(n,b,c,S n) → PermutationPrefix(b,c,S n)

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

Definition DAG

PermutationPrefix(b,c,l) · 1 DivisorComplement(n,d,q) · 1 DivisorComplementPrefix(n,b,c,l) · 1 BetaAt(b,c,i,x) · 1 BoundedPrefix(b,c,l) · 1 InjectivePrefix(b,c,l) · 1

Actual proof prerequisites

succ_le_succ · checked external prerequisite divisor_complement_bounded le_of_succ_le_succ · checked external prerequisite divisor_complement_functional divisor_complement_symmetric divisor_complement_prefix_lookup finite_bounded_injective_surjective · checked external prerequisite

Original expanded first-order statement

forall n b c. ~(n=0) -> (forall dvi_index_permutation_prefix. (exists pvs_gap_permutation_prefixdomain. pvs_gap_permutation_prefixdomain + S (dvi_index_permutation_prefix) = (S n)) -> exists dvi_value_permutation_prefix. ((((exists ff_h_pvs_permutation_prefixentry. ff_h_pvs_permutation_prefixentry + S (dvi_value_permutation_prefix) = S ((S (dvi_index_permutation_prefix)) * c)) /\ exists ff_q_pvs_permutation_prefixentry. b = ff_q_pvs_permutation_prefixentry * S ((S (dvi_index_permutation_prefix)) * c) + (dvi_value_permutation_prefix))) /\ ((((~((dvi_index_permutation_prefix)=0)) /\ ((n)=(dvi_index_permutation_prefix)*(dvi_value_permutation_prefix)))) \/ ((((dvi_index_permutation_prefix)=0 \/ ~(exists pvs_factor_permutation_prefixgraphnondivisor. (n) = (dvi_index_permutation_prefix) * pvs_factor_permutation_prefixgraphnondivisor)) /\ ((dvi_value_permutation_prefix)=(dvi_index_permutation_prefix))))))) -> (((forall pfp_i_permutation_resultbounded. (exists pfp_gap_permutation_resultboundedindex. pfp_gap_permutation_resultboundedindex + S (pfp_i_permutation_resultbounded) = (S n)) -> exists pfp_a_permutation_resultbounded. (((exists ff_h_pfp_permutation_resultboundedentry. ff_h_pfp_permutation_resultboundedentry + S (pfp_a_permutation_resultbounded) = S ((S (pfp_i_permutation_resultbounded)) * c)) /\ exists ff_q_pfp_permutation_resultboundedentry. b = ff_q_pfp_permutation_resultboundedentry * S ((S (pfp_i_permutation_resultbounded)) * c) + (pfp_a_permutation_resultbounded))) /\ (exists pfp_gap_permutation_resultboundedvalue. pfp_gap_permutation_resultboundedvalue + S (pfp_a_permutation_resultbounded) = (S n))) /\ (((forall pfp_i_permutation_resultinjective pfp_j_permutation_resultinjective pfp_a_permutation_resultinjective. (exists pfp_gap_permutation_resultinjectivefirst. pfp_gap_permutation_resultinjectivefirst + S (pfp_i_permutation_resultinjective) = (S n)) -> (exists pfp_gap_permutation_resultinjectivesecond. pfp_gap_permutation_resultinjectivesecond + S (pfp_j_permutation_resultinjective) = (S n)) -> (((exists ff_h_pfp_permutation_resultinjectiveleft. ff_h_pfp_permutation_resultinjectiveleft + S (pfp_a_permutation_resultinjective) = S ((S (pfp_i_permutation_resultinjective)) * c)) /\ exists ff_q_pfp_permutation_resultinjectiveleft. b = ff_q_pfp_permutation_resultinjectiveleft * S ((S (pfp_i_permutation_resultinjective)) * c) + (pfp_a_permutation_resultinjective))) -> (((exists ff_h_pfp_permutation_resultinjectiveright. ff_h_pfp_permutation_resultinjectiveright + S (pfp_a_permutation_resultinjective) = S ((S (pfp_j_permutation_resultinjective)) * c)) /\ exists ff_q_pfp_permutation_resultinjectiveright. b = ff_q_pfp_permutation_resultinjectiveright * S ((S (pfp_j_permutation_resultinjective)) * c) + (pfp_a_permutation_resultinjective))) -> pfp_i_permutation_resultinjective = pfp_j_permutation_resultinjective) /\ (forall pfp_a_permutation_resultsurjective. (exists pfp_gap_permutation_resultsurjectivevalue. pfp_gap_permutation_resultsurjectivevalue + S (pfp_a_permutation_resultsurjective) = (S n)) -> exists pfp_i_permutation_resultsurjective. (exists pfp_gap_permutation_resultsurjectiveindex. pfp_gap_permutation_resultsurjectiveindex + S (pfp_i_permutation_resultsurjective) = (S n)) /\ (((exists ff_h_pfp_permutation_resultsurjectiveentry. ff_h_pfp_permutation_resultsurjectiveentry + S (pfp_a_permutation_resultsurjective) = S ((S (pfp_i_permutation_resultsurjective)) * c)) /\ exists ff_q_pfp_permutation_resultsurjectiveentry. b = ff_q_pfp_permutation_resultsurjectiveentry * S ((S (pfp_i_permutation_resultsurjective)) * c) + (pfp_a_permutation_resultsurjective))))))))

Complete tactic proof in conservative notation

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

83 script commands · 17 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.

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 (4)

divisor complement bounded divisor complement functional divisor complement symmetric divisor complement prefix lookup

01Fix variables and assumptionsL1–5

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

L1
intro n
L2
intro b
L3
intro c
L4
intro hn
L5
intro hp

02Establish hbL6–8

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

L6
have hb : BoundedPrefix(b,c,S n)Definitions: BoundedPrefix(b,c,S n)Original native command in the exact edition
L7
intro i
L8
intro hi

03Establish hvL9–12

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

L9
have hv : ∃ q. BetaAt(b,c,i,q) ∧ DivisorComplement(n,i,q)Definitions: BetaAt(b,c,i,q)DivisorComplement(n,i,q)Original native command in the exact edition
L10
specialize hp (i)
L11
apply hp
L12
exact hi

04Separate the logical casesL13–14

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

L13
cases hv
L14
cases hv_witness

05Construct an explicit witnessL15–15

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

L15
exists x

06Separate the logical casesL16–16

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

L16
split

07Use earlier factsL17–26