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.