D. Structured transforms and clipped precision

This chapter retains the substantive mathematical pages of verification block 4 (v0.4.0). Its dated audit and pending-status passages describe that historical checkpoint; the final status is 56 of 56 registered finite items under the recorded hypotheses. Later chapters supersede earlier pending statements. All compiler and regression counts in this chapter are inherited records, not fresh runs for this edition.

Permalink · Source line 2

Source item 4.3; module CirculantFourier Let \(n>0\), with coordinates indexed by \(\mathbb Z/n\mathbb Z\). Define the actual circulant by

The formal Fourier matrix is

The standard character is not left abstract: a checked theorem identifies these entries with

The value representatives enter only this explicit exponential formula. All modular algebra uses the residue classes themselves.

Normalization and inversion. The proof identifies matrix application with the ordinary counting-measure discrete Fourier transform:

It separately identifies \(F^*x\) with the appropriately scaled inverse transform. Mathlib's checked Fourier inversion theorem and the proved scalar normalization yield both identities

No unitarity assumption is inserted.

Convolution and reconstruction. An explicit bijective change of index proves

This gives the matrix intertwining relation \(FC(c)=\operatorname{diag}(\operatorname{DFT}c)F\). Multiplication by the proved inverse reconstructs the circulant:

The two-transform application formula is also checked for every input vector. The result includes \(n=1\) and arbitrary complex coefficients. Hermiticity is not required.

Claim boundary. This verifies the exact Fourier representation, not an \(O(n\log n)\) implementation of the transform. The latter is an additional algorithmic factorization of the same linear map.

Permalink · Source line 4

Source items 4.4 and 4.5 Toeplitz embedding. For \(n>0\), define

The diagonal is supplied by \(c_0\); the coordinate \(r_0\) is unused. The constructed generator of length \(2n\) is

and the padding map is the actual finite-index sum eliminator that appends \(n\) zeros.

Lean first proves the upper-left block identity

For \(j\le i\), finite modular subtraction has its ordinary value \(i-j\). For \(i<j\), it has wrapped value \(2n+i-j\), whose reversed generator coordinate is \(j-i\). Both branches are checked with the actual finite-index arithmetic.

Splitting the product sum into the original and padded halves then gives

The generator's first half and its middle zero are checked separately. Neither symmetry nor conjugation is involved.

Kronecker application. For \(A\in{\mathbb C}^{m\times m}\), \(B\in{\mathbb C}^{n\times n}\) and \(X\in{\mathbb C}^{n\times m}\), Lean proves

The formal vectorization is explicitly column-major: its pair coordinate \((j,i)\) stores \(X_{ij}\). The right factor is the ordinary transpose, not the conjugate transpose. This distinction is essential over \({\mathbb C}\).

Finite types of multiplication/accumulation events and stored scalar addresses give

The explicit Kronecker matrix has \(n^2m^2\) entries. As in the manuscript, the operation model assigns two scalar operations to each multiply-accumulate term.

Permalink · Source line 46

Source item 4.6; module StructuredTensor Let \(A_0,\ldots,A_{k-1}\) be square factors of order \(d\). Tensor coordinates are represented by a nested product of \(k\) copies of \(\{0,\ldots,d-1\}\). The empty product is a singleton. Lean proves that the coordinate type has cardinality \(d^k\).

The represented matrix is defined recursively using the actual Kronecker product:

The algorithm is defined independently. On each slice with fixed first coordinate, it recursively contracts the trailing modes. It then applies \(A_0\) to the resulting first-coordinate fibers:

Induction, the Kronecker entry formula, and finite-sum distributivity prove

Thus correctness is not inferred merely from agreeing dimension or storage formulas.

Operation events. The event type for \(k+1\) modes is a disjoint union of \(d\) copies of the trailing event type and the events for the final fiber contraction. Its cardinality obeys

Lean proves the closed form

The factor-address type has cardinality

These statements include \(k=0\) and \(d=0\). With no factors, the action is the identity on the singleton coordinate type and incurs zero modeled arithmetic. With \(d=0\) and at least one factor, the coordinate type is empty.

Implementation boundary. These are recursive mathematical contractions with exact complex arithmetic. The event model assumes each intermediate slice is computed once and reused. It is not an instrumented execution trace or a cost bound for every evaluator of the raw functional definition. The count excludes indexing, allocation, data movement, fused instruction effects, and the real-operation cost of a complex scalar operation. Those require a separately declared backend model.

Permalink · Source line 87

Source item 4.7; module WalshTransform The two-point matrix is constructed as

and the full family is defined by \(H_1=[1]\) and

The two-point orthogonality identity is checked explicitly. Kronecker multiplication and induction then prove

The ordinary transpose is sufficient because all constructed entries are real, even though the scalar field is \({\mathbb C}\).

Actual butterfly. For the two halves \(x_0,x_1\) of the input, the independently defined procedure returns

Lean proves that this vector equals \(H_{2N}x\). The argument expands the two first-coordinate cases and applies finite-sum distributivity. It does not assume that the recursive algorithm already represents the matrix.

