Formalization design [connes-000K]
✍️source

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:

  • Construction. The characteristic-two calculation in Lemma [connes-000C], with its Lean realization in § [connes-000U], is concrete algebra and supplies every later carrier.
  • Factor equivalence. Theorem [connes-0007], § [connes-000D], and § [connes-000E] carry heavy operator algebra: compact duals, Haar measure, Fourier transforms, von Neumann closures, and trace transport.
  • Property (T). Definition [connes-0003], § [connes-000V], Theorem [connes-0004], § [connes-000Y], Lemma [connes-0005], and § [connes-000W] carry heavy harmonic and representation theory. Spectral measures and finite detectors are internal; EJZK enters at one boundary.
  • ICC. Theorem [connes-0006] is the lightest lane conceptually, but its implementation in § [connes-000X] still needs exact orbit and finite-quotient displacement calculations.
  • Nonisomorphism. Theorem [connes-0008] is the deepest internal algebraic chain. Characteristic kernels, quotient twists, semisimplicity, and a finite cocycle obstruction must survive an arbitrary isomorphism.

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

  • the square-span certificate implemented in § [connes-000U];
  • the Fourier-shear proof of factor equivalence: its unitary implementation in Theorem [connes-0007], its automatic projection-order transport in § [connes-001C], the four conjugation identities in § [connes-001D], and the measure and closure arguments in § [connes-000D] and § [connes-000E];
  • the quantitative detector and qualitative property-(T) boundary in Definition [connes-0003], § [connes-000V], Theorem [connes-0004], and § [connes-000Y];
  • the three-case ICC criterion in Theorem [connes-0006] and § [connes-000X];
  • the quotient twist in § [connes-000H]; and
  • the proposition-valued assembly in § [connes-0002].

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, Sections 9–10 compare the other two proof architectures, Section 11 scopes the remaining EJZK formalization, and Section 12 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.