Independent signed values · squarefreeness · genuine factor lists · Constructive arithmetic

Möbius values and prime adjunction

n>0 ⇒ ∃!z. Mobius(n,z); Prime(p) ∧ n>0 ∧ p∤n ⇒ μ(pn)=−μ(n)

Define Möbius values from squarefreeness and the parity of actual prime-factor lists, prove unique values, and trace how a fresh prime changes the sign.

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

Open the exact edition →

Focused route

Final dependency cone

Start at theorem MV0015 and follow only the lemmas and conservative definitions supporting mobius_fresh_prime_negates.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G007 milestone → theorem and definition dependencies.
Major independently established statements: MV000C mobius_value_exists_unique · MV000D mobius_one · MV0015 mobius_fresh_prime_negates.
Independently verified Alpha v34 checked-use theorem family: 21 dependency-curried kernel-checked theorem bodies · 64 proof prerequisites · 20 linked definitions · 26 definition-dependency arrows · 660 exact tactic lines · first admitted v31 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 237 bundle nodes; SHA-256 041f1a3471002ff3cd5fc3da2a6cc751ad2f4a4458a497b3de2a26276fd314b8.
Exact mathematical boundary: Mobius(n,z) is positive-domain only, independently defined from squarefreeness and actual prime-factor parity. Signed codes 0, 2 and 1 represent zero, +1 and -1. This family proves values and prime-adjunction laws; the separate Möbius-inversion family supplies the complete G007 endpoint.