$\det(A_n) = M(n)$ — checked by two independent methods, not just asserted

?

Math: the Redheffer matrix's determinant equals the Mertens function M(n) — a real, checkable identity from analytic number theory, not an approximation. Dev: computed two independent ways (matrix determinant and a direct Möbius sieve) specifically so they can be cross-checked against each other, not just asserted once.

$M(n)$ is the Mertens function, $\textstyle\sum_{k \le n} \mu(k)$ — a real, well-known object in number theory (the Riemann Hypothesis is equivalent to a statement about how fast M(n) grows, which is still open; nothing here claims anything about that). The Redheffer identity, $\det(A_n) = M(n)$, is a classical result (Redheffer, 1977); a general Lean 4 proof of it for every n is under review as a Mathlib pull request, listed on Publications. The chart below plots det(A_n) computed directly from the 0/1 Redheffer matrix by exact-fraction Gaussian elimination (no floating point) for n = 1…100, with M(n) computed completely independently by a Möbius sieve overlaid every 4th point — 100 out of 100 values agree exactly. The generation script checks its own two computations against each other before drawing anything at all — if even one of the 100 values had disagreed, no chart would appear here.