# Scalar foundations for the spectral construction

*Original specialization proofs: OpenAI Codex (AI); CC0-1.0. Current source correspondence and reading presentation: GPT-6.1 Sol (OpenAI), Ultra, October 2026.*

The [spectral lesson](spectral-calculus-kernel.md) constructs the operator calculus from the following scalar inputs. Their primary proof route uses complete freely readable programme proofs in the Haar-measure and measure-tools lessons, with the topology support linked below. These are AI-authored human-readable proofs, with their original credits and CC0 terms retained. The previously checked mathlib proofs, pinned to commit 71a80585ee495fc24472fd0eaffc89d94e4fd8d6, remain formal-source comparisons and historical proof credits. The five arguments below prove the specializations used in that construction. They do not claim that the course itself has been formalized or compiled in Lean.

## Complete programme proof bodies

- Haar measure, Theorem 2.2 and Proposition 2.3 supplies the full six-step complex RMK proof and finite-Borel compact inner approximation; the exact source loci are lines 55–78 and 80–88.
- Measure tools, Theorem 1.1 proves Carathéodory's construction, source lines 16–30. Section 2 proves nonnegative integration, sequential MCT, countable integral sums, Fatou and real/complex sequential DCT, lines 36–69. Section 3 proves Hölder/Minkowski, scalar Lp completeness and simple density, lines 75–105. Its L2 pairing is already linear in the first entry.
- Topology support, Proposition 4.2(2), Theorem 5.1 and Corollary 5.2, source lines 130–171, supplies the compact cutoffs and partitions used in the RMK proof.

The download includes each complete unchanged reader and editable programme source, its required local assets and its authorship and licence notices. This is the exact selected proof route; unrelated theorem and navigation links in those full lessons can still require the online programme. The programme-proof record gives exact file hashes, original URLs and the retained component terms.

## Retained pinned mathlib proof comparisons

