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.

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.