Metric and predual foundations for the central-sequence criterion
New original programme exposition: CC0-1.0 to the extent of rights held.
The central-sequence criterion in the main lesson needs an open mapping theorem for all Polish groups, and faithful-state seminorms that give the intrinsic bounded strong* topology. TS1–6 proves the metric, Borel-image and category chain from choice, complete real scalars and the definitions of metrics, continuity and groups. A Polish space is a separable topological space with a compatible complete metric. Borel sets form the smallest sigma-algebra containing the open sets. NT1–2 proves the finite-functional and faithful-state consequences of the exact complete predual/GNS components linked there.
TS1. The metric constructions
A separable metric space has a countable base: balls of positive rational radius about a countable dense set suffice. Given a point in an open set, choose a ball around that point inside the set, then a nearby dense-set point and a rational radius whose ball contains the original point and stays inside the set. A subspace inherits a countable base; choosing one point in each nonempty basic open set makes it separable. Every open cover of a space with a countable base has a countable subcover: for each basic set contained in some cover member choose one such member.
Replace any metric by when a bound is useful. This preserves its topology and Cauchy sequences. For countably many nonempty Polish spaces with bounded complete metrics , the product metric
is complete. A Cauchy sequence is Cauchy in each coordinate; take those coordinate limits, then control the product distance by a finite coordinate sum and the uniformly small remaining tail. The same tail estimate proves that this metric gives the product topology. Finite-coordinate boxes from the countable coordinate bases form a countable base, proving separability. An empty factor gives the empty Polish space.
Closed subsets of a complete metric space are complete in the restricted metric. If are nested, nonempty closed sets with diameters tending to zero, choose . Their tail distances tend to zero, so they have a limit ; closedness places it in every , and the diameter condition makes it the unique common point.
An open subset of a Polish space is Polish. For a nonempty closed complement , its distance function is continuous, since
It is positive on . The map
is a homeomorphism from onto a closed subset of . Indeed a convergent graph sequence cannot approach while its second coordinate stays finite, and elsewhere continuity identifies the limiting second coordinate. Pull back the complete restricted product metric. If is empty, use the original metric; the empty is harmless.
More generally a set is Polish. Use the graph of all the reciprocal-distance functions in , replacing a reciprocal by the constant one when its complement is empty. The same coordinate argument makes this graph closed; the graph map is a homeomorphism onto it. Finally, a finite or countable disjoint sum of Polish spaces is Polish: use bounded complete metrics within each summand and distance two between different summands. A Cauchy sequence eventually stays in one summand, and a countable union of countable bases is a countable base.
TS2. Make Borel conditions topological
Call a topology on admissible if it is finer than the original Polish topology, is Polish, and has exactly the same Borel sets.
Countably many admissible topologies have an admissible common refinement. Include the original topology as coordinate zero and take the diagonal
Each identity is continuous. Since a metric space has a closed diagonal, the displayed set is closed in the product. TS1 makes it Polish. Its topology, transferred to , is precisely the topology generated by the coordinate topologies. Their countable bases give a countable base of finite intersections. Every such basic set is original Borel, so every new open set, being a countable union of basic sets, is original Borel. Refinement gives the reverse Borel inclusion.
Let consist of the subsets that can be made clopen by an admissible topology. A closed set belongs to : split into that closed set and its open complement, using the disjoint-sum topology and TS1. The new basic sets are original Borel, so this topology is admissible. Complements preserve membership in .
For , first take the common refinement of their chosen admissible topologies. Each is clopen there, and is open. Split this refined Polish space into the open set and its closed complement. This is again an admissible topology and makes clopen. Thus is a sigma-algebra containing all closed sets; it contains every Borel set. The common-refinement construction consequently makes any countable family of Borel sets simultaneously clopen.
In particular, every Borel subset has a Polish topology with its original relative Borel sets, for which inclusion into is continuous. If is Borel and is Polish, make the inverse images of a countable base of clopen. In the resulting admissible topology is continuous. These constructions require no classification of standard Borel spaces.
TS3. Separation by following two metric approximations
Call a subset of a Polish space analytic if it is the continuous image of some Polish space, allowing the empty space. A continuous image of a Borel subset of a Polish space is analytic: equip that subset with TS2's Polish topology and use the continuous inclusion. A Borel map also takes Borel sets to analytic sets, after TS2's refinement makes the map continuous.
Let and be disjoint analytic subsets of , with Polish and continuous. We prove that a Borel set contains and misses . If one set is empty, the assertion is immediate.
For a nonempty closed and , choose at each point of an open ball whose closure has domain diameter at most and whose entire closed ball has image under of diameter at most . Continuity permits this by taking the closed ball inside an inverse image of a sufficiently small target ball. A countable subcover exists by TS1. Its intersections with are nonempty closed sets covering , with both diameter bounds. Discard empty intersections.
Recursively this gives closed pieces , indexed by finite sequences, with
and, for ,
Construct pieces with the corresponding bounds for . A finite nonempty list may be repeated to index its cover by natural numbers.
Two sets are Borel-separable when a Borel set contains the first and misses the second. This relation is symmetric, by taking a complement. If , , and every pair has a separator , then
separates . Thus an inseparable pair of parent images has an inseparable pair of child images.
Suppose our original were inseparable. Recursively choose prefixes of length , each extending the preceding prefix, such that are inseparable. Their closures in intersect: otherwise the closed set itself would be a separator. Domain completeness and TS1 give points
For an intersection point of the two target closures, the diameter bounds give
Indeed belong to the corresponding images, whose closures retain their diameter bounds. Hence , contradicting disjointness. A Borel separator therefore exists.
TS4. A Borel formula for an injective image
We now prove the full Borel-image statement: if is Borel between Polish spaces and is Borel, with injective, then is Borel in .
Use TS2 to make clopen and continuous in an admissible Polish topology on , then restrict to . It suffices to treat a continuous injection defined on an entire Polish space. The empty domain has empty image.
Fix a complete compatible metric on . At each positive level , a countable open cover can be chosen with both domain diameter and image diameter at most , by continuity and TS1. Intersect this cover with each parent piece and subtract preceding cover members. We obtain Borel pieces , indexed by a countable tree of finite sequences, with
and both diameter bounds at every positive level. Empty pieces may be retained. The closures of pieces along a branch are nested in ; we do not assume the Borel pieces themselves are closed.
For each , the sets and are analytic by TS2–3 and disjoint by injectivity. Choose a Borel separator and intersect it with , obtaining a Borel set such that
Set and recursively set
The child regions are Borel, disjoint and contained in their parent region. They retain
by induction: an image point in one child lies in none of the separators for its siblings. Define the Borel set
An image point belongs to its successive regions, so .
Conversely, determines a unique compatible branch : regions at a level are disjoint and each child is contained in its parent. These regions are nonempty, so their source pieces are nonempty, since . TS1 applied to the nested closures gives a unique . Choose . The domain diameter bound gives . The image diameter bound and give
Continuity makes , so . Thus , an explicitly Borel image. The initial refinement proves the assertion for the original . Applying it to every Borel subset also proves that a Borel injection has a Borel inverse on its image.
The diagram shows one branch selected by a point of . The two diameter bounds, completeness of the domain and continuity of are the exact reasons that branch comes from an actual source point.
TS5. Category and the neighborhood product
A set is nowhere dense if its closure has empty interior; it is meager if it is a countable union of nowhere dense sets. No nonempty open set in a complete metric space is meager. To prove this, given a nonempty open and closed nowhere dense , choose nested nonempty closed balls, each inside the interior of the preceding ball, with radii tending to zero, with the first inside , and with the -th missing . Such a ball exists because the complement of meets every nonempty open set. TS1 gives a common point in outside all . Taking closures of the nowhere dense sets proves the stated claim.
A set has the Baire property if it differs from an open set by a meager set. These sets form a sigma-algebra. For complements, the complement of an open set differs from its interior by its boundary, a closed nowhere dense set. Countable unions differ from the union of their chosen open sets by a subset of the countable union of the meager errors; a subset of a meager set is meager. Thus every Borel set has the Baire property. A nonmeager set with this property is comeager in some nonempty open set , because its chosen open set cannot be empty.
Let be such a set in a Polish group . Choose . For , the open sets intersect at . Their intersection is nonempty open, hence nonmeager. Left translation is a homeomorphism, so it preserves meager sets. There is therefore a point outside the two meager exceptions in , belonging to both and . Write it as , with . This gives , proving that contains the neighborhood of the identity.
TS6. Open mapping for all Polish groups
Let be a continuous bijective homomorphism of Polish groups. Given a neighborhood of the identity in , continuity of multiplication and inversion supplies an open identity neighborhood with .
The translates cover ; TS1 gives a countable subcover. Their images are translates of and cover , by surjectivity. TS5 shows that cannot be meager, since otherwise , a nonempty complete metrizable space, would be meager in itself. TS4 makes Borel: is Borel, is continuous and injective, and both spaces are Polish. Its Baire property now follows from TS5, whose neighborhood product conclusion gives
containing an identity neighborhood in . Translating this conclusion shows that the image of every open set is open. Hence the bijective continuous has a continuous inverse and is a homeomorphism.
All Polish groups are included. No invariant complete metric, locally compact hypothesis, Haar measure or countable underlying group is assumed.
NT1. Four positive normal functionals and bounded module operations
The complete CP01–06 component constructs the predual of a concrete von Neumann algebra as a Banach quotient of the completed Hilbert projective tensor product. It proves its isometric embedding in , norm closedness, the full duality , and the characterization by square-summable vector series. The complete CF1–10 component supplies its scalar, Hilbert and C*-calculus inputs. Those are proved inputs, not an assumed normal-functional decomposition or trace-ideal theorem.
In this module inner products are linear in the second variable. Thus CP's linear-first coefficient is written , with the same scalar value. For every , the exact CP representation gives
For , put
The squared vector norms sum to at most . Thus each is an actual bounded positive predual functional, by CP's series characterization. Expanding the four expressions, and using , gives
This proves the required four-positive decomposition on arbitrary Hilbert spaces and arbitrary concrete von Neumann algebras. No positive normal extension to all of has been assumed.
The predual is closed under the module operations
In the series, the former replaces the first-variable test vectors by and the second-variable vectors by ; square summability is preserved. The latter exchanges the two vector sequences. From the actual functional norm on ,
If a multiplying element is unitary, multiplication is isometric: applying its inverse gives the reverse inequality. These arguments include the zero algebra.
For a positive functional , C*-positivity and the scalar quadratic test prove
Indeed apply to and choose to minimize the scalar quadratic; if , arbitrarily large scalar multiples force the mixed term to vanish. Positivity makes , by its real values on self-adjoint elements and their complex-linear decomposition. Therefore
At a contraction , apply the preceding inequality to , and bound ; taking the supremum proves the norm assertion.
If is faithful, is norm dense in . Otherwise Hahn–Banach gives a nonzero bounded functional on annihilating this linear subspace. The exact duality identifies it with some , and annihilation says for every . Taking gives , hence , a contradiction. Thus this density assertion is a norm-predual result, rather than a conclusion drawn from weak density alone.
A unital two-positive map satisfies the Schwarz inequality. The positive matrix
remains positive after entrywise application of . Positivity and linearity make preserve adjoints. Testing the resulting matrix on gives . If is a unital completely positive inverse, applying and then its own Schwarz inequality gives
Both inequalities are equalities; injectivity of gives equality in Schwarz for . Expanding that equality for gives . Replacing by proves multiplicativity. Thus inverse normal UCP maps in the automorphism-group argument are actual normal -isomorphisms.
NT2. A faithful state gives the bounded strong* topology
The zero algebra has singleton unitary and automorphism groups, which are Polish with the zero metric on their one point. The faithful-state construction is needed only in the nonzero case.
Suppose has separable predual. Its positive cone has a countable norm-dense family : a subset of a separable metric space is separable, by TS1's countable-base argument. Positive vector functionals separate positive operators in any concrete representation. Consequently
is nonzero, positive and faithful. This series converges in the Banach predual, with norm sum at most one. If for , every summand has zero value; norm density then gives zero value for every positive normal functional, and the separating vector tests force . Normalize by to obtain a faithful normal state.
For any concrete and any faithful normal state , use the complete GNS construction, the complete known-normal-state coefficient proof, and ST1–2. They give a contractive faithful unital representation on its cyclic Hilbert space , a vector , a concrete von Neumann image , and ultraweak continuity of both and its inverse. In particular
Faithfulness makes separating: implies . ST2's full bounded topology comparison transports the intrinsic positive-functional seminorms in both directions. Its spectral, dual-ball and bounded-density premises are part of the exact proved components; a general modular theorem is not used.
The commutant orbit is dense in . Its closed span is invariant under the unitaries of , as is its orthogonal complement. Its projection therefore lies in . Here commuting with all those unitaries implies commuting with every operator: real and imaginary parts of a contraction are each real parts of the unitary , by the complete continuous calculus. Since and is separating, .
Let be a uniformly norm-bounded net in . If
then and . For , commutation gives
and the same estimate applies to adjoints. Density of , and the common operator-norm bound, give strong* convergence on every vector of . ST2 transports this to the intrinsic bounded strong* topology on .
For completeness the positive-functional comparison in that statement is an explicit series estimate. If has a square-summable coefficient representation , then for ,
Use Cauchy–Schwarz for in each term, followed by . At , strong convergence makes each finite initial vector sum vanish, while the uniform norm bound makes the square-summable tail uniformly small. Conversely single-vector positive functionals are among the intrinsic tests. Repeating this for adjoints gives precisely strong* convergence, for arbitrary nets. The converse from intrinsic strong* convergence to the two displayed state seminorms follows directly from their inclusion among those tests.
When is a faithful normal tracial state, traciality makes the two state seminorms equal. Thus on uniformly bounded sets, convergence in is exactly intrinsic strong* convergence. This conclusion does not require separability.
If is separable, the faithful-state GNS space is separable as well. ST1 makes the unit ball of ultraweakly compact. A countable norm-dense family in the predual separates its points and gives its weak-star topology: on the ball, approximation of any functional by this family has error at most twice the norm error. Its coordinate embedding into a countable product of scalar discs therefore makes the ball compact metrizable, hence separable. Choose a countable ultraweakly dense subset of that ball.
All the Hilbert vector coefficients of are normal by ST-C, so is weakly dense in the image of the ball. The norm-closed convex hull of is weakly closed. Here is the Hilbert argument for this last step: for a closed convex set and , a sequence minimizing distance to is Cauchy by the parallelogram identity and the fact that its midpoints lie in . Its limit is the closest point . Varying towards any gives . The corresponding bounded real vector functional separates from , proving weak closedness.
Thus that closed convex hull contains every ball vector . Rational convex combinations of the countable set are countable and norm dense in its convex hull, by approximating each finite list of coefficients within the finite simplex. Their closed linear span contains all , and cyclicity makes that span . It is generated by countably many vectors, so is separable.
NT3. Polar operators and central phase alignment
We first give the bounded polar construction needed here and in FG1. For , continuous positive calculus gives , and
The rule is therefore a well-defined isometry on the range of . Extend it to its closed range and put it zero on ; these two subspaces are orthogonal complements because is self-adjoint. This defines a partial isometry with .
It belongs to , rather than merely to . The operators
have norm at most one by continuous calculus and the C* identity. They vanish on the kernel, and on a vector their difference from has norm at most , because
Thus they converge strongly to ; the weak operator closedness of puts in . Its initial projection is the projection onto , and its final projection is the projection onto . The support itself is the strong limit of : these contractions tend to the identity on the dense range of and vanish on its kernel. Consequently . No unbounded polar-decomposition theorem has been invoked.
Let now , and let be unitary. The bounded polar construction for stays in the center. Normality of gives
so its initial and final projections are the same central support . Hence
This is the phase with value one on the zero support.
We prove its exact estimate without presuming a joint Borel-calculus theorem. For , set
The maximum and its inverse are continuous functions of the positive operator . The operators have norm at most one and converge strongly* to . On the range of , the error after multiplication by has norm at most ; the same assertion for proves the adjoint convergence. The kernel term is constant.
The commutative C*-algebra generated by has the complete character and continuous calculus from CF4–7. At a character, write for the value of , so . If , then , , and . If and , , then , and
by . If and , including , then and , giving
Characterwise positivity therefore gives the operator inequality
Bounded strong* convergence gives strong convergence of the left side to , while the right side converges in norm. The positive cone is strongly closed by its vector tests, so
All operators concerned commute and are normal. Their two squared absolute values therefore agree, and the same inequality holds for and .
For every positive normal functional , both seminorms of are thus at most twice those of . If a bounded central sequence approximates unitaries in intrinsic strong*, their phases are bounded central unitaries approximating in that same topology. This is the full alignment step in the general-center fullness criterion, with included.
FG1. Countable group factors and the finite-factor boundary
For a countable discrete group , use , with basis . Completeness follows directly by taking coordinate limits of a Cauchy sequence and passing its estimates first to finite sums and then to their supremum. Finite coordinate sums are dense, so is separable. Define
These are basis permutations, hence unitaries. Group associativity gives their representation laws and their commutation. Put .
The algebra of group polynomials is ultraweakly dense in . In detail, its norm closure is a unital C*-algebra . The exact BD1–5 proofs retained in the bounded-density component give bounded strong approximation of every element of by elements of , and ultraweak convergence of that bounded approximation. Norm approximation by polynomials makes the ultraweak closures of and the polynomial algebra agree. This supplies the density actually used below; no norm-convergent operator Fourier series is presumed.
The vector functional
is a normal state by CP's single-vector test. It is faithful. If , then for every ; these vectors fill the basis, so . In particular implies .
It is tracial on all of . The group law gives . For fixed , the two functionals and are normal by NT1's module operations and agree on group polynomials. Ultraweak density makes them agree on . For fixed , the two corresponding normal functionals of a second variable consequently agree on all polynomials and then on all of . Thus for arbitrary .
Define the coefficients . Hilbert coordinate expansion gives
If every nonidentity conjugacy class is infinite, then is a factor. For a central , traciality and centrality make its coefficients constant on conjugacy classes, since
Square summability forces every coefficient on an infinite class to vanish. Only the identity coefficient remains, so separation of gives .
The predual of is separable. In CP's projective tensor completion, finite tensors of vectors from countable dense subsets of , with rational complex coefficients, are dense: approximate each factor in a finite representation and use
Completion remains separable, and so does its quotient . This proves the countability-to-predual assertion used by the fullness criterion.
To justify the type assertion, we prove the needed finite-factor alternative. Let be a factor with a faithful finite tracial state and let be a minimal projection. Then . Indeed if a self-adjoint corner element had two different spectral values, choose a number between them. Continuous positive calculus gives nonzero orthogonal positive parts on opposite sides of that number. Their support projections, constructed by the bounded strong limits in NT3, are nonzero orthogonal corner projections. This contradicts minimality. Thus every self-adjoint corner element is scalar, and real/imaginary decomposition proves the assertion.
The closed span of is all of . Its projection commutes with , since the subspace is invariant under and its adjoints, and lies in , since the subspace is also invariant under and its adjoints. Hence ; it contains , so factoriality gives . It follows that for every nonzero projection .
Choose a maximal orthogonal family of projections equivalent to , containing , together with partial isometries having initial projection and final projection . Such a maximal family exists by the maximal principle. Every finite subfamily has total trace equal to its size times the strictly positive trace of , so the whole family has finite size . If , choose . NT3's bounded polar construction gives with nonzero and . Minimality makes , so its final projection enlarges the family, a contradiction. Therefore .
The elements are matrix units: orthogonality gives , so . For every , each belongs to . The finite decomposition
then expresses as a scalar linear combination of the . These matrix units are linearly independent by their corner products. Thus .
For infinite , the group unitaries are linearly independent by applying a finite linear relation to . Hence is infinite-dimensional. When it is a factor, the finite-factor alternative excludes minimal projections; its faithful normalized trace therefore makes it a factor of type . This argument applies both to the free groups of every countable rank at least two and to the finitely supported permutation group, once their explicit infinite-conjugacy-class proofs in the main lesson are used.
FG2. The dyadic product and its escaping trace-zero unitaries
We construct the factor needed to distinguish the free-group example. This proof needs no uniqueness assertion about arbitrary AFD algebras.
Let , with inclusion . Finite matrix tensor products identify these inclusions isometrically: after exchanging basis coordinates, acts as two identical copies of . Form their algebraic increasing union . Its compatible normalized matrix traces give a positive tracial functional , with . Each inclusion preserves the trace, by the finite diagonal sum. Faithfulness holds on this union, because each local matrix trace is faithful.
Complete for the inner product
to obtain , and write . This is a Hilbert completion by CF8/10; the trace Schwarz inequality is NT1's scalar positive-functional argument. Left and right multiplication on the local vectors are bounded. In fact
They therefore extend to ; left multiplication is a unital faithful star representation, and left and right multipliers commute. Its norm is the original matrix norm. To check the lower bound at a finite stage, choose a unit vector realizing , and a rank-one matrix with range . The ratio of its Hilbert-Schmidt norm after left multiplication to its original norm is . The upper bound was just proved.
Let
The vector state is normal by CP. It is faithful: the right orbit of contains the dense local vectors, so and commutation with right multipliers force . The norm closure of the local union is a unital C-star algebra. BD1–5 gives its bounded strong density in , and CP gives ultraweak convergence of the bounded approximants. Thus is ultraweakly dense. The two normal-functional extensions used in FG1 extend its trace law to all of : first keep one local multiplier fixed and extend the other variable, then keep an arbitrary first variable fixed and extend the second. In particular is a faithful normal tracial state on .
We prove the approximation assertion and factoriality directly. For every , there is a unique such that
Finite-dimensional Hilbert projection provides it, and, for matrix units in , its formula is
It fixes , is unital and is -bimodular. For the latter assertion, for , the trace law changes the test of into the test of against ; apply (FG2.1) and then change the trace back. Uniqueness gives .
The map is completely positive. If in , test the matrix on any column with entries in . Bimodularity and (FG2.1) with give
These tests imply matrix positivity in . Indeed, given a vector , choose a unit vector and rank-one matrices sending to and vanishing on . The trace test above is times the quadratic value on this vector. All such values are nonnegative. NT1's actual Schwarz block proof now gives
Order and unitality bound the right side by . Thus .
On , the vector is precisely the orthogonal projection of onto . These finite-dimensional subspaces increase with dense union. Their projections tend strongly to one: approximate a vector by an element of one fixed subspace, on which all subsequent projections are the identity, and use their contraction bound. Consequently
NT2 turns this bounded trace convergence into intrinsic strong* convergence.
If , bimodularity gives for all . A matrix commuting with every matrix unit is scalar: commuting with diagonal units makes it diagonal, and commuting with each off-diagonal unit makes all diagonal entries equal. Thus . Equation (FG2.2) and faithfulness show . Hence is a factor. It contains matrices of all dyadic sizes, so is infinite-dimensional. FG1's proved finite-factor alternative makes it a factor of type . The Hilbert space is separable because it has a countable union of finite-dimensional dense subspaces; CP's tensor quotient, as in FG1, makes separable.
Put , and let be in tensor position , with identities elsewhere. Then
For , it commutes with . For any fixed , trace bimodule bounds and (FG2.2) give
First make the right side small by choosing ; then let . This proves centrality in both intrinsic seminorms, by NT2 and tracial equality of adjoint -norms. The trace commutator is exactly zero. Lemma1.1 in the main lesson therefore makes this sequence centralizing without invoking the existence of a trace on any other finite algebra.
For every sequence of scalars ,
In particular there is no bounded central approximating sequence, since the center was proved scalar. The general-center criterion in Theorem4.1 makes nonfull. Its proof uses NT1–3/TS1–6, not a finite AFD uniqueness theorem.
NT4. Support of a positive normal functional
Let be positive and normal on an arbitrary von Neumann algebra ; zero and nonfaithful functionals are included. We construct the projection needed for the nonfaithful density example and for central localization.
If and , continuous calculus gives
The support construction in NT3 makes these contractions converge strongly to the range projection . CP's vector-series argument makes this bounded strong convergence ultraweak convergence. Positivity and normality therefore give .
If for projections , apply this argument to . Its kernel is , since . Thus , and . An arbitrary family of projections has a join in : its projection onto the closed span of the ranges commutes with all unitaries of , hence lies in . Its finite joins converge strongly to it, because a vector in that closed span is approximated by a finite sum of range vectors and the projections are contractions. Normality now shows that the join of any family of -zero projections is again -zero.
Let be the join of all these zero projections, and put . Then
For the latter assertion, the positive-functional Schwarz inequality gives ; expand using . The restriction to is faithful. Indeed, if in that corner and , its support is at most and at most , so it is zero and . Thus is the support projection . It equals one exactly when is faithful, and is zero for the zero functional.
For the center restriction , the same construction takes place inside the abelian von Neumann algebra . Its support is central. The restriction is faithful on , and . These are precisely the localization assertions used in Corollary1.2; existence of a center-valued trace is a separate prerequisite.
Reading and source scope
Anush Tserunyan's author-hosted notes, dated 26 November 2025, give complete comparison proofs of analytic separation (Theorem 12.6, p.48) and the Borel-image theorem (Theorem 13.3, pp.51–52). Their stated earlier reductions remain part of those source methods. Here the domain and image diameter construction proves separation and inversion directly on the given Polish domains, with topology refinement and category proved above. The human notes retain their own terms; their expression and PDF are not redistributed or given the programme's CC0 licence.