- [OPEN-SCALAR-RMK](https://github.com/leanprover-community/mathlib4/blob/71a80585ee495fc24472fd0eaffc89d94e4fd8d6/Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Real.lean) — For a locally compact Hausdorff X with its Borel sigma algebra and a positive real-linear functional on C_c(X,R), constructs a regular Borel measure realizing the functional. The measure is unique among regular measures. On compact X it is finite. Specialize C_c=C on a compact spectrum, apply integral_rieszMeasure to the constant one for total mass, and apply separately to real and imaginary parts for a complex positive functional.
- [OPEN-SCALAR-RMK-CONTENT](https://github.com/leanprover-community/mathlib4/blob/71a80585ee495fc24472fd0eaffc89d94e4fd8d6/Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean) — The nonnegative functional gives a finite content on compact subsets; the regular-content proof yields its regularity; the Riesz measure is the measure induced by this content.
- [OPEN-SCALAR-CONTENT-REGULAR](https://github.com/leanprover-community/mathlib4/blob/71a80585ee495fc24472fd0eaffc89d94e4fd8d6/Mathlib/MeasureTheory/Measure/Content.lean) — For a content on an R1 topological space with its Borel sigma algebra, the constructed Borel measure is outer regular and, on a weakly locally compact space, regular (finite on compacts and inner regular on open sets).
- [OPEN-SCALAR-REGULAR-BRIDGES](https://github.com/leanprover-community/mathlib4/blob/71a80585ee495fc24472fd0eaffc89d94e4fd8d6/Mathlib/MeasureTheory/Measure/Regular.lean) — Regular measure on an R1 space is weakly regular; outer regularity plus inner compact approximation on open sets gives inner compact approximation on finite measurable sets; for finite total measure this gives inner regularity on every measurable set.
- [OPEN-SCALAR-LP-COMPLETE](https://github.com/leanprover-community/mathlib4/blob/71a80585ee495fc24472fd0eaffc89d94e4fd8d6/Mathlib/MeasureTheory/Function/LpSpace/Complete.lean) — For every measure mu on every measurable space, complete seminormed additive codomain E and p>=1, Lp(E,p,mu) is complete; in particular L2(C,mu) is complete. Proof takes a controlled Cauchy sequence, proves summable a.e. norm increments, constructs the pointwise limit and proves convergence in Lp.
- [OPEN-SCALAR-L2-INNER](https://github.com/leanprover-community/mathlib4/blob/71a80585ee495fc24472fd0eaffc89d94e4fd8d6/Mathlib/MeasureTheory/Function/L2Space.lean) — For real or complex scalar field and any inner-product codomain E, L2 carries the integrated inner product, with its usual L2 norm. Combined with OPEN-SCALAR-LP-COMPLETE this makes scalar L2 a Hilbert space.
- [OPEN-SCALAR-MCT](https://github.com/leanprover-community/mathlib4/blob/71a80585ee495fc24472fd0eaffc89d94e4fd8d6/Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean) — For any measure and a pointwise monotone sequence of nonnegative extended-real measurable functions, integral of supremum equals supremum of integrals; also AE measurable/AE monotone version and convergence formulation.
- [OPEN-SCALAR-DCT-NONNEGATIVE](https://github.com/leanprover-community/mathlib4/blob/71a80585ee495fc24472fd0eaffc89d94e4fd8d6/Mathlib/MeasureTheory/Integral/Lebesgue/DominatedConvergence.lean) — For any measure, a sequence of nonnegative measurable (or AE measurable) functions dominated AE by one function of finite integral and converging AE has converging integrals. Apply to squared L2 error with integrable domination to prove norm convergence of cutoffs.

## OA-MOD-SPECTRAL-BRIDGE-RMK

For compact K, every continuous function has compact support: its closed support is a closed subset of a compact space. Thus C_c(K,R) and the course's C(K,R) are the same real vector space. For a unital *-representation rho, a nonnegative real continuous f has continuous square root h, and rho(f)=rho(h)*rho(h). Therefore the vector functional at xi is real and nonnegative on f and is real linear on real functions. Haar Theorem 2.2 is stated for a positive complex-linear functional. Given the positive real functional I_R required by SK-DEP-RMK, define I(u+iv)=I_R(u)+iI_R(v) for real u,v. The unique real/imaginary decomposition proves complex linearity, and positivity on nonnegative real functions is retained. Apply that full theorem to I and restrict the resulting integral identity to real functions. Conversely, its identities on real and imaginary parts give the identity for every complex continuous function. This establishes the exact real-to-complex correspondence without an additional representation theorem.

For a complex continuous f=u+iv with real continuous u,v, linearity gives the complex integral identity by applying the real identity separately to u and v. The constant one gives total mass equal to the squared norm of xi. This also proves finiteness without a separability hypothesis.

The meaning of “regular” is checked, not silently changed. Haar Theorem 2.2 gives outer regularity and compact inner regularity on open sets. Its full Proposition 2.3(1), source lines 80–88, gives compact inner approximation for finite Borel sets. The retained formal comparison in Measure/Regular.lean, including lines 582–603 and 1122–1123, independently records the corresponding finite-measure bridge. Every measurable set under the finite measure here has finite mass. Consequently for a Borel B and epsilon greater than zero there are compact F contained in B and open O containing B with mu(O minus F) less than epsilon. This is precisely the density argument's input.

SK-02 then constructs a continuous function between the compact and open sets by an explicit distance formula. Its L2 error from the indicator of B is controlled by mu(O minus F). Complex simple functions are approximated by linear combinations of these continuous functions. To approximate an arbitrary square-integrable measurable f by simple functions, first set it to zero on the tail where its modulus exceeds m, then round its real and imaginary parts on the bounded square to a grid of mesh 1/n. The rounding error is at most sqrt(2)/n pointwise, hence its L2 norm is at most sqrt(2 mu(K))/n. The squared integral of the omitted tail tends to zero by monotone convergence applied to the increasing truncated squared modulus. Choosing m and then n proves the density claimed in SK-02. This is the original compact-metric specialization; a separability assumption on H never appears.

## OA-MOD-SPECTRAL-BRIDGE-L2

Measure-tools Theorems 3.1–3.2 prove scalar L2 completeness and its inner-product structure for the given measure; source line 105 already uses the course's linear-first pairing. No convention change is needed on the primary programme route. For the retained pinned mathlib comparison, the source writes its inner product conjugate-linear in the first entry. If that source pairing is denoted by (f,g)_s, define the course pairing by <f,g>=(g,f)_s. It equals the integral of f times the conjugate of g, is linear in f, and has the same diagonal and norm. Hermitian symmetry, positivity and completeness therefore transfer without change of vectors, domains or norm. The source's completeness proof for arbitrary measures applies in particular to each finite mu_j.

The integral pairing is finite by scalar Cauchy–Schwarz. The primary programme proof is Hölder with p=q=2 in measure-tools Theorem 3.1. This can also be obtained from the Hilbert inner-product axioms recorded by the retained formal L2 instance: nonnegativity of the norm of f minus a scalar multiple of g yields the inequality, with g=0 treated directly.

The Hilbert direct sum over an arbitrary index set is handled separately. A summable family of squared norms has at most countable nonzero support because each set of terms exceeding 1/n is finite. Completeness follows by taking coordinate limits of a Cauchy sequence, controlling every finite squared-error sum by the same Cauchy estimate, and then taking the supremum over finite sets. The resulting norm limit belongs to the direct sum. This argument is written in SK-01 and SK-03. It neither replaces an arbitrary Hilbert space by a separable one nor applies DCT to an uncountable index net.

## OA-MOD-SPECTRAL-BRIDGE-MEASURE

For a fixed x with multiplication coordinates x_j, define its finite scalar measure explicitly by \(\mu_x(B)=\sum_j\int_B|x_j|^2\,d\mu_j\). Measure-tools Section 2, Theorem 2.1 supplies the countable nonnegative integral sum and MCT; Theorem 2.2 supplies the real/complex sequential DCT used below. Integrals of a nonnegative simple function against this measure are the sum of the corresponding integrals, by the definition on measurable sets. Increasing simple approximation and MCT extend that identity to every nonnegative measurable function. This proves the exact domain identity and every exchange between the coordinate sum and the squared integral in SK-04–05.

For a bounded sequence f_n converging pointwise to f, apply the exact nonnegative DCT to |f_n minus f| squared, dominated by four times C squared against the finite vector measure when |f_n| is at most C. For a vector-dependent majorant h, the dominator is four times h squared. The manuscript's formulas use these precise bounds. In particular, for imaginary powers the difference of two scalar unitaries has squared modulus at most four.

The parameter s tending to r in the imaginary-power argument belongs to the real line. Sequential dominated convergence proves sequential continuity, which equals continuity for a map from the metric real line into the Hilbert norm. The proof is not a claim of a general net version of DCT.

In the arbitrary-net operator-argument theorem SK-09, DCT is used only to choose one spectral cutoff for the limiting vector and its one finite measure. Convergence of that bounded continuous cutoff along the net was already proved using strong convergence of the Cayley operators and uniform polynomial approximation. The resulting tail estimate is eventual in the directed set and proves all bounded continuous functions. This distinction is necessary when the spectra of the approximating operators escape every bounded interval.

## OA-MOD-SPECTRAL-BRIDGE-BOREL-REPRESENTATIVE

The completed-measure convention does not change the constructed Hilbert spaces. Here is a direct proof. A set measurable for the completion differs from a Borel set by a subset of a Borel null set, by the definition of completion. Let f be a complex function measurable for the completion. Choose completion-measurable simple functions s_n converging pointwise to f, for example by truncation and grid rounding. Replace each of their finitely many level sets by a Borel representative. If those representatives overlap, use the same finite linear combination of their indicators; disjointness is not needed for it to be a Borel function. The resulting Borel function t_n equals s_n outside a Borel null set N_n.

The union N of all N_n is Borel and null. Define g to be the pointwise limit of t_n outside N and zero on N. On the complement of N that limit exists and equals f. The set on which a sequence of complex Borel functions converges is Borel, by the countable Cauchy criterion, and its limit is Borel. Thus g is Borel and equals f almost everywhere. Square integrals and inner products are unchanged by this replacement. The quotient L2 spaces for the Borel measure and its completion are consequently canonically the same.

## OA-MOD-SPECTRAL-BRIDGE-CFC-APPROXIMATION

The existing exact CFC import is an isometric isomorphism from C(spectrum(T)) onto C*(I,T), carrying the coordinate function to T. By definition the latter is the norm closure of unital *-polynomials in T,T*. Pulling that dense algebra back through the isometry proves uniform density of polynomials in z and its conjugate on the spectrum. No extra Stone–Weierstrass import is needed.

For SK-09, one needs this approximation on the whole scalar unit circle, even if the spectra of the Cayley transforms differ. The bilateral shift used there is unitary, and geometric series place its spectrum in that circle. The written finite geometric vectors have squared residual 2/(2N+1) at every unit scalar. Thus none of these scalars has a bounded inverse resolvent, proving that the spectrum is the whole circle. Apply the same existing CFC import to this auxiliary operator. Its countable-dimensional space is only a scalar-approximation witness; the convergence theorem's H remains arbitrary.

The retained mathlib proof components retain Apache-2.0. Human mathematical/formal-source credits from their pinned file headers are Yoh Tanimoto and Oliver Butterley (real RMK), Jesse Reimann and Kalle Kytölä (RMK content), F. van Doorn (contents), Sébastien Gouëzel, F. van Doorn and Yury Kudryashov (regular measures), Rémy Degenne and Sébastien Gouëzel (Lp completeness), Rémy Degenne (L2), Mario Carneiro and Johannes Hölzl (nonnegative integration and convergence), Heather Macbeth (continuous-function density), and Zhouhang Zhou, Yury Kudryashov, Patrick Massot and Louis (Yiyang) Liu (Bochner dominated convergence). The full programme providers retain their own AI credits and CC0 prose terms. The mathlib sources remain linked for research and formal-proof comparison; their code and comments are not included in this edition. The retained original lesson and specialization prose are CC0-1.0. Complete source/proof bindings give source hashes and proof ranges.