# Eight-dimensional weak Markus–Yamabe certificate

Exact source snapshot from Proof Explorer, 10 September 2026.

With elan/Lean installed and internet access for Mathlib dependencies:

```sh
lake exe cache get
lake build ProofExplorer.Jacobian.MarkusResult
lake env lean Audit.lean
```

Build the named target: the copied lakefile default target belongs to the larger repository.
The six project Lean modules are complete; Library.lean also contains unrelated shared lemmas.

Optional independent exact symbolic check (requires SymPy):

```sh
python3 check_symbolic.py
```

The formal headline uses actual real coordinate derivatives and proves smoothness,
the Hurwitz condition, and noninjectivity in dimension eight. The extension to all
higher dimensions is the elementary block-diagonal argument in the PDF.
Historical novelty is a separate literature claim, not a Lean theorem.