# Verification of the kernel penalty theorem

The analytical proof has been accepted after detailed originating-researcher
self-audit. It covers arbitrary closed-range synthesis operators with fixed
coefficient indexing, all partial-isometry competitors, finite exponent
p >= 1, and penalty kappa >= 1. The sharpness examples use nonzero competing
frames. A common rational rotation avoids zero individual frame vectors.

The projection-gap lemma uses invertibility of PQP on the initial space and
a minimizing sequence for the reduced minimum modulus. It does not assume
that spectral extrema are eigenvalues. Strictness is checked separately for
gap less than one and gap equal to one, including the threshold kappa=1.
The contraction-and-defect parametrization is proved in both directions.
The uniqueness proof uses spectral projections and explicitly requires the
complex field. The subspace tilt does not assume its chosen vector is an
eigenvector. A real counterexample, an infinite-dimensional nonsurjective
isometry, and a maximum-metric example record the relevant boundaries.

The unchanged standard-library checker uses fractions and certified rational
enclosures of square roots. It checks 63 rectangular synthesis operators
against 57 rational partial isometries and three penalty values: 10,773
metric comparisons, 228 exact ties, 2,072 common-kernel error identities,
900 small-penalty counterexamples, and eight explicit boundary checks.
The principal metric comparisons use p=2; the small-penalty checks cover
integer p from 1 through 9. Normal and optimized runs agree. These finite
diagnostics do not establish the universal theorem, novelty, or independent
verification. The general result rests on the written proof.

The desktop editor compiler and a separate local Tectonic build both
succeeded. All six PDF pages were opened and visually inspected. Equations,
references, page numbers and the author footnote are legible, with no
clipping, overlapping text, undefined references or overfull boxes. The
portable archive build and checker replays are recorded in build_record.json;
its hashes bind the inspected PDF, source and package contents.

The original proof and source acceptance record remain immutable. Their
historical status-file hash predates acceptance registration and is retained
as history, not confused with the current status. The final manuscript
specifies the topology obstruction on C^2 before embedding it into larger
spaces, states the exact projection-gap limit of the range tilt, and
includes the real-field boundary already checked in the proof audit.

Known metric, norm-optimality and phase ingredients are credited. The
targeted literature audit does not certify absolute novelty. No independent
review or proof-assistant verification occurred. No remote draft, DOI,
upload, website mutation or Hugging Face post occurred for this package.