Positive divisors · actual masks · constructive finite tables · Constructive arithmetic

Actual divisor sums and Möbius tables

ArithTable(N,F) ∧ 0<n≤N ⇒ ∃!z. DivisorSum(F,n,z)

Construct signed tables, tabulate independently defined Möbius values, and mask positive divisors before taking the actual signed prefix sum.

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 1380 native tactic lines and 92 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem DV0022 and follow only the lemmas and conservative definitions supporting signed_divisor_sum_exists_unique.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G007 milestone → theorem and definition dependencies.
Major independently established statements: DV000A mobius_table_exists · DV0025 signed_divisor_sum_positive_source_extensional · DV0022 signed_divisor_sum_exists_unique.
Independently verified Alpha v34 checked-use theorem family: 37 dependency-curried kernel-checked theorem bodies · 92 proof prerequisites · 30 linked definitions · 52 definition-dependency arrows · 1380 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 315 bundle nodes; SHA-256 96740bcedad194ebed5066ae03fa20cd922e702ae925b2c85f4ed45649aa0307.
Exact mathematical boundary: A genuine divisor mask has S n entries, indexed zero through n, and forces its zeroth entry to zero regardless of F(0). Möbius values remain positive-domain only. This family constructs divisor sums and Möbius tables; cancellation and the full G007 endpoint are separately proved later in the same release.