A. Exact semantics, support, and low-rank identities

This chapter retains the substantive mathematical pages of verification block 1 (v0.1.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 items 2.3, 2.5, and 2.6 Let \(R\) be a ring, \(I\) a finite index type, and \((P_a)_{a\in I}\) a family satisfying

Write \(A_{ba}=P_bAP_a\) and let \(E_A=\{(b,a):A_{ba}\ne0\}\). These are exact algebraic zeros, not values discarded by a floating-point threshold.

Reconstruction and action. The checked finite sum is

The proof inserts the complete projector sum on both sides and removes only zero summands. Applying this identity to an arbitrary module gives exact action. A separate finite-matrix theorem establishes

for every rectangular batch of right-hand sides \(Z\).

Composition. Inserting the projector identity between factors yields

If the left side is nonzero, at least one intermediate \(c\) has both \(A_{bc}\ne0\) and \(B_{ca}\ne0\). Consequently \({\operatorname{supp}}(AB)\subseteq{\operatorname{supp}}(A)\circ{\operatorname{supp}}(B)\). No equality of supports is asserted.

Adjoint and tensor products. With an involution and self-adjoint projectors, the formalization proves

For actual finite matrices and actual Kronecker products, it proves

The self-adjointness hypothesis is explicit in the adjoint theorem. The tensor theorem is not a statement about an uninterpreted tensor symbol.

Concrete coordinates. Given any tag map from finite scalar coordinates to packet addresses, coordinatePackets constructs diagonal zero-one matrices. Their orthogonality and completeness are proved. The construction allows unequal packet sizes and unused packet addresses. Its action is checked entrywise: it retains exactly the coordinates carrying the selected tag.

The underlying ring-valued projector calculus is imported from the unchanged, freshly recompiled Paper VII foundation. Reuse is recorded separately from the new Paper VIII declarations.

Permalink · Source line 4

Source items 6.1, 6.2, and 6.3 A path of length \(n\) in the Lean predicate TransferPath is a directed walk: vertices may repeat. This is the notion required by matrix powers. At length zero the endpoints coincide. At length \(n+1\), a nonzero last block is appended to a length-\(n\) walk.

Define the active contribution sum recursively by

The checked identity is

Its proof is induction using the exact composition theorem, not an assumed support recurrence. When no active walk exists, the corresponding contribution sum is zero, and hence the actual block of \(A^n\) vanishes.

Nilpotence certificate. If no walk of length \(h+1\) exists between any pair of packets, then

Every block vanishes, and reconstruction forces the whole operator to vanish. A second theorem derives the required absence of walks from a supplied level map

It proves that a length-\(n\) walk increases the level by at least \(n\). This certifies the acyclic case with a bounded height. This block does not implement or verify an algorithm that constructs a topological ordering or computes the longest path.

Polynomial support. For the actual finite sum

the checked support lies in the union of the support relations of the powers. The formalization treats the \(j=0\) contribution explicitly, so the constant term is not accidentally omitted.

Cancellation control. Lean verifies the rational example

The coordinate block \(A_{00}\) is nonzero, and a length-two active walk from zero to zero exists. Nevertheless the corresponding block of \(A^2\) is zero. This is an exact counterexample to replacing support inclusion by equality.

Permalink · Source line 45

Source items 5.1, 5.3, and 5.4 Let \(A=D_A+U_AV_A^*\) and \(B=D_B+U_BV_B^*\) have rectangular factor widths \(r_A\) and \(r_B\). The formalization constructs

and proves

These are actual concatenated matrices with \(r_B+r_A\) columns. Expanding the product and grouping the terms with common right factors proves the identity. The separate rank theorem establishes

It bounds actual matrix rank, not just the number of stored columns. Packet diagonality of \(D_AD_B\) follows from diagonality of both factors and the checked block-composition formula.

Woodbury. For \(D\) and

both invertible, Lean checks the ordinary matrix inverse formula

The proof specializes Mathlib's classical Woodbury identity. A separate theorem derives invertibility of \(D+UV^*\) from the two stated assumptions. A further theorem verifies that multiplying the proposed inverse by any batch \(Z\) solves the updated system. Invertibility of the update is not inserted as an extra premise.

Norm bound. Over the real or complex scalars, all matrix norms in the following theorem are Hilbert-space operator norms, including the rectangular factors:

After the checked inverse identity, the proof uses the triangle inequality and two rectangular operator-norm product bounds.

Not covered here. The arbitrary product-chain rank corollary, optimal small-core recompression, singular-value approximation theorem, chain perturbation bounds, and numerical stability of a particular solve implementation are not marked complete by these results. Algebraic representability is not a GPU execution-time guarantee.

Permalink · Source line 84

Source item 8.1 and two uniform consequences Let \(X\) be a normed space over a nontrivially normed field. The formal objects are actual continuous linear maps \(X\to X\), with their operator norm. Let \(a(e)\) identify the source packet of edge \(e\), and suppose

Set

The exact operator and vector identities are proved first:

Applying the finite triangle inequality and the defining operator-norm estimate gives

If \({\left\lVert\Delta_e\right\rVert}\le\varepsilon_e{\left\lVert A_e\right\rVert}\), then the formal relative certificate is

The source additionally assumes that each exact block is source supported. The proof of this bound does not need that assumption. The checked statement therefore uses weaker sufficient hypotheses without weakening the conclusion.

Uniform operator estimates. Two additional checked consequences are

and, when \({\left\lVert P_a\right\rVert}\le1\) for every packet,

These estimates are uniform in the input vector and can be used as inputs to later chain analyses. The chain results themselves are not included in this block's completed inventory.

Implementation boundary. The maps \(\Delta_e\) and their bounds must be supplied or justified for a numerical implementation. This formalization does not establish IEEE rounding behavior, prevent overflow or underflow, model a CUDA kernel, or certify the recorded device speedups. Those are distinct claims and require separate evidence.

Permalink · Source line 125

Boundary audit for item 8.4; evidence for this release Positive budget is necessary. The source minimizes

with positive sensitivities and costs, but it does not explicitly impose \(\tau>0\). For a nonempty edge set, Lean proves

It follows that every nonpositive budget is infeasible. A one-edge, unit-sensitivity, zero-budget instance is checked as an exact boundary example.

The amended nonempty-index statement should require \(\tau>0\). Nonemptiness also makes the sum of positive costs in the displayed optimizer's denominator positive. The empty edge set should be treated separately. Existence, optimality, and uniqueness of the corrected optimizer are not proved in this release. Item 8.4 remains boundary-audit-only.

Fresh Lean run. All six modules completed with exit code zero under Lean 4.34.0-rc2 and Mathlib revision aeb72f1e9981b6d35b426b16dca7759be3e7ba06.

All 60 theorem-level audits and the separate coordinate-projector construction audit use only propext, Classical.choice, and Quot.sound. Warnings were treated as errors. The deliberately false equality and the deliberate admitted-proof placeholder were both rejected. All 17 verifier regression tests passed.

Failures are retained. Nine of the 15 captured development checks failed before correction. Their snapshots and compiler logs remain separate from the active modules and the successful final run. The initial long runtime-extraction command was also interrupted by the host limit. A second extraction completed, and the final run verified the restored runtime and dependency pins.

Reproducibility. The release includes exact sources, module-level commands, source and compiled-artifact hashes, axiom logs, the complete source-result coverage ledger, and a checkpointed verifier. The original CPU suite passed 37,392 checks. It does not reproduce GPU timings.

Remaining scope. Forty-six manuscript-proved items remain not fully covered, plus four separately tracked classical inputs. Mathlib's imported proofs were not independently rechecked, and earlier papers were not rebuilt in full. The next work can build on these semantics to address the cost models, compiler, recompression, and numerical-analysis statements without treating empirical performance as a theorem.

Permalink · Source line 170