Characteristic-two tensor kernel (Zhou §2) [connes-0011]
✍️source

    1. Tensor retraction in characteristic two [connes-001E]

      Lemma. Characteristic-two tensor retraction [connes-000C]
      delta_diagonalconcreteSquareSpanData
      L∃∀N

        Let \(k=\mathbb F_2\), \(A=k[t]^3\), and let \[C=(A\otimes _k A)^{\mathrm {Flip}}.\] The diagonal function \(\Delta (a)=a\otimes a\) lands in \(C\). Although \(\Delta \) is not a linear map, Zhou's characteristic-two calculation produces a surjective linear retraction \(\delta :C\to A\) satisfying \(\delta (\Delta (a))=a\) [zhou2026icc, Section 2, Lemma 2.1]. The retraction is equivariant for the diagonal \(\mathrm {SL}_3(k[t])\)-action.

        2. Formalizing the characteristic-two retraction [connes-000U]
        delta_diagonalconcreteSquareSpanData
        L∃∀N

          The Lean carriers and diagonal for Lemma [connes-000C] are Connes.Construction.PaperKernel.C and Connes.Construction.PaperKernel.diagonal; the coefficientwise map and retraction equation are Connes.Construction.PaperKernel.delta and Connes.Construction.PaperKernel.delta_diagonal.

          The implementation fixes the standard polynomial and coordinate bases. It takes the coefficientwise Hadamard product on \(k[t]\), applies it in the three coordinates of \(A\), lifts the resulting bilinear map through the tensor product, and restricts it to \(C\). The Boolean identity \(x^2=x\) gives \(\delta (a\otimes a)=a\).

          The basis-dependent formula implements a basis-free role: a linear left inverse to the diagonal squares, equivariant for the diagonal \(\mathrm {SL}_3(k[t])\)-action. Equivariance is not proved by expanding an arbitrary fixed tensor. The submodule Connes.Construction.PaperKernel.squareSpan is the span of the squares \(a\otimes a\); the equation is immediate on each square, hence on their span.

          The basis calculation in Connes.Construction.PaperKernel.concreteSquareSpanData proves that every flip-fixed tensor belongs to this span. The SquareSpanData interface therefore hides the coordinates from later sections. Consumers need only the spanning result, so a future basis-free construction could replace the formula without changing the action or theorem interfaces.

          References

            Reference. ICC property-(T) groups without W-star-superrigidity [zhou2026icc]

            @misc{zhou2026icc,
  title = {ICC Property-(T) Groups Without W*-Superrigidity},
  author = {Zhou, Shuoxing},
  year = {2026},
  eprint = {2608.02327},
  archivePrefix = {arXiv},
  primaryClass = {math.OA},
  url = {https://arxiv.org/abs/2608.02327}
}

            Context

              Notes on formalizing counterexamples to Connes' rigidity conjecture [connes-0001]
              📄PDF

              These notes treat the OpenAI, Zhou, and Anthropic counterexamples to Connes' rigidity conjecture as three distinct formalization targets. All three proofs are in scope; the current detailed development follows Zhou's construction.

              Introduction [connes-0010]

              Connes' rigidity conjecture [connes-000O]

                For a countable discrete group \(\Gamma \), the group von Neumann algebra \(L(\Gamma )\) is generated by the left regular representation of \(\Gamma \). When \(\Gamma \) has infinite conjugacy classes (ICC), meaning that every nonidentity conjugacy class is infinite, \(L(\Gamma )\) is a \(\mathrm {II}_1\) factor. The reconstruction question asks how much of \(\Gamma \) remains visible in that analytic completion.

                Kazhdan's property (T) says that a unitary representation with almost invariant unit vectors has a nonzero invariant vector [ershov2010noncommutative, Section 3.1]. ICC makes the group von Neumann algebra a factor, while property (T) imposes representation-theoretic rigidity. These are the two hypotheses in the conjecture and in all three counterexample constructions below [zhou2026icc, Section 1, pp. 1–2].

                Connes first proved that, for an ICC property-(T) group, \(\operatorname {Out}(L(\Gamma ))\) and the fundamental group \(\mathcal F(L(\Gamma ))\) are countable [zhou2026icc, Section 1, p. 1].

                He subsequently proposed that such groups should be \(W^*\)-superrigid: for every countable group \(\Lambda \), an isomorphism \(L(\Lambda )\cong L(\Gamma )\) should force \(\Lambda \cong \Gamma \). Zhou's introduction states this original 1982 conjecture and distinguishes it from the later, narrower rigidity question for higher-rank lattices [zhou2026icc, Section 1, pp. 1–2].

                The counterexamples considered here disprove the broad conjecture. They do not settle that higher-rank-lattice question.

                Counterexample background [connes-000P]

                  The OpenAI and Zhou counterexamples were obtained independently and at nearly the same time. Zhou records that his preliminary manuscript predated the public OpenAI announcement, while acknowledging that the two projects were concurrent [zhou2026icc, Section 1, pp. 2–3].

                  OpenAI gives a countable family of pairwise nonisomorphic ICC property-(T) groups with isomorphic group factors [openai2026tenadvances, Chapter 4]. Zhou gives an explicit pair through a different action-changing construction [zhou2026icc, Theorem A and Section 3].

                  The later Anthropic proof gives another explicit pair by comparing a split extension with a nonsplit one [anthropic2026icc, Sections 3–5].

                  These are not three presentations of one proof. The algebraic datum hidden by the factor sits at a different level in each construction, and each factor argument removes it by a different measurable mechanism. The mathematical and formalization motivations for comparing them are stated next. The detailed OpenAI and Anthropic architectures appear in § [connes-000M] and § [connes-000N]; Sections 2–7 below follow Zhou's proof in its original order.

                  Motivation [connes-000Z]

                    The motivation for this formalization experiment is threefold.

                    Mathematical motivation

                      The three counterexamples form a controlled test of nonfaithfulness. OpenAI varies the abelian kernel [openai2026tenadvances, Chapter 4]; Zhou fixes the kernel while varying the action and module structure [zhou2026icc, Sections 1 and 3]; and Anthropic fixes both while varying the extension class [anthropic2026icc, Sections 3–5]. In each construction, a genuine group distinction survives algebraically but disappears after measurable crossed-product transport. The comparison asks which distinctions survive representation, twisting, duality, and analytic completion. Property (T) here serves as a control condition: failure of reconstruction persists for groups with strong representation-theoretic rigidity.

                      Formalization motivation

                        Formalization asks where the information is lost. Named interfaces for the characteristic-two retraction, Fourier shear, measurable transport, continuous closure, spectral detection, and characteristic-module obstruction turn the claim that a factor forgets structure into an auditable dependency map. This separates direct translation from designed bridges and makes the project a consumer of Mathlib and TauCeti. Missing or bespoke interfaces mark candidates for reusable contributions to those libraries.

                        Agent-assisted work and human examination

                          The project also tests whether an agent-authored formalization can be brought to a standard suitable for human examination and digestion. Literature grounding, the exact external premise boundary, provenance, technical proof replay, mathematical audit, and companion notes answer different questions. Technical verification checks the formal statement and its replay; source and mathematical review ask whether the theorem, definitions, hypotheses, and supporting facts match the intended mathematics. A reader can then trace a claim from the literature to its Lean declaration, downstream use, audit status, and executable check.

                          Formalization design [connes-000K]

                          The Lean development turns the preceding motivations into one construction stage and four certificate lanes: factor equivalence, property (T), ICC, and group nonisomorphism. The final theorem assembles those four endpoints.

                          The diagram is a map of both the proof and the notes. Solid arrows are internal Lean developments. The dashed arrow is the sole substantive mathematical input left external: the Ershov–Jaikin-Zapirain–Kassabov property-(T) theorem for \(\mathrm {EL}_3(\mathbb F_2[t])\). Each lane uses a separate port at the construction and theorem nodes.

                          The mathematical weight is uneven:

                          Most definitions and algebraic laws translate directly. Six interfaces require special design:

                          The formalization lessons are discussed in § [connes-000A], § [connes-000F], § [connes-001C], § [connes-001D], and § [connes-000J].

                          The code has two layers. Reusable group theory, linear algebra, topology, measure theory, and operator algebra live in a foundation layer. Zhou-specific carriers and certificates live in construction and paper layers. This separation lets the paper-facing modules state small consumer interfaces while coordinate or finite calculations remain behind named certificates.

                          The public formalization plan and statement map give the complete module and declaration crosswalk.

                          Each lane exports the smallest object needed by its next consumer: a spatial witness, a qualitative property-(T) certificate, orbit and displacement data, or a twist-stable module obstruction.

                          Four corrections were mathematically decisive:

                          • replace identity-action scaffolds by Zhou's actions;
                          • make the ICC abstraction handle the finite \(\operatorname {Sp}_4(\mathbb F_2)\) factor;
                          • follow the quotient automorphism induced by a hypothetical group isomorphism; and
                          • tie the factor target to the Fourier shear and completed von Neumann closures.

                          The final interface remains proposition-valued. Its assembly and trust boundary are detailed in § [connes-0002] and Theorem [connes-0009]; the remaining EJZK work is scoped in § [connes-000B], § [connes-000G], and § [connes-000I]; the representation-universe boundary is recorded in § [connes-000L].

                          Section 1 separates the mathematical introduction, counterexample background, three motivations, and design. Sections 2–7 correspond respectively to Zhou's Sections 2–7; their headings record that correspondence without reusing Zhou's section number as the note title. Section 8 collects proof-engineering adaptations. The challenge and its verification role are described in § [connes-001M]; § [connes-0018] and § [connes-0019] compare the other two proof architectures; § [connes-001A] scopes the remaining EJZK formalization; and § [connes-001B] records the human–agent contribution and review workflow.

                          The formalization adapts selected public Lean proof blocks and organization patterns from a pinned openai/ten-proofs snapshot, but does not import that repository. The project records declaration-level adaptations in its public port map; the concrete Zhou carriers, corrected theorem boundaries, and final assembly are local to this development.

                          Characteristic-two tensor kernel (Zhou §2) [connes-0011]
                          ✍️source

                            Tensor retraction in characteristic two [connes-001E]

                              Lemma. Characteristic-two tensor retraction [connes-000C]
                              delta_diagonalconcreteSquareSpanData
                              L∃∀N

                                Let \(k=\mathbb F_2\), \(A=k[t]^3\), and let \[C=(A\otimes _k A)^{\mathrm {Flip}}.\] The diagonal function \(\Delta (a)=a\otimes a\) lands in \(C\). Although \(\Delta \) is not a linear map, Zhou's characteristic-two calculation produces a surjective linear retraction \(\delta :C\to A\) satisfying \(\delta (\Delta (a))=a\) [zhou2026icc, Section 2, Lemma 2.1]. The retraction is equivariant for the diagonal \(\mathrm {SL}_3(k[t])\)-action.

                                Formalizing the characteristic-two retraction [connes-000U]
                                delta_diagonalconcreteSquareSpanData
                                L∃∀N

                                  The Lean carriers and diagonal for Lemma [connes-000C] are Connes.Construction.PaperKernel.C and Connes.Construction.PaperKernel.diagonal; the coefficientwise map and retraction equation are Connes.Construction.PaperKernel.delta and Connes.Construction.PaperKernel.delta_diagonal.

                                  The implementation fixes the standard polynomial and coordinate bases. It takes the coefficientwise Hadamard product on \(k[t]\), applies it in the three coordinates of \(A\), lifts the resulting bilinear map through the tensor product, and restricts it to \(C\). The Boolean identity \(x^2=x\) gives \(\delta (a\otimes a)=a\).

                                  The basis-dependent formula implements a basis-free role: a linear left inverse to the diagonal squares, equivariant for the diagonal \(\mathrm {SL}_3(k[t])\)-action. Equivariance is not proved by expanding an arbitrary fixed tensor. The submodule Connes.Construction.PaperKernel.squareSpan is the span of the squares \(a\otimes a\); the equation is immediate on each square, hence on their span.

                                  The basis calculation in Connes.Construction.PaperKernel.concreteSquareSpanData proves that every flip-fixed tensor belongs to this span. The SquareSpanData interface therefore hides the coordinates from later sections. Consumers need only the spanning result, so a future basis-free construction could replace the formula without changing the action or theorem interfaces.

                                  Factor equivalence by Fourier shear (Zhou §3) [connes-0012]

                                    Spatial factor equivalence [connes-001F]

                                      Theorem. Spatial implementation of the factor equivalence [connes-0007]
                                      SpatialWitnessisNormaltracialEquiv_of_spatialWitnesspaperGroupFactors_isomorphic
                                      L∃∀N

                                        The group von Neumann algebra \(L(G)\) is represented on \(\ell ^2(G)\) as the von Neumann closure of the left regular operators. Its canonical trace is the vacuum coefficient at \(\delta _e\). Consequently a unitary \(U:\ell ^2(G)\simeq \ell ^2(H)\) gives the required tracial equivalence once two facts are proved: conjugation by \(U\) carries one closed operator algebra onto the other, and \(U\delta _e=\delta _e\).

                                        These are precisely the fields of Connes.FactorWitness.SpatialWitness.

                                        The theorem Connes.FactorWitness.tracialEquiv_of_spatialWitness restricts unitary conjugation to the two group von Neumann algebras. Connes.StarAlgEquiv.isNormal records the automatic preservation of projection suprema by the induced star-algebra equivalence and its inverse. The equation \(U\delta _e=\delta _e\) proves preservation of the canonical trace. Neither property is supplied as an extra assumption.

                                        For Zhou's groups, the concrete unitary composes the two Fourier models with the fiber shear. The measure-transport and von Neumann closure obligations are separated in § [connes-000D] and § [connes-000E]. Together they construct Connes.PaperFactorClosure.paperSpatialUnitary, Connes.PaperFactorClosure.paperSpatialWitness, and Connes.PaperFactorClosure.paperGroupFactors_isomorphic. This is the \(*\)-isomorphism asserted in [zhou2026icc, Proposition 3.4]; the Lean statement also records its projection-supremum preservation and preservation of the canonical trace.

                                        Nonadditive shear and measure transport [connes-000D]
                                        EquivariantHaarHomeomorphpaperHaarHomeomorph
                                        L∃∀N

                                          Proposition 3.2 proves that the fiber shear preserves Haar measure and strictly conjugates the two actions. Its quadratic correction is generally not additive, so Zhou's Remark 3.3 does not claim a compact-group automorphism. Proposition 3.4 uses only the resulting equivariant measure-space isomorphism after Fourier transform [zhou2026icc, Proposition 3.2, Remark 3.3, and Proposition 3.4].

                                          The independent crossed-product discussion in [openai2026tenadvances, Chapter 4, Section 2.3, equation (2.1)] states the same abstract mechanism: group-law compatibility of the underlying compact spaces is not required.

                                          The Lean boundary mirrors this distinction. The concrete Connes.PaperCrossedHaar.paperFiberShearHomeomorph and Connes.PaperCrossedHaar.paperHaarHomeomorph package continuity, measure preservation, and action equivariance, but no additive-homomorphism field.

                                          At the foundation layer, Connes.CrossedProduct.EquivariantHaarHomeomorph projects this topological witness to the measurable transport interface. The extra topology is an implementation aid, not a stronger mathematical premise for the crossed-product identification.

                                          A measurable equivariant isomorphism is mathematically sufficient for the abstract transport. The concrete homeomorphism is formally convenient because pullback preserves continuous coefficients. The proof uses that extra structure for the density bridge and forgets it at the measurable boundary, without falsely requiring an additive equivalence. The separate closure step is recorded in § [connes-000E].

                                          Continuous coefficients and von Neumann closure [connes-000E]
                                          continuousCrossedClosure_mem_iff
                                          L∃∀N

                                            Coordinate characters have norm-dense linear span in the continuous functions by Stone–Weierstrass. Since continuous coefficients act continuously as crossed-product multipliers, the generic continuous-coefficient closure theorem Connes.CrossedProduct.vonNeumannClosure_crossedGeneratorSetOfContinuousCoefficients_eq upgrades that density to equality of the generated von Neumann closures.

                                            Pullback along the homeomorphism then gives Connes.CrossedProduct.continuousCrossedClosure_mem_iff. This does not say that continuous functions are norm-dense in \(L^\infty \); it compares the von Neumann closures generated after adjoining all continuous coefficients.

                                            The paper-facing proof applies the transport and closure bridges once to each action, then composes the Fourier models with the shear. This removes parallel action-one/action-two closure plumbing while preserving Zhou's Proposition 3.4 endpoint and section order. Mapping a convenient generating family remains an intermediate step; the consumer-facing contract is equivalence of membership in the completed von Neumann algebras.

                                            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]

                                                      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.

                                                                ICC by orbit displacement (Zhou §5) [connes-0014]

                                                                  ICC criterion [connes-001J]

                                                                    Theorem. Orbit and displacement criterion for ICC [connes-0006]
                                                                    isICC_of_product_quotientpaper_gammaOne_iccpaper_gammaTwo_icc
                                                                    L∃∀N

                                                                      For a countable group, the ICC condition asks that every nonidentity conjugacy class be infinite. In a semidirect product \(N\rtimes (S\times Q)\), the proof can be separated from the concrete formulas by supplying two kinds of certificates:

                                                                      1. every nonidentity \(a\in N\) has an infinite \(S\)-orbit; and
                                                                      2. every nonidentity \(q\in Q\) admits \(a\in N\) whose displacement \(a(q\cdot a)^{-1}\) is nonidentity and has an infinite \(S\)-orbit.

                                                                      The structure Connes.PaperICC.ActionData is exactly this direct-consumer boundary. The generic theorem Connes.PaperICC.isICC_of_product_quotient then proves that these certificates imply ICC by splitting a nonidentity element into three exhaustive cases.

                                                                      • A nontrivial \(S\)-coordinate inherits an infinite conjugacy class from \(S\).
                                                                      • A pure kernel element uses the first certificate.
                                                                      • A surviving \(Q\)-coordinate reduces to the second certificate.

                                                                      This organization follows the cases used in [zhou2026icc, Section 5] without building the concrete tensors into the reusable ICC theorem.

                                                                      Formalizing the ICC criterion [connes-000X]
                                                                      isICC_of_product_quotientpaper_gammaOne_iccpaper_gammaTwo_icc
                                                                      L∃∀N

                                                                        The paper-specific work behind Theorem [connes-0006] is confined to orbit calculations in ICCOrbits.lean. Those calculations construct the action data and yield Connes.PaperICC.paper_gammaOne_icc and Connes.PaperICC.paper_gammaTwo_icc.

                                                                        The displacement certificate is the finite-quotient input. Conjugating an element with nontrivial \(Q\)-coordinate by a kernel element changes its kernel coordinate by \(a(q\cdot a)^{-1}\). Asking directly for an infinite family of conjugates would duplicate this algebra for each action. The certificate instead exposes the one displacement whose infinite \(S\)-orbit suffices.

                                                                        Nonisomorphism by characteristic modules (Zhou §6) [connes-0015]

                                                                          Characteristic-module obstruction [connes-001K]

                                                                            Theorem. Characteristic modules detect nonisomorphism [connes-0008]
                                                                            firstProduct_semisimplepaperCharacteristicModuleEquivpaperGroups_not_isomorphic
                                                                            L∃∀N

                                                                              The Section 6 invariant is semisimplicity of a module obtained from the characteristic abelian kernel. This is suitable for formal transport: a group isomorphism identifies the characteristic kernels, descends to an automorphism \(\sigma \) of the finite quotient, and induces a linear equivalence between the first quotient module and the second module with its action restricted along \(\sigma \). Semisimplicity is invariant under that linear equivalence.

                                                                              The characteristic-kernel and quotient-twist boundaries used here are separated in § [connes-000H].

                                                                              On the first side, explicit decomposition into simple summands culminates in Connes.PaperModuleSemisimple.firstProduct_semisimple.

                                                                              On the second side, a nonsplit submodule obstruction is proved for every quotient twist \(\sigma \). The bridge Connes.PaperNonisomorphism.paperCharacteristicModuleEquiv turns a hypothetical group isomorphism into the forbidden module equivalence.

                                                                              The public contradiction is Connes.PaperModuleSemisimpleTransport.paperGroups_not_isomorphic. This records the invariant used in [zhou2026icc, Section 6] while keeping the group-theoretic, finite-certificate, and module-theoretic arguments in separate files.

                                                                              Characteristic kernels and quotient-twisted transport [connes-000H]

                                                                                The characteristic-kernel step maps an abelian normal subgroup to both factors of \(\mathrm {SL}_3(\mathbb F_2[t])\times \operatorname {Sp}_4(\mathbb F_2)\). It therefore needs two vanishing results:

                                                                                The product argument applying both inputs is paperSemidirectNormalAbelian_le_kernel. This confines finite enumeration to the symplectic factor and keeps both factor-specific proofs out of the abstract module transport.

                                                                                Design adaptation: twisting does not repair nonsplitting. Restriction along a group automorphism is an equivalence of module categories, with inverse given by restriction along the inverse automorphism. The formal proof nevertheless exports the exact twisted obstruction needed by the consumer, so no unproved categorical transport principle remains hidden at the final contradiction.

                                                                                Theorem assembly and trust boundary (Zhou §7) [connes-0016]

                                                                                  Exact external boundary [connes-0002]
                                                                                  theoremAelementaryGroup
                                                                                  L∃∀N

                                                                                    The public theorem is Connes.theoremA. Its sole mathematical parameter is \(\operatorname {HasKazhdanPropertyT}(\mathrm {EL}_3(\mathbb F_2[t]))\). The corresponding Lean boundary consists of Connes.PaperPropertyT.elementaryGroup and EJZKInput.

                                                                                    All spectral, factor, ICC, and nonisomorphism certificates downstream of that parameter are constructed in the project. This is completeness for the load-bearing content of Zhou's Theorem A under the project's definitions, not a claim that every expository sentence of [zhou2026icc] has been encoded.

                                                                                    The dependency boundary is deliberately narrow:

                                                                                    The solution import graph contains no axiom, opaque declaration, sorry, or admit. Lean's axiom report for Connes.theoremA contains only:

                                                                                    • propext;
                                                                                    • Classical.choice; and
                                                                                    • Quot.sound.

                                                                                    These are the usual Lean foundations used by the imported library. The one sorry in an independent Comparator challenge is outside the theorem's import graph.

                                                                                    Theorem A [connes-001L]

                                                                                      Theorem. Assembly of Theorem A [connes-0009]
                                                                                      theoremAtheoremA
                                                                                      L∃∀N

                                                                                        The final assembly has four independent certificate branches. The spectral branch proves property (T) for both concrete groups from the EJZK input and the internally constructed finite detectors. The other branches provide ICC, the trace-preserving group-factor equivalence, and nonisomorphism. The theorem Connes.PaperTheoremACompletion.theoremA only gathers those endpoints; it performs no additional mathematical construction.

                                                                                        The source-facing declaration Connes.theoremA unwraps the one-field EJZK input and states the full existence conclusion. Its single substantive mathematical premise is \(T(\mathrm {EL}_3(\mathbb F_2[t]))\). The local equality \(\mathrm {EL}_3=\mathrm {SL}_3\), all transfers, and every certificate for the two groups are already proofs in the import graph.

                                                                                        Kernel and source trust boundary. The precise external premise, axiom report, and meaning of completeness are recorded once in § [connes-0002].

                                                                                        Formalization adaptations [connes-0017]

                                                                                          Dependency placement and consumer boundaries [connes-000A]
                                                                                          completion_of_spectralDatapaperSpatialWitnessActionData
                                                                                          L∃∀N

                                                                                            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:

                                                                                            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.

                                                                                            Structure forgetting and equivalence reuse [connes-000F]
                                                                                            EquivariantHaarHomeomorphcontinuousCrossedClosure_mem_iff
                                                                                            L∃∀N

                                                                                              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.

                                                                                              Normality of the factor isomorphism [connes-001C]
                                                                                              IsProjectionSupremumisNormal
                                                                                              L∃∀N

                                                                                                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].

                                                                                                Four conjugation identities [connes-001D]

                                                                                                  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.

                                                                                                  Proposition-valued final assembly [connes-000J]
                                                                                                  theoremAtheoremA
                                                                                                  L∃∀N

                                                                                                    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.

                                                                                                    Comparator challenge and auditability [connes-001M]

                                                                                                      The Comparator challenge is an independent statement file, not a second formalization of Zhou's proof. Its purpose is to make the theorem small enough that a reader familiar with the mathematics and Lean can inspect the definitions, compare them with Zhou's Sections 3–7, and check that the solution proves the same statement [zhou2026icc, Sections 3–7]. It therefore uses the following design criterion: define no more vocabulary than is needed to state Theorem A. General notions should come from Mathlib when its definitions have the required meaning; a genuinely general local construction is a candidate for upstreaming rather than permanent duplication. The self-contained challenge at the synchronized commit is the file to inspect. The declaration links below point to the mirrored solution-side declarations, which have the same public contracts and are rendered by doc-gen4.

                                                                                                      The declarations in that file divide into four groups.

                                                                                                      • Mathematical-domain foundation. groups, ICC, representations, their invariant and almost-invariant vector predicates, and property (T) state the group-theoretic side. The operator-algebraic side starts from ℓ². It comprises the bicommutant, the algebra and its carrier, the point mass, the trace, and the witness. The witness combines a star-algebra equivalence, trace preservation, and normality. The normality predicate defines normality by preservation of suprema in both directions. The predicate isomorphism asks only for a nonempty equivalence structure. These definitions support the factor-isomorphism proposition in the conclusion, using Mathlib's conjugacy classes, unitary operators, star subalgebras, and von Neumann algebras underneath.
                                                                                                      • Theorem-specific data. The abbreviations \(\mathbb F_2\), \(\mathbb F_2[t]\), and \(\mathrm {SL}_3(\mathbb F_2[t])\), together with their inferred countability instances, fix the coefficient ring and ambient matrix group. The subgroup and EJZK group declarations name the exact \(EL_3(\mathbb F_2[t])\) premise from Zhou's Proposition 4.1. The declaration Connes.theoremA then states property (T) and ICC for both groups, factor equivalence, and nonisomorphism from Zhou's Theorem A.
                                                                                                      • Paper-shape adaptation and transport. membership, reindexing, and unitaries build the operators, while representation turns Mathlib's general \(\ell ^p\) carrier into the left regular \(\ell ^2(G)\) model used in Section 3. The polynomial countability proof similarly transports an existing countability instance across Mathlib's polynomial–finitely-supported-function equivalence. These declarations adapt library representations; they add no hypothesis to Theorem A.
                                                                                                      • Verification boundary. The challenge imports Mathlib, not the solution, and leaves only the body of Connes.theoremA unspecified. Comparator compares its elaborated statement and definition closure with the solution, checks the permitted axiom set, and replays the exported proof with the Lean kernel and nanoda. This checks technical identity and proof acceptance. Literature fidelity and the correctness of the mathematical definitions remain separate review questions.

                                                                                                      Recent simplifications illustrate the design. The reindexing proof now shares Connes.memℓp_reindex between its forward and inverse maps. It keeps the two pointwise action laws in Connes.leftRegularRepresentation, since they fix the left-action convention used in [zhou2026icc, Section 3].

                                                                                                      Mathlib now supplies the conjugacy-class operation, the centralizer star subalgebra, and the commutant of a von Neumann algebra. The challenge reuses those APIs. In particular, Connes.vonNeumannClosure remains Zhou's bicommutant construction, but its implementation can form the first StarSubalgebra.centralizer and then apply VonNeumannAlgebra.commutant; no separate proof of the outer commutant's double-commutant condition is needed.

                                                                                                      The concrete elementary subgroup and explicit EJZK premise are theorem-specific and should remain near the challenge. The trace-preserving factor witness is local statement vocabulary chosen to match Theorem A; it should remain local unless Mathlib adopts the same contract. By contrast, an arbitrary-index \(\ell ^2\) reindexing linear isometry and a bundled left regular unitary representation are genuinely general and plausible Mathlib contributions: the present library has the ingredients but no direct API with these contracts. If those are upstreamed, the reindexing lemma and the two action-law proofs can disappear from the challenge. Without that library API, further proof compression would mainly conceal the chosen left-action convention rather than remove mathematics.

                                                                                                      OpenAI proof architecture [connes-0018]

                                                                                                        Changing the kernel while preserving the measured action [connes-000M]
                                                                                                        paperHaarEquivpaperGroupFactors_isomorphic
                                                                                                        L∃∀N

                                                                                                          Chapter 4 of [openai2026tenadvances] constructs a countable family \(\Gamma _n=E_n\rtimes K\). The acting property-(T) group \(K\) is fixed, while the discrete abelian kernels \(E_n\) are dual to different compact group laws on one underlying probability space. Binary carry changes the compact group structure but not its Borel probability space or the relevant \(K\)-action.

                                                                                                          Pontryagin duality therefore presents every group factor by the same measured crossed product \(L^\infty (X\times Y)\rtimes K\) [openai2026tenadvances, Chapter 4, Sections 2.3, 4, and 6.1–6.2].

                                                                                                          The proof separates the information forgotten by the group-factor functor from the information retained by the abstract group. The common measured action gives isomorphic factors.

                                                                                                          For the first pair, order-four torsion already distinguishes the groups. For the full family, the parameter \(n\) is recovered from an intrinsic finite-orbit subgroup of \(E_n[2]/2E_n\); finite-index embeddings simultaneously prove mutual commensurability [openai2026tenadvances, Chapter 4, Sections 5.1, 6.2, and 6.4–6.5].

                                                                                                          The same chapter proves property (T) by a relative-property-(T) spectral estimate and a Boolean-polynomial support bound, rather than taking it only from a classical lattice theorem [openai2026tenadvances, Chapter 4, Sections 5.2–5.5].

                                                                                                          This is not Zhou's deformation. Zhou keeps both the discrete kernel and the quotient fixed and changes the action; the quadratic shear then conjugates the two dual actions [zhou2026icc, Section 1, pp. 2–3]. Here the action on the underlying measured space is already common, while the compact group law, hence its discrete dual, changes.

                                                                                                          The present Lean development formalizes Zhou's action-changing route. Its Fourier and crossed-product interfaces are conceptually reusable, but the shifted carry groups, the infinite family, and its finite-orbit invariant are not claims of the current formalization. This change of kernel is also what lets the OpenAI construction produce an infinite fiber, whereas Zhou's theorem selects one explicit pair.

                                                                                                          The balance of proof weight is correspondingly different. Once the compact models are identified as the same measured \(K\)-space, the factor comparison is short. More of the work lies in constructing the shifted family, proving the initial relative-property-(T) estimate, and extracting an intrinsic invariant that distinguishes every parameter. Zhou instead puts substantial weight into the explicit action conjugacy and into transporting a module obstruction through an arbitrary group isomorphism.

                                                                                                          Anthropic proof architecture [connes-0019]

                                                                                                            Changing the extension class and measurably gauging it away [connes-000N]
                                                                                                            paperFiberShear_conjugates_paperActionspaperGroupFactors_isomorphic
                                                                                                            L∃∀N

                                                                                                              The construction in [anthropic2026icc] fixes both the kernel \(A=\mathbb Z^4\) and quotient \(Q=\operatorname {Sp}_4(\mathbb Z)\). It compares the split semidirect product \(\Gamma _0=A\rtimes Q\) with an extension \(\Gamma _\tau \) defined by a nonzero two-torsion class \([\tau ]\in H^2(Q,A)\).

                                                                                                              The algebraic difference lies neither in the kernel nor in the action, but in the extension cocycle. The class is obtained as a Bockstein of the theta-characteristic cocycle [anthropic2026icc, Sections 3.1–3.3].

                                                                                                              After Fourier transform, the two group factors become an untwisted and a twisted crossed product over \(\mathbb T^4\). A Borel choice of representatives for \(\mathbb R^4/\mathbb Z^4\) produces an integral carry cocycle. The paper combines that carry with a quadratic refinement of the symplectic form to construct phases \(\Psi _g\); their coboundary is exactly the dual twist \(u_\tau \).

                                                                                                              The resulting gauge is a trace-preserving isomorphism of the crossed products [anthropic2026icc, Sections 2.3 and 5.1–5.3, especially Theorems 5.1 and 5.2].

                                                                                                              Nonisomorphism survives because \([\tau ]\ne 0\): one extension splits and the other does not [anthropic2026icc, Section 4]. The paper proves ICC directly and obtains property (T) from the classical \(\operatorname {Sp}_4(\mathbb Z)\) and relative-property-(T) input, followed by finite-index permanence [anthropic2026icc, Lemmas 3.7–3.8].

                                                                                                              The constructions vary three different algebraic data:

                                                                                                              • OpenAI changes the kernel through a different compact dual law;
                                                                                                              • Zhou changes the action through a nonsplit module extension; and
                                                                                                              • Anthropic changes the group-extension class in \(H^2\).

                                                                                                              Their measurable repairs also differ: an already common measured action, an explicit conjugacy of actions, and a one-cochain that untwists a crossed-product two-cocycle. Remark 7.1 of [anthropic2026icc] describes the last point as a torsion class becoming measurably trivial on the connected dual while its branch defects are repaired by the quadratic carry terms.

                                                                                                              Formalizing this proof would not be a small refactor of the Zhou development. The current factor-transport layer treats untwisted crossed products and strict action conjugacy. The Anthropic route would need:

                                                                                                              • explicit group-extension cohomology;
                                                                                                              • cocycle-twisted crossed products;
                                                                                                              • Borel fundamental-domain representatives; and
                                                                                                              • a verified measurable gauge.

                                                                                                              Its property-(T) lane appears shorter than the current EJZK boundary, but its factor lane introduces new infrastructure. These claims are not included in the present Lean theorem.

                                                                                                              EJZK formalization outlook [connes-001A]

                                                                                                                EJZK route and effort estimate [connes-000B]
                                                                                                                elementaryGroup
                                                                                                                L∃∀N
                                                                                                                SimpleGraph.lapMatrix
                                                                                                                L∃∀N

                                                                                                                  The exact property-(T) input is classical and mathematically well established. The literature survey in [ershov2017rootgraded, Section 1.2, pp. 3–4] recalls that Kazhdan's 1967 theorem, together with subsequent work of Vaserstein, gives property (T) for \(G_\Phi (\mathbb F[t])=E_\Phi (\mathbb F[t])\) when \(\mathbb F\) is finite and \(\Phi \) is a reduced irreducible classical root system of rank at least two.

                                                                                                                  Taking \(\Phi =A_2\) and \(\mathbb F=\mathbb F_2\) yields the required \(E_{A_2}(\mathbb F_2[t])=\mathrm {EL}_3(\mathbb F_2[t])\) instance. The open boundary is therefore one of formalization completeness, not mathematical uncertainty.

                                                                                                                  The only remaining substantive premise is property (T) for \(\mathrm {EL}_3(\mathbb F_2[t])\). The route estimated below specializes the 2010 elementary-group theorem to \(R=\mathbb F_2[t]\) and \(n=3\). Its graph and six-root estimates are cited in the implementation layers below. The later root-graded treatment supplies broader supporting language.

                                                                                                                  Our central estimate remains 24–28 thousand new Lean lines; a wider plausible range is 18–35 thousand. That range is about \(0.8\)–\(1.5\) times the roughly 23,000 lines already in the project. We expect the proof search and engineering to require two to four times the effort of the present formalization.

                                                                                                                  This estimates one explicit, quantitative route that fits the present Lean interfaces; it is neither a measure of confidence in the theorem nor a lower bound for formalizing the classical route. The literature supports the route and its decomposition, not these LOC or effort figures.

                                                                                                                  The six implementation layers, with overlapping uncertainty ranges, are:

                                                                                                                  1. quantitative Kazhdan subsets, constants, and relative ratios, with a bridge to the current qualitative predicate; our internal allocation is 2–3.5 thousand lines;
                                                                                                                  2. the six additive root-subgroup embeddings and the direct \(A_2\) commutator relations; our internal allocation is 2–4 thousand. A Steinberg-group detour is optional, not required for this direct matrix-group specialization;
                                                                                                                  3. fixed-space angles, codistance, and the class-two nilpotent estimate; our internal allocation is 5–9 thousand;
                                                                                                                  4. the unweighted standard-Laplacian boundary case on six vertices. This is Section 5.4 of [ershov2010noncommutative]. Our internal allocation is 1.5–3 thousand; the weighted criterion in Section 5.5 is a separate generalization;
                                                                                                                  5. the packaged relative-ratio estimate for the union of all six root subgroups in [ershov2010noncommutative, Proposition 6.1, p. 34]; our internal allocation is 3–5.5 thousand. Six repeated Lean instantiations would be an implementation choice, not six mathematical inputs; and
                                                                                                                  6. assembly plus the exact qualitative export theorem for the elementary-group property-(T) boundary; our internal allocation is 1.5–3 thousand.

                                                                                                                  The allocations overlap. Their subtotal also excludes integration adapters, proof-search retries, and pin-specific repair risk, so it is not an arithmetic derivation of the 18–35 thousand-line envelope.

                                                                                                                  The existing analytic shell is not part of the missing estimate. Connes.spectral_criterion_unconditional already constructs the positive spectral functional and closes the scalar/PVM route from finite spectral detection to property (T).

                                                                                                                  The remaining work is the quantitative root-subgroup, fixed-space, graph, and detector mathematics listed above; it should reuse that shell rather than construct another PVM layer.

                                                                                                                  Available Mathlib and TauCeti infrastructure [connes-000G]
                                                                                                                  SimpleGraph.lapMatrixSimpleGraph.posSemidef_lapMatrix
                                                                                                                  L∃∀N

                                                                                                                    The pinned Connes project uses Mathlib revision c2d7843e with Lean 4.34.0-rc2. Mathlib supplies the graph Laplacian and its positivity theorem, exposed by the declaration links above, but not the Ershov–Jaikin-Zapirain graph-of-groups criterion, Kazhdan ratios, root gradings, codistance, or the graph argument.

                                                                                                                    Kassabov's estimates for a free associative integer ring require quotient transport before application to \(\mathbb F_2[t]\) [kassabov2005universal, Theorem 2.2 and Lemmas 2.3–2.7]. For an arbitrary finitely generated ring and module, the cleaner calibration is [ershov2017rootgraded, Appendix Theorem A.1]. The direct route is the earlier quantitative development [ershov2010noncommutative, Sections 2–6 and Appendix A].

                                                                                                                    TauCeti at revision ac3bfb3 uses Mathlib ac1b4db and Lean 4.34.0-rc1. Its diagonal-dominance proof consumes the same Mathlib Laplacian facts.

                                                                                                                    Its source and roadmap contain no direct property (T), Kazhdan, codistance, root-graded-group, or magic-graph lane. Recent algebraic-group root-space additions do not supply the root-graded-group criterion used by EJK. TauCeti is therefore not a drop-in dependency for this boundary; aligning project pins would not reduce the missing mathematics.

                                                                                                                    Alternative EJZK routes and literature anchors [connes-000I]
                                                                                                                    elementaryGroup
                                                                                                                    L∃∀N

                                                                                                                      Bounded elementary generation is not presently shorter. Nica's [nica2019bounded, Theorem 2, p. 2] gives \[\nu _3=\frac {3\cdot 3^2-3}{2}+29=41,\] and its proof invokes the Kornblum–Artin theorem for irreducibles in polynomial arithmetic progressions, stated as [nica2019bounded, Theorem 3, p. 2]. That input is absent from the pinned Mathlib revision.

                                                                                                                      Our internal estimate for a self-contained Nica–Kassabov route is 20–45 thousand lines and three to six times the current engineering effort, with roughly 70 percent internal uncertainty.

                                                                                                                      Assuming Kornblum–Artin gives our internal estimate of 8–15 thousand lines, but merely moves the external boundary. Our internal estimate for a reusable formalization of the generic EJK theorem is 45–90 thousand lines; that generality is unnecessary for Zhou's application.

                                                                                                                      The route decomposition has four literature anchors:

                                                                                                                      None states our LOC or effort ranges.

                                                                                                                      Representation-space universe boundary [connes-000L]
                                                                                                                      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.

                                                                                                                        Disclosure of AI use [connes-001B]

                                                                                                                          Human direction and agent implementation [connes-000R]

                                                                                                                            This is a human-directed, substantially agent-implemented formalization and exposition project. The division of work was concrete.

                                                                                                                            Human mathematical and proof direction

                                                                                                                            • selected Zhou's theorem and required completion of every Zhou-internal argument, with property (T) for \(\mathrm {EL}_3(\mathbb F_2[t])\) as the single explicit external premise;
                                                                                                                            • fixed Zhou's Sections 2–7 as the proof order and required the overview to show one construction feeding factor equivalence, property (T), ICC, and nonisomorphism; and
                                                                                                                            • required comparison of the OpenAI, Zhou, and Anthropic proofs by the algebraic information each factor forgets, followed by the EJZK formalization outlook.

                                                                                                                            Human review and exposition contract

                                                                                                                            • required literature grounding, declaration-level provenance, public privacy boundaries, and Tau Ceti rubric review;
                                                                                                                            • required Linux Comparator verification with statement and axiom checks, confinement, Lean-kernel replay, and nanoda replay, while keeping technical acceptance distinct from mathematical audit;
                                                                                                                            • specified notes about the formalization rather than a restatement of the source papers, including proof architecture, mathematical weight, special designs, the threefold motivation, proof-family comparison, and unresolved boundaries; and
                                                                                                                            • reviewed rendered output and required corrections to headings, prose, diagrams, cross-references, navigation, privacy, and publication wording.

                                                                                                                            Human direction in recent refactoring

                                                                                                                            • requested repeated searches against the pinned Mathlib API, simplification of the challenge, and proof golf while preserving the exact theorem contract;
                                                                                                                            • treated heartbeat overrides as performance and refactor signals, required measured thresholds, and requested review of overlapping APIs and preparation of the Palomar metadata; and
                                                                                                                            • required the companion notes to track the Lean changes and identified Connes.vonNeumannClosure by manual inspection as a remaining simplification candidate.

                                                                                                                            Agent implementation and review

                                                                                                                            • reconciled the literature and public Lean sources, adapted attributed proof blocks, implemented the Lean development, and refactored its public interfaces;
                                                                                                                            • implemented the resulting Mathlib reuse, action-indexed definitions, challenge and proof golf, measured heartbeat cleanup, and bicommutant simplification;
                                                                                                                            • ran full builds, Linux Comparator and nanoda checks, Lean-kernel replay, and clean-room reviews; reconciled the changes with the literature and public source; and repaired the resulting findings; and
                                                                                                                            • prepared the Palomar metadata and public documentation, then synchronized the mathematical notes, diagrams, comparisons, and formalization estimates under the human-specified structure and constraints.

                                                                                                                            The working cycle was: human proof and review contract \(\longrightarrow \) agent implementation \(\longrightarrow \) role-separated agent review and repair \(\longrightarrow \) human inspection and correction \(\longrightarrow \) approved landing.

                                                                                                                            Agent role separation is not independent human review; the project's audit ledger records the remaining review boundary. Public proof transfers are identified in the port map.