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

Möbius values and prime adjunction

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.

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

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: research checkpoint map → 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.
Public research checkpoint, independently verified: 21 theorems in a complete dependency-closed HA bundle · 64 proof prerequisites · 20 linked definitions · 26 definition-dependency arrows · 660 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 237 bundle nodes; SHA-256 041f1a3471002ff3cd5fc3da2a6cc751ad2f4a4458a497b3de2a26276fd314b8. Inspect the checkpoint receipt, literal bundle, and source files →
Exact mathematical boundary: Mobius(n,z) is defined only for positive n. The canonical signed codes are 0 for zero, 2 for +1, and 1 for −1. The function is defined independently of any divisor-sum identity. These values and prime-step lemmas are prerequisites for G007; divisor-sum cancellation and full Möbius inversion remain open in this checkpoint. No signed-table proof is included here.