Spectral criterion for split abelian extensions [connes-001H]
✍️source

    Theorem. Spectral bridge for split abelian extensions [connes-0004]
    spectral_criterion
    L∃∀N

      A split extension \(A\rtimes H\) with \(A\) abelian turns the restriction of a unitary representation to \(A\) into harmonic analysis on the Pontryagin dual \(\widehat A\). For a vector \(\xi \), a projection-valued spectral measure \(P\) yields the positive scalar measure \[\mu _\xi (B)=\langle P(B)\xi ,\xi \rangle .\] Its total mass is \(\lVert \xi \rVert ^2\); kernel displacement becomes the energy \(\int _{\widehat A}|\chi (a)-1|^2\,d\mu _\xi (\chi )\); and quotient-fixed vectors give invariant measures. A positive atom at the trivial character yields a nonzero invariant vector through its spectral projection.

      Context

        Property (T) by spectral transfer (Zhou §4) [connes-0013]

          Qualitative property (T) [connes-001G]

            Definition. Qualitative property (T) interface [connes-0003]
            HasKazhdanPropertyTHasRelativePropertyT
            L∃∀N

              Let \(G\) be a countable discrete group. A unitary representation \(\pi \) has almost-invariant unit vectors if every finite \(K\subset G\) and every \(\varepsilon >0\) admit a unit vector \(\xi \) satisfying \[\lVert \pi (g)\xi -\xi \rVert <\varepsilon \qquad (g\in K).\] The project defines property (T) by requiring every such representation to contain a nonzero invariant vector. Relative property (T) for a subgroup \(N\leq G\) requires every such representation to contain a nonzero vector fixed by \(N\).

              Property-(T) transfer interface [connes-000V]
              HasKazhdanPropertyTHasRelativePropertyTelementaryGroup
              L∃∀N

                The exact Lean boundary for Definition [connes-0003] uses the almost-invariance and property-(T) predicates Connes.UnitaryRepresentation.HasAlmostInvariantUnitVectors, Connes.HasKazhdanPropertyT, and Connes.HasRelativePropertyT. This qualitative form matches the final consumer, while quantitative Kazhdan sets and constants remain local to any future proof of the EJZK input.

                The transfer argument uses the fixed subspace \(H^N\) of a normal subgroup \(N\) and its orthogonal complement. Relative property (T) produces a nonzero vector in \(H^N\); property (T) of the quotient then acts on \(H^N\). The relative-and-quotient transfer theorem Connes.PropertyTTransfer.hasKazhdanPropertyT_of_relative_and_quotient packages this step without exposing the concrete presentation of Zhou's groups to the spectral proof.

                A future EJZK development should use Kazhdan pairs, ratios, or spectral gaps internally, then export Connes.PaperPropertyT.elementaryGroup for property (T) of the elementary group. Demanding a particular constant at the public boundary would strengthen the paper's hypothesis and couple every consumer to an arbitrary estimate.

                Spectral criterion for split abelian extensions [connes-001H]
                ✍️source

                  Theorem. Spectral bridge for split abelian extensions [connes-0004]
                  spectral_criterion
                  L∃∀N

                    A split extension \(A\rtimes H\) with \(A\) abelian turns the restriction of a unitary representation to \(A\) into harmonic analysis on the Pontryagin dual \(\widehat A\). For a vector \(\xi \), a projection-valued spectral measure \(P\) yields the positive scalar measure \[\mu _\xi (B)=\langle P(B)\xi ,\xi \rangle .\] Its total mass is \(\lVert \xi \rVert ^2\); kernel displacement becomes the energy \(\int _{\widehat A}|\chi (a)-1|^2\,d\mu _\xi (\chi )\); and quotient-fixed vectors give invariant measures. A positive atom at the trivial character yields a nonzero invariant vector through its spectral projection.

                    Formalizing the spectral bridge [connes-000Y]
                    spectral_criterion
                    L∃∀N

                      The project records the group-theoretic data consumed by Theorem [connes-0004] in Connes.SplitAbelianExtension. The analytic layer can therefore use the kernel, quotient action, and section without unfolding a semidirect product.

                      The scalar measure and displacement interfaces are formalized in Connes.ProjectionValuedSpectralMeasure, and the finite-detection argument is packaged by Connes.spectral_criterion.

                      The direct consumer boundary is the following positive-atom estimate. If an invariant probability measure \(\mu \) satisfies \[c(1-\mu (\{1\}))\leq \sum _{a\in J}\int |\chi (a)-1|^2\,d\mu (\chi )\] for some \(c>0\), then sufficiently small displacement on the finite detector \(J\) forces \(\mu (\{1\})>0\).

                      Over \(\mathbb F_2\), characters take values through the two-element circle subgroup. The local equivalence Connes.BinaryPontryaginDual.pointwisePontryaginDualEquiv identifies the dual of a linear dual with its evaluation module. This replaces implicit Fourier coordinates by an explicit additive equivalence; it is a formalization bridge, not an additional hypothesis.

                      Elementary generation of SL₃ [connes-001I]

                        Lemma. Elementary matrices and special linear transport [connes-0005]
                        elementarySubgroup_eq_topelementaryEquivSL3
                        L∃∀N

                          Let \(R=\mathbb F_2[t]\). The subgroup \(\mathrm E_3(R)\) is generated by transvections \(I+rE_{ij}\) for \(i\ne j\). Zhou's Proposition 4.1 first uses Euclidean row reduction to identify it with \(\mathrm {SL}_3(R)\), then invokes the property-(T) theorem of [ershov2017rootgraded, Theorem 1.1 and Section 1.2]. The equality step is not part of the remaining external boundary.

                          Consequently the multiplicative equivalence Connes.PaperPropertyT.elementaryEquivSL3 transports property (T) from the elementary group named by the cited theorem to \(\mathrm {SL}_3(R)\).

                          Formalizing elementary generation and transport [connes-000W]
                          elementarySubgroup_eq_topelementaryEquivSL3
                          L∃∀N

                            The formalization proves the equality used in Lemma [connes-0005] by determinant-preserving row operations and Euclidean descent on polynomial entries, culminating in Connes.SpecialLinear.elementarySubgroup_eq_top.

                            It then constructs Connes.PaperPropertyT.elementaryEquivSL3 and transports property (T) across the named multiplicative equivalence. The external premise therefore names the exact group in the cited theorem, while the paper-facing consumer works with \(\mathrm {SL}_3(R)\).

                            Rewriting subgroup equality into carrier equality would expose dependent coercions throughout Section 4. Keeping transport at one explicit equivalence also lets later finite-index and quotient arguments remain independent of the chosen presentation.