Representation-space universe boundary [connes-000L]
✍️source
HasKazhdanPropertyT
L∃∀N

    The cited literature formulates property (T) by quantifying over unitary representations. The basic definitions and elementary-group theorem appear in [ershov2010noncommutative, Section 3.1 and Theorem 1.1]; the root-graded generalization is [ershov2017rootgraded, Theorem 1.1]. Lean must also make the size of each carrier explicit.

    The current Connes.HasKazhdanPropertyT takes a group in Type u and quantifies over Hilbert carriers in the same Type u. This conventional interface is sufficient for the theorem schema formalized here.

    It matches the spectral consumer: spectral_criterion_unconditional is uniform in each K : Type u and each UnitaryRepresentation G K, rather than selecting one concrete \(\ell ^2\) or regular representation.

    The interface does not assert universe independence. A classical theorem quantifying over carriers in every universe implies this predicate by restriction to Type u; thus EJZK safely supplies the premise used here. The converse is nontrivial and is not part of the present interface.

    For a countable group, that converse has a two-stage route:

    1. Choose witnesses for every finite subset and a cofinal sequence of positive accuracies. The closed span of their group orbits is invariant, complete, separable, and still has almost-invariant unit vectors. An invariant vector there remains invariant in the original representation.
    2. Choose a countable Hilbert basis, reindex it by a small countable type, and conjugate the action onto the resulting \(\ell ^2\) carrier in the group's universe. The same-universe predicate then gives the polymorphic statement.

    The pinned Mathlib already contains separability of spans (TopologicalSpace.IsSeparable.span), separability of closures (TopologicalSpace.IsSeparable.closure), completeness of closed spans (Submodule.topologicalClosure.completeSpace), and Hilbert-basis existence (exists_hilbertBasis).

    At the pinned TauCeti revision, the continuous-representation library provides invariant restriction (TauCeti.ContRepresentation.subrepresentation), unitarity under restriction (TauCeti.ContRepresentation.IsUnitary.subrepresentation), and transport along an isometry (TauCeti.ContRepresentation.IsUnitary.congr).

    Its compact-group lane also standardizes finite-dimensional carriers (TauCeti.IrrepModel) by an orthonormal basis, following the explicit finite-dimensional universe convention in its roadmap.

    Neither pinned codebase assembles the countable invariant span, gives its Hilbert basis a small countable index, or transports the full property-(T) predicate across that model. Together these form the lowering seam.

    They are more focused than generalizing the entire Connes.spectral_criterion_unconditional stack, but remain separate from closing the EJZK premise and from the present formalization.