Constructed Möbius witnesses · weighted divisor folds · forward and reverse · Constructive arithmetic

Full finite signed Möbius inversion

ArithTable(N,F) ∧ ArithTable(N,G) ∧ DivisorTransform(N,F,G) ⇒ ∃M H. MobiusTable(N,M) ∧ DirichletTable(N,M,G,H) ∧ ArithPositiveEqual(H,F,N)

Recover every original positive value from its divisor transform using actual finite Möbius-weighted sums.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem MI0008 and follow only the lemmas and conservative definitions supporting mobius_inversion_iff.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G007 milestone → theorem and definition dependencies.
Major independently established statements: MI0005 mobius_inversion_for_actual_mobius_table · MI0006 mobius_inversion_arithmetic_tables · MI0008 mobius_inversion_iff.
Independently verified Alpha v34 checked-use theorem family: 8 dependency-curried kernel-checked theorem bodies · 28 proof prerequisites · 35 linked definitions · 68 definition-dependency arrows · 458 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 531 bundle nodes; SHA-256 22e7e61d5d4567df695d67830b465664fbe5a070f0367196e5cfd542ccba5b75.
Exact mathematical boundary: The full finite signed G007 theorem includes the reverse equivalence and actual witnesses at N=0. The divisor-transform premise covers every required positive quotient. F(0), G(0) and H(0) are unrestricted; only the historical Möbius witness retains its separate zero convention. Full G009 multiplicative closure is admitted in Alpha v32; G091 prime-power fields remain open.