# Prerequisite proofs and reading order The lessons state their hypotheses at each use. The following register identifies the actual programme lessons supplying the selected proofs. The register specifies the selected proof interfaces,their exact mathematical versions and the prerequisite boundaries used by this course. Public links identify available editions; the checked mathematical revisions and any public-edition differences are retained in the source records. Start with completely positive finite models, completely bounded extension and matrix norms. Continue through tensor positivity, lifting, semidiscreteness, hypertraces, averaging and the bidual theorem. These supply the approximation tools used later. The tensor-product and CAR lessons precede finite AFD uniqueness, central sequences, strong stability and MASAs. The three bilinear-inequality lessons form their own consecutive chain. For the first finite injective proof, read weighted tracial adjoints, trace-preserving finite models, balanced Kraus families and unitary couplings in that order. Central disintegration and tracial envelopes then give the general nonfactor result. The second finite proof runs from invariant states through repaired small matrix corners to maximality. The finite expected-subfactor theorem and scalar MASA pinching precede that second proof. The semifinite MASA regularity conclusion additionally uses the finite injective theorem: read its finite branch first and return to its type II-infinity regularity step after unitary couplings. The finite scalar-pinching argument does not use that later branch. The basic entry requirements are Hilbert-space and Banach-space functional analysis, Hahn–Banach separation, weak-star compactness, measure integration, C*-functional calculus, states and GNS representations. Arbitrary-cardinality or nonunital inputs are retained where stated. Separable-predual, faithful-state, trace, normal-expectation and irreducibility hypotheses are imposed only at their actual uses. | Preceding programme lesson | Responsible programme course | Selected proof content and locators | | --- | --- | --- | | [Completely positive maps](https://kokunoyumeto.github.io/open-math-courses-public/courses/foundations-of-von-neumann-algebras/completely-positive-maps.html) | Foundations of von Neumann algebras and its foundation remainder | Theorem 6.1 and normal/commutant dilation span; Proposition 7.1 dual order; Theorem 7.3 dominated-functional complete order isomorphism; Theorem 7.3(4) full dominated composition and norm proof | | [Operator density from finite vector tests](operator-density-foundations.html) | Positive maps and finite-dimensional approximation | ODF01 bounded product and ultraweak series-tail estimate; ODF02 supported nonunital representation; ODF03 finite-vector bicommutant; ODF04 real self-adjoint density; ODF05 direct rational resolvents; ODF06 positive matrix density with the target norm bound; ODF07 strong* and ultraweak contraction-ball density. Human method: [Kaplansky, Theorem1 and Lemmas1–5](https://msp.org/pjm/1951/1-2/pjm-v1-n2-p06-p.pdf). | | [A finite regular measure from positive function covers](compact-rmk-from-function-covers.html) and [compact rectangles and measure completion](scalar-topology-completion-bridges.html) | Positive maps and finite-dimensional approximation; scalar integration and compact-metric topology | RM01–RM05 construct the finite regular Borel measure of a positive real-linear functional on a compact metric space, prove its mass, Borel measurability, outer and compact-inner regularity, representation and uniqueness. SC01 proves compactness of every closed rectangle; SC02 constructs completion of any measure without finiteness or sigma-finiteness. SS1–SS2 and SS4 supply scalar Hilbert completeness, compact-metric facts and measurable representatives. Classical positive-functional methods are credited to [Fremlin, Chapter43](https://www1.essex.ac.uk/maths/people/fremlin/chap43.tex). | | [Full normal GNS coefficients](normal-representations-and-finite-trace-corners.html#normal-functional-gns-topology), [arbitrary normal-weight GNS](../OA-FLOW/OA-FLOW-NF.html#oa-flow.nf.5), and [whole weight normality](../OA-FLOW/OA-FLOW-EW.html#ew-1) | Modular foundations and the every-weight comparison used by constant CAR states | Concrete predual norm closure and complete vector-series pullbacks prove full ultraweak continuity. EW1–5 preserve arbitrary normal weights, complete finite domains, all bounded nets and infinite values. CV4 is the explicitly attributed CC BY4.0 human convexity component. | | [Bounded-graph modular foundations](bounded-graph-modular-foundations.html) and [whole-graph fixed modular corners](fixed-modular-corners-from-whole-graphs.html) | Constant CAR states and the periodic core; all-weight modular comparison | BG1–6 prove normalization/fullification at arbitrary left-Hilbert-algebra scope, with full S/F domains and bounded-vector intersections. FC1–5 prove the exact corner GNS, adjoint and spectral restrictions for every faithful normal semifinite weight, allowing infinite corner weight. Their scalar/spectral and finite-ideal/weight inputs are linked at the exact consumed scope. Human primary method: [Rieffel–Van Daele1977, §5 and appendix](https://msp.org/pjm/1977/69-1/pjm-v69-n1-p17-s.pdf). | | [Periodic fixed-corner spectra](periodic-corner-spectra-from-factor-contact.html) and [the all-weight modular intersection](../OA-FLOW/OA-FLOW-MG.html#oa-flow.mg.4) | Positive maps and finite-dimensional approximation; crossed products and the flow of weights | PP01–PP04 prove the periodic hull using interval filters and explicit factor contact in every nonzero fixed corner. PP05 gives the CAR application with all integer degrees. The separate MG0–4 identity retains all faithful normal semifinite weights and exact type III separable-predual corner transport. Classical definitions and contact method: [Connes1973, printed170/174–175](https://numdam.org/article/ASENS_1973_4_6_2_133_0.pdf). | | [Predual compactness from positive vector control](predual-compactness-from-uniform-control.html) | Positive maps and finite-dimensional approximation | PC01 constructs positive normal vector envelopes; PC02 proves Baire, uniform boundedness and the needed one-way weak-compactness extraction; PC03 proves the complete faithful-state bounded metric; PC04–PC05 produce one controller; PC06–PC07 prove normality and compactness of the weak* closure by graph extension; PC08 supplies the faithful-state test. PC09 constructs Bernoulli probability, the exact L1 predual and the weak-null coordinate functionals. Classical method: [Akemann, Theorem II.3 and Lemmas II.3a–c](https://www.ams.org/journals/tran/1967-126-02/S0002-9947-1967-0206732-8/). | | [Natural-cone construction](natural-cone-construction.html), [cyclic realization](cyclic-cone-realization.html), and [cone geometry](standard-cone-geometry.html) | Positive maps and finite-dimensional approximation; the earlier modular operator proofs | NC01–NC01b construct the chosen faithful normal semifinite weight, its normal GNS representation, original involution graph and full left Hilbert algebra. NC00–NC08 construct the cone from bounded multiplication, including the original graph cores, positive form extension, endpoint duality, both quarter-power descriptions, Gaussian self-duality and algebra preservation. CR01–CR07 prove the mass-one Fourier correction, support-corner transport, quarter-error iteration, direct real-separation density and cyclic normal-functional realization. CG01–CG10 prove supports, orthogonal decomposition, squared-distance estimates, corner commutants and the arbitrary-algebra passage. Classical methods: [Hiai, Lemmas3.3 and3.17–3.19](https://arxiv.org/pdf/2004.02383v1), [Araki](https://msp.org/pjm/1974/50-2/pjm-v50-n2-p02-p.pdf), and [Haagerup](https://journals.msp.org/mscand/article/download/2067/2066/2098). | | [Contractive retractions and the algebraic structure of expectations](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#contractive-expectations) | Modular theory and weights | Section 3 orthogonal left support estimate; Section 4 nonunital retraction theorem; Section 5 matrix positivity test; Section 6 CP and complete contractivity | | [Injective von Neumann algebras](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#injective-von-neumann-algebras) | Injective factors | Definition 1.2; Theorem 2.1; Corollary 2.2; B5 normal representation comparison; Proposition 1.4 opposite systems; Proposition 2.3(a)–(d) full corner/product/arbitrary-amplification proofs; Lemma 4.1 and Theorems 4.2–4.3 full commutant and directed permanence proofs; Theorem 5.1 full amenable-normalizer averaging proof | | [Multiplicity of a von Neumann algebra on a Hilbert space](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-FOUND-REMAINDER/reader/supplements/normal-representation-comparison.html) | Foundations of von Neumann algebras and its foundation remainder | Fact 2.7; Remark 3.2 | | [Spatial tensor products of von Neumann algebras](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-FOUND-REMAINDER/reader/supplements/spatial-tensor-products.html) | Foundations of von Neumann algebras and its foundation remainder | Proposition 3.1(4), full positive normal vector realization proof; Theorem 8.2, full arbitrary-cardinality cyclic decomposition proof; Theorem 9.2 full normal slice/module/Fubini proof; Theorem 10.1 full normal product/predual/support proof; Section 11 Lemmas 11.1–11.3 and Theorem 11.4 full commutation proof | | [Trace inequalities for finite von Neumann algebras](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#trace-inequalities-for-finite-von-neumann-algebras) | Injective factors | Theorem 2.1 full semifinite joint-distribution proof, with Background B1–B9; Theorem 3.1 full Powers–Stormer proof; Lemma 4.1 layer-cake proof; Proposition 4.3 full spectral-truncation proof; Example 4.4 stricter bound obstruction | | [Traces on von Neumann algebras](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-FOUND-REMAINDER/reader/supplements/traces-on-von-neumann-algebras-part-a-def-v-2-1-to-def-v-2-17.html) | Foundations of von Neumann algebras and its foundation remainder | Proposition 1.6(c) full semifinite projection proof; Theorem 5.2 full center-valued trace proof; Lemmas 5.6 and 5.7 and full Theorem 5.5 proof for normal or singular finite traces; Corollary 5.12 full central decomposition proof; Corollary 5.4 full center-valued trace projection comparison proof | | [Integration for a trace, the commutation theorem, and applications](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#traces-on-von-neumann-algebras-part-b-thm-v-2-18-to-prop-v-2-36-exerci) | Foundations of von Neumann algebras and its foundation remainder | Proposition 2.4 full bounded-vector proof; Theorem 3.1 full commutation theorem proof; Theorem4.1 and Corollary4.2 full semifinite commutant/type comparison proofs; Proposition8.10 full finite-projection extended-trace criterion proof | | [Projections and types of von Neumann algebras](https://kokunoyumeto.github.io/open-math-courses-public/courses/foundations-of-von-neumann-algebras/projections-and-types-of-von-neumann-algebras.html) | Foundations of von Neumann algebras and its foundation remainder | Theorem 14.1 full finite joins/sums and modularity proof; Proposition 11.2 and Corollary 11.3 full faithful normal abelian-commutant proof; Proposition 3.5 full central-support and induced-kernel proof; Proposition13.3 full type II halving proof; Proposition13.4 and Corollary13.5 full properly infinite halving/division proofs; Proposition14.2 full finite complementary-projection equivalence proof; Proposition15.2 complete countable absorption and sigma-finite infinite-projection equivalence proof; Lemma7.4 full finite full-central-support projection proof; Lemma8.2 and Proposition8.4 and Lemma8.5 full matrix splitting proof; Proposition9.1, Lemmas9.3/9.5/10.2 and Theorem10.3 full finite type I structure proof | | [Weights and the Hilbert spaces of multiplication](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#weight-hilbert-algebra) | Modular theory and weights | Section 13 complete existence proof, orthogonal normal-state supports and finite-subset sum | | [General weights: finite domains, GNS spaces, and normal representations](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#weight-gns) | Modular theory and weights | Section 8 full finite positive cutoff equivalence proof; Section 7 full normal GNS representation proof for arbitrary normal weights, including states | | [Fixed elements and changes of density](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#centralizers-and-perturbations) | Modular theory and weights | Section 8 full construction, normality, semifiniteness and exact support proof; Section 11 full supported modular-group proof; Section 5 full finite-domain cyclicity and unitary weight invariance criterion | | [Changing the Hilbert space of a regular crossed product](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#15-regular-model-independence) | Crossed products and the flow of weights | Haar and operator-algebra prerequisite contract; Coefficient operators and left translations, full construction/covariance proof (R2–R3); Normality from compact monotonicity, full faithful normal construction proof (R4–R6) | | [Building an intrinsic flow from modular coordinates](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#04-core-and-flow) | Crossed products and the flow of weights | Core in a weight chart, Stone generator and affiliation; Why the dual weight has an inner modular action, full proof; Removing the modular density, full proof; only existence/NSF trace is used | | [Extending the dual weight beyond the common involution domain](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#13-dual-weight-construction) | Crossed products and the flow of weights | Two domains and representations; General left Hilbert algebra-to-weight prerequisite contract; Constructing the weight on the crossed product (W1), full existence argument | | [How the dual weight moves crossed-product generators](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#14-dual-weight-modular-action) | Crossed products and the flow of weights | General closed Tomita graph and modular implementation prerequisites (A6–A7); Modular operator of the dual weight (A8–A10), full identification argument; Two generator formulas (A11–A16), full coefficient/group computation | | [Every bounded functional becomes normal in one representation](prerequisites.html#cstar-universal-bidual) | Foundations of von Neumann algebras; scalar and density prerequisites | Complete Proposition1.1 and the construction before Section2: four positive parts, all-state sum, predual isometry, bidual structure and positive normal extension. [PCY01–PCY04](positive-functionals-and-essential-cyclic-vectors.html#pcy01) proves the nonunital norm limit, essential cyclic vector and state norming. General representation extensions and second adjoints retain separate prerequisites. | | [AF-algebras](https://kokunoyumeto.github.io/open-math-courses-public/courses/foundations-of-von-neumann-algebras/af-algebras.html) | Foundations of von Neumann algebras and its foundation remainder | Definition 4.1 and Proposition 4.2 full norm/universal construction; Example 4.3; Lemma 4.4; Theorem 4.5 and Remark 4.6 full compatibility proofs; Definition 4.7 and Proposition 4.8 full sequential AF/separability proof; Example 5.3 full UHF/CAR finite-string and inductive-limit comparison | | [The modular group and its analytic algebra](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#modular-fundamental-theorem) | Modular theory and weights | Section 5 full JMJ commutation proof; Section 6 full covariance, automorphism and weight invariance proof | | [Trace densities and noncommutative integration](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#trace-integration) | Modular theory and weights | Section 6 full isometric onto trace pairing and positive-cone proof | | [Pointwise inner flows and continuous implementers](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#136-pointwise-inner-flows-and-continuous-implementers) | Crossed products and the flow of weights | Complete theorem and proof, equations (1)–(46), including Borel section, alternating bicharacter, measurable twist, integrability, common-conull disintegration and character cancellation | | [Conditional expectations from modular invariance](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#modular-expectations) | Modular theory and weights | Section 1–08 full forward existence, compression normality, weight preservation and uniqueness/GNS projection proofs | | [Polish spaces and standard Borel spaces](https://kokunoyumeto.github.io/open-math-courses-public/courses/foundations-of-von-neumann-algebras/polish-spaces-and-standard-borel-spaces.html) | Foundations of von Neumann algebras and its foundation remainder | Background F1–F4 prerequisite declaration; Theorem3.6 complete refinement, tree-separation, Borel image and inverse proof | | [Compact and trace-class operators, the predual of B(H), and the operator topologies](https://kokunoyumeto.github.io/open-math-courses-public/courses/foundations-of-von-neumann-algebras/compact-and-trace-class-operators-the-predual-of-b-h-and-the-operator-topologies.html) | Foundations of von Neumann algebras and its foundation remainder | Theorem2.3 full Schmidt/self-adjoint compact spectral decomposition proof; Definition4.1, Lemma4.2, Theorem4.3, Corollary4.4 and Theorem4.6 full trace-class completeness, summability, ideal and absolute trace proofs | | [Banach algebras, spectrum, holomorphic functional calculus and Gelfand theory](https://kokunoyumeto.github.io/open-math-courses-public/courses/foundations-of-von-neumann-algebras/banach-algebras-spectrum-holomorphic-functional-calculus-and-gelfand-theory.html) | Foundations of von Neumann algebras and its foundation remainder | Definition6.4 and Proposition6.5 complete surrounding-cycle/germ proof; Theorems6.7 and6.10 full homomorphism, spectral mapping and composition proofs; Theorems8.1 and8.2 full spectral semicontinuity and resolvent Lipschitz proof | | [Compact and trace-class operators, the predual of B(H), and the operator topologies](https://kokunoyumeto.github.io/open-math-courses-public/courses/foundations-of-von-neumann-algebras/compact-and-trace-class-operators-the-predual-of-b-h-and-the-operator-topologies.html) | Foundations of von Neumann algebras and its foundation remainder | Lemma3.1 and Theorem3.3 full basis-independent Hilbert-Schmidt, ideal, compactness and Hilbert completeness proofs; Lemma11.1 and Theorem11.2 full finite-rank spectral-block approximation and summable off-diagonal removal proof | | [Polar decomposition of functionals and weak compactness in preduals](https://kokunoyumeto.github.io/open-math-courses-public/courses/foundations-of-von-neumann-algebras/polar-decomposition-of-functionals-and-weak-compactness-in-preduals.html) | Foundations of von Neumann algebras and its foundation remainder | Lemma10.1 full bidual closure compactness proof; Theorem10.2 full seven-condition equivalence, including all proof directions; Lemmas10.3 and10.4 full reduction, spectral cutoff, Baire and finite-functional proofs. Ordinary multipliers use PC00–PC09 above for the compactness criterion and its example inputs. Other invoking lessons retain the stated foundation locators. | | [Measurable fields of Hilbert spaces and their direct integrals](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-FOUND-REMAINDER/reader/supplements/measurable-fields-direct-integrals.html) | Foundations of von Neumann algebras and its foundation remainder | Definitions2.1/8.1; Lemma2.2; full Theorems3.1/5.1/6.2/8.2/9.1/10.1 and their construction proofs | | [Direct integrals of von Neumann algebras](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-FOUND-REMAINDER/reader/supplements/direct-integrals-of-von-neumann-algebras-commutants-and-centres-takesa.html) | Foundations of von Neumann algebras and its foundation remainder | BackgroundB1-B12; full Proposition1.3; Propositions2.2/2.3; Lemma3.1; Theorems3.2/4.1/4.3; Lemma5.1 full countable generator proof | | [Continuous decompositions, modular invariants, and canonical extensions](https://kokunoyumeto.github.io/open-math-courses-public/courses/OA-APPROX/prerequisites.html#139-continuous-decomposition-invariants-and-canonical-extensions) | Crossed products and the flow of weights | Sections The three type III subtypes and Modular spectrum from the kernel of the center flow, including equations14-18 and the full supplied proof; use only the periodic case for a typeIII factor | The finite dyadic uniqueness and general injectivity/AFD proofs also supply the corresponding approximation bridges for the injective-factor course. The theorem about every representation of a general connected locally compact group requires further representation theory and is not asserted here. General weight, expectation and fusion constructions retain their modular-course ownership; factor classification and the subfactor chapter are outside this course. The offline collection contains all fifty lessons and locally linked companion readings,their editable sources,component licence notices and local reader runtimes. Open the collection `index.html`; the course lies under `courses/OA-APPROX/`. The human CC BY, CC BY-SA, Design Science License and GFDL components retain their separate terms and attribution. [BC1–5](../OA-FLOW/OA-FLOW-BC.html#oa-flow.bc.1) supplies all finite balanced-weight domains and cocycle identities. BC3 uses the entire compressed GNS graph, its adjoint and all spectral domains for matrix-subcorner restriction; BC4 uses the complete identical-weight graph; BC5 transports both full initial and closed graphs by the GNS unitary. These proofs retain arbitrary faithful normal semifinite weights, arbitrary ambient Hilbert multiplicities and infinite corner weight. Their canonical weight/GNS/modular and scalar/projection prerequisites retain the separately stated validation boundaries. [BW1–5](bounded-vector-weight-interface.html#bw1) supplies the whole bounded-vector foundations of WF1–6, WR1–7 and MW1–4 from BG1–6. Both multiplication ideals, their adjoint intersections, mixed products and covariance act on the full bounded-vector spaces; the polar column is constructed directly from a bounded range isometry. Those three weight providers retain all arbitrary faithful normal semifinite weights, infinite positive values, entire finite ideals and full GNS graphs. Their scalar/spectral/contraction and general-weight normal-minorant proofs have separately specified exact dependencies. ## Collective binary pinching The complete [simultaneous pinching construction](abelian-pinching-and-relative-commutants.html#theorem-5-1) uses one normalized direct-sum energy for the entire finite list, a finite Re/Im spectral grid and one binary cut in every current corner. Its15/16 squared-energy factor does not consume the separate 3/4 single-unitary spectral bound. The seven results and twelve solved exercises use their stated hypotheses. The exact prerequisite contracts are the state-preserving modular expectation and its GNS projection, normal positive pairings and ultraweak compactness, bounded spectral calculus, GNS/Hilbert completion, central support and polar decomposition, type II trace cuts and finite-factor comparison, and bounded faithful-state to strong* convergence. ## Faithful-state expectation and compatible matrix limits [SE1–SE5](state-expectations-from-bounded-graphs.html#se1) proves the state centralizer/fixed-algebra identity, shifted real-parameter Gaussian filters, full restricted Tomita and adjoint domains, algebra-valued GNS compression, all-net normality and uniqueness. The two original consumers use this state contract rather than the broader general-weight expectation route. Its exact roots are BG1–6, FF normal GNS and its actual Gaussian Fourier span, SF full spectral calculus, CP6 predual/normal pairings and NF6 normality. The expected-subfactor proof also constructs finite-stage trace projections (MC1), verifies factorhood by their GNS limit, and identifies the compatible dyadic tensor by a trace-preserving GNS unitary. The AFD regularity clauses still have their stated finite corner/containment and later finite injective-factor prerequisites. The semifinite matrix-decomposition span is independent of that later finite injective result; referencing this span from the later corollary creates no proof cycle. ## Trace approximation and finite levels The two original finite AFD and semiregular lessons use [SE1–SE5](state-expectations-from-bounded-graphs.html#se1) for trace expectations. The full [PB1–PB2 argument](hyperfinite-finite-factors.html#bounded-trace-topology) proves concrete-predual density and bounded trace topology without a trace-density representation theorem. It needs CP6’s actual onto predual duality and the complete Hahn–Banach proof. Formula [MC1](masas-in-expected-semifinite-subfactors.html#theorem-2-1), before that proof’s separate AFD regularity branch, supplies the finite-stage projection and dyadic factor limit. Consuming this exact span introduces no cycle through the later AFD corner theorem. [DP1–DP2](semiregular-masas-and-scalar-pinching.html#lemma-2-1) gives every diffuse trace cut, a positive integral dyadic multiplicity with exact sum, an exact excess-to-deficit transfer and the full square-root trace error. The semiregular construction retains an arbitrary given MASA and all its normalizers. Its scalar pinching uses the complete decreasing-factor and two-refinement contracts with normalized corner weights; it does not assert ambient irreducibility for the smaller decreasing factors. The direct [OA1 proof](hyperfinite-finite-factors.html#theorem-6-3) establishes the outer example using the distant Pauli tensor leg. The complete general center-trace and properly infinite projection bodies are now explicitly consumed by the stronger original Lemmas6.1–6.2; their earlier source contracts remain separately scoped. AP Remark9.1.7 only refers the general center-trace existence to a book; its tracial Proposition9.1.8 does not close that gap. AP Exercises2.7/15.10/5.11 are statement or hint comparisons, not imported complete proofs. ## General finite traces and finite outer actions [FCT0–8](../OA-FLOW/OA-FLOW-FCT.html#oa-flow.fct.0) proves the full normal center trace for arbitrary finite algebras, including nonsigmafinite centers, and its faithfulness, uniqueness, comparison and automorphism naturality. [PC0–7](../OA-FLOW/OA-FLOW-PC.html#oa-flow.projection.pc1) supplies arbitrary orthogonal sums, corner centers, full projection Schroeder–Bernstein, properly infinite central halving and finite joins. Lemma6.1 uses separating normal center states, with no global faithful scalar state. Lemma6.2 uses the whole finite/properly infinite split at its original arbitrary-algebra scope. [Finite Fourier coefficients](finite-outer-actions.html#lemma-1-1) give the complete finite-group realization. Its [closed central-kernel proof and normal inverse](finite-outer-actions.html#lemma-1-3) uses [ST1–2](../OA-FLOW/OA-FLOW-ST12.html#oa-flow.st.1) on the whole domain. The exact [FJ1–FJ3 tracial commutant proof](finite-outer-actions.html#tracial-commutant) uses only the faithful finite trace, dense commutant orbit and bounded whole-space extension. It does not consume a general weight-modular or representation-amplification theorem. The invariant-stage fixed-factor argument explicitly proves separable predual before applying finite AFD uniqueness. The Peterson author notes provide complete selected general projection, approximate central-state and tracial conjugation methods. AP Exercise5.11 remains a statement/hint comparison, not a complete imported proof. AP footnote13 requires an infinite countable group for its escaping Bernoulli sites, and its output-index formula needs the inverse for a left action. The repeated finite-group index has its own whole local proof. The full normal representation amplification and canonical finite-projection trace bodies in NA0–6 now supply the later hyperfinite commutant paragraph; their exact earlier source contracts remain individually scoped; the unsupported weak-cluster-to-norm step in Peterson5.3.5 is not used here. The shared FCT reader still has an explicitly unused paid complementary bibliography entry. ## Normal representations and canonical finite trace corners The complete [NAR1–NAR4 root construction](normal-representations-and-finite-trace-corners.html#na-square-root) is a norm-convergent polynomial series with positive coefficients of exact sum one and tail at most1/sqrt(N+1) on positive contractions. It also supplies the bounded root in the selected PC1 polar input, avoiding a spectral-theorem prerequisite in this route. [NA0–NA2](normal-representations-and-finite-trace-corners.html#na0) proves the full arbitrary-index matrix algebra, canonical diagonal trace, all-net normality, semifinite cuts and the finite-projection criterion in a factor. The infinite-trace contradiction builds a countable shift inside the projection; it does not compare arbitrary infinite-trace projections. [NA3–NA4](normal-representations-and-finite-trace-corners.html#na3) realizes each normal positive functional from its actual CP vector series by a bounded dominated form. The complete Hilbert Riesz proof represents that form, whose operator commutes with the amplified algebra. All maximal orthogonal cyclic summands are then embedded, with arbitrary multiplicity. No positive normal extension, positiveL1 density theorem or Peterson5.3.5 weak-cluster step is used. [NA5–NA6](normal-representations-and-finite-trace-corners.html#na5) consumes only the exact FJ tracial helper and the already closed original Corollary5.2 proof. The later unnumbered commutant application therefore introduces no proof cycle. Proper identity representations have the stated extra zero-action summand; none of the original numbered statements is narrowed. The author-open AP draft §8.2–8.3 supplies the trace and module comparisons; its separable infinite/infinite comparison Proposition8.3.8 is not consumed. ## Scalar order, finite interpolation and exact lifting The complete [operator-system extension](completely-positive-finite-models.html#theorem-2-3) includes its direct block norm and actual [dual-ball compactness argument](completely-positive-finite-models.html#dual-ball-compactness). It retains arbitrary Hilbert multiplicity and nonclosed systems. The exact [scalar dilation and faithful representation](completely-positive-lifting.html#faithful-scalar-gns) use only the preceding unital dilation body and finite Lemma2.2. Those exact spans introduce no cycle through the lifting theorem. The [explicit locally compact interpolation](completely-positive-finite-models.html#theorem-3-3) constructs its compact supports directly from a finite function list, with an omitted zero sample; no partition-of-unity theorem is imported. The [quasicentral proof](completely-positive-lifting.html#lemma-2-1) supplies the full convex separation and ideal support. Its [two-root estimate](completely-positive-lifting.html#lemma-2-2) uses NAR1–4's exact uniform coefficient tail. The [selection proof](completely-positive-lifting.html#theorem-3-2) chooses from an arbitrary approximating net and has tail at most2^(1-k) on the firstk dense tests. Nonunital cutoffs retain arbitrary B andJ and the exact final lift norm. These two lessons contain thirty numbered results and seventeen solved exercises. Gabe Lemma2.6's reference-out selection and Olesen's book-referred ideal inputs are supplied by written local bodies. Olesen's finite-domain extension into an arbitrary quotient is not imported. C*-calculus,unitization,the concrete predual and the tensor-positivity converse have separate exact proof records. ## Tensor norms from finite matrix tests The [complete tensor construction](tensor-positivity-nuclearity.html#tn01) builds Hilbert tensors, state density by finite-coordinate separation, every spatial representation bound, the commuting-action maximum and its coefficient recovery. The [split unitization sequence](tensor-positivity-nuclearity.html#tn06) supplies the nonunital nuclearity argument. The [proof diagram](tensor-positivity-nuclearity.html#tensor-norm-diagram) displays the exact Gram mass and maps. The lesson contains eleven results and seven solved exercises. CF,cone realization,enveloping/predual and preceding density arguments have their exact separate proof bindings. ## Scalar representation before matrix positivity The [scalar-to-matrix construction](scalar-gns-and-matrix-cstar-norms.html#mg01) proves positive scalar extensions, scalar GNS, a faithful isometric direct sum, the canonical matrix C*-norm, boundedness and complete positivity of scalar positive functionals, and complete contractivity/isometry of algebraic *-homomorphisms. Its order avoids using complete positivity to construct the faithful representation needed to justify matrix positivity. It uses the unchanged full CF1–10 scalar bodies at their stated choice/scalar-calculus boundary. The exact current consumer edges recorded here are finite-model Lemmas2.2 and4.2, tensor Lemma1.1 and lifting Theorem3.2. Actual Shirbisheh v2/Peterson2015 comparison clauses, printed errors, referred-out steps and complete local replacements are recorded individually. No human PDF/text redistribution right is inferred. The lifting lesson already states that its unital assertions use nonzero algebras, so its state/unit-defect step has the required nonzero domain; the zero-domain concern is outside that existing convention. ## Normal Jordan decomposition by scalar rotation The [NJ01–NJ06 proof](normal-jordan-from-scalar-norm-attainment.html#nj01) gives the exact normal norm-additive Jordan decomposition and uniqueness consumed in tensor Lemma2.1 and, through it, Theorem3.1. Concrete quotient duality, scalar compactness and a norming self-adjoint contraction produce a unitary. Its positive normal functional splits by an explicit strong rational range projection. No general functional polar/support theorem, Borel calculus, bidual/enveloping construction or faithful normal state is a premise of this selected proof. Exact CP01–CP06 and CF/MG01 versions are identified alongside their selected Peterson2015 source comparisons. ## Universal state coefficients and the nonunital norm limit The complete [state representation and bidual proof](../foundations-of-von-neumann-algebras/the-universal-enveloping-von-neumann-algebra-of-a-c-star-algebra-and-w-star-algebras.html#constructing-the-bidual-before-using-it) identifies the concrete predual with A* by an onto isometry and transports the von Neumann structure to A**. [PCY01–PCY04](positive-functionals-and-essential-cyclic-vectors.html#pcy01) supplies the exact nonunital positive-functional norm and essential cyclic-vector antecedents. CF, MG, CP, ODF, F09 and SEP give the selected scalar, matrix, Hilbert, predual, approximation and finite-coordinate separation proofs. This resolves the selected bidual/positive-normal-extension input to tensor Theorem3.1, with its exact full prerequisites. ## Ideal kernels and normal extensions The complete [ideal-closure proof](../foundations-of-von-neumann-algebras/the-double-commutant-theorem.html#oa-fnd-bi-10) uses its scalar inverse-order,full Vigier and bounded vector-series topology arguments. [Lemma 2.1](../foundations-of-von-neumann-algebras/the-universal-enveloping-von-neumann-algebra-of-a-c-star-algebra-and-w-star-algebras.html#oa-fnd-wa-02) supplies the normal extension and its central-kernel isomorphism, including degenerate essential spaces and a normal inverse proved through the preadjoint. The [second-adjoint proof](../foundations-of-von-neumann-algebras/the-universal-enveloping-von-neumann-algebra-of-a-c-star-algebra-and-w-star-algebras.html#second-adjoints-of-homomorphisms) proves inclusion ranges using annihilators. [Nuclear biduals, Proposition 4.1](nuclear-biduals-and-extensions.html#proposition-4-1) now gives a direct normal-inverse proof for the full ideal/quotient splitting. The selected consumers are Lemma 1.1, Corollary 3.2, Proposition 4.1 and Theorem 4.2, with the entire solutions to Exercises 6–7 retained and pinned. The other three consumers have separately specified nuclearity,injectivity,semidiscreteness and central-support inputs. ## Nuclear bidual constructions Proposition2.1 uses the complete local Arveson operator-system extension and unital dilation proofs, minimal tensor injectivity and nuclear norm equality. It constructs the nonunital essential dilation support and the first-factor representation explicitly; no scalar-dual-map inverse is used. Lemma1.1 uses all state normal-extension central kernels, finite Boolean partitions, explicit corner/product retractions, Vigier convergence and pointwise ultraweak compactness. The lesson contains six numbered results and eight complete solved exercises. Exact proof versions and source scope are recorded in `source-provenance.json#current_nuclear_bidual_structural_reconstruction`. ## Averaging: normal representation comparison The complete comparison uses CP01–06 quotient predual and balanced summable coefficients, elementary domination by a positive paired series, the entire bounded-form commutant construction, arbitrary-cardinality cyclic decomposition, the explicit matrix-entry amplification commutant and zero-extension corner. Its scalar roots and Hilbert representation are CF Sections6–8; the bounded dominated-form method is compared with the actual Anantharaman–Popa Lemma2.5.3 proof. No standard-cone positive-vector or trace-class spectral decomposition result is needed. Theorem1.3 still uses standard-pair existence JMJ=Mprime with its exact Tomita/left-Hilbert prerequisites. The lesson contains twelve numbered results and ten complete solved exercises. Current versions and the full consumer graph are in `source-provenance.json#current_averaging_normal_representation_comparison`. ## Crossed-product coefficient compression Theorem3.2 now constructs normal ucp Theta_f:Q→M by the isometry W_f and its constant-commutant intertwining. CP04–06 proves normality and bounded predual-tail convergence; H0.1 and given-Haar positivity provide normalized compact functions in arbitrary identity neighborhoods. Direct composition with the assumed normal cpc finite matrix models, followed by an explicit finite-test directed net, gives semidiscreteness. The inherited crossed-product tensor-bound/squared-norm-localization/commutant-criterion route is removed from the main proof rather than moved. The two linked lessons contain sixteen solved exercises. Exercise6 gives the neighborhood contradiction and Exercise10 identifies the compression maps and original generators. The finite-model lesson comparison description is corrected. Exact current versions are in `source-provenance.json#current_crossed_product_cp_compression`. ## General Haar existence in the regular construction The HR-06 → HR-04 → HR-01 → SC-01 proof chain constructs a nonzero left Haar measure in the outer-regular Borel convention for an arbitrary LCH group. H0 supplies compact shrinking, finite partitions and finite-product compactness; the exact prior CF choice/scalar body supplies the tail ultrafilter. Fremlin Chapter44 441C/E, pp.2–4, is the selected free finite-cover method; the source416M step is replaced by the complete local Borel construction. HR03 and SC03–SC07 supply the density and convergence arguments at their stated inputs. ## Scalar integration and compact-continuous density The exact current CF-01 → SC-00–07 scalar proof chain, together with the earlier SC-01/H0/HR-01 versions, supplies HR-03 finite-exponent Cc density without global sigma finiteness or countable topology. Free Axler and Lebl author proofs, source editions, entire selected spans and omissions are recorded in current_scalar_integration_and_Cc_density; full endpoint and null-set arguments are proved locally. The owned regular prelude explicitly conjugates the first-variable scalar/tensor forms to its second-variable convention, preserving norm and completeness. Vector-valued integration and the full regular Hilbert-valued identification remain the next exact source obligations; later Haar/product/modular and standard-pair/core/hypertrace/coursewide structure duties are not inferred complete. ## Vector integration and the regular Hilbert model The full current L24 finite-exponent conventions and Propositions4.1–4.2, HR08/09, the complete scalar/Cc/Riesz chain and H0/CF Hilbert tensor proofs supply the new owned measurable-section/tensor/bounded-field construction. The source comparison uses Williams draft3.1,1.87–1.91 and AppendixB.1; its external measure/paracompactness and bidual/convex-hull routes are not imported as missing premises. The direct simple-integral/norm-completion proof keeps arbitrary Banach/Hilbert spaces and arbitrary LCH groups. Raw global/local null sets and Linfinity conventions are not equated. Carrier-qualified Radon products and vector Fubini are specified below. The HR05 Radon-product scalar/section/Tonelli/Fubini/rectangle/tensor proof and L24 Proposition4.3 vector argument use the exact CF/H0/SC/HR and Banach-integration prerequisites. The owned carrier expansion proves outer strong measurability explicitly. Fremlin Chapter41,417A–C/G/N/P,provides the Radon-product comparison with its locally determined conventions and sigma-finite strip restriction. Its ordinary-product,extension and monotone-class antecedents are not substituted for the local prerequisites. HR07 Haar uniqueness/product transport and L24 Section3 group modular/inversion/translation use the exact CF/H0/SC/HR/product/vector proofs. The complete owned expansion supplies positive-continuous weighted Radon regularity, the normalized Borel inversion identity and left regular strong continuity on arbitrary Hilbert spaces. Fremlin442A–K and443G provide the Haar comparison;their wider quasi-Radon and measure-topology antecedents are outside the local premise set. Only the actual left-L2 regular input is annotated in the original two consumer rows. The group modular function and translations are distinct from operator-algebra modular actions; the latter have their own standard-pair,weight and core prerequisites. ## Current arbitrary-algebra standard-pair construction Complete arbitrary-algebra faithful normal semifinite weight, direct Hilbert sum/normal representation, dense multiplication algebra and its whole involution-closability proof now instantiate full BG1-6 and give the J-pair used in Theorem1.3. All required selected bounded spectral, contraction-density, compact-ball, predual-series, scalar contour/Fourier and CF/SC primitives are bound at complete exact free programme/source versions. The complete owned proof is averaging-crossed-products-injectivity.md#construct-the-standard-pair-for-an-arbitrary-algebra. It constructs the orthogonal normal vector-state family, finite-subsum weight and exact arbitrary Hilbert sum; proves the normal faithful image and whole multiplication-involution closability; then invokes the fully bound BG1–6 argument. Source-provenance.json#current_arbitrary_algebra_standard_pair_construction records every current full proof/source/version/locator edge. ## Current given-weight GNS and order-normal functional proofs Complete arbitrary-weight finite ideal, linear extension, null quotient and GNS construction, all four semifinite cutoff/density implications, normal-semifinite finite-star density, and whole finite-positive-functional order/ultraweak equivalence are now supplied. They prove full ultraweak continuity of the GNS representation for every normal weight, including nonfaithful and nonsemifinite inputs, at the exact free bounded/scalar/spectral/predual/closed-form roots. The complete owned argument is averaging-crossed-products-injectivity.md#construct-the-gns-space-for-a-given-normal-weight. Source-provenance.json#current_given_weight_GNS_and_order_normal_functionals binds the whole selected GW1–5, NF1–5, FF4 form representation, STC, GNS2–5 and WF5 arguments, their exact current versions and the prior free CF/SC/SF/BD/CP/ST roots. The independent FF4 integral-form application and later GW6/WR/EW uses are separate selected arguments. ## Current given-weight closability, recovery and modular action Complete whole-cone normal-minorant and bounded GNS graph/convex closure proofs now supply the entire arbitrary faithful-n.s.f.-weight finite-star closability, fullification and original-weight/GNS recovery. Both full bounded-vector ideals, opposite finite-cone bijection/density, modular and J covariance, canonical opposite weight and its whole finite ideal, GNS antiunitary and dominated-functional implementing vector are proved at complete free roots. Given-weight involution,recovery and point-ultraweak modular action are the specified inputs to Theorem4.1. Natural-cone, all remaining original50/327/504 mathematics and paid-expression/organization duties remain individual. The complete owned argument is averaging-crossed-products-injectivity.md#recover-a-given-weight-and-its-modular-action. Source-provenance.json#current_given_weight_closability_recovery_and_modular_action binds the full EW1–5, CV1–4, CI1–3, BW1–5, WF1–6, WR1–7 and MW1–4 proofs at the prior exact complete free CF/SC/SF/BD/CP/ST/GW/NF/BG roots. The standalone FF5 form-invariance argument is selected;later extended-cone operations are outside this proof scope. CV4 retains its verified publisher attribution, CC BY4.0 and corrections; the native arXivv1 hash is explicitly distinguished from publisher version/readings. ## Current KMS characterization, analytic core and whole-cone trace criterion Full finite-star KMS existence, explicitly integrated entire algebra with every real spectral-power graph core, arbitrary faithful-normal-semifinite-weight modular-group uniqueness and the whole-cone trace criterion are proved from their exact complete prerequisites. Theorem4.1 uses the KMS/trace criterion and the separately specified full dual-weight/core/trace and semifinite-hypertrace inputs. General-weight invariance is an explicit uniqueness hypothesis; finite-functional invariance is proved from KMS. Natural-cone/standard-form, normalized cocycle/centralizer perturbation and every remaining original50/327/504 proof and paid-expression/organization duty remain individual; no entire foreign course or inherited lesson structure is cleared. The complete owned argument is averaging-crossed-products-injectivity.md#prove-the-kms-characterization-and-the-whole-cone-trace-criterion. Source-provenance.json#current_KMS_characterization_analytic_core_and_trace_criterion binds complete KT1–5, KU1–4 and SF1–3 to exact source/reader versions at33 earlier full free proof bundles and entire CF1–10. The native Hiai2020v1 source and full state-proof/weight-statement locators are explicit. Scalar seam continuation, Gaussian finite domains and the corrected star/orbit conventions are proved; no omitted weight proof or external three-lines/Stone theorem is imported. ## Current centralizer density, whole domains and modular normalization Complete arbitrary-algebra nonsingular-centralizer-density construction, all finite/GNS domains, bounded and unbounded modular formula, exact balanced cocycle normalization, whole-cone inverse perturbation and conditional faithful-normal-semifinite trace conversion are proved at entire current free roots. Only full MA1-2,BC1-5,CZ1-3 and the complete standalone first AS1 strip lemma are qualified; whole CZ0,MA3/AS3/AS4, arbitrary cocycle realization and Radon-Nikodym classification converse are not inferred. Theorem4.1 uses these centralizer-perturbation and density-removal arguments together with its full dual-weight/core/trace and hypertrace inputs. The complete owned argument is averaging-crossed-products-injectivity.md#construct-centralizer-densities-on-their-whole-finite-domains. Source-provenance.json#current_centralizer_density_full_domains_modular_formula_and_normalization binds BC1–5,MA1–2,CZ1–3 and the standalone first AS1 strip lemma to their full prerequisite arguments,including CF1–10. Hiai2020v1 and the authorized Numdam Connes1973 edition have exact source versions and native-page locators;their human-source rights remain in force. Full KMS identification replaces the unconsumed general analytic-generator prerequisites. ## Current full continuous-core dual weight and trace The full faithful normal semifinite dual weight on every continuous core is constructed at exact free roots, with complete finite/GNS domains, closed involution/adjoint and all Borel modular domains, both modular generator formulas, the full affiliated implementing density, the whole core trace, exact normalized cocycle and dual-action scaling. This closes the continuous-core and trace-existence prerequisite used by originalTheorem4.1. General noninvariant-action dual weights and arbitrary cocycle realization are outside this selected scope. GDW4 and RF5 are the selected arguments;broader claims of those provider lessons are outside this proof scope. The entire owned argument is averaging-crossed-products-injectivity.md#construct-the-full-dual-weight-and-trace-on-the-continuous-core. Source-provenance.json#current_full_dual_weight_continuous_core_domains_and_trace binds GDW4 and RF5 to their full prerequisite arguments,including CF1–10. The actual Haagerup1978 publisher scan and authorized author-hosted Teschl2009 source versions, hashes and whole native-page locators are recorded; original human rights are retained. Complete finite/GNS domains, all modular spectral domains, both generator formulas, the affiliated density, full trace and normalized dual-action scaling are proved. The lesson contains twelve numbered arguments and ten solved exercises. The complete [finite-trace corner construction](hypertraces-finite-injectivity.html#semifinite-trace-corner-bootstrap) supplies the scalar-trace passage for the continuous core: nonzero finite-trace cuts, arbitrary maximal orthogonal family, finite partial sums tending strongly to one, faithful normal tracial corner states, normal cpc incoming matrix maps and all normal-functional error tests. Theorem4.1 now uses that construction and the full core trace explicitly. Corollary6.3 retains its broader projection-semifinite argument. Source-provenance.json#current_semifinite_trace_corner_bootstrap identifies the full argument and human method comparison. The three Grothendieck lessons contain the direct completed-residual lift, scalar state detectors, optimized clipping budget, complete main two-dimensional Gaussian proof, nearest-orthant separation, finite third-root averages, continuous original-algebra polar cutoffs and repeated constant improvement. Together they contain fifteen numbered results and thirty solved exercises. Their exact versions, human source method boundaries and result spans are recorded in source-provenance.json#current_grothendieck_free_proof_reconstruction and result-source-uses.json. Pisier's free Kyoto Steps1–2 supplies an actual sharp-upgrade comparison; Step3 is an outline. Naor–Regev–Vidick supplies an actual full matrix argument, without an inferred arbitrary-algebra extension. Scalar C*-calculus, the universal-bidual contracts and scalar complex Cauchy/maximum-principle inputs remain explicit transitive proof duties. The ITP/CAR/Bogoliubov/constant-CAR main routes explicitly supply finite-mode matrix norms and corner-inverse simplicity, compatible compressed covariance densities, rational bounded strong* approximation, local central expectations, the exact product-overlap expectation tower, full unbounded Duhamel domains and a dyadic small Hilbert–Schmidt diagonal perturbation. The constant-state proof excludes finite projections using a finite-corner trace and computes S(M) through the entire product modular domain and every-weight comparison. Its upper bound does not consume the general MG4 type III corner-transport result. The finite-ideal MG0–1, balanced BC1–3, CS3 fixed-corner and BG/FC/PP proofs retain their complete stated scopes and earlier weight/spectral/Hilbert-algebra prerequisites. Historical human comparisons are exact: Araki–Woods2.12 changes reference representations and2.13 is a sufficient ITPFI overlap comparison; Dereziński's referred-away Takesaki exercises/classification are not construction premises. Exact versions of the thirty-four results and forty-six solved exercises are specified in source-provenance.json#current_car_itp_bogoliubov_free_reconstruction. The complete solutions in the seven ITP/CAR/Bogoliubov/constant-CAR and Grothendieck problem sets are reconstructed from their full mathematical obligations and current free arguments. The seven lessons contain forty-nine numbered results and seventy-six solved exercises,including their examples and additional identities. CAR19.4 now supplies the full convex gauge and strict Hahn–Banach separation argument. The finite-factor trace branch consumes the complete local CAR18 coefficient realization, CAR19 projective predual/compactness/fixed-point arguments, Constant8 projection comparison and ITP10 Hilbert/operator foundations; it does not require a general semifinite trace-weight theorem. The all-weight MG/BC/FC/CS subtype route and general ITP modular semifiniteness have their separate exact proof records. Exact current exercise versions and source limits are recorded in source-provenance.json#current_seven_lesson_complete_exercise_reconstruction. The three Grothendieck lessons contain fifteen numbered results and thirty solved exercises. The current derivation paths construct a completed lift, eliminate the completion kernel by the full numerical-reality/Gaussian argument, choose common states and improve the four-state constant by locally convergent power series and a proved scalar strip estimate. Norm-preserving functional extension and arbitrary compact dual balls are supplied in full in the completion lesson. The direct nonunital route constructs two-sided positive contractions with both δ/4 errors, then takes a limit in the projective-tensor dual ball. The optional canonical bidual identity and every original exercise duty remain. The canonical polar input consumes only the full CF/MG/CP/ODF/NJ/PCY, positive-part coefficient, state-predual bidual and concrete support/polar proofs recorded in source-provenance.json#current_grothendieck_free_foundation_and_architecture; it does not consume a general representation extension, Sakai theorem or weight theory. The constant-CAR modular intersection consumes MG0–1 and the MG3 every-weight lower bound, together with complete CS0–3, BC1–3 and FC1–5. Its exact acyclic foundation graph and actual proof/source/version readings are in source-provenance.json#current_constant_car_all_weight_free_foundations. The full CF/SC/SF/CP/GNS/FF/CV/GW/NF/EW/BG/BW/WF/WR/MW/RF/AL/PC scopes are retained, including arbitrary faithful n.s.f. weights, infinite values and closed domains. NF uses FF4 and the initial invariant-form covariance, not the later NF-dependent FF GNS appendix; GW uses only the earlier elementary WF2 bounded-net fact. The product coefficient resolvent supplies the upper bound, so general MG4 type-III corner transport, KMS uniqueness and arbitrary-cocycle realization are not inputs. Constant-CAR11 supplies the concrete predual and full ultraweak closure, corner factoriality and circle/Fourier normalization from tensor-completion8.4. Product/CAR/ITP application premises retain their separately recorded scopes. The constant-CAR lesson contains eight numbered results and twelve complete solved exercises. The selected constant-CAR weight route consumes the literal proof versions collected in the reviewed weight foundations. This component contains the BG/BW/full-graph route and the CV4 CC BY4.0 attribution and mathematical modification notice. Each proof is identified by its exact selected source version. Complete selected source/version/hash/character locators are retained in source-provenance.json. ## Spatial commutation and arbitrary product supports The spatial proof component supplies STP1–19 at arbitrary representation, Hilbert-space and index cardinality, including nonfaithful states. Its bounded separate spectral bands prove the whole tensor involution graph without a product-measure prerequisite. The domination/amplification/corner proof removes the standard-representation restriction. Its product-state support is a decreasing finite-set net; its central-carrier limit gives the distinct normal GNS kernel. ITP16 supplies coefficient separability and the general faithful product modular graph; CAR15.9 computes the endpoint supports of its actual supported-column model. The exact acyclic consumed graph and retained versions are in source-provenance.json#current_spatial_tensor_and_arbitrary_product_supports. Generic abstract C*-tensor norms,bidual extensions,general inner-flow implementation and density/perturbation are distinct proof scopes. All20 original statements and22 literal whole solution blocks remain. ## General semifiniteness at the original normal-state scope The complete component supplies countability, full pointed support corners, arbitrary matrix NSF traces and nonzero-corner transfer, general factor trace uniqueness, actual trace-integrable normal-state densities, full unbounded centralizer perturbation/inverse domains, the affiliated Laplace generator, general-center continuous internal implementation, and the complete Borel-selection and MT/TI/WG/RD selected proof bodies. ITP Section8 reconstructs both implications using its original sequence, separable-predual and arbitrary normal-state hypotheses. The exact acyclic graph, source versions, free human reading boundaries and distinct reuse terms are in source-provenance.json#current_general_semifiniteness_free_foundations. The lesson contains thirteen numbered results and twelve solved exercises. ## Abstract tensor norms and universal biduals [The complete component](components/abstract-tensor-and-universal-bidual-foundations.md) constructs the generic minimal norm, full injective tensor maps, unit padding, arbitrary block regrouping, four-positive-functional decomposition, universal state representation, concrete-predual restriction isometry, bidual multiplication, normal extension and full unit-ball image, central kernel, entire corner predual and globally normal inverse. The exact retained scalar/coefficient bodies and current GNS/cyclic/density proof versions are bound in source-provenance.json#current_abstract_tensor_and_universal_bidual_free_foundations. Local scalar positivity and real Hilbert closure proofs close the two small auxiliary implications. ITPSection2 uses these proofs at its original mathematical scope. The Section8 semifiniteness criterion and its stated hypotheses are separate from the abstract tensor/bidual construction. ## Finite-state operator-space realization [The complete lesson](src/abstract-operator-spaces.md) supplies finite state-set compactness and the strict positive-coefficient separation step by distance to the nonnegative orthant, the finite Gram quotient, full matrix contractivity, norm detection and the arbitrary Hilbert direct sum. Its exact scalar/Hilbert prerequisites are the retained CF1–10 and full current MG01, as bound in source-provenance.json#current_abstract_operator_space_finite_state_closure. No completely bounded extension/factorization theorem or omitted thesis state-selection proof is consumed. All3 original statements and6 whole solved exercises retain their full mathematical obligations. ## Complete matrix dilation and bidual arguments [The complete extension lesson](src/completely-bounded-extension.md) supplies the explicit matrix-unit unitary and every dilation corner, plus the full finite-matrix bidual norm, product and amplification identities. Its consumed closure uses exact retained CF1–10/CP01–06, MG/PCY/ODF arguments and scalar universal state-coefficient bidual construction, the whole finite-target scalar extension and arbitrary-Hilbert limit from completely-positive-finite-models Section2, and the entire unital dilation proof from completely-positive-lifting. Every current input is versioned in source-provenance.json#current_completely_bounded_extension_free_closure. The scalar/Hilbert references of these selected bodies are rebound to the exact retained CF proofs. The lesson contains eight numbered results and nine solved exercises. ## Full trace-adjoint and rational-channel inputs [The complete tracial lesson](src/tracial-adjoints-and-rational-matrix-models.md) proves its full P00–P06 scalar/matrix/Hilbert inputs, ordinary normal cp trace adjoint, weighted Hilbert norm bound and both rational-record Kraus maps, with the entire commutator inequality. Exact retained CF1–10/CP01–06 and first/second-variable coefficient conventions are bound in source-provenance.json#current_tracial_adjoint_and_rational_channel_free_closure. No general Radon–Nikodym theorem,injectivity/semidiscreteness theorem or Haagerup article body is a premise of this construction. The tracial-adjoint lesson contains three numbered results and ten solved exercises. The following trace-preserving lesson has a separate injectivity-to-semidiscreteness incoming duty, which is not claimed closed by this record. ## Exact faithful-trace finite-model inputs [Trace-preserving finite models](src/trace-preserving-finite-models.md) uses the direct faithful-trace hypertrace Section5.1 matrix construction, exact trace realization/density/spatial/scalar proofs, the qualified weighted adjoint/rational channel and bounded-polar argument. Its N1–N3 prove normal unital maps and trace-2-norm approximation from the original subunital models. Exact35-node route and full selected versions are in source-provenance.json#current_trace_preserving_finite_model_free_inputs. The stronger center-valued finite/semifinite and continuous-core branches are not required here. The trace-preserving lesson contains five numbered results and ten solved exercises. ## Natural cones, exact marginals and semidiscrete models The complete NC00–NC08 proof now binds the frozen scalar, spectral, closed-form and full modular graphs at exact versions. NC00c constructs the common analytic multiplication algebra with both bounded ideals, conjugation and all complex-power domains. NC02 proves the full form operator-domain criterion; CG07 proves actual ultraweak corner transport. CG01–CG09a precedes CR00–CR07; CG10 then realizes every normal positive functional on an arbitrary algebra. The independent NJ01–NJ06 argument supplies norm-additive normal positive parts. Tensor Lemma2.1 includes full support normalization and exact marginal correction. Semidiscrete Theorem2.1 has its full generic converse,with all seven result inputs specified. The tensor component has all eleven result routes;the seven-result semidiscrete component has its separately specified proof scope. All18 original statements and13 whole solved exercises remain. Exact versions and the acyclic graph are in source-provenance.json#current_natural_cone_and_exact_marginal_free_inputs. ## Complete tensor nuclearity and type I inputs TN07 proves quotient completeness using summable representatives, the exact kernel-distance limits, the C*-identity and the closed range of a homomorphism. Its predecessor is the complete positive approximate-identity F09 and frozen CF1–10. The universal predual and transported bidual product, ODF06 positive-matrix density and the full cone/marginal argument supply tensor Theorem3.1 without a cyclicity, faithful-state or separability restriction. All four formerly separate result routes3.1,4.1,4.2,5.1 are now supplied; all eleven original statements and seven whole solutions remain. The type I proof consumes only H00–H02, bounded polar T04a, C01–C02 and central contact C04 with exact frozen calculus/Hilbert bindings, and its complete local irreducible norm-detection proof. No general type classification or comparability theorem is imported. Corollary4.2 retains the dual trace-class norm; the coefficient complete-order identification is not asserted isometric for the operator norm. Full versions and the acyclic graph are in source-provenance.json#current_complete_tensor_nuclearity_free_inputs. ## Complete nuclear-bidual and extension inputs All six original numbered arguments and eight full solutions have complete free mathematical input routes. The proofs use the exact BC1–BC5 graph versions identified in the source register. The exact quotient, central preadjoint inverse, nonunital dilation, finite central covers, core/trace/corner transfer and trace-class predual norm are preserved. Coordinate duality, cyclic central support and interval models are supplied in full. Exact proof record: source-provenance.json#current_complete_nuclear_bidual_extension_free_inputs. - abf/CF1-10 ← declared scalar/set primitives and complete written foundation - abf/MG01 ← abf/CF1-10 - abf/MG05 ← abf/CF1-10 - abf/PCY01 ← abf/CF1-10, abf/MG05 - abf/F09 ← abf/CF1-10 - abf/PCY02 ← abf/PCY01, abf/F09 - abf/MG02 ← abf/MG01, abf/CF1-10 - abf/ODF02 ← abf/F09, abf/CF1-10 - abf/ABF-positive-norm-criterion ← abf/CF1-10 - abf/PCY03 ← abf/PCY02, abf/MG02, abf/ODF02, abf/ABF-positive-norm-criterion - abf/PCY04 ← abf/PCY03, abf/MG01, abf/CF1-10 - abf/ABF-four-positive-parts ← abf/MG01, abf/PCY03, abf/PCY04, abf/CF1-10 - abf/MG03 ← abf/MG01, abf/MG02, abf/CF1-10 - abf/ODF03 ← abf/ODF02, abf/CF1-10 - abf/ABF-real-Hilbert-closure ← abf/CF1-10 - abf/ODF04 ← abf/ODF03, abf/ABF-real-Hilbert-closure - abf/ODF05 ← abf/ODF04, abf/CF1-10 - abf/MG04 ← abf/MG03, abf/CF1-10 - tensor/CF1-10 ← declared scalar/set primitives and complete written foundation - tensor/SF0-basic-Hilbert ← tensor/CF1-10 - tensor/CP01-06 ← tensor/CF1-10, tensor/SF0-basic-Hilbert - tensor/ODF01 ← tensor/CP01-06, tensor/CF1-10 - abf/ODF06 ← abf/ODF05, abf/MG04, abf/F09, abf/CF1-10, tensor/ODF01 - abf/ODF07 ← abf/ODF06, abf/MG04, tensor/ODF01 - abf/CP01-06 ← tensor/CP01-06 - abf/ABF-predual-restriction ← abf/ABF-four-positive-parts, abf/MG03, abf/ODF07, abf/CP01-06 - abf/ABF-bidual-product ← abf/ABF-predual-restriction, abf/ODF06, abf/CP01-06, abf/CF1-10 - abf/ABF-normal-extension ← abf/ABF-bidual-product, abf/ODF02, abf/ODF07, abf/CP01-06 - abf/ABF-central-quotient ← abf/ABF-normal-extension, abf/F09, abf/CP01-06, abf/CF1-10 - semidiscrete/CF1-10 ← declared scalar/set primitives and complete written foundation - semidiscrete/MG01 ← semidiscrete/CF1-10 - semidiscrete/MG02 ← semidiscrete/MG01, semidiscrete/CF1-10 - semidiscrete/MG03 ← semidiscrete/MG01, semidiscrete/MG02, semidiscrete/CF1-10 - semidiscrete/MG04 ← semidiscrete/MG03, semidiscrete/CF1-10 - semidiscrete/SF0-basic-Hilbert ← semidiscrete/CF1-10 - semidiscrete/CP01-06 ← semidiscrete/CF1-10, semidiscrete/SF0-basic-Hilbert - semidiscrete/CPFM-2 ← semidiscrete/MG01, semidiscrete/MG04, semidiscrete/CF1-10, semidiscrete/CP01-06 - semidiscrete/D1 ← semidiscrete/MG04, semidiscrete/CP01-06, semidiscrete/CF1-10, semidiscrete/CPFM-2 - semidiscrete/TA-P03 ← semidiscrete/CF1-10 - semidiscrete/D2 ← semidiscrete/TA-P03, semidiscrete/CF1-10 - semidiscrete/H-SEP ← semidiscrete/CF1-10 - semidiscrete/SD3.1 ← semidiscrete/D1, semidiscrete/D2, semidiscrete/H-SEP, semidiscrete/CP01-06, semidiscrete/CF1-10 - cb/CF1-10 ← declared scalar/set primitives and complete written foundation - cb/MG01 ← cb/CF1-10 - cb/MG02 ← cb/MG01, cb/CF1-10 - cb/MG03 ← cb/MG01, cb/MG02, cb/CF1-10 - cb/MG04 ← cb/MG03, cb/CF1-10 - cb/CPFM-block-norm ← cb/MG04, cb/CF1-10 - cb/CP01-06 ← cb/CF1-10 - cb/CPFM-dual-ball-compactness ← cb/CP01-06, cb/CF1-10 - cb/CPFM-scalar-matrix-correspondence ← cb/MG04, cb/CF1-10 - cb/CPFM-positive-scalar-extension ← cb/MG01, cb/CF1-10 - cb/CPFM-arbitrary-H-extension ← cb/CPFM-block-norm, cb/CPFM-dual-ball-compactness, cb/CPFM-scalar-matrix-correspondence, cb/CPFM-positive-scalar-extension - NBE-injectivity-retraction-criterion ← semidiscrete/SD3.1, cb/CPFM-arbitrary-H-extension - tensor/MG01 ← tensor/CF1-10 - tensor/MG02 ← tensor/MG01, tensor/CF1-10 - tensor/MG03 ← tensor/MG01, tensor/MG02, tensor/CF1-10 - tensor/MG04 ← tensor/MG03, tensor/CF1-10 - NBE-amplification-corner-opposite-products ← NBE-injectivity-retraction-criterion, tensor/MG04, tensor/CF1-10 - tensor/H00-02 ← tensor/CF1-10 - tensor/H-T04a ← tensor/H00-02, tensor/CF1-10 - tensor/C01-02 ← tensor/H00-02, tensor/H-T04a, tensor/CF1-10 - NBE1.1 ← abf/ABF-normal-extension, abf/ABF-central-quotient, NBE-amplification-corner-opposite-products, tensor/C01-02, tensor/CF1-10, tensor/CP01-06 - tensor/MTN-Hilbert ← tensor/CF1-10 - tensor/MTN-compressions ← tensor/MTN-Hilbert, tensor/CF1-10 - tensor/MTN-matrices ← tensor/MG03, tensor/MG04 - tensor/MTN-independence ← tensor/MTN-compressions, tensor/MTN-matrices - tensor/MTN-contractivity ← tensor/MTN-independence, tensor/MTN-Hilbert - tensor/CPFM-2 ← tensor/MG01, tensor/MG04, tensor/CF1-10, tensor/CP01-06 - tensor/LIFT-UCP ← tensor/MG04, tensor/CF1-10 - tensor/CPFM-MinFunctor ← tensor/CPFM-2, tensor/LIFT-UCP, tensor/MTN-contractivity, tensor/MG04, tensor/CF1-10 - tensor/CPFM-MatrixNorm ← tensor/MTN-contractivity, tensor/MG04, tensor/CF1-10 - tensor/MG05 ← tensor/CF1-10 - tensor/PCY01 ← tensor/CF1-10, tensor/MG05 - tensor/F09 ← tensor/CF1-10 - tensor/PCY02 ← tensor/PCY01, tensor/F09 - tensor/ODF02 ← tensor/F09, tensor/CF1-10 - tensor/ABF-positive-norm-criterion ← tensor/CF1-10 - tensor/PCY03 ← tensor/PCY02, tensor/MG02, tensor/ODF02, tensor/ABF-positive-norm-criterion - tensor/PCY04 ← tensor/PCY03, tensor/MG01, tensor/CF1-10 - tensor/ABF-four-positive-parts ← tensor/MG01, tensor/PCY03, tensor/PCY04, tensor/CF1-10 - tensor/TENSOR-nonunital-state-coefficient ← tensor/ABF-four-positive-parts, tensor/MG01, tensor/MG02, tensor/CF1-10, tensor/CPFM-2 - tensor/H-COMPACT ← tensor/CF1-10, tensor/CP01-06 - tensor/H-SEP ← tensor/CF1-10 - tensor/TN07 ← tensor/CF1-10, tensor/F09 - tensor/TN01-05 ← tensor/MTN-contractivity, tensor/MTN-Hilbert, tensor/CPFM-MinFunctor, tensor/CPFM-MatrixNorm, tensor/CPFM-2, tensor/LIFT-UCP, tensor/TENSOR-nonunital-state-coefficient, tensor/H-COMPACT, tensor/H-SEP, tensor/TN07 - tensor/TP1.1 ← tensor/TN01-05, tensor/MG01, tensor/MG04, tensor/CF1-10, tensor/H-COMPACT, tensor/TENSOR-nonunital-state-coefficient - tensor/TP1.2 ← tensor/TP1.1, tensor/MG04, tensor/CP01-06, tensor/CF1-10 - tensor/TP1.3 ← tensor/TN01-05, tensor/H-SEP, tensor/H-COMPACT, tensor/CF1-10 - tensor/TP1.5 ← tensor/TP1.2, tensor/MG04, tensor/CF1-10 - tensor/TP-dominated-complete-order ← tensor/CP01-06, tensor/CF1-10, tensor/MG04 - tensor/NJ01-06 ← tensor/CF1-10, tensor/CP01-06, tensor/MG01 - tensor/CG01 ← tensor/CF1-10, tensor/CP01-06 - tensor/NC01 ← tensor/CG01, tensor/CF1-10, tensor/CP01-06 - tensor/SC00-10 ← tensor/CF1-10 - tensor/elementary-scalar ← declared scalar/set primitives and complete written foundation - tensor/TC8.4-disk-quarter-phase ← tensor/elementary-scalar - tensor/constant11.4-exact-circle-Cauchy-Fourier-normalization ← tensor/TC8.4-disk-quarter-phase, tensor/elementary-scalar - tensor/SF-SB0-6-and-full-SF1-4 ← tensor/SC00-10, tensor/SF0-basic-Hilbert, tensor/constant11.4-exact-circle-Cauchy-Fourier-normalization - tensor/FF-scalar-interchange-and-FF1-3 ← tensor/SC00-10, tensor/SF-SB0-6-and-full-SF1-4, tensor/constant11.4-exact-circle-Cauchy-Fourier-normalization - tensor/MF-SB-scalar-vector-kernel ← tensor/SC00-10, tensor/FF-scalar-interchange-and-FF1-3, tensor/SF-SB0-6-and-full-SF1-4 - tensor/BD1-5 ← tensor/CF1-10, tensor/SF0-basic-Hilbert - tensor/BG1-6 ← tensor/MF-SB-scalar-vector-kernel, tensor/BD1-5, tensor/SF-SB0-6-and-full-SF1-4 - tensor/BW1-5 ← tensor/BG1-6, tensor/BD1-5, tensor/SF-SB0-6-and-full-SF1-4 - tensor/NC00a ← tensor/BG1-6, tensor/BW1-5 - tensor/ODF03 ← tensor/ODF02, tensor/CF1-10 - tensor/ABF-real-Hilbert-closure ← tensor/CF1-10 - tensor/ODF04 ← tensor/ODF03, tensor/ABF-real-Hilbert-closure - tensor/ODF05 ← tensor/ODF04, tensor/CF1-10 - tensor/NC01b ← tensor/NC01, tensor/NC00a, tensor/BG1-6, tensor/BW1-5, tensor/ODF01, tensor/ODF05, tensor/CP01-06, tensor/CF1-10, tensor/H-COMPACT - tensor/WF2-pure-bounded-net-supremum ← tensor/CF1-10 - tensor/GW1-5 ← tensor/CF1-10, tensor/CP01-06, tensor/WF2-pure-bounded-net-supremum - tensor/FF4-closed-form ← tensor/CF1-10, tensor/SF-SB0-6-and-full-SF1-4 - tensor/GNS1-5 ← tensor/CF1-10 - tensor/ST12 ← tensor/CF1-10, tensor/CP01-06, tensor/BD1-5, tensor/GNS1-5 - tensor/STC-vector-series-state ← tensor/GNS1-5, tensor/CP01-06, tensor/ST12 - tensor/NF1-5 ← tensor/GW1-5, tensor/FF4-closed-form, tensor/SF-SB0-6-and-full-SF1-4, tensor/CP01-06, tensor/ST12, tensor/STC-vector-series-state - tensor/FF5-initial-invariant-form-covariance ← tensor/FF4-closed-form - tensor/CV1-4 ← tensor/CF1-10, tensor/CP01-06, tensor/SF0-basic-Hilbert - tensor/EW1-5 ← tensor/GW1-5, tensor/NF1-5, tensor/FF4-closed-form, tensor/FF5-initial-invariant-form-covariance, tensor/CV1-4 - tensor/CI1-3 ← tensor/SF-SB0-6-and-full-SF1-4 - tensor/WF1-6-canonical-weight ← tensor/BG1-6, tensor/BW1-5, tensor/CP01-06, tensor/SF-SB0-6-and-full-SF1-4, tensor/WF2-pure-bounded-net-supremum - tensor/WR1-7 ← tensor/GW1-5, tensor/NF1-5, tensor/EW1-5, tensor/ST12, tensor/CP01-06, tensor/CI1-3, tensor/BG1-6, tensor/BW1-5, tensor/WF1-6-canonical-weight - tensor/MW1-4 ← tensor/WR1-7, tensor/BW1-5, tensor/SF-SB0-6-and-full-SF1-4, tensor/ST12, tensor/CP01-06 - tensor/NC00-interface ← tensor/NC01b, tensor/BG1-6, tensor/BW1-5, tensor/WR1-7, tensor/MW1-4, tensor/SF-SB0-6-and-full-SF1-4 - tensor/NC01a ← tensor/NC00a, tensor/BW1-5, tensor/CF1-10 - tensor/NC02 ← tensor/FF4-closed-form, tensor/FF5-initial-invariant-form-covariance, tensor/SF-SB0-6-and-full-SF1-4, tensor/CF1-10 - tensor/NC03 ← tensor/NC00-interface, tensor/NC00a, tensor/NC01a, tensor/NC02, tensor/SF-SB0-6-and-full-SF1-4 - tensor/NC00c ← tensor/NC00-interface, tensor/FF-scalar-interchange-and-FF1-3, tensor/SF-SB0-6-and-full-SF1-4, tensor/BW1-5 - tensor/NC04 ← tensor/NC03, tensor/NC00c, tensor/SF-SB0-6-and-full-SF1-4 - tensor/NC05 ← tensor/NC04, tensor/FF-scalar-interchange-and-FF1-3, tensor/SF-SB0-6-and-full-SF1-4 - tensor/NC06 ← tensor/NC05, tensor/NC01a, tensor/NC00c, tensor/BW1-5 - tensor/NC07 ← tensor/NC00-interface, tensor/FF5-initial-invariant-form-covariance, tensor/SF-SB0-6-and-full-SF1-4 - tensor/CG02-06 ← tensor/CG01, tensor/NC05, tensor/NC06, tensor/NC07, tensor/CF1-10, tensor/CP01-06 - tensor/CG07 ← tensor/CG02-06, tensor/ST12, tensor/CP01-06, tensor/CF1-10 - tensor/NC08 ← tensor/NC01b, tensor/NC03, tensor/NC04, tensor/NC05, tensor/NC06, tensor/NC07, tensor/BG1-6, tensor/BW1-5 - tensor/CG08-09a ← tensor/CG07, tensor/NC08, tensor/CF1-10, tensor/CP01-06 - tensor/CR01 ← tensor/SC00-10, tensor/FF-scalar-interchange-and-FF1-3, tensor/SF-SB0-6-and-full-SF1-4, tensor/constant11.4-exact-circle-Cauchy-Fourier-normalization - tensor/CR02-03 ← tensor/CR01, tensor/NC08, tensor/CG08-09a, tensor/SF-SB0-6-and-full-SF1-4 - tensor/CR04-05 ← tensor/CR02-03, tensor/CG07, tensor/CG08-09a, tensor/CF1-10 - tensor/CR06-07 ← tensor/CR04-05, tensor/CG02-06, tensor/CP01-06, tensor/CF1-10 - tensor/CG10 ← tensor/CG08-09a, tensor/CR06-07, tensor/CG07 - tensor/TP2.1 ← tensor/TP1.1, tensor/TP1.5, tensor/TP-dominated-complete-order, tensor/NJ01-06, tensor/CG10, tensor/CG02-06, tensor/MG01, tensor/MG04, tensor/CF1-10 - tensor/ODF06 ← tensor/ODF05, tensor/MG04, tensor/F09, tensor/CF1-10, tensor/ODF01 - tensor/ODF07 ← tensor/ODF06, tensor/MG04, tensor/ODF01 - tensor/ABF-predual-restriction ← tensor/ABF-four-positive-parts, tensor/MG03, tensor/ODF07, tensor/CP01-06 - tensor/ABF-bidual-product ← tensor/ABF-predual-restriction, tensor/ODF06, tensor/CP01-06, tensor/CF1-10 - tensor/TN06 ← tensor/TN01-05, tensor/TN07, tensor/CF1-10 - tensor/CPFM4.3 ← tensor/CPFM-MinFunctor, tensor/CPFM-MatrixNorm, tensor/TN01-05, tensor/CF1-10 - tensor/CPFM1.1-1.2 ← tensor/CF1-10 - tensor/TP3.1 ← tensor/TP1.1, tensor/TP1.2, tensor/TP1.3, tensor/TP2.1, tensor/CG07, tensor/CG08-09a, tensor/CG10, tensor/TP-dominated-complete-order, tensor/ABF-predual-restriction, tensor/ABF-bidual-product, tensor/ODF06, tensor/ODF07, tensor/TN06, tensor/TN07, tensor/F09, tensor/CPFM4.3, tensor/CPFM1.1-1.2, tensor/H-SEP, tensor/MG04, tensor/CF1-10 - cb/ST-unital-dilation ← cb/MG04, cb/CF1-10 - NBE2.1 ← tensor/TP3.1, tensor/TN01-05, cb/CPFM-arbitrary-H-extension, cb/ST-unital-dilation, tensor/F09, tensor/CF1-10 - NBE-series-domination-comparison ← tensor/CP01-06, tensor/CF1-10 - weight/CF1-10 ← declared scalar/set primitives and complete written foundation - core/CF1-to-CF10 ← weight/CF1-10 - core/SF0 ← core/CF1-to-CF10 - core/SC00-to-SC07 ← core/CF1-to-CF10 - core/SC8-to-SC9 ← core/CF1-to-CF10, core/SC00-to-SC07 - core/SF-SB0-to-SB6 ← core/CF1-to-CF10, core/SC00-to-SC07, core/SC8-to-SC9, core/SF0 - core/CP1-to-CP6 ← core/CF1-to-CF10, core/SF0 - core/BD1-to-BD3 ← core/SF0, core/SF-SB0-to-SB6 - core/BD4-to-BD5 ← core/BD1-to-BD3, core/CP1-to-CP6 - core/owned-orthogonal-normal-vector-state-weight ← core/CF1-to-CF10, core/SF0, core/SF-SB0-to-SB6, core/CP1-to-CP6, core/BD4-to-BD5 - core/ST1-to-ST2 ← core/CF1-to-CF10, core/CP1-to-CP6, core/SF-SB0-to-SB6, core/BD1-to-BD3, core/BD4-to-BD5 - core/owned-direct-sum-normal-representation ← core/owned-orthogonal-normal-vector-state-weight, core/ST1-to-ST2, core/CP1-to-CP6 - core/owned-full-multiplication-involution-closability ← core/owned-direct-sum-normal-representation, core/SF0 - core/FF-scalar-and-FF1 ← core/CF1-to-CF10, core/SC00-to-SC07, core/SC8-to-SC9 - core/SF4 ← core/CF1-to-CF10, core/SC8-to-SC9 - core/MF-SB1-to-SB4 ← core/CF1-to-CF10, core/SC00-to-SC07, core/SC8-to-SC9, core/FF-scalar-and-FF1, core/SF4 - core/BG1-to-BG6 ← core/SF0, core/SF-SB0-to-SB6, core/BD1-to-BD3, core/MF-SB1-to-SB4 - core/owned-arbitrary-algebra-standard-pair ← core/owned-orthogonal-normal-vector-state-weight, core/owned-direct-sum-normal-representation, core/owned-full-multiplication-involution-closability, core/BG1-to-BG6 - NBE-commutant-permanence ← NBE-series-domination-comparison, NBE-amplification-corner-opposite-products, core/owned-arbitrary-algebra-standard-pair - weight/SC00-10 ← weight/CF1-10 - NBE-invariant-mean-R ← weight/SC00-10, tensor/CF1-10, tensor/CP01-06 - NBE-averaging-injectivity ← NBE-invariant-mean-R, NBE-commutant-permanence, tensor/CP01-06, tensor/CF1-10 - core/owned-full-regular-Hilbert-and-product-integration ← core/SC00-to-SC07, core/CF1-to-CF10 - NBE-real-regular-representation ← core/owned-full-regular-Hilbert-and-product-integration, weight/SC00-10, tensor/CP01-06, tensor/CF1-10 - NBE-real-core-injective ← NBE-averaging-injectivity, NBE-real-regular-representation - core/CI1-to-CI3 ← core/CF1-to-CF10, core/SF-SB0-to-SB6 - core/GDW4-full-pointwise-graph ← core/owned-full-regular-Hilbert-and-product-integration, core/CI1-to-CI3, core/SC00-to-SC07, core/CF1-to-CF10 - core/SC00-to-SC09 ← weight/SC00-10 - core/SF1-to-SF3 ← core/SF-SB0-to-SB6, core/CP1-to-CP6, core/CF1-to-CF10, core/SC00-to-SC09 - weight/SF0-basic-Hilbert ← weight/CF1-10 - weight/elementary-scalar ← declared scalar/set primitives and complete written foundation - weight/TC8.4-disk-quarter-phase ← weight/elementary-scalar - weight/constant11.4-exact-circle-Cauchy-Fourier-normalization ← weight/TC8.4-disk-quarter-phase, weight/elementary-scalar - weight/SF-SB0-6-and-full-SF1-4 ← weight/SC00-10, weight/SF0-basic-Hilbert, weight/constant11.4-exact-circle-Cauchy-Fourier-normalization - weight/FF-scalar-interchange-and-FF1-3 ← weight/SC00-10, weight/SF-SB0-6-and-full-SF1-4, weight/constant11.4-exact-circle-Cauchy-Fourier-normalization - core/FF-scalar-interchange-and-FF1 ← weight/FF-scalar-interchange-and-FF1-3 - core/RF5-full-generator ← core/SF-SB0-to-SB6, core/SF1-to-SF3, core/SF0, core/SC8-to-SC9, core/FF-scalar-interchange-and-FF1, core/CF1-to-CF10 - core/WF5-bounded-monotone ← core/CF1-to-CF10, core/SF0, core/SF-SB0-to-SB6, core/BD1-to-BD3 - core/GW1-to-GW5 ← core/CF1-to-CF10, core/SF0, core/SF-SB0-to-SB6, core/WF5-bounded-monotone, core/BD4-to-BD5 - core/FF4-form-representation ← core/CF1-to-CF10, core/SF-SB0-to-SB6 - core/GNS2-to-GNS5 ← core/CF1-to-CF10, core/SC8-to-SC9 - core/STC-known-normal-state ← core/GNS2-to-GNS5, core/CP1-to-CP6, core/ST1-to-ST2 - core/NF1-to-NF5 ← core/GW1-to-GW5, core/CF1-to-CF10, core/SF0, core/SF-SB0-to-SB6, core/FF4-form-representation, core/STC-known-normal-state, core/CP1-to-CP6, core/ST1-to-ST2, core/WF5-bounded-monotone, core/BD4-to-BD5 - core/FF5-form-invariance ← core/FF4-form-representation, core/SF-SB0-to-SB6 - core/CV1-to-CV4 ← core/CF1-to-CF10 - core/EW1-to-EW5 ← core/GW1-to-GW5, core/NF1-to-NF5, core/CF1-to-CF10, core/SF0, core/SF-SB0-to-SB6, core/FF4-form-representation, core/FF5-form-invariance, core/CV1-to-CV4, core/CP1-to-CP6, core/BD4-to-BD5 - core/BW1-to-BW5 ← core/BG1-to-BG6, core/CF1-to-CF10, core/SF0, core/SF-SB0-to-SB6, core/BD1-to-BD3 - core/WF1-to-WF6 ← core/BW1-to-BW5, core/BG1-to-BG6, core/CF1-to-CF10, core/SF0, core/SF-SB0-to-SB6, core/BD1-to-BD3, core/BD4-to-BD5 - core/WR1-to-WR7 ← core/GW1-to-GW5, core/NF1-to-NF5, core/EW1-to-EW5, core/CV1-to-CV4, core/CP1-to-CP6, core/ST1-to-ST2, core/CI1-to-CI3, core/BG1-to-BG6, core/BW1-to-BW5, core/WF1-to-WF6 - core/MW1-to-MW4 ← core/WR1-to-WR7, core/WF1-to-WF6, core/BW1-to-BW5, core/BG1-to-BG6, core/CI1-to-CI3, core/CP1-to-CP6, core/ST1-to-ST2 - core/BC1-to-BC5 ← core/GW1-to-GW5, core/NF1-to-NF5, core/WR1-to-WR7, core/MW1-to-MW4, core/CI1-to-CI3, core/SF1-to-SF3, core/CP1-to-CP6, core/CF1-to-CF10 - core/KT1-to-KT5 ← core/GW1-to-GW5, core/WR1-to-WR7, core/MW1-to-MW4, core/EW1-to-EW5, core/CP1-to-CP6, core/SF-SB0-to-SB6, core/SF1-to-SF3, core/SF4, core/FF-scalar-interchange-and-FF1, core/CF1-to-CF10, core/SC00-to-SC09 - core/MA1-to-MA2 ← core/KT1-to-KT5, core/WR1-to-WR7, core/MW1-to-MW4, core/CI1-to-CI3, core/GW1-to-GW5, core/SF1-to-SF3, core/SF4, core/CP1-to-CP6 - core/owned-full-centralizer-forward-action ← core/MA1-to-MA2 - core/CZ1-to-CZ3 ← core/owned-full-centralizer-forward-action, core/GW1-to-GW5, core/EW1-to-EW5, core/SF-SB0-to-SB6, core/SF1-to-SF3, core/CP1-to-CP6, core/CF1-to-CF10 - core/AS1-first-strip-lemma ← core/SF4 - core/KU1-to-KU4 ← core/KT1-to-KT5, core/WR1-to-WR7, core/MW1-to-MW4, core/EW1-to-EW5, core/CP1-to-CP6, core/SF1-to-SF3, core/SF4, core/FF-scalar-interchange-and-FF1, core/CF1-to-CF10 - core/owned-given-weight-GNS-normality ← core/GW1-to-GW5, core/NF1-to-NF5, core/FF4-form-representation, core/WF5-bounded-monotone, core/STC-known-normal-state, core/CP1-to-CP6, core/ST1-to-ST2 - core/owned-given-weight-recovery-and-modular-action ← core/EW1-to-EW5, core/WR1-to-WR7, core/WF1-to-WF6, core/BW1-to-BW5, core/MW1-to-MW4, core/CI1-to-CI3, core/owned-given-weight-GNS-normality - core/owned-KMS-characterization-analytic-core-and-trace-criterion ← core/KT1-to-KT5, core/KU1-to-KU4, core/SF1-to-SF3, core/owned-given-weight-recovery-and-modular-action - weight/FF4-closed-form ← weight/CF1-10, weight/SF-SB0-6-and-full-SF1-4 - core/FF4-full-closed-form-representation ← weight/FF4-closed-form - core/FF5-standalone-form-invariance ← core/FF4-full-closed-form-representation, core/SF-SB0-to-SB6 - core/owned-centralizer-density-domain-modular-normalization ← core/BC1-to-BC5, core/MA1-to-MA2, core/CZ1-to-CZ3, core/AS1-first-strip-lemma, core/owned-KMS-characterization-analytic-core-and-trace-criterion, core/owned-given-weight-recovery-and-modular-action, core/FF5-standalone-form-invariance - core/owned-full-dual-weight-and-core-trace ← core/GDW4-full-pointwise-graph, core/RF5-full-generator, core/owned-centralizer-density-domain-modular-normalization, core/owned-given-weight-recovery-and-modular-action, core/owned-full-regular-Hilbert-and-product-integration, core/BG1-to-BG6, core/BW1-to-BW5, core/WF1-to-WF6, core/WR1-to-WR7, core/MW1-to-MW4 - trace/CF1-10 ← declared scalar/set primitives and complete written foundation - trace/CP01-06 ← trace/CF1-10 - trace/H-COMPACT ← trace/CF1-10 - trace/P00 ← trace/CF1-10, trace/CP01-06 - trace/P01 ← trace/P00, trace/CF1-10 - trace/P03 ← trace/P00, trace/P01, trace/CF1-10 - trace/P05 ← trace/P01, trace/P03, trace/CF1-10 - trace/POLAR ← trace/CF1-10, trace/CP01-06, trace/P00, trace/P03 - trace/H-REP ← trace/CF1-10, trace/CP01-06, trace/H-COMPACT, trace/P05, trace/POLAR - trace/P04 ← trace/P00, trace/P01, trace/CF1-10 - trace/H-MD ← trace/CF1-10, trace/P00, trace/P01, trace/P04 - trace/H-HYPERTRACE ← trace/H-REP, trace/H-MD - trace/H-SEP ← trace/CF1-10 - trace/H-SP ← trace/CF1-10, trace/P00, trace/H-SEP - trace/H-FP ← trace/CF1-10, trace/P00, trace/P01, trace/P03, trace/POLAR - trace/H-PS ← trace/H-FP, trace/P03, trace/P01 - trace/H-U ← trace/CF1-10, trace/P03 - trace/H-DEN ← trace/H-SP, trace/H-SEP, trace/H-PS, trace/H-FP, trace/CP01-06, trace/H-U - trace/H-COM ← trace/H-REP, trace/P05, trace/CF1-10 - trace/H-SC ← trace/H-REP, trace/H-MD, trace/H-HYPERTRACE, trace/H-DEN, trace/H-SP, trace/H-FP, trace/H-COM - trace/H-5.1 ← trace/H-SC, trace/H-SP, trace/H-SEP, trace/H-REP, trace/POLAR, trace/CF1-10, trace/P04 - NBE-threshold-cut ← tensor/H00-02, tensor/CF1-10 - NBE-finite-trace-bootstrap ← trace/H-5.1, NBE-threshold-cut, NBE-amplification-corner-opposite-products, tensor/C01-02, tensor/CP01-06, tensor/CF1-10 - NBE-normal-coefficient-transfer ← NBE-real-regular-representation, tensor/CP01-06, tensor/CF1-10 - NBE-injective-semidiscrete ← NBE-real-core-injective, core/owned-full-dual-weight-and-core-trace, NBE-finite-trace-bootstrap, NBE-normal-coefficient-transfer - semidiscrete/Q1 ← semidiscrete/CF1-10 - semidiscrete/Q2 ← semidiscrete/Q1, semidiscrete/CF1-10 - semidiscrete/Q3 ← semidiscrete/Q2, semidiscrete/CF1-10 - semidiscrete/SD4.1 ← semidiscrete/CPFM-2 - semidiscrete/SD4.3 ← semidiscrete/Q3, semidiscrete/SD4.1, semidiscrete/MG04, semidiscrete/CF1-10 - NBE-predual-equivalence ← NBE-injective-semidiscrete, semidiscrete/SD4.3 - tensor/TP-CP-tensor-positivity ← tensor/CPFM-MinFunctor, tensor/LIFT-UCP, tensor/TN01-05, tensor/MG04, tensor/CF1-10 - tensor/TP4.1 ← tensor/TP3.1, tensor/TP1.1, tensor/TP-CP-tensor-positivity, tensor/TN01-05, tensor/MG01, tensor/MG04, tensor/CF1-10 - tensor/TP-coefficient-dual ← tensor/MG04, tensor/CF1-10 - tensor/TP-adjoint-dual ← tensor/TP-coefficient-dual, tensor/CF1-10 - tensor/TP4.2 ← tensor/TP3.1, tensor/TP4.1, tensor/TP1.1, tensor/TP-coefficient-dual, tensor/TP-adjoint-dual, tensor/CF1-10 - NBE3.1 ← NBE2.1, NBE1.1, NBE-commutant-permanence, NBE-predual-equivalence, tensor/TP4.2, abf/ABF-bidual-product - NBE3.2 ← NBE3.1, NBE1.1, abf/ABF-normal-extension, abf/ABF-central-quotient, NBE-injective-semidiscrete, NBE-amplification-corner-opposite-products - NBE4.1 ← abf/ABF-normal-extension, abf/ABF-central-quotient, tensor/TN07, tensor/F09, tensor/CF1-10, tensor/CP01-06 - NBE4.2 ← NBE4.1, NBE3.1, NBE-amplification-corner-opposite-products - NBE-order-laboratory ← tensor/TP-dominated-complete-order, tensor/TP1.1, tensor/CF1-10, tensor/F09 - NBE-coordinate-model ← tensor/CF1-10, tensor/CP01-06, abf/ABF-bidual-product - NBE-interval-model ← tensor/MG04, tensor/CF1-10, weight/SC00-10, tensor/TP3.1 - tensor/C04 ← tensor/C01-02, tensor/CF1-10 - NBE-cyclic-support ← tensor/C04, tensor/C01-02, tensor/TN07, tensor/ODF07, abf/ABF-central-quotient, tensor/CP01-06 - NBE-all8-solutions ← NBE1.1, NBE4.1, NBE3.1, NBE-order-laboratory, NBE-coordinate-model, NBE-interval-model, NBE-cyclic-support - COMPLETE-nuclear-bidual ← NBE1.1, NBE2.1, NBE3.1, NBE3.2, NBE4.1, NBE4.2, NBE-all8-solutions ## Complete averaging and injectivity inputs All twelve original numbered arguments and ten full solutions have complete free mathematical inputs. General Haar,scalar,vector,product and translation arguments are bound to their exact complete source versions. The finite-dimensional proof constructs matrix blocks. The type I proof constructs a full abelian corner, arbitrary orthogonal final projections, a unitary normal corner model and central product. No direct-integral or general type I classification proof is assumed. Existing core, trace/corner, normal transfer and trace-class predual proofs retain their actual complete versions. Exact proof record: source-provenance.json#current_complete_averaging_free_inputs. ## Complete free-group norm averaging inputs All seven original results and ten whole solved exercises have complete free mathematical inputs. Local proofs construct unique word reduction and the group law, arbitrary-index Hilbert completeness, regular unitaries and the faithful canonical trace, state continuity, the complete norm average and Neumann inverse, and the rank-one characters. Positive calculus and arbitrary-Hilbert adjoints use the exact complete retained CF1–10 component. The actual free human comparison is de la Harpe v1, Definition9 p.7 and complete Theorem14 pp.10–11, with its own unchanged distribution terms. Boundary actions, a countable-group reduction and K-theory are not admitted premises. Exact mathematical record: source-provenance.json#current_complete_free_group_averaging_inputs. ## Complete free-group projection inputs All seven original results and ten whole solved exercises retain their original scope. Complete PA1–5 proofs supply arbitrary-Hilbert compact spectra, the usual complete trace-class ideal and absolute trace, scalar Cauchy–Goursat and contour formulas, and holomorphic calculus for a general Banach-algebra element on any given neighborhood. The finite-rank unit term is retained in the two-representation resolvent identity. Earlier exact free-word/Hilbert/faithful-trace and CF1–10 components supply their complete selected inputs. Schick arXiv v5,Lemmas2.6,2.8,2.9,pp.7–11,provides the free method comparison at its stated distribution terms;external trace-ideal,K-theory density and general relative Hilbert-module theorems are not local premises. The entire proof prose and organization were reconstructed. Exact mathematical record: source-provenance.json#current_complete_free_group_projection_inputs. ## Complete central-sequence topology inputs TS1–6 proves the full Polish metric, Borel-refinement, analytic-separation, injective-image and category/open-mapping chain. Lemma3.1 and Theorem3.2 have their full Polish-group hypotheses. The central-sequence lesson contains ten numbered results and eleven solved exercises. Normal-predual/GNS/strong-star topology,general finite center-valued trace and finite AFD uniqueness have their full individual proof records. Tserunyan author notes,26November2025,Theorem12.6,p48,and Theorem13.3,pp51–52,provide the free source comparison. Their expression/PDF and earlier referenced premises are not imported. Exact record: source-provenance.json#current_complete_central_sequence_topology_inputs. ## Complete normal-functional and faithful-state topology inputs NT1–2 supplies the four-positive normal-functional decomposition, module and adjoint bounds, faithful-state predual density, actual Schwarz block argument and inverse-UCP multiplicativity, bounded strong-star/2-norm equivalence, and GNS separability. Exact qualification consumes eighteen whole earlier provider spans on a twelve-node ancestor graph; all are literal in the retained licensed frozen component, including the relocated full GNS2–5 argument. TS1–TS6 and NT1–NT2 supply the specified five topology result routes. Full remaining result and solved-exercise routes are specified in source-provenance.json#current_complete_central_sequence_inputs. General center-valued trace,phase/group-factor/type arguments and finite AFD uniqueness have separate complete proof records. The central-sequence lesson contains ten numbered results and eleven solved exercises. Exact record: source-provenance.json#current_complete_central_sequence_normal_topology_inputs. ## Arbitrary-center finite traces The complete PC0–7/FCT0–7 component retains its original programme licence and exact original/source-body correspondence; only navigation targets are adjusted. The current route checks every spectral, normal-predual, central support, finite cancellation, tiling and arbitrary-assembly predecessor. FCT1 proves a conditional stability lemma; FCT3 and FCT6 supply its premises before application, so the existence route is acyclic. Corollary1.2 applies to every finite algebra without a separability or countable-decomposition restriction. These trace and topology arguments supply nine result routes and all eleven solved-exercise input routes. Proposition6.1 uses the full AF1–AF5 finite AFD uniqueness construction. Exact record: source-provenance.json#current_complete_central_sequence_finite_trace_inputs. ## Complete current central-sequence lesson Every one of the ten original results and all eleven whole exercise arguments now has a full exact free prerequisite route. AF1–5 supplies finite-dimensional matrix decomposition and weighted trace projections, arbitrary scalar cuts, finite projection repair, dyadic approximation, exact nesting and the full normal tracial-completion identification. It uses no unproved corner amenability/AFD or arbitrary expectation theorem. All source hypotheses, conclusion scopes, constants and full solution obligations are retained; original literal snapshots remain provenance. Exact record: source-provenance.json#current_complete_central_sequence_inputs. ## Complete central-sequence quotient and exact lifts All six original result routes and all ten whole exercise routes are complete at the exact versions in source-provenance.json#current_complete_central_sequence_exact_lift_inputs. CQ1–7 supplies the C* quotient construction, faithful trace Hilbert isometry, complete-ball von Neumann argument and whole-domain normal automorphisms, cancellation of a finite subpiece in equivalent possibly infinite endpoints, countable infinite pieces with both state masses small, the direct minimal-projection scalar test, and full partition balancing. The hypotheses and complete solutions include prescribed endpoints and nonunital matrix support. ## Complete fullness, hypercentrality and all corners All six original results and all ten whole solved exercises are closed at the exact versions in source-provenance.json#current_complete_fullness_hypercentrality_inputs. FH0–5 supplies finite-factor trace normality without adding a hypothesis, whole-center finite halving, compact-orbit displacement, the exact finite-matrix normal tail map and its whole range, the complete L-infinity[0,1] product-R example, and both-square strong-star perturbation estimates. General-factor ordinary/some/every-ultrafilter selections, every nonzero corner, the full center, all original constants and all complete solution obligations are retained. The current route does not admit the presently inaccessible MathNet endpoint as a proof premise. ## Complete strong stability and tensor absorption All five original results and ten whole solved exercises are closed at source-provenance.json#current_complete_strong_stability_inputs. SS0–4 supplies exact finite coordinates and the finite unitary average, the original p^(3/2) bound, trace-preserving whole-domain normality, the full variable matrix product, normal GNS spatial splitting and the entire stable type I example. Both nonfactor summability routes and every absorption equivalence retain their original hypotheses and conclusions. Exact finite-head removal and lifting inside the relative commutant produce actual commuting coordinate systems. ## Complete centrally trivial automorphisms and decreasing AFD factors All eight original results and twelve whole solved exercises are closed at source-provenance.json#current_complete_centrally_trivial_inputs. CT0–5 supplies normal transport and topology, every automorphism of R approximately inner, the tensor relative commutant, entire finite/infinite Bernoulli products, direct finite fixed-algebra irreducibility, separate diffuse II1 and AFD proofs, and compact twisted-orbit minimization without separability. Both-state constants, general separable-predual factor group assertions, all four absorption characterizations, every-ultrafilter action and decreasing scalar intersection retain their whole original obligations. ## Complete finite outer actions and whole trace commutants All six original results and eight whole solved exercises are closed at source-provenance.json#current_complete_finite_outer_action_inputs. FO0–4 supplies the full finite-trace Hilbert commutant, entire-domain normal faithful range/inverse, arbitrary central kernel and actual matrix-base products and averaging. General outer finite-group fixed factors retain nonseparable preduals; countable invariant finite stages give R, while a directed family gives local AFD. The standard nondegenerate covariant convention and proper identity corner boundary are explicit. All whole nonfactor/flip/Z3/free-group/index/order exercises, FJ identities and the unchanged diagram remain. ## Complete continuous outer actions and the regular/CAR route The whole three-result/eight-solution scope is closed at source-provenance.json#current_complete_continuous_outer_action_inputs. CO0–5 supplies the complete local Haar/cutoff/L2/regular representation and tracial CAR route, all finite/trivial/unused-mode cases, whole complex Hilbert–Schmidt criterion, full point-predual continuity and normal target transport. Exact selected Haar and measure proofs retain their original notices. No source real-Clifford/typeIII conclusion is substituted for the current tracial theorem. ## Complete Bogoliubov generator and scalar inputs The six-result/twelve-whole-solution mathematical scope is closed at source-provenance.json#current_complete_bogoliubov_inputs. BG0–4 supplies exact complete tracial CAR/product inputs, arbitrary unbounded self-adjoint groups on the entire common domain, all-real-time Hilbert–Schmidt Duhamel, scalar chord/logarithm/singular sums and whole AutR density. The source is identified by its exact selected version. Human free comparison criteria and their broader proof dependencies remain separate. ## Complete hyperfinite finite-algebra and vacuum inputs The9result/10whole-solution mathematical scope is closed at source-provenance.json#current_complete_hyperfinite_finite_inputs. HF0–5 supplies arbitrary-subalgebra expectations, fulltracialcommutant/predual topology, allstatecutoffs without assumed spectralmeasures, generalfinitecenter/any-algebra finitelevelimplementation and wholevacuum/tracedirectsum. Exact AF1–5 and NA0–6 versions retain wholecorners/arbitraryHilbert scope; NA6 depends on the already proved current Corollary5.2, avoiding a cycle. ## Complete finite CP model inputs The16result/8whole-solution mathematical scope is closed at source-provenance.json#current_complete_finite_cp_model_inputs. FCP0–5 supplies complete finite-algebra structure, every positive contractive approximate identity, generic min/max tensor norms, unital/nonunital dilation and nonfaithful commuting actions, exact embedded unitization, full arbitrary commutative representation, all matrix tests and weak/norm separation. ## Complete tracial-adjoint inputs The3result/10whole-solution mathematical scope is closed at source-provenance.json#current_complete_tracial_adjoint_inputs. P00–P06 and exact retained CF1–10/CP1–6 supply the complete finite coordinate adjoint, normality, all-matrix positivity, density/diagonalization, rectangular Kraus rules, trace Hilbert completion and full weighted norm argument. Both rational-record state identities, exact half-weighted commutator estimate, fixed blocks and all unitary changes are included. ## Complete trace-preserving model inputs The5result/10whole-solution mathematical scope is closed at source-provenance.json#current_complete_trace_preserving_model_inputs. Exact complete tracial-adjoint providers and thirteen direct faithful-trace hypertrace arguments supply the incoming models. Every N1–N3 unit/topology estimate, both rational perturbations, normalized-state identity, complex pairing, finite-list budget, polar complement extension and whole diagram is included. ## Complete hypertrace inputs The13result/8whole-solution mathematical scope is closed at source-provenance.json#current_complete_hypertrace_inputs. Full PC/FCT, homogeneous central assembly, spectral thresholds, commutative characters, and bounded NF1–4 normality supply the exact prerequisites. The parameter example,three figures,singular-trace averaging and both arbitrary semifinite corner passages are included. Exercise6 uses the four stated prose multiplication marks. ## Complete completely bounded extension inputs The8result/9whole-solution mathematical scope is closed at source-provenance.json#current_complete_completely_bounded_extension_inputs. Exact complete scalar, matrix/GNS, nonunital cyclic-vector, operator-density and universal-bidual providers supply the incoming construction. All-n matrix norms and bidual identifications, arbitrary-H extension, full unital dilation, every original zero/nonunital case and full diagram are included. ## Complete abstract operator space realization inputs The entire abstract-operator-spaces lesson preserves three original results and six whole solved exercises. Its finite-state pair controls every middle size. The direct orthant-distance separation, finite Gram quotient, conjugate Hilbert coefficient, norm-detecting tuples, arbitrary direct sum, minimum example and completion are proved in full. Complete retained CF1–10 and MG01 provide the exact scalar, norming-state and Hilbert prerequisites; the proof imports no CB extension theorem. The complete binding graph and current source versions are in source-provenance.json#current_complete_abstract_operator_space_inputs. Gupta–Mandayam–Sunder v3, Theorem 1.3.1 (printed23–25; native28–30), supplies the freely accessible method comparison; its state-selection inequality (1.3) is omitted there and is supplied locally. The following Section1.3.3 proof treats max only; the minimum example used here is proved locally. Effros–Ruan Theorem2.2(1), printed248, is expressly stated by reference. Human rights notices remain intact. ## Complete completely positive lifting inputs The lifting lesson contains fourteen numbered results and nine solved exercises. The complete quasicentral, quotient, nonunital, exact-gluing and norm-controlled selection proofs are bound in source-provenance.json#current_complete_completely_positive_lifting_inputs. The nuclearity consequence consumes the full tensor Theorem3.1 and its exact96-node free closure; its graph uses no lifting theorem. Finite-model prerequisites consume19 complete qualified nodes. The retained square-root construction transfers through the independent scalar-GNS/matrix representation proofs. Gabe v4 and Olesen Section2.4 are compared at actual full proof locators; referred or scope-mismatched steps are not imported. ## Whole tensor positivity and nuclearity inputs The tensor-positivity lesson contains eleven numbered results and seven solved exercises. The complete40 current proof/context/solution intervals cover the whole source, and each mathematical graph node has a complete argument binding or an explicit primitive/aggregate role. The full typeI construction consumes H00--H02,T04a,C01--C02,C04 with exact current versions and retained CF calculus. Each of the seven solutions has its own route; Exercise7 consumes the complete finite-model Proposition5.3 ideal-compression argument, Proposition5.2 and FCP0 approximate identities. Exact bindings are in source-provenance.json#current_complete_tensor_positivity_nuclearity_inputs. The linked author,university and publisher materials retain their stated reuse terms. ## Whole semidiscrete finite-model inputs The semidiscrete lesson contains seven numbered results and six solved exercises. The26 exact current proof/context/solution intervals cover the whole source. Every mathematical graph node has a complete argument binding or an explicit primitive/aggregate role. The commutant converse consumes the complete independent normal exact-marginal/cone/normal-Jordan routes. REP supplies the entire balanced-series, dominated-form, cyclic and amplification construction before the separate standard-pair argument, without an injectivity or semidiscreteness premise. D1 retains exact dual-order indices; D2 retains the trace-class Banach norm. Q1–Q3 and Corollary4.3 supply all positivity, block contradiction, support approximation and complete-positivity steps. Exact versions are in source-provenance.json#current_complete_semidiscrete_finite_model_inputs. The current author-hosted Anantharaman–Popa PDF differs from the retained historical copy; both versions stay distinguished. The linked sources retain their stated expression-reuse terms. ## Whole nuclear-bidual and extension inputs The nuclear-bidual lesson contains six numbered results and eight solved exercises,with both examples and the full interval diagram. The28 complete current intervals cover the entire source. Each of the305 acyclic graph nodes has a complete proof binding or an explicit primitive/aggregate role. All eight whole solutions have individual routes. The retraction criterion uses semidiscrete Proposition4.1, and the predual passage uses Theorem3.1. The entire unchanged dilation body is rebound at its current source offset. The selected core/weight/trace/corner and balanced-weight versions remain exact, with no unreviewed foreign KMS substitution. See source-provenance.json#current_complete_nuclear_bidual_extension_inputs. The complete retained AS bounded-strip, GDW pointwise-graph, MA finite-domain and KU uniqueness arguments are readable in nuclear-bidual-retained-core-arguments.html. Their exact programme bodies, conventions and notices are preserved with prerequisite links rebased. The selected provider versions are specified separately from other editions. The GDW summable-error closed-graph step is explicit and separately bound. ## Whole averaging and crossed-product inputs The averaging lesson contains twelve numbered results and ten solved exercises. The51 complete current intervals include23 contiguous whole sections covering the full source. Each of352 acyclic nodes has a complete argument binding or an explicit primitive/aggregate role;325 provider bindings retain exact reviewed versions. The arbitrary-LCH regular Hilbert, product and Haar arguments are explicit prerequisites of the real-line core instance. The current whole semidiscrete retraction, tensor/normalization and predual equivalences are bound directly. Every whole solution has its own route. The prerequisite links identify the exact core arguments;human draft exercise prompts are distinguished from proofs. See source-provenance.json#current_complete_averaging_crossed_product_inputs. ## Whole free-group norm-averaging inputs The free-group norm-averaging lesson proves reduced-word normal form, arbitrary-index Hilbert-space completeness, the regular operator algebra and faithful trace directly. CF1–10 supplies adjoints and positive C*-algebra calculus. The finite cancellation argument and general orthogonal-range estimate yield scalar norm averages, simplicity and uniqueness of trace. Rank-one characters are constructed from approximate eigenvectors. Each of the ten solved exercises has its own complete argument and dependency route in source-provenance.json#current_complete_free_group_norm_averaging_inputs. De la Harpe, Definition9 and the full proof of Theorem14, provides the freely readable Powers comparison. The local construction supplies the partition without boundary-action theorems and uses the inverse series in the difference from the identity. ## Free-group projection analytic dependencies The projection lesson uses the complete free-word, arbitrary-index Hilbert-space, regular algebra and faithful-trace arguments, with exact CF1–10 adjoint and C*-calculus foundations. PA1–5 proves compact spectra, the ordinary complete trace ideal and absolute diagonal trace, scalar contours and full generic holomorphic calculus for actual representation units. The explicit basis map, finite differences, spectral pairing and inside-algebra projection alignment give the final rank-two conclusion. Each of ten complete solutions has a separate route in source-provenance.json#current_complete_whole_free_group_projection_inputs. Schick’s full Lemmas2.6,2.8,2.9 provide freely readable comparisons; their referenced trace-ideal and K-theory premises are not imported. ## Invariant states and trace Hilbert spaces The invariant-state proof uses the complete measurable-operator and positive L1-predual construction, including the full bounded-functional normality argument. TL1–6 supplies actual L2 completion, sharp product bound, cyclicity, finite trace expectations, decreasing intersections, exact II1 trace cuts and ordinary-trace rank. Finite tracial instances of binary pinching and compatible matrix induction lead to irreducible AFD containment; the complete decreasing-AFD argument and two refinements give global scalar pinching. All three original results and ten whole solutions have exact routes in source-provenance.json#current_complete_invariant_state_inputs. Popa1986 and the Anantharaman–Popa author draft provide the actual bounded comparisons recorded there. ## Semiregular MASAs and scalar pinching The semiregular-MASA lesson proves factor orbit matching, strong sums of partial normalizers, corner regularity, exact diffuse trace cuts and controlled dyadic movement. Its compatible first-corner construction contains the entire prescribed MASA, and MC1 with the trace-GNS unitary identifies the growing matrix factor. TL3–TL4 supplies finite trace expectations and the exact decreasing-space intersection. The complete finite-trace pinching/MASA and decreasing-AFD routes give both scalar refinements. All five original results, twelve whole solutions and the trace-transfer figure have exact versions in source-provenance.json#current_complete_semiregular_masa_inputs. The full AP Lemma12.1.2 and Popa1981 compatible matrix construction are comparisons at their actual hypotheses; their more general complement arguments and the existence of a different MASA are not silently substituted. ## Small matrix corners The matrix-corner lesson uses full bounded polar/spectral calculus and the actual trace Hilbert-space product, cyclicity and multiplication bounds. It proves both-tail cutoff estimates, a stronger squared polar error, orthogonal range repair, a complete recursive Gram modulus and the exact square-root trace-ratio coefficient bound. The scalar selection is bound to the current full semiregular/scalar theorem through the unchanged invariant-state corner argument. All four original results and ten whole solutions have exact routes in source-provenance.json#current_complete_small_matrix_corner_inputs. AP Lemma11.1.12, Remark11.1.13 and Lemmas11.1.14–16 supply complete free comparisons; the more extensive amenability proof is not a substitute prerequisite. Orthogonality is asserted for the initial projections, while range supports may overlap. ## Small corners and maximality The small-corner lesson uses the full external finite-rank model and the current repaired matrix-corner corollary. Finite trace expectations are TL3; support-corner bounded density is BD1–BD5. Injectivity passes to corners by the completely positive extension/compression proof; the center-of-a-corner and quotient-predual arguments retain the factor and separability hypotheses. The maximality theorem applies to arbitrary finite faithfully tracial algebras, using a full directed chain argument and the new support’s squared error budget. The separable injective conclusion uses the independently bound exact-containment and dyadic trace-GNS proof. All four original results, Definition2.1 and ten whole solutions have exact routes in source-provenance.json#current_complete_small_corner_second_proof_inputs. Popa1986 Proposition2.2 and Section3 and AP Definition11.1.4, Theorem11.1.5 and complete Theorem11.1.17 provide human comparisons. The general nonfactor injective converse is a separate argument. ## Properly infinite algebras and dyadic approximation The properly infinite lesson uses the complete projection comparison, halving, finite central-part and absorption proofs, the actual normal GNS/predual construction, bounded support-corner density, and the current full injectivity–semidiscreteness theorem. Its internal reconstruction is derived by the Choi square-root calculation and orthogonal commutant isometries. Arbitrary properly infinite algebras have local AFD; separable predual supplies the countable dense set and increasing dyadic exact-containment construction. All seven original results and ten entire solutions have exact routes in source-provenance.json#current_complete_properly_infinite_inputs. The full four-page Elliott–Woods paper is read from the AMS. ## Central traces and finite AFD structure The central-trace lesson uses the complete arbitrary finite PC/FCT trace and projection construction, finite trace expectationTL3, projection rotation and bounded trace topology. It proves prescribed central dimension cuts, finite joint dyadic rank rounding, exact retention of the old factor and all constants in the corrected-corner estimate. The separable center-times-R theorem identifies the product trace Hilbert spaces. Directed AFD injectivity uses finite matrix-unit averages, closed commutants and the full arbitrary-algebra standard representation; all three separable central-type sequence constructions are explicit. All five original results and ten entire solutions have exact routes in source-provenance.json#current_complete_central_trace_inputs. The current author draft supplies complete selected factor and commutant-method comparisons; its by-reference unrestricted trace remark is not an admitted proof. ## Balanced reconstruction and unitary couplings The balancing lesson uses the complete arbitrary finite PC/FCT center-trace and projection proofs, normal finite-trace expectationTL3, full internal Choi Kraus construction and trace-preserving finite unitary-input models. It proves both norm-averaging constructions, normal countable balanced cp sums, exact defect completion and the coupling identity. Every original result and all ten whole solutions are routed in source-provenance.json#current_complete_balanced_kraus_inputs. Nonfactor defect equality remains center-valued; factor balancing requires no separability. ## Multiplier ultraproducts and normal embeddings The multiplier lesson uses the complete normal-functional/state-topology NT1/NT2, C*quotient CQ1, CF/CP, SF/BD and centralizing-sequence quotient proofs. Its own arguments construct exact uniform multipliers, the faithful quotient state, a faithful C*state Hilbert representation, two-vector completeness and arbitrary strong-Cauchy-net closure before normality. Constant embeddings, the separable-predual finite centralizing quotient, actual chosen convergent-family actions, dense possibly nonunital representatives and type I collapse are explicit. All nine original results and fourteen entire solutions are routed in source-provenance.json#current_complete_multiplier_ultraproduct_inputs. The free Ocneanu direct proof and Ando-Haagerup corner method are distinguished; the latter external ideal-correspondence theorem is not an admitted premise. ## Unitary couplings and finite injective factors The coupling lesson uses the complete faithful normal multiplier quotient, finite projection and center-trace construction, trace-Hilbert functional calculus, balanced Kraus models and dyadic exact-containment theorem. Its own arguments give finite fourth-root sampling, the full trace-Lipschitz and variational estimates, polar unitary representatives and nonfactor relative-commutant comparison. Corollary 5.2 constructs the countable II∞ spatial matrix decomposition independently of the injective-to-AFD conclusion. All seven original results and ten whole solutions have individually routed proofs in source-provenance.json#current_complete_unitary_coupling_inputs. Haagerup is the mathematical antecedent of the sampling/clipping/ultrapower route; Anantharaman–Popa Exercise 8.1 states the countable decomposition whose full proof is supplied here. ## Central disintegration and measurable matrix assembly The finite nonfactor lesson uses the full finite-factor and properly infinite approximation theorems, directed AFD-to-injectivity, finite center-valued trace, normal-functional topology, Gelfand and GNS constructions, compact-metric measure representation and Gram repair. MF1–9 proves the countable Gram field, L2 localization and completion, measurable operators, both diagonal commutants, compact continuous-equation selections, supported commutant fields, algebra generation, centers and fixed-base field uniqueness. Tensor stabilization is explicit. All four original results and twelve whole mathematical solution duties are routed in source-provenance.json#current_complete_central_disintegration_inputs. The scalar budget for the rational-matrix exercise is valid for every positive tolerance. ## Injective algebras and separable tracial envelopes The tracial envelope uses exact trace-preserving finite models, bounded density, faithful-state topology and the full semidiscrete retraction theorem. Positive normal functionals are paired with actual measurable positive L1 densities; finite central supports supply faithful tracial cuts for each normal neighborhood. General local AFD uses the complete finite and properly infinite theorems and an explicit finite invariant Kraus average. PC1–7 supplies central comparison, corner centers, finiteness and source-countable absorption; the lesson constructs the full finite-support nonfactor matrix reduction. Central finite AFD structure, finite typeI splitting and trace-preserving expectations supply the center-times-R and subalgebra conclusions. All six original statements and twelve whole solutions are routed in source-provenance.json#current_complete_tracial_envelope_inputs. ## Ultraproduct expectations and fast reindexing The expectation and chosen-family covariance use the full multiplier quotient, faithful normal quotient state, constant normal embedding and order-normal positive-functional/predual theorem. The centralizing C* estimates are general; its complete finite normal embedding uses separable predual and a countable diagonal metric construction. The tail example uses the full tracial matrix product and trace/predual density. The fast theorem uses common-unit subalgebras, separable predual, a countable group of constant lifts, exact quotient relations, fixed positive multiplier moduli, finite ultrafilter selections and full bounded-net normal extension. Its complete ordered expectation identity supplies the final specialization exercise in the preceding lesson. All nine statements and eighteen whole solutions are bound in source-provenance.json#current_complete_ultraproduct_expectation_inputs and source-provenance.json#current_complete_fast_reindexing_inputs. ## Slow reindexing and semi-lift compatibility The slow theorem uses the complete faithful-state multiplier quotient and normal expectation, general chosen-family semi-lift construction, separable centralizing normal embedding, countable rational join/intersection construction and fixed two-sided multiplier moduli. Two finite selections give nested outer neighborhoods and a finite level diverging along the ultrafilter. The full current fast faithful-state extension supplies every bounded-net, order-normal and concrete-predual step. The exact tensor example uses the full dyadic tracial product and normal-predual density. All four results and twelve whole solutions are bound in source-provenance.json#current_complete_slow_reindexing_inputs. The action clause compares the actual outer semi-lift on the image with its constant lift and the image of that constant lift on the domain. ## Ordinary multipliers and predual compactness The full ordinary multiplier algebra uses bounded faithful-state strongstar topology, double-centralizer coordinate identities and both adjoint moduli. The complete PC00-PC09 criterion uses positive coefficient-series envelopes, normal support/GNS and concrete preduals, a complete faithful-state metric, Baire and spectral projection cuts, finite positive controllers, real Hahn-Banach graph extension and dual-ball compactness. Only weak-compact-to-subsequence extraction is needed. The Bernoulli example includes compact prefix cylinders, positive-functional measure representation, scalar completion/L2 and the exact L1 predual. All four results and twelve whole solutions are bound in source-provenance.json#current_complete_ordinary_multiplier_inputs. ## Index selection and uniform multiplier control The construction uses the complete type-I multiplier quotient and normal constant embedding, faithful normal expectation, chosen-family actions and centralizing normal subalgebra. Countable norm-dense rational data and norm-controlled representatives support finite outer row and inner column intersections with one positive row-independent two-sided modulus. The entire norm Cstar extension proves all four clauses and the exact faithful-state kernel identity. The finite-trace two-norm estimates give the full nonfactor trace-null quotient embedding. The weighted-state swap example includes the intrinsic obstruction for every dense rational algebra and every lift choice. All five results and twelve whole solutions are bound in source-provenance.json#current_complete_index_selection_inputs. ## Abelian pinching and relative commutants The faithful-state expectation uses complete bounded-graph modular data, Gaussian invariant graph approximation, faithful normal GNS representations, algebra-valued compression and full all-net normality. Finite pinching and scalar expectations give orthogonal GNS blocks and nested gap projections. Central-support/polar exhaustion proves the arbitrary-index relative corner isomorphism. A normalized tuple convex-orbit argument and finite real/imaginary spectral grid yield simultaneous binary cuts with15/16energy and2^mcount. Directed projection limits and bounded ultraweak cluster points give the full MASA gap criterion. Nonfactor scalar approximation, II1dyadic trace transfers and equivalent-atom comparison, the finite typeIendpoint, both displacement estimates and all twelve entire solutions are bound in source-provenance.json#current_complete_abelian_pinching_inputs. ## MASAs in expected semifinite subfactors Normal-state support and exact null left ideals make the expected-subfactor map faithful. Complete faithful-state pinching and equal atoms drive coherent dyadic matrix induction; full finite-stage trace expectations prove the factor and product-traceGNSidentification. FiniteAFDcorner and exact containment preserve all diagonal gaps and all d-squared entry budgets. Projection comparison, finite joins and source-countable infinite comparison give common semifinite coordinates. DirectedAFD-to-injectivity, explicit compressed ucp corner retraction and an independent complete finite injective-factor theorem supply the infiniteAFDclause. Coordinate strong sums prove the product-diagonal MASA and scalar relative commutant. FullSE1-SE5proves the irreducible state-centralizer corollary. All four results and twelve whole solutions are bound in source-provenance.json#current_complete_expected_semifinite_masa_inputs. ## Group MASAs and singular affine examples Complete continuous Cstar calculus and square-summable coordinates supply H00-H04. Direct matrix products prove the regular commutants; positive-net and series-vector arguments prove the canonical trace and normality. Right-coset amplification and compression give the actual bounded subgroup expectation and Fourier-support characterization. Both directions of the subgroup-orbit criterion, affine ICC/malnormality and finite-factor classification prove the MASA setting. Complete translated-support coefficients, finite exclusions in every characteristic and a uniform trace-square estimate prove ordinary singularity without bounded operator-norm truncations. Unitary generation and exact double-coset coordinates supply the finite/infinite index conclusions. All six results and ten complete solutions have full proof routes in source-provenance.json#current_complete_group_masa_inputs. ## Double cosets and intrinsic MASA multiplicity Full group-MASA, regular-commutant, trace, Hilbert/predual and finite-factor proofs supply the setting. A weighted positive common-fixed-vector operator and bounded inverses give the canonical central subgroup projection. Exact regular-product basis maps and all finite-compression matrix coordinates prove the full two-block commutant, including inter-copy operators and arbitrary-index nets. Bounded polar decomposition, trace bounds for joins and summable cutoffs prove order-normal trace-square continuity and abstract-isomorphism trace preservation. Complete maximal-ideal/quotient/character arguments, finite rank and full central support prove intrinsic finite size; a proper shift separates the infinite case. The actual trace-space unitary transports both actions, Jandthecanonicalcomplement. All four results and ten entire solutions have exact full routes in source-provenance.json#current_complete_double_coset_inputs. ## Finite-field towers and prescribed MASA multiplicities Integer division, Bezout, prime factorization, finite-group orders and cyclic subgroups support complete polynomial division, repeated-root, quotient-field, basis and finite splitting-field arguments. Frobenius gives finite fields and divisor-degree embeddings. Algebraic cyclotomic products, monic integer division, an explicit large value and the squarefree order argument give a prime congruent to one modulo the required index. Divisible coprime degrees keep every relevant primary valuation fixed; unique primary subgroups and nested coprime complements give the full countable union decomposition and exact cyclic quotient. Complete current affine ICC, MASA/singularity, regular product, full inter-copy matrix commutant and abstract trace-space pair-isomorphism proofs give each finite multiplicity, the index-one endpoint and the rational infinite example. All five results and ten complete solutions have exact full routes in source-provenance.json#current_complete_finite_field_tower_inputs. ## Symmetric tensor norms and Rademacher truncation Full real and complex norm-preserving extension and finite-coordinate bounds give algebraic tensor separation and genuine projective completions. ScalarA-H and R00-R12 prove compactness, polynomial approximation, continuous rectangle integration and the general Banach spectrum/radius theorem. F01-F08 construct forced unitizations, all calculus identifications, positive cone/order and the zero-at-zero original-algebra restriction. Spectral evaluation, functional extension and an explicit complex quadratic provide states and symmetric square detectors without a representation theorem. Full finite-sign fourth moments, continuous clipping, every double residual and exact optimization yield the bounded27/16cost and2/3residual. Complete residual approximations, summable series and explicit parameters give the81/16lift with every requested positive excess; algebraic/telescoping solutions are independent of completed surjectivity. Every nonunital/nonseparable/zero endpoint and all ten complete solution duties are retained in source-provenance.json#current_complete_symmetric_tensor_inputs. ## Tensor completion, injectivity and state domination Real and complex Hahn-Banach extension, finite scalar compactness and genuine Cauchy completions construct the projective algebra and its normalized functionals. Forced unitizations, complete C*-calculus and positive order give marginal states and all nonunital cases. Scalar exponential series, rectangular disk and annulus areas, radial Riemann integrals and continuous Banach norm integration supply every Gaussian heat identity, exchange, tail and derivative bound. The numerical-reality test makes the canonical tensor kernel vanish. The factor2 real-completion embedding and unique positive-tolerance lifts give the exact81/16 real norm comparison. Maximal proper filters prove arbitrary disk-product compactness; closed coordinate equations give arbitrary real/complex dual balls and state spaces, and explicitly monotone cofinal subnets give the directional-limit route. A finite orthant minimum and all weighted tests give common real states; two complex self-adjoint parts and mean states give the preliminary81/16 bound. Six complete results and ten whole solutions are bound in source-provenance.json#current_complete_tensor_completion_inputs. ## The sharp noncommutative bilinear inequality Complete real/complex functional extension, scalar completeness/series and C*-calculus/order/forced unitization support the full proof. The all-state representation, complete four-positive-functional/coefficient argument, bounded operator density and concrete predual construction identify the canonical Banach bidual with its transported product. Explicit represented roots, inverse/support limits and polar partial isometries give the full polar and projection-cutoff inputs. Original-algebra continuous cutoffs and local norm series prove every polar-power domain, product and holomorphy assertion. Scalar circle averages and a rectangle maximum argument prove the strip bound and all boundary/zero limits. Exact finite third-root moments and noncommuting ordered pairings give the family estimates. Four independent normers, finite orthant separation and arbitrary compact state products give common states. The finite81/16starting bound, square-root coefficient improvement and actual cofinal subnets reach the form norm, with a separate attained-infimum proof. Two-sided finite-set positive contractions, bothdelta/4errors and projective dual compactness give norm-preserving nonunital extensions; a second Banach-bidual route has its exact independent norm identity. Explicit orthogonal isometries give universal coefficient1optimality and the symmetric corollary has coefficient4. All four full results and ten whole solutions are bound in source-provenance.json#current_complete_sharp_bilinear_inputs. ## Infinite tensor products and reference states Directed normed and C*-limits include noninjective, nonunital and zero systems, exact quotient norms and eventual kernels. Complete Hilbert and minimal tensor norm arguments supply arbitrary pointed products, normal coefficient maps, the canonical universal bidual, central quotient and globally normal inverse. Full spatial commutation, normal slices and arbitrary state supports supply factorality, relative commutants and faithful trace products. General positive modular half-powers have their full domains, spectral-band cores and Tomita closure; the identical two-level calculation is a separate concrete model. Finite-leg slice intertwiners, scalar normalization, ordered phases and expectation towers give the innerness criterion. The general semifiniteness argument retains its sequence and separable predual hypotheses and every normal reference state. It uses full support corners, matrix trace transfer, finite-trace projection nets, measurable trace densities, order-normal positive coefficient functionals, continuous internal implementers and inverse centralizer perturbation with all KMS domains and the whole positive-cone trace criterion. Twelve complete solutions include the completed CAR occupation-state identification and finite-corner obstruction for constant nonhalf densities, arbitrary pure-state full-operator products and universal-versus-reference predual separability. Exact complete arguments appear in source-provenance.json#current_complete_infinite_tensor_inputs. ## Fermions, Fock space and quasi-free factors Arbitrary exterior Fock spaces supply exact normalized occupation vectors, bounded creation and annihilation, all CAR signs and irreducibility. Finite matrix units and multiplicity unitaries give the exact concrete norm, compatible completions and simplicity. Finite compressed covariances define compatible positive occupation densities; all determinant moments identify the whole reduced doubled-Fock cyclic representation, including covariance endpoints. Finite even parity blocks and their exact norms give both ordinary even-leg spatial tensor identifications. Complementary fields and the fully implemented continuous gauge action prove factorality for every covariance. Real finite-vector separation and a bounded rational contraction map give strong* approximation in every representation, including zero and degenerate representations. Reducing blocks and endpoint-aware cyclic matrix spaces give the full completed product-state identification. The half-state has a unique faithful normal trace and is type II1 at arbitrary infinite one-particle dimension. Faithful constant states on separable infinite-dimensional spaces have the exact modular inner-time group; away from half, a normal trace on each hypothetical finite corner gives a contradiction. All ten complete solutions retain their full finite and infinite scope. Exact complete arguments appear in source-provenance.json#current_complete_car_fock_inputs. ## Constant CAR states and the periodic core The faithful identical two-level product has its full completed CAR GNS bridge, Tomita involution, adjoint and product domains. Normal local compression and the dense commuting right orbit give the whole strong* expectation limit. The occupation diagonal is maximal abelian and normally isomorphic to the completed Bernoulli multiplication algebra. A direct binary measure construction, full complex integration and cylinder density prove the complete invariant-function lemma. Finite-density traces, fixed permutation unitaries and diffuse occupation projections give the type II1 centralizer through the full finite matrix alternative. The periodic normal regular representation, Fejer completeness and every integer Fourier connection give factorial corners and the period-circle factor. The real lattice transform retains every carry sign; measurable phases and separating vector slices give the entire continuous-core center and its dual rotation. Explicit product coefficient resolvents give the upper modular spectrum bound. The complete finite-ideal GNS-filter proof and balanced full-graph fixed-corner comparison give the lower bound for every faithful normal semifinite weight, including infinite total weight. All twelve full solutions retain their finite and infinite hypotheses, complex estimates, positive and negative carry cases, measurable branch and finite-matrix counterexample. Exact complete arguments and primitive boundaries appear in source-provenance.json#current_complete_constant_car_inputs. ## Finite measured groupoids: complete proof inputs The six results and ten complete solutions in `finite-measured-groupoids-and-afd-algebras` use the fixed finite-class AF exhaustion, the supplied invariant source-counting measure, topology refinement and Lusin–Souslin. Disjoint stage graphs give the counting and completed saturation formulas. The regular left/right actions provide the faithful normal trace; diagonal closure and exact matrix coordinates precede center partition averaging. The nonfactor AFD conclusion uses bounded density and the concrete predual. Ergodic type II₁ and separability then give the tracial matrix product through the finite AFD uniqueness proof. The exact 87-node input record is `source-provenance.json#current_complete_finite_groupoid_inputs`.