Theorem A [connes-001L]
✍️source

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

      Context

        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]
            ✍️source

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