Earlier proofs for the foundational readings

The results used here are proved in these lessons or earlier programme lessons. A paper citation is a source for writing a proof, rather than a substitute for that proof. The linked sections below specify the mathematical input and its hypotheses.

Bounded Hilbert spaces and continuous calculus

BK01 links the full Hilbert-space proofs HS01–03, continuous functional calculus Theorem 5.1 and positivity/square-root results in Section 8 of the earlier foundation course. BK then proves its bounded operator results, retaining arbitrary Hilbert spaces and nets.

Concrete-predual foundations and their exact proof inputs

CP01–14 proves the concrete projective-tensor and quotient duality on arbitrary complex Hilbert spaces. Its exact external Hilbert contracts are HS Theorem 2.3, Theorem 3.1 and Corollary 3.2. HB Theorems 2.1–2.2 and Corollary 2.3 prove real and complex norm-preserving extension on arbitrary normed spaces and subspaces; no completeness or closedness is required. HB Section 6 proves strict real locally convex separation; CP10 explicitly includes the empty convex-set case. BK03–04 supply the already proved arbitrary-net operator-topology and bounded-monotone assertions.

For CP12 the exact earlier input is the bounded support result for positive ultraweakly continuous functionals in UE, “State support and continuity tools”, source lines 93–102, using BI Lemma 8.1 and Theorem 8.3(1,3), lines 541–592. CP06 supplies ultraweak continuity, CP07 proves the Cauchy–Schwarz compression, and CP11 supplies the corner specialization. This exact component uses no universal-bidual construction, abstract-predual theorem, generic normal-weight finite-domain result or NW converse. CP12 also proves a positive-approximation criterion with the supremum condition stated as its hypothesis; it does not assume an unproved characterization of all normal weights.

The complete source/reader bodies listed in the programme-proof record accompany the offline download. The CP proof-input record specifies their hashes and hypotheses. These are exact selected input contracts; the full parent course, its downstream prerequisites and the transitive proof graph are not declared complete.

Scalar inputs for the spectral lesson

The five full specialization bridges now use Haar Theorem 2.2 and Proposition 2.3 for RMK/regularity, and measure-tools Theorems 1.1, 2.1–2.2 and 3.1–3.2 for measure construction, convergence and scalar L2. The real-to-complex RMK correspondence and the already linear-first L2 pairing are explicit. The original arbitrary-Hilbert direct-sum, Borel-representative and CFC approximation arguments remain. The pinned mathlib proofs and human contributor credits remain as formal/historical evidence. No unrestricted net-DCT or full theorem-closure claim is made.

Closed-form foundations and their exact proof inputs

QF01–11 proves closed-form representation and directed convergence on arbitrary Hilbert spaces. Its Hilbert inputs are HS01–03: completion, projection, Riesz, bounded forms and adjoints. QF01 explicitly extends the bounded adjoint to rectangular maps by Riesz; BK01 gives the range/annihilator identity. BK07 proves the bounded rectangular left polar decomposition used in representation before any closed-form theorem. SK04–07 supply bounded Borel and unbounded spectral integrals, exact domains, square roots, inverse ranges and form pairings. SK09 supplies compact-interval approximation and continuous-calculus convergence for bounded strong nets. Measure tools, Section 2, with the scalar spectral specialization, supplies sequential scalar MCT/DCT. QF proves its directed limits by finite-energy estimates.

The optional affiliation conclusion uses BK02, BK08, and SK08. The exact QF proof-input record identifies all selected complete providers, hypotheses and source ranges. The existing offline download contains their unchanged full bodies, including the selected scalar and topology support. QF representation uses no prior unbounded polar or closed-operator T-star-T theorem, relative derivative or general-weight modular theorem.

Graph closure and the Tomita polar data

TC01–13 proves the adjoint, graph and polar statements with their full domains. Its complete prerequisites are the earlier Hilbert-space proofs HS01–03, the bounded bicommutant proof BK02, closed-form representation QF03, spectral construction and transport SK04–08, and sequential scalar convergence. The matrix and probability-space models additionally use HS04/08 and the complete scalar L2 construction. TC01 links each proof and states the exact convention and scope; the proof-input record identifies the selected source ranges.

Every previously selected full prerequisite body is retained in the offline edition. The general closed-involution results require no separability. Existence of a cyclic separating vector is a hypothesis of the vector model. The modular commutant theorem, modular invariance and arbitrary-weight closability are subsequent theorems, not premises or conclusions of this lesson.

The real coercive equation

The supporting proof constructs real orthogonal projection and the real Riesz vector, then proves the invertibility and sharp norm estimate directly. Its elementary complex Hilbert inequalities and positive matrix square roots have the earlier programme proofs linked in its introduction.