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

Actual divisor sums and Möbius tables

Public research checkpoint, not admitted to Alpha or Stable. Alpha v30 remains 3222 checked-use theorems; Stable remains 432. The on-demand Alpha Lean service does not yet expose these checkpoint theorems; their independently checked literal bundles and unchanged sources are available below.

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

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: research checkpoint map → 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.
Public research checkpoint, independently verified: 37 theorems in a complete dependency-closed HA bundle · 92 proof prerequisites · 30 linked definitions · 52 definition-dependency arrows · 1380 exact tactic lines. Not Alpha-enrolled; no Alpha checked-use authority; not Stable. Alpha v30 remains 3222 theorems and Stable remains 432. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 315 bundle nodes; SHA-256 96740bcedad194ebed5066ae03fa20cd922e702ae925b2c85f4ed45649aa0307. Inspect the checkpoint receipt, literal bundle, and source files →
Exact mathematical boundary: These are constructed divisor-sum and Möbius-table prerequisites, not full Möbius inversion. A divisor mask has S n entries indexed 0 through n, with entry zero forced to zero regardless of F(0). Mobius itself remains positive-domain only. Prime-toggle divisor cancellation and G007 inversion remain open.