Constructed prime toggles · signed anti-invariance · the unit boundary · Constructive arithmetic

Möbius divisor cancellation

n≠0 ⇒ ∃M z. MobiusTable(n,M) ∧ DivisorSum(M,n,z) ∧ ((n=1 ∧ z=2) ∨ (n≠1 ∧ z=0))

Construct a prime-factor toggle and prove cancellation of the actual Möbius divisor sum, including the separate value at one and unrestricted input-table value at zero.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem MC001C and follow only the lemmas and conservative definitions supporting mobius_divisor_sum_cancellation_on_positive_values.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G007 milestone → theorem and definition dependencies.
Major independently established statements: MC001A mobius_divisor_sum_cancellation · MC001B mobius_divisor_sum_cancellation_exists · MC001C mobius_divisor_sum_cancellation_on_positive_values.
Independently verified Alpha v34 checked-use theorem family: 28 dependency-curried kernel-checked theorem bodies · 99 proof prerequisites · 39 linked definitions · 71 definition-dependency arrows · 1569 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 377 bundle nodes; SHA-256 f858f6bd9e09d6ec33b48689b385222153ad9d326eccb8239ac5776b39955542.
Exact mathematical boundary: The input n is positive. Signed code 2 denotes +1, so the actual sum is +1 at n=1 and zero for n>1. The positive-values result permits arbitrary F(0), which the divisor mask excludes. Prime-square multiples contribute zero. Full G007 inversion is established in its separate family.