# Lean 4 / Mathlib formalization of the algebraic core of WP28

`src/WP28Algebra.lean` (mirrored in the Lake project `wp28proofs/Wp28proofs/WP28Algebra.lean`) contains 27 machine-checked
statements, with no `sorry`, covering the deterministic parts of the proofs:

| Paper item | Lean theorems |
|---|---|
| Vandermonde constraints (eq. 4) for (1,2), (1,2,4), (1,2,4,8), (1,2,3); β_r and A_r (Table 2) | `vandermonde_12/124/1248/123`, `beta_2/3/4`, `beta_3_pattern123`, `amp_2/3` |
| Theorem 2(ii): exact biases of J₂, J₃ | `exact_bias_J2`, `exact_bias_J3` |
| Theorem 2(iv): Newton map, error identity, q-fold identity | `newton_map`, `newton_error`, `newtonErr_closed` |
| Theorem 2(iv): basin of attraction (convergence iff \|u\| < 1) | `basinIter_abs`, `basin_converges`, `basin_diverges` |
| Theorem 2(v): boundary constant algebra −θ₀(βc^r)^{2^q} | `boundary_constant` |
| Theorem 1 proof: exponent algebra of the frontier (√N m^{−r2^q} = 1 at α(r,q); negative power below) | `frontier_exponent`, `frontier_below` |
| Theorem 2(i): Gamma inverse moments from Γ(s+1) = sΓ(s); E R_n, E R_n², Var θ̂_n | `gamma_inv_moment1/2`, `exponential_remainder_moments` |
| Theorem 2(iii): Beta inverse moments as Gamma ratios; exact Var J₂ and E J₂ | `beta_inverse_moments`, `var_J2_exact`, `mean_J2_exact` |

Not formalized (and not claimed to be): the probabilistic statements (O_p bounds, Lemmas 3–7, the CLT/Slutsky steps of Theorems 1–3),
which depend on measure-theoretic infrastructure beyond the scope of this check; they are verified by SymPy (`theory/symbolic_checks.py`)
and by the Monte Carlo evidence.

## Reproduce
```bash
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y   # once
cd theory/lean/wp28proofs && lake exe cache get && lake build      # Lean 4 v4.35.0, Mathlib master (lake-manifest.json)
```
`lake build` must end with `Build completed successfully` and no `sorry` warnings (`bash scripts/check_lean.sh`).