Exact arithmetic count. Each pair of slices forms one sum and one difference at every trailing coordinate. The event type therefore gives

The closed form and its logarithmic re-expression are both checked:

The logarithm in the formal count is the natural-number binary logarithm, with its power-of-two identity proved by Mathlib. The case \(N=1\) has zero arithmetic events.

A further action theorem gives

which identifies the inverse after division by the nonzero scalar \(N\). This result concerns exact arithmetic, not floating-point error accumulation through a butterfly implementation.

Permalink · Source line 123

Source item 8.5; module ClippedPrecision Let \(E\) be a finite nonempty set and suppose

The feasible set is

and the objective is the same logarithmic objective used in item 8.4:

Strictly positive caps are stated explicitly. A zero or negative cap cannot admit a positive tolerance at that coordinate.

Constructive parameterization. Write \(t=1/\lambda\) and set

Lean proves that \(\Phi\) is continuous and nondecreasing, with \(\Phi(0)=0\). At the finite positive scale

every coordinate is saturated, so \(u(T)=m\) and \(\Phi(T)=\sum_es_em_e\). The intermediate value theorem produces \(t>0\) with \(\Phi(t)=\tau\). The multiplier is not assumed to exist.

Strictness below saturation. If \(t<u\) and \(\Phi(t)\) is below the maximum, at least one coordinate is unsaturated at \(t\). That coordinate strictly increases; every other coordinate is nondecreasing. Hence \(\Phi(t)<\Phi(u)\). This proves uniqueness of the scale and, by reciprocation, the exact manuscript statement

when \(0<\tau<\sum_es_em_e\).

At the maximal budget, the minimizing vector remains unique but the multiplier need not be. The one-coordinate case \(s=c=m=1\) is checked: both \(\lambda=1\) and \(\lambda=1/2\) produce the same tolerance \(1\).

Permalink · Source line 165

Source item 8.5, continued Existence of a multiplier alone does not prove optimality. The formal proof supplies a global supporting inequality, rather than invoking an assumed Karush–Kuhn–Tucker optimality oracle.

Fix the feasible vector \(u=u(t)\) obtained above and any feasible competitor \(\varepsilon\). For each coordinate, Lean proves

When \(u_e=tc_e/s_e\), this is equality. When \(u_e=m_e\), the capped condition implies \(s_e/t\le c_e/m_e\), while \(\varepsilon_e-m_e\le0\). Multiplying by this nonpositive difference gives the required inequality in the correct direction.

The equal-budget constraint then yields

Applying the checked inequality \(\log z\le z-1\) for \(z>0\) gives

Since

we obtain \(J(u)\le J(\varepsilon)\) for every feasible competitor.

If \(\varepsilon\ne u\), one coordinate has ratio different from \(1\). The logarithmic inequality is strict there, and its positive weight preserves strictness in the sum. Consequently,

This proves the unique global minimizing vector for every positive feasible budget, including the maximal endpoint.

Numerical boundary. Existence uses real continuity and the intermediate value theorem. This is a mathematical construction, not an executable floating-point multiplier search with a certified stopping tolerance. The companion exact-rational water-filling routine is an independent regression mirror and is not itself the compiled Lean construction.

Permalink · Source line 203

Cumulative release evidence Lean verification. All 23 modules were rebuilt in a fresh output directory under Lean 4.34.0-rc2 and Mathlib revision aeb72f1e9981b6d35b426b16dca7759be3e7ba06. Every final module returned exit code zero, with warnings treated as errors. The 247 theorem audits and 22 construction audits used only propext, Classical.choice, and Quot.sound, or subsets thereof. Active proof sources contain no admitted proofs or added axioms. The false-equality and admitted-proof negative controls were rejected. All 17 verifier regression tests passed.

Development failures. Of 20 captured development checks in this block, 12 failed and eight passed. Failures included incomplete development lemmas, import visibility, finite-index instance reduction, and warning diagnostics. Failed source snapshots and compiler logs are retained separately from the successful fresh cumulative run. The first request for interactive runtime recovery was unsupported; noninteractive archive assembly and extraction succeeded, with every part hash and the combined hash verified.

Independent regressions. The Python mirrors passed 180 exact-rational Kronecker cases, 120 tensor cases, 96 Walsh cases, 240 Toeplitz cases, and 600 clipped-allocation cases. The latter include 60 maximal-budget cases and 1,800 rejected infeasible budgets. These are finite checks, not additional universal theorems or executions of the Lean definitions.

A separate complex128 Fourier regression covered 96 cases at lengths 1 through 24. Maximum absolute errors were approximately \(3.34\times10^{-14}\) for diagonalization, \(2.98\times10^{-15}\) for unitarity, and \(2.04\times10^{-13}\) for application, all below the declared \(10^{-10}\) threshold. These numerical checks are not substituted for the symbolic Lean proof.

Ten manuscript-proved items remain:

Permalink · Source line 241

Four classical inputs remain separately recorded. This release does not rerun the original numerical corpus or GPU benchmarks, rebuild Papers I–VII in full, or independently recheck every imported Mathlib proof.

Permalink · Source line 266