B Formalization and theorem correspondence
On this page · Permalink · Source line 1
The formal companion covers exact finite Gram algebra, disjoint block refinement, reindexing, streamed actions, nonnegativity, coefficient order, and arithmetic consequences of supplied enclosures. It does not establish the Gaussian reduction, Fourier inversion, analytic remainders, spectral post-verification algorithm, or transcendental interval-library correctness. A theorem that assumes an enclosure does not construct that enclosure.
Scope
Recorded kernel evidence. The retained compiler record accepts 26 theorem declarations and 8 definitions, with a 34-declaration axiom audit. The audited dependencies are confined to propext, Classical.choice, and Quot.sound. No sorryAx or custom axiom appears. A valid arithmetic control was accepted, while false arithmetic and an acceptance proof missing its error-budget premise were rejected. This volume preserves that evidence and the pinned sources. It does not claim a new Lean compilation.
B.1 How the formal model represents the engine
On this page · Permalink · Source line 21
The factor has a finite sample index type \(I\) and an arbitrary variant index type \(V\). A variant block is a finite set \(s\subseteq V\). The factor entries are exact real numbers, \(A:I\times V\to{\mathbb R}\). The Lean type is Row -> Variant -> Real. The sample coordinates carry a Fintype instance. The variants carry a DecidableEq instance to support finite-set unions, singleton blocks, and reindexing.
The residualized weighted factor in the main text is
For this companion, \(A\) is supplied. Proving that a particular floating-point residualization procedure computes that mathematical factor would require additional implementation and numerical-error reasoning. These modules do not assume a covariance model or a distribution for the vector \(v\).
There are five central finite-algebra definitions:
The source uses ordinary finite sums in \({\mathbb R}\). The factor convention is the sample Gram \(AA^\top\), matching stream_sample_gram. It is not the dual Gram \(A^\top A\). The case-study statistic \(Q=\tfrac12 v^\top Kv\) requires the additional scalar factor \(\tfrac12\) when applying these identities.
B.2 Exact block refinement
On this page · Permalink · Source line 52
The principal refinement theorem is gramEntry_union. Its hypotheses are finite sets \(s,t\subseteq V\) and \(\operatorname{Disjoint}(s,t)\). It proves, for all sample coordinates \(i,j\),
Disjointness prevents repeated columns from being counted twice. It is a mathematical condition, not a performance assumption. The theorem applies to empty blocks and zero factors. It does not require positive weights, since \(A\) is already supplied as a real factor.
The proof unfolds gramEntry and invokes the finite-sum union identity. No numerical approximation is involved. Repeated application establishes invariance along any explicitly checked sequence of binary disjoint splits. The source does not encode a whole scheduler or its memory allocation policy. A scheduler correctness proof would additionally track complete coverage, disjointness, and termination at every split.
The same refinement has formal consequences for the operator action and the quadratic statistic:
These are matrixAction_gram_union and quadraticForm_gram_union. The independent streamedAction_union proves the corresponding streamed accumulation identity directly.
The reindexing theorem gramEntry_reindex handles a bijection \(e:V\simeq V\). It moves the block to \(e(s)\) and transforms the factor to \(A'_{ik}=A_{i,e^{-1}(k)}\). The resulting Gram entry is unchanged. Permuting only the coordinates without moving their factor columns falls outside this statement.
B.3 Streamed actions and the sum-of-squares identity
On this page · Permalink · Source line 90
matrixAction_gram_eq_streamed proves
This is the exact algebra behind multiplication by a sample Gram matrix without constructing that matrix. Lean checks the finite-sum interchange and associativity of real multiplication. It does not assert that a given sequence of device operations has exact real semantics.
The next theorem, quadraticForm_gram_eq_energy, proves
It expands the action, interchanges the finite sums, factors each coordinate sum, and identifies the product of a projection with itself. The resulting quadraticForm_gram_nonneg states \(0\le v^\top K_s v\) for every real vector \(v\). This is positive semidefiniteness of the supplied Gram form.
These identities are useful together. Refinement preserves the represented operator, streaming preserves its action, and the energy identity verifies its positivity. They do not require the eigenvalues or the spectral theorem. The full engine subsequently uses numerical rank compression and spectral information, whose correctness contracts are separate.
B.4 A complete exact algebra example
On this page · Permalink · Source line 117
Consider one sample coordinate and two variant columns with
The two singleton Gram contributions are \(9\) and \(16\). Their disjoint union has Gram entry \(25\). Matrix multiplication gives \(Kv=50\) and \(v^\top Kv=100\). The streamed action instead computes
The energy expression gives
Thus the engine statistic with the stated half normalization is \(Q=50\). All paths are exact real identities. This example explains the type and normalization choices. The universal theorems establish them for arbitrary finite sample coordinates and variant blocks.
If the two blocks overlap in one column, their sum repeats that column's outer product. For \(s=t=\{1\}\) and \(A_{i1}=3\), the union has contribution \(9\) while the sum of the two blocks is \(18\). This is why gramEntry_union requires disjointness.
B.5 Supplied coefficient intervals
On this page · Permalink · Source line 143
The separate definition
models a supplied diagonal quadratic form. Its coefficients need not be eigenvalues obtained by a proved diagonalization. It has three theorems:
weightedSquares_mono: if \(l_k\le u_k\) for every \(k\in s\), then \(\sum l_kz_k^2\le\sum u_kz_k^2\).weightedSquares_nonneg: if \(c_k\ge0\) for every \(k\in s\), then \(\sum c_kz_k^2\ge0\).weightedSquares_tail_imp: coefficientwise order gives the pointwise implication \(q\le\sum l_kz_k^2\Rightarrow q\le\sum u_kz_k^2\).
The first and third allow signed coefficients because squares remain nonnegative. The second has an explicit nonnegativity hypothesis.
The pointwise implication is a prerequisite for probabilistic tail sandwiching. It does not itself state a probability inequality or build a coupling. To turn it into such a statement, one must supply measurable random coordinates on a common probability space and use monotonicity of measure. To apply it to matrix spectra, one must also establish that each true coefficient lies inside the supplied interval.
B.6 Enclosures and error ledgers
On this page · Permalink · Source line 169
The interval module uses two elementary predicates:
The equivalence errorBound_iff_enclosed proves
There is no extra nonnegativity hypothesis: if this predicate holds, then the radius is necessarily nonnegative. The definition accepts arbitrary real inputs, and the theorem states the exact logical equivalence.
For the K-COS error ledger, distinguish the ideal analytic quantity \(x\), an exact finite transform \(m\), and the computed estimate \(\widehat x\). If
then errorBound_compose proves
The proof is the triangle inequality. The hypotheses must be proved independently. In particular, \(a\) can contain a support/alias bound and an omitted-mode bound. This theorem only composes those supplied facts.
errorBound_accept adds the hypothesis \(a+b\le\varepsilon\) and concludes \(|x-\widehat x|\le\varepsilon\). This is the arithmetic core of acceptance by a proved budget. A sequence of numerically stable estimates, without valid bounds, does not satisfy its hypotheses.
B.7 Safe transformations of an enclosure
On this page · Permalink · Source line 205
The remaining interval statements are reusable exact-real rules. enclosed_add adds two enclosed quantities. enclosed_scale scales the interval by a nonnegative real factor. enclosed_widen permits an explicitly wider interval. enclosed_intersect combines two independently valid enclosures of the same quantity using \(\max\) on the lower endpoints and \(\min\) on the upper endpoints.
enclosed_positive requires a strictly positive lower endpoint. It then proves that the enclosed quantity is positive. This is relevant before applying a logarithm to a corrected tilted finite sum. A lower endpoint equal to zero does not establish positivity.
Finally, enclosed_monotone transports an interval through a supplied monotone function. Its hypothesis is global monotonicity on \({\mathbb R}\). The source does not directly instantiate this rule with the real logarithm, which needs a positive-domain formulation. A log-tail certificate therefore still needs both positivity and a separate domain-correct monotonicity argument. The interval-library implementation also requires its own correctness contract.
B.8 Declaration inventory and theorem correspondence
On this page · Permalink · Source line 227
All names below are prefixed by KomorebiQCOS. The inventory counts project theorems only. Imported mathlib theorems are not counted.
| Declaration | Exact formal scope |
|---|---|
gramEntry_empty | Empty variant block gives zero. |
gramEntry_singleton | One column gives its outer product. |
gramEntry_symm | Real Gram entry symmetry. |
gramEntry_union | Disjoint binary block refinement. |
gramEntry_reindex | Factor-column permutation invariance. |
matrixAction_gram_eq_streamed | Gram action equals streamed factor action. |
matrixAction_add | Operator-action additivity. |
matrixAction_gram_union | Action refinement invariance. |
streamedAction_union | Streamed accumulation over disjoint blocks. |
quadraticForm_add | Quadratic-form additivity in the matrix. |
quadraticForm_gram_eq_energy | Gram form equals factor energy. |
quadraticForm_gram_nonneg | Positivity of the supplied Gram form. |
quadraticForm_gram_union | Statistic refinement invariance. |
weightedSquares_mono | Pointwise coefficientwise order. |
weightedSquares_nonneg | Positivity for nonnegative coefficients. |
weightedSquares_tail_imp | Pointwise tail-event implication. |
enclosed_order | A valid enclosure has ordered endpoints. |
enclosed_add | Additive interval composition. |
enclosed_scale | Nonnegative scaling. |
enclosed_widen | Valid interval widening. |
enclosed_intersect | Intersection of valid enclosures. |
errorBound_iff_enclosed | Absolute-error/enclosure equivalence. |
errorBound_compose | Analytic and arithmetic budget composition. |
errorBound_accept | Acceptance below a supplied tolerance. |
enclosed_positive | Positive lower endpoint proves positivity. |
enclosed_monotone | Supplied monotone transformation. |
The exact-block, hierarchical-blocking, and streamed-action sections of the main text map to the Gram theorems under the definitions above. The error-ledger and acceptance sections map only to the arithmetic consequences of already valid bounds. The matrix-to-tail bridge maps to pointwise coefficient order only. The detailed machine-readable concordance includes source filenames and implementation anchors.
B.9 Reproduction and trusted dependencies
On this page · Permalink · Source line 272
The companion includes the pinned toolchain and dependency manifest, two mathematical modules, a root import, an axiom audit, controls, and retained build logs. From the companion directory, run:
lake exe cache get
lake build
lake env lean AxiomAudit.leanReproduction requires the pinned compiler and dependencies. Compiler binaries and the mathlib cache are not distributed in this package. The retained runtime record includes an executable-location adapter and its source. It did not modify the compiler or proof kernel.
The positive and negative controls supplement the theorem build. The axiom audit records each declaration's dependencies. Classical choice, propositional extensionality, and quotient soundness are the reported foundational dependencies. Any sorryAx occurrence would indicate an admitted proof. A clean admission scan alone does not establish acceptance. The retained compiler logs and axiom output provide that evidence.
B.10 Remaining formal obligations
On this page · Permalink · Source line 294
An end-to-end formal certificate would also require:
Gaussian whitening and central, signed, and noncentral reductions under their exact hypotheses.
Spectral decomposition and a proved connection between the input matrix, its factor, and coefficient intervals.
Probability monotonicity under a common measurable coupling.
Exponential tilting and the transform/payoff inversion identity.
Support, alias, and omitted-mode bounds with their rank and moment-generating-function domain conditions.
Exact interval semantics for input literals, directed rounding, roots, complex transforms, logarithms, and transcendental operations.
A verified implementation-to-bound correspondence, including input parsing and output endpoint conversion.
These are separate obligations. The retained checks establish the finite algebra and enclosure arithmetic listed in the inventory, not the additional analytic or numerical layers.