Möbius divisor cancellation — exact evidence

Current Alpha v34 checked use; first admitted v31; not Stable. Original HA and the independently compiled Lean checker have freshly verified the complete bundle before this page was generated.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

377 checked bundle nodes · 1081 proof edges · 27012 body proof nodes.

Literal self-contained proof bundle · SHA-256 f858f6bd9e09d6ec33b48689b385222153ad9d326eccb8239ac5776b39955542

mobius_divisor_cancellation_candidate.py

Unchanged historical local checkpoint record · Historical snapshot manifest. Those records retain their original non-admitting flags; current authority comes from the separate freshly verified v31 release.

Exact theorem nodes and inherited prerequisites