Place instances at their mathematical source. The compact-dual topology, second-countability, and measurable-space instances belong beside the Pontryagin dual construction in Section 3, not at their first measure-theoretic use in Section 4. Likewise, the additive group instance for a representation module belongs at the module boundary in Section 6. Early placement makes Zhou's section order an acyclic dependency discipline instead of a directory convention.

Concrete examples are:

• the dual topology instances paperKernelTopology and paperKernelDiscreteTopology;
• the Borel instances paperCharacterMeasurableSpace and paperCharacterBorelSpace; and
• the representation-module carrier instance representationAsModuleAddCommGroup.

Isolate certificates from structural theorems. The finite symplectic enumeration, concrete orbit witnesses, and detector estimates live in dedicated files. Their consumers see named propositions or small structures. This prevents an exhaustive certificate, coordinate calculation, or normalization choice from contaminating a generic transfer theorem.

State the direct consumer boundary. The external theorem is requested as property (T) of the elementary group, not as a stronger numerical constant. The factor bridge asks for a spatial unitary that maps completed algebras and the vacuum. The ICC bridge asks for orbit and displacement data. Each boundary contains exactly what its next theorem consumes, which makes hypothesis strength and reuse auditable.

The formalization uses the topology of the fiber shear at an intermediate step. It defines the shear as an equivariant measure-preserving homeomorphism because pullback must preserve continuous coefficients. Once this density argument is complete, the crossed-product theorem uses only the underlying equivariant measurable equivalence.

Zhou's shear need not be additive, so the Lean proof does not treat it as a compact-group automorphism. Continuity is retained for the density argument and then forgotten. This matches the two roles separated in [zhou2026icc, Proposition 3.2 and Remark 3.3].

A second lesson came from the reverse inclusion between the generated operator algebras. Mathlib's continuous pullback is already a star-algebra equivalence, so its surjectivity proves that inclusion without a separate involutivity calculation. Similarly, the inverse law for conjugation by a linear isometry equivalence replaces a pointwise operator calculation. In both cases, an equality that first looked computational follows from the inverse laws of an equivalence.

Zhou's Proposition 3.4 identifies the two group factors by combining Fourier transform with the fiber shear [zhou2026icc, Proposition 3.4]. The Lean development records two properties of the resulting star-algebra equivalence explicitly. Preservation of projection suprema in both directions follows automatically from the star-algebra equivalence between these concrete operator subalgebras, while preservation of the canonical trace is proved from the spatial unitary.

The definition Connes.IsProjectionSupremum says that \(p\) is a projection, every member of \(S\) is a projection below \(p\), and \(p\) lies below every projection that is an upper bound for \(S\). The last condition ranges only over projections, rather than all upper bounds as in the stronger ambient predicate IsLUB.

For star subalgebras of bounded operators, the usual order on projections is characterized by \(p\leq q\iff pq=p\). A star-algebra equivalence preserves multiplication, so Connes.IsProjectionSupremum.map_starAlgEquiv uses this characterization to preserve projection suprema. Applying the same argument to the equivalence and its inverse gives Connes.StarAlgEquiv.isNormal.

This refactor leaves the definitions of projection supremum and normal star-algebra equivalence independent of bounded operators. The operator order appears only in the theorem that applies those definitions to the group factors in Theorem [connes-0007].

To identify the generated von Neumann algebras, Lean checks what each chosen unitary does to the regular-representation generators. There is one calculation for the abelian kernel and one for the acting group in each of Zhou's two group constructions, giving four identities in all.

For the first group, see the kernel calculation and the acting-group calculation. For the second group, see the corresponding kernel calculation and acting-group calculation.

These calculations spell out a step summarized by the Fourier and crossed-product identifications in [zhou2026icc, Proposition 3.4]. They carry the generators through the Fubini equivalence for a semidirect product and then through the Fourier unitary.

Most explicit heartbeat settings disappeared during the later proof cleanup. These four declarations still require a larger elaboration limit because Lean must simplify nested equivalences and pointwise operator formulas. The limit controls elaboration time; it adds no mathematical assumption.

Keep final assembly proposition-valued. Section 7 combines previously proved endpoints. It does not accept a broad record containing the desired conclusion as a field. This “certificate isolation” makes #print axioms meaningful and lets semantic review trace each conjunct to the file where its mathematics occurs.

The nonisomorphism conjunct is stated directly as the absence of a multiplicative equivalence, \(\neg \operatorname {Nonempty}(\Gamma _1\simeq \Gamma _2)\), rather than through a project-local synonym. This is Lean's standard expression for the absence of a group isomorphism, so the result proved in Section 6 can be used directly.

The same assembly pattern applies when a linear paper proof crosses topology, analysis, finite computation, and algebraic transport: export small propositions from those layers, then combine them only at the theorem boundary.