The coefficient-square order estimate bounds diagonal multiplication in the actual finite-vector form norm. Extend it and its proved adjoint to the completion. Translation is the unitary permutation of coordinates. The coordinate formulas give covariance on a dense set and hence on the completion. Applying \(\pi _\alpha (b)\) to the identity-coordinate vector with coefficient \(b^*\) gives the reverse norm inequality.

Evaluation of the integrated operator on an identity-coordinate vector recovers \(\alpha _{k^{-1}}(f(k))b\) at coordinate \(k\). If the operator vanishes, take \(b=\alpha _{k^{-1}}(f(k))^*\) and use the C\(^*\)-identity to show that every coefficient vanishes. The norm and its C\(^*\)-identity come from the ambient adjointable operators. Continuous coefficient families indexed by countably many group elements have separable range; their complex span and its closure remain separable.

The finite-vector map \(z\delta _g\mapsto z\delta _g\) preserves the coefficient inner product and therefore the norm. Both finite-vector images are dense, so it extends to a Hilbert-module unitary. Conjugation by this unitary sends every crossed-product generator to \(z\lambda _g\). The closed generator spans on the two sides coincide under this equivalence and its inverse, giving the stated restricted star-algebra equivalence.

Conjugation by \(U_g\), with inverse conjugation by \(U_{g^{-1}}\), is the constructed star-algebra automorphism of adjointable maps. The proved rank-one transport formula preserves finite-rank spans and their norm closure. Restrict the automorphism and its inverse to that compact ideal; the group laws and the equivariance of inclusion follow from the actual conjugation formulas.

Embed the amplified descended module isometrically in the actual indexed regular module and intertwine finite integration with its regular coefficient action. For a degenerate source representation, localized approximate-unit vectors lie in the embedded range and suffice for the norm estimate; no surjectivity onto the whole regular module is assumed. Faithful tensor amplification detects the operator norm. Extend the bounded finite star homomorphism through its actual dense image.

Extend the actual interval module by the pointwise coefficient representation into \(C([0,1],B\rtimes _r\Gamma )\). The balanced diagonal action integrates globally. Its reduced bound follows from actual fibre norms and the supremum norm of the coefficient-valued inner product. The fibre/interior-tensor unitary intertwines the whole source representation, grading and operator. Its endpoint isomorphisms give the full target witness. Transport the original localized compact defects through actual tensor compactness and norm closure.

The actual full-homotopy transport descends through the existing quotient relations. Completed tensor unitaries identify descent of direct sums with direct sums of descents, proving additivity. The actual opposite-cycle isomorphisms agree with negatives; zero follows by target-group cancellation. No new or weakened equivalence relation is introduced.

The comparison preserves balancing and the full coefficient-valued inner product, extends through completion, and has dense range by actual coefficient approximate units. Its pure-tensor formula intertwines the whole source action. The creation-map calculation proves all four connection compactness laws, including the adjoint companions, and extends by continuity. For positivity, transport the original positive-modulo-compacts condition and compress by arbitrary completed crossed source elements. A represented coefficient approximate unit converges on these products. Closedness of positivity modulo module compacts gives the full quadratic condition, including cross terms. Apply the existing product criterion and uniqueness theorem.

Compare actual graded product representatives using the tensor product criterion. Completed whole-cycle unitaries identify descent with the native even/graded and odd coordinate, signed-source and external-even Clifford pictures. The actual crossed pair star equivalence transports coefficient and source gradings. Existing injective bridges give the even-even, even-odd and odd-even laws. The odd-odd law uses the already genuine Pauli row/column Morita reduction to the coordinate/signed-source graded product. Thus the comparison uses the existing native products and signs; its conclusion is not an input.

Compact orbit representatives admit a nonnegative compactly supported seed \(f\) positive somewhere on every orbit. Properness makes its translated supports locally finite, so the invariant orbitwise square sum is continuous, finite and positive. Divide \(f\) by its square root. The resulting finite normalization identity also gives the convergent topological sum. Compact transporters bound the global support of every mixed coefficient. On a closed invariant piece, compact transporters are contained in those of the ambient proper action; apply the same construction to its compact intrinsic orbit quotient.

Global finite support bundles the mixed coefficients in the actual twisted coefficient algebra. Inversion and conjugation exchange the two cutoffs. Expanding the coefficient of a product factors out \(c(x)e(g^{-1}x)\) and leaves the normalized sum \(\sum _t d(t^{-1}x)^2=1\). Thus the mixed elements multiply as stated. Taking equal cutoffs proves the projection identities, and exchanging the two cutoffs gives both partial-isometry equations.

Prove the finite coefficient-pushforward reduced norm bound and extend through concrete regular closures. On the actual same descent module, the two completed source representations agree, giving an identity-module whole-cycle isomorphism. The native homomorphism-cycle product bridge identifies its representatives with source precomposition. Passing through the genuine quotients proves naturality without assuming the desired compatibility.

Properness preserves compact support of a pulled-back cutoff and equivariance preserves its normalized orbitwise sum. Compute the finite algebraic projection coefficients, pass through the actual reduced crossed homomorphism, and apply nonunital projection \(K_0\) naturality. The mixed-cutoff partial isometry removes the particular normalized cutoff choice.

Use descent naturality for the exact native source-pullback product defining the transition. Move the actual cutoff class through reduced coefficient restriction by cutoff naturality, and apply the existing native product functoriality. For a bounded piece map, Chapter 6 supplies the genuine proper restriction. Global properness of the ambient equivariant map is not assumed.

Evaluate the restricted colimit map on a piece representative. The actual Chapter 6 reindex map sends it to the same piece of the full diagram, so the piece formula proves the assembly equality. Identifying the colimits retains the essential upper-bound cofinality hypothesis. For two cofinal systems, compose the first equivalence with the inverse of the second and cancel by the actual additive-equivalence laws. Mere pointwise coverage of the ambient space cannot replace cofinality.

Piece transition and bounded-map compatibility use the actual native source-pullback naturality and cutoff projection naturality. Every colimit class has an actual piece representative, so the piece identities give pushforward and homotopy-equivalence compatibility. The explicit cofinal index comparisons retain their essential upper-bound hypotheses. Apply the established fixed-point CW uniqueness equivalence for universal proper models; no arbitrary model equivalence is assumed.