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

[mdumitrean]

PR: #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.