Dependency placement and consumer boundaries [connes-000A]

✍️source

completion_of_spectralDatapaperSpatialWitnessActionData

L∃∀NAGENTDRAFTED

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.

Index shared structure by the action. Zhou's two groups have the same abelian kernel and acting group, but different actions [zhou2026icc, Sections 2–5]. Lean therefore defines their common semidirect-product carrier through paperGammaOf, then indexes the split extension lambdaExtension, finite extension finiteExtension, spectral data SpectralData, and ICC data ActionData by the chosen action. The final theorems for the two groups specialize these definitions to the two concrete actions. The actions and their finite certificates remain distinct, while the shared structural arguments are proved once.

Keep the bicommutant boundary visible. The group von Neumann algebra in Zhou's factor comparison is the bicommutant of the left regular operators [zhou2026icc, Section 3 and Proposition 3.4]. The definition Connes.vonNeumannClosure still expresses that same bicommutant. Its Lean implementation now bundles the first StarSubalgebra.centralizer as a von Neumann algebra and applies VonNeumannAlgebra.commutant for the outer commutant. This removes a duplicated proof of the outer commutant's double-commutant condition; it does not replace the bicommutant by a topological closure or change the mathematical boundary.

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.