# Reproducing the new supporting theorem

Copy the included `source/` subtree to a working directory. With the pinned Lean/Mathlib dependencies available, run:

```sh
lake build OrchardMath.Millennium.HardyRecurrenceAudit
lake env lean OrchardMath/Millennium/HardyRecurrenceAudit.lean
```

Both the delivered theorem and explicit external restatement should list only `propext`, `Classical.choice` and `Quot.sound`. See the [retained output](source/research/millennium/iterations/0030/lean-audit.log).

The coordinator's accepted run rebuilt these sources with the existing pinned dependency installation. No clean dependency-download experiment is claimed. The [original reproduction guide](REPRODUCE.md) describes dependency setup, the earlier sign-identity target and the finite comparisons; all its files remain included unchanged.

The new theorem assumes the recurrence and nonnegative weights. A successful compilation does not identify the actual rational series or prove the full Hardy theorem.