Actual quotient witnesses · finite beta maps · reversible divisors · Constructive arithmetic

Complementary divisors and finite involutions

n≠0 ⇒ ∃b c. DivisorComplementPrefix(n,b,c,S n) ∧ PermutationPrefix(b,c,S n)

Construct complementary positive divisors and their actual finite permutation, fixing zero and every nondivisor in the surrounding interval.

Open the definition-aware map Read the final theorem See campaign milestone G007

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 certificate

Fully expanded arithmetic

Inspect all 480 native tactic lines and 34 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem DI000B and follow only the lemmas and conservative definitions supporting divisor_complement_prefix_involution.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G007 milestone → theorem and definition dependencies.
Major independently established statements: DI0001 positive_divisor_quotient_exists_unique · DI000A positive_divisor_involution_exists · DI000B divisor_complement_prefix_involution.
Independently verified Alpha v34 checked-use theorem family: 12 dependency-curried kernel-checked theorem bodies · 34 proof prerequisites · 10 linked definitions · 13 definition-dependency arrows · 480 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 140 bundle nodes; SHA-256 deffb1e384e64cd2cb56b4c1603a0fdde7578cec15e80618f5b06197fabf6fed.
Exact mathematical boundary: 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.