Unconditional simple-on-critical-line proportion for ζ raised to 0.6728005676 (kernel-checked) — see PR #17

PR: https://github.com/anthropics/formal-math/pull/17

This work extends the `zeta23/` project beyond the paper's Montgomery–Taylor endpoint
(0.672500703679) with fully formal, unconditional improvements of the proportion of
zeta zeros that are simple and on the critical line:

| A | bound | certificate |
|---|---|---|
| 1/80 | 0.672755620655 | 2,969 kernel-replayed modules |
| 51/4000 | 0.6727837118 | 8,953 |
| 257/20000 | 0.6727949489 | 30,153 |
| **129/10000** | **0.6728005676** | 56,924 |

- Method: a positive spectral penalty from six translates of the MT kernel, fed into the
zero-count ledger; the only numerical input per target is a 5D affine inequality
`A ≤ E₆(g) + B₆·Σg`, proved by `decide +kernel` replay of an exact rational
branch-and-bound certificate over a Lean-checked envelope of the kernel.
- Also included: the `Union` (simple-or-on-line) and `LineDecimal` (certified decimal
enclosure of the MT constant) comparator topics — 24 new Mathlib-only trusted statements
in total, all in the Palomar template layout.
- Every audited declaration depends only on `propext`, `Classical.choice`, `Quot.sound`;
no `native_decide`, floating point, or external oracle. Audits, independent exact
replays and build logs are in `zeta23/AUDIT.md` and `zeta23/certificates/sextuple/`.
- The method is near its ceiling: any catalog gives at most ≈ 0.6728111 with this kernel
(analysis in `zeta23/certificates/sextuple/a1290/`).

Note: the certificate chains are ≈100k kernel modules (≈430 CPU-hours), so CI cannot
rebuild them on a hosted runner; the committed logs are the record of those builds.