Draft notes [uts-0001]
✍️source

1. draft notes captured by topic

1.1. Drafts for Notes on Topos Theory and Type Theory [tt-000L]

Example. (co)limit in Set [leinster2016basic, 5.1.22, 5.2.16] [tt-004W]

In $\mathbf {Set}$, the limit is constructed as a subset of a product, the colimit is a quotient of a sum.

Add this after Definition [tt-002G].

Lemma. Representable functor and adjoint [tt-0022]

Lemma 4.24.2 in The Stacks project.

Shaef theory [tt-005B]

Definition. concrete category [riehl2017category, 1.6.17] [tt-0053]

A concrete category is a category ${\cal C}$ equipped with a faithful functor $\mathscr {F} : {\cal C} \to \mathbf {Set}$.

Add this to where this would be used.

Definition. cone [kostecki2011introduction, 4.9] [tt-0027]

Let ${\cal C}^{{\cal J}}$ be a functor category, where ${\cal J}$ is a small category.

Let $\Delta _O$ be a constant functor, which assigns the same object $O$ in ${\cal C}$ to any object $J$ in ${\cal J}$.

Let $K \in \operatorname {Ob}({\cal J})$ and let $j \in \operatorname {Arr}({\cal J})$ such that $j: J \to K$. Let $\mathscr {F}$ be any functor in ${\cal C}^{{\cal J}}$, i.e. it's a diagram in ${\cal C}$ of shape ${\cal J}$.

A natural transformation $\pi : \Delta _O \to \mathscr {F}$, defined as a family of arrows $\pi _J: O \to \mathscr {F}(J)$, such that the diagram

$\text{[math]}$ commutes, is called a cone on the functor (diagram) $\mathscr {F}$ with vertex $O$.

This is the alternative definition of Definition [tt-0028], it should be incooporated with Definition [tt-0040].

Definition. creates limits [leinster2016basic, 5.3.5] [tt-0058]

A functor $\mathscr {F}: {\cal C} \to {\cal D}$ creates limits (of shape ${\cal J}$) if whenever $\mathscr {D}: {\cal J} \to {\cal C}$ is a diagram in ${\cal C}$,

for any limit cone $\left ( V_{{\cal D}} \xrightarrow {q_J} \mathscr {F} \mathscr {D}(J) \right )_{J \in {\cal J}}$ on the diagram $\mathscr {D} \mathbin {\bullet } \mathscr {F}$, there is a unique cone $\left (V_{{\cal C}} \xrightarrow {p_J} \mathscr {D}(J) \right )_{J \in {\cal J}}$ on $\mathscr {D}$ such that $\mathscr {F}(V_{{\cal C}})=V_{{\cal D}}$ and $\mathscr {F}\left (p_J\right )=q_J$ for all $J \in {\cal J}$
this cone $\left (V_{{\cal C}} \xrightarrow {p_J} \mathscr {D}(J)\right )_{J \in {\cal J}}$ is a limit cone on $\mathscr {D}$.

Simplify wording and put it in § [tt-0023] together with Lemma [tt-0059].

Example. direct limit [rosiak2022sheaf, example 68] [tt-004X]

Direct limits is the colimit of a diagram indexed by the ordinal category $\omega $. In other words, for a diagram \[ X_1 \to X_2 \to X_3 \to X_4 \to \cdots \] its colimit is the direct limit $\lim \limits _{\to } X_n$, defining a diagram of shape $\omega +1$ :

$\text{[math]}$

Observe then that the colimit of a sequence of sets with the inclusions \[ X_0 \hookrightarrow X_1 \hookrightarrow X_2 \hookrightarrow \cdots \] recovers their union $\bigcup \limits _{n \geq 0} X_n$.

Add this after Definition [tt-002G].

Corollary. evaluation functor preserves limits of ... [leinster2016basic, 6.2.6] [tt-0046]

An important corollary of Theorem [tt-0045].

The Yoneda embedding preserves limits, for any small category [leinster2016basic, 6.2.12]. But it does not preserve colimits in general [leinster2016basic, 6.2.14].

Every presheaf can be expressed as a colimit of representables in a canonical (though not unique) way, this is Theorem [tt-004D], and dual to Lemma [tt-002N].

fill in details.

Definition. filtered category [rosiak2022sheaf, def. 285] [tt-004Z]

A category ${\cal J}$ is filtered (or directed) if

it is not empty
for every pair of objects $J, J^{\prime } \in {\cal J}$, there exists $K \in {\cal J}$ and $f: J \to K$ and $f': J' \to K$
for every two parallel arrows $u, v: i \rightarrow j$ in ${\cal J}$, there exists $K \in {\cal J}$ and $w: J \to K$ such that \[u \mathbin {\bullet } w = v \mathbin {\bullet } w\]

This is a generalization of the notion of a (upward) directed poset from order theory.

Add this to where this would be used.

Definition. filtered colimit [rosiak2022sheaf, def. 285] [tt-0050]

A filtered colimit is a colimit of a functor $\mathscr {F}: {\cal J} \to {\cal C}$, where ${\cal J}$ is a filtered category.

In particular, a colimit over a filtered poset $P$ is the same as the colimit over a cofinal subset $Q$ of that poset, where $Q$ as a cofinal subset means that for every element $p \in P$, there exists an element $q \in Q$ with $p \leq q$.

Theorem. general adjoint functor theorem [leinster2016basic, 6.3.10] [tt-004E]

Limit-preservation alone does not guarantee the existence of a left adjoint. This theorem specifies the conditions under which a limit-preserving functor has a left adjoint. This theorem requires the definition of weakly initial set.

fill in details.

Theorem. limits in a functor category [leinster2016basic, 6.2.5] [tt-0045]

Limits in a functor category are computed pointwise.

fill in details.

This theorem helps proving Lemma [tt-0047].

Remark. local, global [rosiak2022sheaf, p. 1] [tt-005C]

In a very general and rough way, by local we typically understand that something is being compared to what is around or nearby it; this is as opposed to the global, generally understood to mean compared to everything or across an entire domain of interest. Satisfying a property at a local level does not necessarily entail that the same will obtain at the global level.

Lemma. preserves if creates [leinster2016basic, 5.3.6] [tt-0059]

Let $\mathscr {F}: {\cal C} \rightarrow {\cal D}$ be a functor and ${\cal J}$ a small category. Suppose that ${\cal D}$ has, and $\mathscr {F}$ creates, limits of shape ${\cal J}$. Then ${\cal C}$ has, and $\mathscr {F}$ preserves, limits of shape ${\cal J}$.

Same as Definition [tt-0058].

Definition. section, choice [leinster2016basic, sec. 3.1] [tt-003E]

Let $f: X \to Y$ be an arrow in a category ${\cal C}$. A section (or right inverse) of $f$ is an arrow $i: Y \to X$ in ${\cal C}$ such that $i \mathbin {\bullet } f = \mathit {1}_X$.

In $\mathbf {Set}$, any arrow with a section is certainly surjective. The converse statement is called the axiom of choice:

Every surjection has a section.

It is called choice because specifying a section of $f: X \to Y$ amounts to choosing, for each $y \in Y$, an element of the nonempty set $\{x \in X \mid f(x)=y\}$.

It's closely related to § [tt-004T], need to figure out how to incooperate.

Definition. sequence [leinster2016basic, sec. 3.1] [tt-003D]

A function with domain $\mathbb N$ is usually called a sequence.

Related to § [tt-004T].

Definition. slice category [kostecki2011introduction, eq. 12] [tt-0009]

The slice category ${\cal C} \downarrow X$, is the category whose objects are arrows in ${\cal C}$ with fixed codomain $X$, such that the diagram $\text{[math]}$ commutes, where colored arrows are in ${\cal C} \downarrow X$.

It's also denoted ${\cal C} / X$ or ${\cal C}_{/X}$.

The slice category is a special case of the comma category.

It's also called overcategory, as it's a slice category over $X$ [zhang2021type, 3.5].

revamp and add co-slice category, maybe following [rosiak2022sheaf, def. 21], or better, follow Basic category theory, to explain how a slice category is a special case of comma category.

Definition. sum, coproduct [leinster2016basic, 5.2.2] [tt-003L]

A sum or coproduct is a colimit over a discrete category, i.e. it is a colimit of shape $J$ for some discrete category ${\cal J}$.

Possibly belong to § [tt-0023].

Remark. summary [tt-0055]

$\text{[math]}$

This diagram summarizes § [tt-002P].

Add this to § [tt-002P].

1.2. Drafts for Notes on Algebraic Geometry [ag-000C]

Notes on Algebraic Geometry [ag-0001]

August 13, 2024
Utensil Song

What is Algebraic Geometry? [ag-0005]

Algebraic geometry deals with solution sets of systems of polynomial equations [borisov2024adventures, sec. 1] from an geometric view, with many algebraic concepts imitating the notions of analysis and topology [kriz2021introduction, p. vii], but has the advantage of being able to deal with singularities [mehrle2017algebraic, lect. 1, sec. 1] and other pathological objects.

Algebraic geometry has developed in waves, each with its own language and point of view, see [hartshorne1977graduate, p. xiv] for some discussion. The older language is closer to the geometric intuition, while the newer language developes powerful techniques to solve problems in great generality, but the study of the latter is considered tedious, or even depressing, by many, when not accompanied with tangible applications [grothendieck1964elements, p. 12].

Remark. the grand plan [ag-0002]

We will use [kriz2021introduction] as a holistic guide to the organization of materials, which has done a great job of having the minimal prerequisites, being self-contained, and covering most of the topics that concern us, including the geometric motivation.

For a similar purpose, we use the formalization papers [bordg2022simple] and [buzzard2022schemes] to guide the path, at least the part towards schemes, and their counterparts in the Mathlib of Lean 4.

For prerequisites in basic algebra and commutative algebra, we will use [knapp2006basic] and [knapp2007advanced], and notes by Andreas Gathmann [gathmann2023plane][gathmann2013commutative] and David Mehrle [mehrle2015commutative]. For the geometric motivation and intuition, we will use [cox1997ideals] and [borisov2024adventures].

For upstream treatment of algebraic geometry, we will use [grothendieck1964elements] (particularly the English translation available at ryankeleti/ega) and [fantechi2006fundamental]. For modern notes, we will use [vakil2024rising], [gathmann2022algebraic] and [mehrle2017algebraic], with an eye on the classic textbook [hartshorne1977graduate].

We also need to tap into the language of Stacks in a modern setting, as treated in [khan2023lectures], with preliminaries on $\infty $-categories and derived categories.

See the plan for notes on algebraic geometry for an early discussion of the plan.

Convention. rings and fields [gathmann2013commutative, 0.1] [ag-0008]

A ring, usually denoted $R$, is always assumed to be a commutative ring (i.e. $a+b=b+a$ and $a b=b a$ for all $ a, b \in R$) with 1 (i.e. the multiplicative identity element, or called multiplicative unit).

$1 \neq 0$ is not required, where $0$ is the additive neutral element. If $1=0$, then $R$ must be the zero ring (or called the trivial ring), which consisting of one element, and is denoted $\{0\}$.

Subrings must have the same unit, and ring homomorphisms are always required to map $1$ to $1$.

A field, usually denoted $K$, is a commutative ring with $1$, where every nonzero element has a multiplicative inverse (thus division can be defined).

Definition. formal variable, formal expression [ag-0009]

A formal variable is an arbitrary symbol that is used to represent some mathematical object, and assumes nothing about the value or nature of the object.

A formal expression is mathematical expression with formal variables, assuming nothing but the formal variables participate in the expression have operations that are used in the expression.

A formal expression can be evaluated by replacing the formal variables with actual mathematical objects that have the operations defined in the expression.

When there is no ambiguity, we may omit the word "formal" and simply say variables or an expression.

Definition. monomial [cox1997ideals, 1.1.1] [ag-0003]

A monomial in $n$ formal variables $x_1, \ldots , x_n$, denoted $x^\alpha $, is a formal expression of the form \[ x_1^{\alpha _1} x_2^{\alpha _2} \cdots x_n^{\alpha _n} \] where $n \in \mathbb N$, $\alpha =\left (\alpha _1, \ldots , \alpha _n\right )$ is an $n$-tuple of nonnegative integers.

The total degree of the monomial is denoted $|\alpha |=\alpha _1+\cdots +\alpha _n$.

Definition. polynomial [cox1997ideals, 1.1.2, 1.1.3] [ag-0004]

A polynomial $f$ over a ring $R$ in $n$ variables is a finite linear combination (with coefficients $a_\alpha $ in $R$ ) of monomials, i.e. the formal expression of the form \[ f=\sum _\alpha a_\alpha x^\alpha , \quad a_\alpha \in R, \]

The set of all polynomials in $x_1, \ldots , x_n$ with coefficients in $R$ is denoted $R\left [x_1, \ldots , x_n\right ]$.

$a_\alpha x^\alpha $ is called a term of $f$ if $a_\alpha \neq 0$.

The total degree of $f \neq 0$, denoted $\operatorname {deg}(f)$, is the maximum $|\alpha |$ such that the coefficient $a_\alpha $ is nonzero. The total degree of the zero polynomial is undefined.

Remark. polynomial ring [cox1997ideals, 1.1.3] [ag-0007]

Under addition and multiplication, $R\left [x_1, \ldots , x_n\right ]$ satisfies all axioms of a commutative ring, and for this reason we will refer to $R\left [x_1, \ldots , x_n\right ]$ as a polynomial ring.

Definition. affine space [gathmann2013commutative, 0.3] [ag-000A]

The ($n$-dimensional) affine space over a field $K$, denoted $\mathbb {A}_K^n$, is \[ \left \{\left (c_1, \ldots , c_n\right ): c_i \in K \text { for } i=1, \ldots , n\right \} \] which is just $K^n$ as a set, without the its additional structures as a $K$-vector space and a ring.

We'll often use the term affine $n$-space to indicate the dimension. Particularly, an affine 1-space is called an affine line, an affine 2-space is an affine plane.

Definition. affine variety [gathmann2013commutative, 0.3] [ag-000D]

Let $S \subset K\left [x_1, \ldots , x_n\right ]$ be a set of polynomials. The zero locus (or zero set) of $S$ is \[ V(S):=\left \{x \in \mathbb {A}_K^n: f(x)=0 \text { for all } f \in S\right \} \subset \mathbb {A}_K^n \]

An affine algebraic variety over $K$ is a subset of $\mathbb {A}_K^n$ of this form. It's usually simply called an affine variety over $K$, or an affine $K$-variety.

If $S=\left (f_1, \ldots , f_k\right )$ is a finite set, $V(S)$ can be written as $V\left (f_1, \ldots , f_k\right )$.

Obviously, it is the set of all solutions of the system of polynomial equations $f_1\left (x_1, \ldots , x_n\right )=\cdots =f_s\left (x_1, \ldots , x_n\right )=0$ [cox1997ideals, 1.2.1], denoted $\operatorname {Sol}(S;K)$ [dolgachev2013introduction, p. 1].

Remark. affine v.s. projective [michalek2021invitation, ch. 2] [ag-000E]

The prefix "affine" of affine variety is used to distinguish it from a projective variety. Affine varieties arise from arbitrary polynomials, while projective varieties arise from systems of homogeneous polynomials, i.e. linear combinations of monomials of fixed degree.

Since affine varieties are the general case, they are sometimes simply called varieties.

Figure out its relation to affine space in Geometry, which preserves parallelism and ratio of lengths for parallel line segments, but not distances and measures of angles.

Example. varieties [ag-000F]

$\mathbf {V}\left (10 x^2-x^3-y^2\right )$ from [cox1997ideals, p. 24]:

$\text{[math]}$

$\mathbf {V}\left (x^2-y^2 z^2+z^3\right )$ from [cox1997ideals, p. 7, p. 16]:

$\text{[math]}$

Figure. Implicit surfaces [uts-000J]

#define AS_LIB 1

int get_shape() {
    return int(iTime) % 52;
}

#include "/forest/shader/implicit.glsl"

void mainImage( out vec4 fragColor, in vec2 fragCoord )
{
    vec2 uv = 2.*(fragCoord-iResolution.xy/2.)/iResolution.y; // contains [-1,1]^2
    vec3 col = vec3(0.);
    
    // Camera rays
    vec3 camPos = vec3(4.,0.,0.);
    vec3 camDir = - normalize(camPos);
    vec3 rayPos, rayDir;
    float zoom = 1.3; // 1.8*cos(iTime);
    // if (checkKey(KEY_E)) zoom = 0.5;
    float fov = 0.4*zoom;
    float fov_ortho = 1.5*zoom;
    #if perspective
        // perspective cam
        rayPos = camPos;
        rayDir = normalize(camDir + fov*vec3(0., uv.x, uv.y));
    #else
        // orthographic cam
        rayPos = camPos + fov_ortho*vec3(0., uv.x, uv.y);
        rayDir = camDir;
    #endif
    // for perspective background in orthographic mode
    vec3 cubemapDir = normalize(camDir + fov*vec3(0., uv.x, uv.y));
    
    // Mouse-controlled rotation
    vec2 mouse = initMouse + vec2(0.015625*sin(iTime*PI), 0.0); // initMouse; // iMouse.xy == vec2(0.,0.) ? initMouse : (iMouse.xy/iResolution.xy - 0.5);
    float yaw = clamp(- mouse.x * 2.*PI * 1., -PI,PI);
    float pitch = clamp( mouse.y * PI * 1.2, -PI*0.5, PI*0.5);
    // pitch and yaw rotations (column-wise matrices)
    mat3 rot = mat3(cos(yaw), sin(yaw), 0., -sin(yaw), cos(yaw), 0., 0., 0., 1.);
    rot = rot * mat3(cos(pitch), 0., -sin(pitch), 0., 1., 0., sin(pitch), 0., cos(pitch));
    // apply
    camPos = rot*camPos;
    camDir = rot*camDir;
    rayPos = rot*rayPos;
    rayDir = rot*rayDir;
    cubemapDir = rot*cubemapDir;
    
    //cubemapDir = vec3(cubemapDir.x, cubemapDir.z, cubemapDir.y);
    
    vec3 hitPoint = raycast(rayPos, rayDir);
    
    if (hitPoint == BINGO) { fragColor = vec4(BINGO,1.0); return; }
    //if (hitPoint == NOHIT) { fragColor = vec4(NOHIT,1.0); return; }
    //if (hitPoint == NOBOUNDHIT) { fragColor = vec4(NOBOUNDHIT,1.0); return; }
    //if (hitPoint == ESCAPEDBOUNDS) { fragColor = vec4(ESCAPEDBOUNDS,1.0); return; }
    //if (hitPoint == MAXDISTREACHED) { fragColor = vec4(MAXDISTREACHED,1.0); return; }
    //if (hitPoint == MAXITERREACHED) { fragColor = vec4(MAXITERREACHED,1.0); return; }
    
    if (hitPoint == NOBOUNDHIT  || hitPoint == NOHIT || hitPoint == ESCAPEDBOUNDS || hitPoint == MAXITERREACHED) {
        //fragColor = vec4(vec3(0.2),1.0); return;

        // make background transparent
        fragColor = vec4(0.0,0.0,0.0,0.0); return;
        
        col = with_background(cubemapDir);
        
        #if showBoundingCube
        // darken bounding cube
        if (hitPoint != NOBOUNDHIT) { col *= vec3(0.7); }
        #endif

        fragColor = vec4(col,1.0); return;
    }

    vec3 grad = gradf(hitPoint+1.1*EPS*(-rayDir));
    float s = -sign(dot(grad,rayDir));
    
    col = with_color_mode(grad, s, hitPoint, camPos);

    col = clamp(col, 0., 1.);

    col = with_surface_pattern(col, hitPoint);

    col = with_shading(col, grad, s, rayDir);
    
    col = clamp(col, 0., 1.);

    fragColor = vec4(col,1.0);
}

adapted from Rogolop's Implicit surfaces

appendix [ag-000B]

For draft notes, see Drafts for Notes on Algebraic Geometry.

Definition. affine variety [cox1997ideals, 1.2.1] [ag-0006]

Let $f_1, \ldots , f_s$ be polynomials in $K\left [x_1, \ldots , x_n\right ]$. The affine variety defined by $f_1, \ldots , f_s$ is \[ \mathbf {V}\left (f_1, \ldots , f_s\right )=\left \{\left (a_1, \ldots , a_n\right ) \in \mathbb {A}_K^n \mid f_i\left (a_1, \ldots , a_n\right )=0 \text { for all } 1 \leq i \leq s\right \} \]

Obviously, it is the set of all solutions of the system of polynomial equations $f_1\left (x_1, \ldots , x_n\right )=\cdots =f_s\left (x_1, \ldots , x_n\right )=0$.

Definition. affine variety [gathmann2013commutative, 0.3] [ag-000D]

An affine algebraic variety over $K$ is a subset of $\mathbb {A}_K^n$ of this form. It's usually simply called an affine variety over $K$, or an affine $K$-variety.

If $S=\left (f_1, \ldots , f_k\right )$ is a finite set, $V(S)$ can be written as $V\left (f_1, \ldots , f_k\right )$.

the plan for notes on algebraic geometry [uts-000F]

The approach we would like to take is similar to the one we took in our Notes on Topos Theory and Type Theory: determine some goals, find some references that sketch out a path to those goals, and then write notes jumping between many references to fill in the gaps.

Goal 1: To be able to state "an affine scheme is a scheme", which means we need all the basics of prime ideals, Zariski topology, sheaves, spectrum of a ring, stalks, locally ringed spaces etc. as sketched out in [bordg2022simple] which has organized the minimum preliminaries in a formal way, but we might also need to refer to [buzzard2022schemes] and Mathlib to ensure that we can properly find the Lean counterparts.

Goal 2: To properly understand the geometric topic of algebraic geometry, we also need many basic correspondence in the Algebra-Geometry dictionary, which can be found in [cox1997ideals], including ideals, varieties, Gröbner Bases, elimination Theory, the relation between irreducible Varieties and prime Ideals, projective algebraic geometry etc. This book provides concrete intuitions and examples for working with the abstract concepts. We might also branch out from there to write notes about ray-tracing the implicit surfaces of algebraic varieties (see some links for rendering implicit surfaces for some links), and the use of Macaulay2 and Singular to do computations in AG.

Goal 3: A challenging goal is to be able to read EGA [grothendieck1964elements] and some materials surrounding it:

EGA: we will use the English translation available at ryankeleti/ega, with the French version (year 1960) available at Numdam, both use the word scheme to mean separated scheme, and prescheme to mean scheme. A Chinese translation is also available and has an index of terminology in Chinese, English, and French, which is useful. We would like to include terminology in all three languages for key concepts in our notes, showing only the English version by default.
FGA: we will use [fantechi2006fundamental] instead of the original FGA. This is an explained and extended version of FGA, that has the advantage of being in English and from a little more modern viewpoint.
SGA: Although topos is first introduced in SGA, but we are not ready to read SGA yet.
The rising sea: [vakil2024rising] is a modern introduction to algebraic geometry, used by many courses, e.g. math256 (which also has an English synopsis of EGA). Some courses, e.g. Algebraic Geometry Spring 2024 , also follows lecture notes by Andreas Gathmann [gathmann2022algebraic] (found on Math 8253: Algebraic Geometry).
FAC [serre1955faisceaux]: there is an English version Coherent Algebraic Sheaves translated by Piotr Achinger and Lukasz Krupa. This is no longer the modern treatment of AG, so it's only used as a reference.
GAGA [serre1956geometrie]: there is only the French version and the Chinese translation. The evaluation is the same as FAC.

We need some modern notes to avoid being lost in the old language, for that, besides The rising sea, we have chosen [borisov2024adventures] and [mehrle2017algebraic].

Goal 4: We also need to tap into the language of Stacks in a modern setting, as treated in [khan2023lectures], with preliminaries on $\infty $-categories and derived categories.

1.3. Drafts for Notes on Clifford Algebras [ca-001K]

Formalized Clifford Algebra Programme [fcap-0001]
📄PDF

August 2, 2026
Utensil Song

These are the accompanying mathematical notes for the experimental research project FCAP. FCAP is read “F-cap,” and studies whether Lean can serve both as a formal language for the abstract and concrete mathematics of Clifford algebras and as an implementation language for efficient symbolic and numerical computation. It is also a coined acronym for “Formalized Clifford Algebra Programme.”

FCAP's formalization is still at an early spike-test stage. The current storyline follows that agent-led spike test through coordinate representations and orthogonal-product transport.

Coordinate representations [fcap-0002]

A basis of the generating module gives coordinates on the exterior algebra, and the exterior equivalence transports those coordinates to the Clifford algebra. The empty and singleton coordinates fix the scalar and generator conventions. Orthogonality then controls how certain ordered products pass between the two algebras.

Definition. Transported exterior-basis coordinates [wieser2024formalizing, 9.3.5] [fcap-0003]

Let $R$ be a commutative ring in which $2$ is invertible, let $M$ be an $R$-module, and choose a basis $b$ indexed by a linearly ordered type. Write $E_b(s)$ for the exterior-basis vector indexed by a finite subset $s$. For a quadratic form $Q$, the Mathlib linear equivalence CliffordAlgebra.equivExterior from $\mathcal {C}\kern -2pt\ell (Q)$ to $\bigwedge _R M$ gives a coordinate basis \[B_{Q,b}(s) = \operatorname {equivExterior}(Q)^{-1}(E_b(s)).\] This basis is transported through a linear equivalence. It does not say that the equivalence preserves multiplication or that Clifford multiplication becomes exterior multiplication. The basis-free construction is developed in [wieser2022formalizing].

The exterior equivalence is treated in [wieser2024formalizing, 9.3.5].

Two calculations anchor the choice. The empty subset maps to the scalar unit, \[B_{Q,b}(\varnothing ) = 1,\] and a singleton maps to the corresponding Clifford generator, \[B_{Q,b}(\{i\}) = \iota _Q(b(i)).\] These are module-level identities: they determine the first two coordinate types but do not determine multiplication of arbitrary coordinates.

For subsets with several elements, a coordinate formula additionally needs an ordering convention and its attendant signs. No such convention is implicit in the transported basis.

Lemma. Orthogonal pair transport [wieser2024formalizing, 8.4] [fcap-0004]

Let $R$ be a commutative ring in which $2$ is invertible, let $M$ be an $R$-module, and let $Q$ be a quadratic form on $M$. Write $T_Q$ for the linear equivalence from $\mathcal {C}\kern -2pt\ell (Q)$ to the exterior algebra supplied by CliffordAlgebra.equivExterior. It is a module equivalence, not an algebra equivalence.

For vectors $m,n \in M$, the change-of-form calculation for $T_Q(\iota _Q(m)\iota _Q(n))$ has one extra scalar contribution, evaluated by the bilinear form associated to $-Q$. If $m$ and $n$ are $Q$-orthogonal, that contribution vanishes. The resulting two-generator calculation is \[T_Q\bigl (\iota _Q(m)\iota _Q(n)\bigr )=\iota _0(m)\iota _0(n).\] This is the first point at which an orthogonality hypothesis changes the transport calculation. It does not turn $T_Q$ into a multiplicative map.

The change-of-form construction is the relevant mathematical background in [wieser2024formalizing, 8.4], and the Lean construction of $\operatorname {equivExterior}$ is described in [wieser2024formalizing, 9.3.5]. The concrete geometric-product discussion in [wieser2024formalizing, 2.1.2] motivates the role of orthogonality, but does not provide this note's formal interface.

Thus orthogonality removes precisely the scalar correction in the two-generator change-of-form identity. No basis or reordering convention is needed.

Lemma. Vanishing list contraction [wieser2024formalizing, 8.4, (8.54)] [fcap-0005]

Let $R$ be a commutative ring, $M$ an $R$-module, $Q$ a quadratic form on $M$, and $d : M \to R$ a linear functional. For a list $l$ of generators, define an ordered product by \[P_Q([])=1, \qquad P_Q(m::l)=\iota _Q(m)P_Q(l),\] and write $C_{Q,d}$ for left contraction by $d$. The condition $\forall m\in l,\ d(m)=0$ forces $C_{Q,d}(P_Q(l))=0$.

There is one induction calculation. The empty product contracts to zero. At a head $m$, the generator recurrence \[C_{Q,d}(P_Q(m::l))=d(m)P_Q(l)-\iota _Q(m)C_{Q,d}(P_Q(l))\] is the local rule in [wieser2024formalizing, 8.4, (8.54)]. The hypothesis deletes the first summand, and the induction hypothesis deletes the second. This turns the recurrence into a finite-list vanishing criterion rather than a calculation for one fixed product.

The conclusion depends only on the ordered recurrence and pointwise vanishing of $d$ on the list. In particular, it is independent of a basis or any reordering convention.

Theorem. Pairwise orthogonal list transport [wieser2024formalizing, 8.4, (8.55)] [fcap-0006]

Let $R$ be a commutative ring in which $2$ is invertible, let $M$ be an $R$-module, and let $Q$ be a quadratic form on $M$. For a list $l$ of vectors, write \[P_Q([])=1, \qquad P_Q(m::l)=\iota _Q(m)P_Q(l),\] and write $T_Q$ for the linear equivalence CliffordAlgebra.equivExterior from $\mathcal {C}\kern -2pt\ell (Q)$ to $\bigwedge _R M$. In the corresponding zero-form product notation, suppose every earlier vector in $l$ is $Q$-orthogonal to every later vector. Then \[T_Q(P_Q(l))=P_0(l).\] The order of the list is unchanged. The equality concerns this product under the stated orthogonality condition; it does not say that $T_Q$ preserves arbitrary products.

The calculation proceeds from the head of the list. The one-generator change-of-form recurrence separates $T_Q(P_Q(m::l))$ into the zero-form generator $\iota _0(m)$ times the transported tail and a left-contraction correction. Pairwise orthogonality makes the associated dual vector vanish on every member of the tail. The criterion in Lemma [fcap-0005][fcap-0005] therefore kills the correction, and the induction hypothesis transports the tail.

The contraction recurrence in [wieser2024formalizing, 8.4, (8.54)], the change-of-form recurrence in [wieser2024formalizing, 8.4, (8.55)], and the exterior equivalence in [wieser2024formalizing, 9.3.5] supply the local identities. Their induction over a pairwise-orthogonal list gives the displayed theorem; the source locations do not state that finite-list consequence separately.

The order of the list is fixed throughout. Reordering would require an additional permutation-sign calculation and is not a consequence of this theorem.

Spin-representation roadmap [fcap-0019]

This appendix follows the mathematical dependencies of the spin-representation roadmap of Tau Ceti. The filtered Clifford algebra first exposes its exterior shadow. Reflections then lead to the global Pin and Spin extensions, while bivectors provide the algebraic infinitesimal orthogonal action. The Lie functor records the separate differential bridge from smooth group homomorphisms. A polarization joins the algebraic group and Lie constructions in the exterior spinor model. The real-signature recurrence and classification form a parallel algebraic branch and do not depend on the spinor-module or double-cover join.

The exterior shadow of a Clifford algebra [fcap-000F]

The Clifford relation lowers word length by two. Filtering by word length therefore separates a word from its contraction terms: the highest-degree part is alternating, and the associated graded algebra is the exterior algebra.

Definition. Word-length filtration [chevalley1954algebraic, II.1.2 and II.1.6, pp. 40--42] [fcap-000G]

filtration filtration_mul
L∃∀N

Chevalley constructs the classical filtration after choosing a finite basis of a vector space over a field. TauCeti's coordinate-free version below is defined for a quadratic form on a module over a commutative ring. The leading-symbol equivalences in Lemma [fcap-000H][fcap-000H] and Theorem [fcap-000I][fcap-000I] additionally assume that $2$ is invertible.

Let $R$ be a commutative ring, let $M$ be an $R$-module, and let $Q:M\to R$ be a quadratic form. In the Clifford algebra $\mathcal {C}\kern -2pt\ell (Q)$, define $F_n\mathcal {C}\kern -2pt\ell (Q)$ to be the $R$-submodule spanned by all products of at most $n$ generators: \[F_n\mathcal {C}\kern -2pt\ell (Q)=\operatorname {span}_R\left \{\iota (v_1)\cdots \iota (v_r):0\le r\le n\right \}.\] The empty product gives $F_0\mathcal {C}\kern -2pt\ell (Q)=R1$. Concatenating words makes the filtration multiplicative; in fact, \[F_i\mathcal {C}\kern -2pt\ell (Q)\,F_j\mathcal {C}\kern -2pt\ell (Q)=F_{i+j}\mathcal {C}\kern -2pt\ell (Q).\] Thus multiplication descends to the successive quotients and makes \[\operatorname {gr}_F\mathcal {C}\kern -2pt\ell (Q)=\bigoplus _{n\ge 0}F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\] a graded algebra, with $F_{-1}\mathcal {C}\kern -2pt\ell (Q)=0$.

Lemma. The leading symbol is exterior [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000H]

changeForm_prod_map_ι_sub_prod_map_ι_mem_filtration filtrationLeadingTerm_apply_ιMulti
L∃∀N

Retain the coordinate-free commutative-ring and module setting of Definition [fcap-000G][fcap-000G], and assume that $2$ is invertible in $R$. This is TauCeti's extension of Chevalley's finite-basis, vector-space leading-symbol argument. For vectors $v_1,\ldots ,v_n\in M$, the Clifford relation replaces an interchange by its alternating term plus a scalar contraction. Each contraction removes two generators. Consequently \[\iota (v_1)\cdots \iota (v_n) \equiv v_1\wedge \cdots \wedge v_n\pmod {F_{n-2}},\] where the right-hand side is read through the zero-form exterior model. In particular, the class of the Clifford word in $F_n/F_{n-1}$ depends alternately on the vectors and is the leading exterior symbol.

Proof.

Move a generator through the word using \[\iota (u)\iota (v)+\iota (v)\iota (u)=B_Q(u,v)1.\] The swapped word contributes the alternating sign, whereas the polar term has two fewer generators. Iterating separates the fully alternating word from terms in $F_{n-2}$. Equivalently, changing from $Q$ to the zero quadratic form changes a word only below its leading filtration degree.

Theorem. The graded pieces are exterior powers [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000I]

filtrationGradedPieceEquivExteriorPower filtrationLeadingTerm_eq_filtrationGradedEquiv_symm
L∃∀N

Let $R$, $M$, and $Q$ be as in Lemma [fcap-000H][fcap-000H]. Chevalley's finite-dimensional field argument motivates the identification. TauCeti proves the following coordinate-free commutative-ring and module equivalence. For every $n\ge 0$, the leading-symbol map gives \[F_n\mathcal {C}\kern -2pt\ell (Q)/F_{n-1}\mathcal {C}\kern -2pt\ell (Q)\simeq \bigwedge ^n_R M.\] At $n=0$ this is the scalar equivalence $F_0/0\simeq R=\bigwedge ^0_RM$. For $n>0$, the inverse sends a decomposable exterior product to the class of the corresponding Clifford word.

The point of the quotient is that every contraction term has already fallen into a lower filtration step. Alternation is therefore exact in the graded piece even though it is not exact in the Clifford algebra itself.

Theorem. PBW equivalence with the exterior algebra [meinrenken2013clifford, Proposition 2.6, pp. 33--34] [fcap-000J]

filtrationAssociatedGradedEquivExterior
L∃∀N

Meinrenken's Proposition 2.6 assumes a finite-dimensional vector space over a characteristic-zero field. TauCeti proves the corresponding extension for an additive commutative group $M$ with a module structure over a commutative ring $R$, a quadratic form $Q$ on $M$, and invertible $2\in R$. Under these hypotheses, the equivalences of Theorem [fcap-000I][fcap-000I] respect multiplication of homogeneous classes and assemble into a graded-algebra equivalence \[\operatorname {gr}_F\mathcal {C}\kern -2pt\ell (Q)\simeq _{\mathrm {grAlg}}\bigwedge _R M.\] The class of a product of an $i$-word and a $j$-word is carried to the exterior product of their leading symbols in degree $i+j$.

This is a PBW theorem for the Clifford filtration. It does not make $\mathcal {C}\kern -2pt\ell (Q)$ and $\bigwedge _RM$ isomorphic as algebras. The quadratic form survives in the lower-degree contraction terms of Clifford multiplication; only the associated graded multiplication forgets it.

Example. The degree-two symbol [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000K]

filtrationAssociatedGradedEquivExterior_apply_of_succ
L∃∀N

For $u,v\in M$, write the Clifford product as \[\iota (u)\iota (v) =\frac 12\bigl (\iota (u)\iota (v)-\iota (v)\iota (u)\bigr ) +\frac 12B_Q(u,v)1.\] The second summand belongs to $F_0$. Hence the degree-two class of $\iota (u)\iota (v)$ is $u\wedge v$. This is the two-generator instance of Chevalley's leading-symbol calculation cited in the title. The surviving half-commutator is the Clifford bivector studied next; the scalar polar term is invisible to the leading symbol.

Remark. Basis proof and quotient proof [fcap-000L]

Chevalley's proof chooses a basis, proves that ordered Clifford monomials form a basis, and identifies the underlying vector space with the exterior algebra [chevalley1954algebraic, II.1.2 and II.1.6, pp. 40--42]. Panyushev uses the resulting stable filtration and exterior associated graded as standard representation-theoretic background [panyushev2001exterior, Section 2, p. 7].

The quotient construction above is TauCeti's coordinate-free commutative-ring and module extension of that finite-dimensional field proof. It builds each graded piece from the word-length submodule and its predecessor, handles degree zero separately, and then takes their direct sum. This is a change of packaging and generality, not a stronger claim about unfiltered Clifford multiplication.

Reflections and square-normalized Clifford lifts [fcap-0007]

A nonisotropic vector acts on the generating space by a reflection through twisted Clifford conjugation. Normalizing such vectors gives elements of Pin, while determinant parity detects the even products that belong to Spin. The cards pass from local lifts to reflection generation, Pin surjectivity, and finally Spin surjectivity onto the special orthogonal group.

Convention. Quadratic-form sign [lawson2016spin, I.1, (1.3)--(1.4), p. 8] [fcap-0008]

Lawson and Michelsohn write \[v^2=-q(v)1, \qquad vw+wv=-2q(v,w),\] where $2q(v,w)=q(v+w)-q(v)-q(w)$. Mathlib and TauCeti instead use a quadratic form $Q$ with \[\iota (v)^2=Q(v)1.\] The conventions agree after setting $Q=-q$. The orthogonal group and its reflections are unchanged by this global sign reversal. A vector with $q(v)=1$ therefore has $Q(v)=-1$ in the convention used below. Mathlib's generator-square rule CliffordAlgebra.ι_sq_scalar uses this $Q$-convention.

Definition. Reflection in a nonisotropic vector [lawson2016spin, I.2, (2.12), p. 14] [fcap-0009]

reflection
L∃∀N

Let $F$ be a field of characteristic different from $2$, let $Q$ be a quadratic form on an $F$-vector space $V$, and write \[B_Q(x,y)=Q(x+y)-Q(x)-Q(y)\] for its polar form. If $Q(v)\ne 0$, the reflection with normal vector $v$ is \[\rho _v(w)=w-\frac {B_Q(v,w)}{Q(v)}v.\] It fixes $v^\perp $ pointwise, sends $v$ to $-v$, and preserves $Q$. Multiplying $v$ by a nonzero scalar does not change $\rho _v$.

Lemma. Twisted Clifford conjugation is a reflection [lawson2016spin, I.2, Proposition 2.2 and (2.8), p. 13; (2.11)--(2.12), p. 14] [fcap-000A]

Let $\alpha $ denote the grading involution of $\mathcal {C}\kern -2pt\ell (Q)$. For $Q(v)\ne 0$, the Clifford generator $\iota (v)$ is invertible with \[\iota (v)^{-1}=Q(v)^{-1}\iota (v).\] Its twisted adjoint action on a generator is the reflection in Definition [fcap-0009][fcap-0009]: \[\alpha (\iota (v))\,\iota (w)\,\iota (v)^{-1}=\iota (\rho _v(w)).\]

Proof.

The generator-square rule CliffordAlgebra.ι_sq_scalar and the anticommutator rule CliffordAlgebra.ι_mul_ι_add_swap give \[\iota (v)\iota (w)+\iota (w)\iota (v)=B_Q(v,w).\] Since $\alpha (\iota (v))=-\iota (v)$ and $\iota (v)^2=Q(v)$, substitution yields \[-\iota (v)\iota (w)\frac {\iota (v)}{Q(v)} =\iota (w)-\frac {B_Q(v,w)}{Q(v)}\iota (v) =\iota (\rho _v(w)).\] The ordinary adjoint differs by the leading minus sign; the twisted adjoint is the action that gives the reflection itself.

Lemma. Square-normalized Pin lift [lawson2016spin, I.2, Definition 2.3 and (2.26), pp. 14, 18] [fcap-000B]

reflection_mem_range_pinToOrthogonal_of_isSquare
L∃∀N

Lawson--Michelsohn make this product-and-scaling argument for a finite-dimensional quadratic vector space over a field. The statement below is TauCeti's extension to a quadratic module over a commutative ring. It assumes that $2$ and $Q(v)$ are invertible.

Let $R$ be a commutative ring, let $Q$ be a quadratic form on an $R$-module $M$, and suppose $2$ and $Q(v)$ are invertible. If there is a scalar $c$ such that \[c^2=-Q(v)^{-1},\] then $Q(cv)=-1$. The normalized Clifford generator $\iota (cv)$ belongs to the Pin group and its twisted adjoint action is $\rho _v$, because $\rho _{cv}=\rho _v$. Consequently \[\rho _v\in \operatorname {range}(\operatorname {pinToOrthogonal}).\] Equivalently, the required hypothesis is that $-Q(v)^{-1}$ is a square. The conclusion is existential: it asserts that a Pin lift exists, not that a canonical square root has been chosen.

Theorem. Paired reflections have a product-square Spin lift [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000C]

reflection_mul_reflection_mem_range_spinToOrthogonal_of_isSquare
L∃∀N

The cited product formulas are stated for a finite-dimensional quadratic vector space over a field. TauCeti packages the same scaling and Clifford-product calculation over the commutative-ring and module hypotheses inherited from Lemma [fcap-000B][fcap-000B].

Let $R$, $M$, and $Q$ be as in Lemma [fcap-000B][fcap-000B]. Suppose $Q(v)$, $Q(w)$, and $2$ are invertible. If there is a scalar $c$ such that \[c^2=Q(v)^{-1}Q(w)^{-1},\] then \[Q(cv)Q(w)=1.\] Set $x=\iota (cv)\iota (w)$. The element $x$ is a product of invertible Clifford generators, and \[x^{*}x =\iota (w)\iota (cv)^2\iota (w) =Q(cv)Q(w)=1.\] Thus $x$ is a unitary element of the Lipschitz group. It has even degree, so it belongs to the Spin group. Its twisted adjoint action is the ordered product of reflections, and therefore \[\rho _v\rho _w\in \operatorname {range}(\operatorname {spinToOrthogonal}).\]

Proof.

The displayed square identity gives $Q(cv)Q(w)=c^2Q(v)Q(w)=1$. Each generator is a Clifford unit and lies in the Lipschitz group, while the star calculation above establishes the unitary condition. The twisted adjoint is multiplicative on Clifford units, and scalar rescaling does not change a reflection. Hence the action of $x$ is $\rho _{cv}\rho _w=\rho _v\rho _w$; its even degree supplies the remaining Spin condition.

Equations (2.24)--(2.26) give the product descriptions and scaling invariance used here. The product-square condition is sharper than asking for separate normalizations of $v$ and $w$: one scalar normalizes the product even when neither vector has been normalized separately.

Example. A Euclidean unit normal [lawson2016spin, I.2, (2.12), p. 14; (2.24)--(2.26), p. 18] [fcap-000D]

Let $V=\mathbb {R}^n$ with Euclidean inner product and use the sign convention \[Q(x)=-\langle x,x\rangle .\] For a unit vector $v$, one has $Q(v)=-1$; thus $c=1$ satisfies the square condition in Lemma [fcap-000B][fcap-000B]. The Clifford generator $\iota (v)$ is already Pin-normalized, and its action is the familiar hyperplane reflection \[\rho _v(w)=w-2\langle v,w\rangle v.\] For orthonormal $v,w$, the even product $\iota (v)\iota (w)$ lies in Spin and lifts the composition $\rho _v\rho _w$. This is the Euclidean specialization of the general Pin and paired-Spin lifting statements in Lemma [fcap-000B][fcap-000B] and Theorem [fcap-000C][fcap-000C].

Remark. From individual lifts to generation [lawson2016spin, I.2, Proposition 2.2, Definition 2.3, and (2.24)--(2.26), pp. 13--18] [fcap-000E]

Lawson and Michelsohn supply the twisted-adjoint reflection formula, the definitions of Pin and Spin, the description by products of normalized vectors, and the square-root obstruction to normalization. The square-witness statements in Lemma [fcap-000B][fcap-000B] and Theorem [fcap-000C][fcap-000C] isolate the precise algebraic hypotheses under which one or two reflections lift.

An individual lift does not by itself show that all orthogonal transformations lift. That global conclusion requires finite dimension, nondegeneracy, and the Cartan--Dieudonne factorization developed next.

From reflection generation to Pin and Spin [fcap-000U]

One reflection can enlarge the fixed subspace of an orthogonal transformation. Iterating this correction proves that reflections generate the orthogonal group. Once each reflection has a Pin lift, generation gives the Pin cover; determinant parity then restricts that cover to Spin over the special orthogonal group.

Lemma. Fixed-subspace correction by reflections [cartan1981theory, Section 10, pp. 10--12] [fcap-000V]

exists_mem_subgroup_mul_eqOn_sup_span_singleton_of_reflection_mem
L∃∀N

Cartan proves reflection factorization by an induction that enlarges the fixed subspace. The subgroup-valued statement below is a formalized TauCeti lemma extracted from that method. Cartan's one- or two-reflection correction is repackaged as an element of $H$ acting trivially on $W+Kx$.

Let $K$ be a field of characteristic different from $2$, let $Q$ be a quadratic form on a $K$-vector space $V$, and let $H\le O(V,Q)$ contain every reflection in a nonisotropic vector. Suppose $g\in O(V,Q)$ fixes a subspace $W$ pointwise and $x\in W^{\perp }$ has $Q(x)\ne 0$. Then there is an element $r\in H$ such that \[rg\vert _{W+Kx}=\operatorname {id}.\] The correction leaves the previously fixed space untouched and fixes one additional nonisotropic direction. It is either one reflection or a product of two reflections.

Proof.

Compare $x$ with $g(x)$. When $g(x)-x$ is nonisotropic, reflection in that difference carries $g(x)$ to $x$; because the difference is orthogonal to $W$, the reflection fixes $W$. In the exceptional case $g(x)+x$ is nonisotropic: reflection in this sum carries $g(x)$ to $-x$, and reflection in $x$ supplies the second factor. Both factors fix $W$, so their product gives the required correction.

Lemma. Pin-range refinement of the correction [cartan1981theory, Section 10, pp. 10--12]; [lawson2016spin, I.2, (2.26) and Theorem 2.9, pp. 18--19] [fcap-0018]

exists_mem_range_pinToOrthogonal_mul_eqOn_sup_span_singleton
L∃∀N

Under the hypotheses of Lemma [fcap-000V][fcap-000V], suppose moreover that $K$ is separably closed and take $H$ to be the range of the Pin action. Over a separably closed field, TauCeti's fixed-sign square condition from Theorem [fcap-000X][fcap-000X] holds, so every reflection factor used by the correction has a square-normalized Pin lift by Lemma [fcap-000B][fcap-000B]. The correcting element $r$ can therefore be chosen in \[\operatorname {range}(\operatorname {pinToOrthogonal}),\] and still satisfies $rg\vert _{W+Kx}=\operatorname {id}$. The statement concerns the correcting element in the Pin-action range; in the exceptional case it is the image of a product of two Pin lifts, not the image of a single reflecting vector.

Theorem. Cartan--Dieudonne generation [lawson2016spin, I.2, Theorem 2.7, p. 17] [fcap-000W]

subgroup_eq_top_of_reflection_mem
L∃∀N

Let $K$ be a field of characteristic different from $2$, let $V$ be finite-dimensional, and let $Q$ be nondegenerate. Every orthogonal transformation is a product of reflections in nonisotropic vectors. Equivalently, if a subgroup $H\le O(V,Q)$ contains every such reflection, then \[H=O(V,Q).\] This formulation asserts generation only; it records neither a sharp bound on the number of reflection factors nor a parity formula for such a factorization.

Proof.

Begin with the zero fixed subspace, whose restricted polar form is nondegenerate. If the current nondegenerate fixed subspace is not all of $V$, its orthogonal complement is nonzero and nondegenerate, hence contains a nonisotropic vector. The correction step of Lemma [fcap-000V][fcap-000V] enlarges the fixed subspace by that orthogonal line and preserves nondegeneracy. Finite-dimensional induction eventually makes the corrected product the identity, expressing the original transformation as a product of reflections. Cartan gives this fixed-vector induction, including the isotropic-difference case, in [cartan1981theory, Section 10, pp. 10--12].

Theorem. Surjectivity of the Pin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-000X]

pinToOrthogonal_surjective_of_isSquare pinToOrthogonal_surjective
L∃∀N

Let $K$, $V$, and $Q$ be as in Theorem [fcap-000W][fcap-000W]. Suppose every scalar $-Q(v)^{-1}$ attached to a nonisotropic vector is a square in $K$. Then the twisted-adjoint homomorphism is surjective: \[\operatorname {pinToOrthogonal}:\operatorname {Pin}(V,Q)\twoheadrightarrow O(V,Q).\] Indeed, Lemma [fcap-000B][fcap-000B] puts every reflection in its range, and Theorem [fcap-000W][fcap-000W] says that those reflections generate the target. In particular the conclusion holds over a separably closed field.

Lawson and Michelsohn ask whether a nonzero vector can be rescaled to quadratic length either $+1$ or $-1$; see (2.26) and the discussion preceding Theorem 2.9. Under the convention $Q=-q$, TauCeti's hypothesis asks for the particular scalar $-Q(v)^{-1}$ to be a square, so every reflecting vector is normalized to one fixed sign. This is a sufficient and generally stronger condition, not an equivalent reformulation of Lawson--Michelsohn's condition.

Example. A planar rotation as two reflections [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000Y]

In an oriented Euclidean plane, let $u$ and $v$ be unit normals whose directed angle is $\frac {\theta }{2}$. Reflection in $u^{\perp }$ followed by reflection in $v^{\perp }$ is rotation through $\theta $. With the convention $Q=-\langle -,-\rangle $, both vectors have $Q=-1$, and \[s=\iota (v)\iota (u)\in \operatorname {Spin}(V,Q)\] lifts that rotation. In an oriented orthonormal basis $e_1,e_2$, the familiar rotor form is \[\pm s=\cos \left (\frac {\theta }{2}\right )+\sin \left (\frac {\theta }{2}\right )\,\iota (e_1)\iota (e_2),\] after choosing the central sign and the order convention for the two reflections. This is the two-dimensional specialization of the paired lift in Theorem [fcap-000C][fcap-000C]; the half-angle appears because the Spin element acts by conjugation on vectors.

Lemma. Determinant parity detects the even lift [lawson2016spin, I.2, Theorems 2.7 and 2.9, pp. 17--19] [fcap-001A]

det_reflection mem_even_of_det_pinToOrthogonal_eq_one
L∃∀N

Let $R$ be a commutative ring in which $2$ is invertible, let $M$ be a finite free $R$-module, and let $Q$ be a quadratic form on $M$. A reflection in a vector of invertible quadratic value has determinant $-1$. Therefore a product of $r$ such reflections has determinant \[(-1)^r.\] In particular, every product of an even number of reflections belongs to $SO(M,Q)$.

Lawson--Michelsohn state this parity argument for quadratic vector spaces over a field. The finite-free commutative-ring statement above is the formalized extension: its determinant calculation uses freeness and finiteness, while invertibility of $2$ identifies the fixed part of the grading involution with the even subalgebra.

The Clifford lift remembers this parity. If $p\in \operatorname {Pin}(M,Q)$ and its orthogonal action has determinant $1$, then $p$ lies in the even Clifford subalgebra. Hence $p$ is a Spin element. Thus any Pin lift of a special orthogonal transformation is automatically even.

Proof.

Multiplicativity of the determinant gives the first assertion from $\det (\rho _v)=-1$. For the second, the grading involution of a Lipschitz element is its determinant sign times that element. If the determinant is $1$, the involution fixes the Pin element. Because $2$ is invertible, the fixed submodule of the grading involution is precisely the even Clifford subalgebra.

Theorem. Surjectivity of the Spin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-001B]

spinToSpecialOrthogonal_surjective_of_isSquare spinToSpecialOrthogonal_surjective
L∃∀N

Let $K$ be a field of characteristic different from $2$, let $V$ be finite-dimensional, and let $Q$ be nondegenerate. Suppose that for every nonisotropic $v\in V$, the scalar $-Q(v)^{-1}$ is a square in $K$. Then the twisted-adjoint action restricts to a surjection \[\operatorname {Spin}(V,Q)\twoheadrightarrow SO(V,Q).\] The underlying homomorphism is TauCeti.CliffordAlgebra.spinToSpecialOrthogonal, and its action on vectors is the usual Spin action by TauCeti.CliffordAlgebra.coe_spinToSpecialOrthogonal_apply.

Indeed, the square-normalization hypothesis and Cartan--Dieudonne generation give the Pin surjection of Theorem [fcap-000X][fcap-000X]. It lifts an element of $SO(V,Q)$ to Pin; the lift has determinant $1$, so Lemma [fcap-001A][fcap-001A] shows that it is even and therefore lies in Spin. The restriction square

$\text{[math]}$ commutes because both vertical maps are induced by the same twisted Clifford conjugation. Over a separably closed field the square condition is automatic, so nondegeneracy and finite dimension suffice. The general restriction principle from a surjective Pin action is TauCeti.CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_pinToOrthogonal_surjective.

The square condition is TauCeti's fixed-sign sufficient hypothesis, stronger in general than Lawson--Michelsohn's option to normalize each vector to either sign; see Theorem [fcap-000X][fcap-000X]. For a positive-definite real geometric form $q$, the Clifford convention is $Q=-q$; hence $-Q(v)^{-1}>0$ for every nonzero $v$, so the reflecting vectors can be normalized over $\mathbb {R}$. This observation does not assert the square condition for arbitrary real signatures.

Lemma. The real Spin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001C]

zmodTwoMulEquivKerSpinToSpecialOrthogonal
L∃∀N

For a real quadratic space of signature $(p,q)$, the kernel of the Spin action is the scalar pair: \[(\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \simeq \ker \bigl (\operatorname {Spin}(p,q)\longrightarrow SO(p,q)\bigr ).\] The nontrivial residue class maps to the scalar Clifford element $-1$. Thus the two kernel elements are precisely $1$ and $-1$. This is the kernel used in Gallier's real double-cover theorem.

TauCeti proves the analogous algebraic statement over a field $K$: $V$ is nontrivial and finite-dimensional, $Q$ is nondegenerate, and $2$ is invertible in $K$. Under exactly those hypotheses it constructs the displayed canonical multiplicative equivalence. This is a generalization of the cited real result, not an attribution of arbitrary-field kernel classification to Gallier.

Theorem. The algebraic Spin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001D]

spinDoubleCoverOfSurjective spinDoubleCover
L∃∀N

Let $K$ be a characteristic-zero field, let $V$ be finite-dimensional, and let its bilinear form be nondegenerate. Meinrenken defines Spin as the even part of the norm-one Clifford group. Its kernel is the scalar pair. If the Spin action is surjective, these data form the group extension \[1\longrightarrow (\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \longrightarrow \operatorname {Spin}(Q)\longrightarrow SO(Q)\longrightarrow 1.\] The left map sends the nontrivial class to $-1$; the right map is the Spin action. TauCeti packages this generic construction from an explicit surjectivity proof. The group-extension constructor used in that package is GroupExtension.ofMulEquivKer.

Meinrenken warns that the map to $SO(V)$ need not be surjective over a general field; it is surjective when every element of $K$ has a square root, because lifts can then be rescaled to have norm one. TauCeti separates this issue explicitly. Its generic construction assumes a field, a nontrivial finite-dimensional module, invertible $2$, a nondegenerate quadratic form, and a supplied surjectivity proof. Over a separably closed field, Theorem [fcap-001B][fcap-001B] supplies that proof and yields the specialized extension.

Lemma. The real Pin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001E]

zmodTwoMulEquivKerPinToOrthogonal
L∃∀N

For a real quadratic space of signature $(p,q)$, the Pin action has the same two-element kernel: \[(\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \simeq \ker \bigl (\operatorname {Pin}(p,q)\longrightarrow O(p,q)\bigr ).\] Its nontrivial generator is the image in Pin of the scalar Spin element $-1$. The identification is obtained by comparing the Pin kernel with the Spin kernel, not by adding a second pair of central elements. Gallier's real double-cover proof uses exactly the quotient by $\{\pm 1\}$.

TauCeti transports the Spin-kernel equivalence to Pin over a field $K$ when the module is nontrivial and finite-dimensional, $Q$ is nondegenerate, and $2$ is invertible. These are the formal theorem's exact assumptions; the cited scholarly claim is the real case.

Theorem. The algebraic Pin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001F]

pinDoubleCoverOfSurjective pinDoubleCover
L∃∀N

In Meinrenken's characteristic-zero, finite-dimensional, nondegenerate setting, Pin is the kernel of the norm on the Clifford group. Its scalar kernel and any proof that the Pin action is surjective determine the group extension \[1\longrightarrow (\mathbb Z/2\mathbb Z)_{\mathrm {mult}} \longrightarrow \operatorname {Pin}(Q)\longrightarrow O(Q)\longrightarrow 1.\] The inclusion sends the nontrivial class to the scalar $-1$, and the projection is the Pin action. Meinrenken notes that surjectivity can fail over a general field and that square roots for all field elements suffice to normalize lifts. TauCeti's generic theorem instead assumes a field, a nontrivial finite-dimensional module, invertible $2$, a nondegenerate quadratic form, and an explicit surjectivity proof. Its separably closed specialization obtains that proof from the formal Cartan--Dieudonne route.

Remark. Algebraic extension versus topological cover [fcap-000Z]

The extensions in Theorem [fcap-001D][fcap-001D] and Theorem [fcap-001F][fcap-001F] are exact sequences of abstract groups. They record a surjective homomorphism and its two-element kernel. No topology on the groups is used.

For real quadratic spaces of arbitrary signature, Gallier proves that the two maps \[\operatorname {Pin}(p,q)\longrightarrow O(p,q),\qquad \operatorname {Spin}(p,q)\longrightarrow SO(p,q)\] are topological double covers [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40].

Gallier then treats the compact groups: $\operatorname {Spin}(n)$ is path-connected for $n\geq 2$, and for $n\geq 3$ it is simply connected and hence the universal cover of $SO(n)$ [gallier2014clifford, Section 1.8, pp. 40--42]. These claims are not being extended here to arbitrary signature. Kostant identifies the differential of the complex Spin cover with the quadratic Clifford Lie algebra [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]. Those conclusions require topological or Lie-theoretic structure not supplied by an abstract group extension. They are not asserted by the four cards above.

Bivectors and the orthogonal Lie algebra [fcap-000M]

The second exterior power singled out by the PBW filtration has a second life inside the Clifford algebra. Its half-commutators are closed under the commutator bracket, and their action on generators is exactly the infinitesimal orthogonal action.

Convention. Bivector normalizations [meinrenken2013clifford, Section 2.2.5, Proposition 2.5, p. 33] [fcap-000N]

bivector_def bivector_lie_ι
L∃∀N

Meinrenken works throughout this chapter with finite-dimensional vector spaces over a characteristic-zero field. The cards below retain his normalization and formulas but follow TauCeti's extensions. Each card states the commutative-ring, module, invertible-$2$, finite-dimensional, or nondegeneracy assumptions it needs.

Meinrenken starts with a symmetric bilinear form $B$ and the relation \[uv+vu=2B(u,v)1.\] For the associated quadratic form $Q(v)=B(v,v)$, the polar form used here is $B_Q=2B$.

Meinrenken's quantization formula and the half-commutator agree: \[q(u\wedge v)=uv-B(u,v)1 =\frac 12(uv-vu)=:\beta (u,v).\] The induced action on a vector is \[[\beta (u,v),x] =B_Q(v,x)u-B_Q(u,x)v =2\bigl (B(v,x)u-B(u,x)v\bigr ).\] This is Meinrenken's formula $-2\iota _{B(x,-)}(u\wedge v)$ and Kostant's formula $-2\iota _x(u\wedge v)$ in the corresponding contraction convention [kostant1997clifford, Section 2.4, (12) and Theorem 8, pp. 283, 286]. The factor of two belongs to the passage from $B$ to the unhalved polar form $B_Q$; it is not an additional rescaling of $\beta $.

Definition. Clifford bivector [meinrenken2013clifford, Section 2.2.5, Proposition 2.5, p. 33] [fcap-000O]

bivectorExterior equivExterior_bivectorExterior
L∃∀N

For the formalized extension described in Convention [fcap-000N][fcap-000N], let $R$ be a commutative ring in which $2$ is invertible, let $M$ be an $R$-module, and let $Q$ be a quadratic form on $M$. The Clifford bivector of $u,v\in M$ is \[\beta _Q(u,v)=\frac 12\bigl (\iota (u)\iota (v)-\iota (v)\iota (u)\bigr ).\] It is alternating in $u$ and $v$, so it induces a linear map \[\beta _Q:\bigwedge _R^2M\longrightarrow \mathcal {C}\kern -2pt\ell (Q).\] The exterior model is a left inverse on its image: \[\operatorname {equivExterior}_Q\bigl (\beta _Q(z)\bigr )=z \qquad (z\in \bigwedge _R^2M).\] Hence $\beta _Q$ is injective.

Lemma. A bivector acts by an infinitesimal rotation [meinrenken2013clifford, Section 2.2.10, Theorem 2.1, pp. 39--40] [fcap-000P]

bivector_lie_ι
L∃∀N

For $u,v,x\in M$, the commutator of the bivector with a Clifford generator is \[[\beta _Q(u,v),\iota (x)] =\iota \left (B_Q(v,x)u-B_Q(u,x)v\right ).\] The endomorphism \[A_{u\wedge v}(x)=B_Q(v,x)u-B_Q(u,x)v\] is skew-adjoint for $B_Q$, since \[B_Q(A_{u\wedge v}x,y)+B_Q(x,A_{u\wedge v}y)=0.\] Thus commutation by a degree-two Clifford element preserves the generating module and realizes the elementary infinitesimal orthogonal transformation attached to $u\wedge v$.

Proof.

Expand the half-commutator and move $\iota (x)$ past $\iota (u)$ and $\iota (v)$ using the Clifford relation. The cubic terms cancel; the two polar terms combine to the displayed generator. Symmetry of $B_Q$ then makes the skew-adjointness equation cancel in pairs.

Theorem. Exterior bivectors are the quadratic Clifford Lie algebra [meinrenken2013clifford, Section 2.2.10, Theorem 2.1, pp. 39--40] [fcap-000Q]

bivectorExteriorEquivQuadraticLieSubalgebra bivectorLieEquiv
L∃∀N

Over the commutative ring and module of Definition [fcap-000O][fcap-000O], let $\mathfrak {cl}^{(2)}(Q)$ be the submodule of $\mathcal {C}\kern -2pt\ell (Q)$ spanned by the elements $\beta _Q(u,v)$. This is TauCeti's module-general extension of Meinrenken's characteristic-zero vector-space construction. The commutator formula of Lemma [fcap-000P][fcap-000P], together with the Jacobi identity, shows that this submodule is closed under commutators. Transporting its bracket across $\beta _Q$ gives a Lie algebra structure on $\bigwedge _R^2M$ and a Lie equivalence \[\bigwedge _R^2M\simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] On a decomposable bivector the equivalence is exactly \[u\wedge v\longmapsto \frac 12(uv-vu).\] No choice of basis enters this identification.

Theorem. Quadratic elements realize the orthogonal Lie algebra [meinrenken2013clifford, Section 2.2.10, Proposition 2.12, p. 40] [fcap-000R]

soEquivQuadratic soEquivQuadratic_lie_ι
L∃∀N

Meinrenken states this realization over a characteristic-zero field. TauCeti proves the extension below over any field of characteristic different from $2$. Let $K$ be such a field, let $V$ be finite-dimensional, and let $Q$ be nondegenerate. Write $\mathfrak {so}(V,B_Q)$ for the Lie algebra of endomorphisms skew-adjoint for the polar form. Then commutation on generators gives a Lie equivalence \[\mathfrak {so}(V,B_Q)\simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] If $A\in \mathfrak {so}(V,B_Q)$ corresponds to $z_A\in \mathfrak {cl}^{(2)}(Q)$, then \[[z_A,\iota (x)]=\iota (Ax)\qquad (x\in V).\] Combining this equivalence with Theorem [fcap-000Q][fcap-000Q] gives the basis-free chain \[\bigwedge _K^2V\simeq _{\mathrm {Lie}}\mathfrak {so}(V,B_Q) \simeq _{\mathrm {Lie}}\mathfrak {cl}^{(2)}(Q).\] Kostant identifies the same degree-two subspace with $\operatorname {Lie}(\operatorname {Spin}(V))$ and the first equivalence with the differential of the double cover [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287].

Example. An elementary skew matrix [meinrenken2013clifford, Section 2.2.10, Proposition 2.12, p. 40] [fcap-000S]

bivectorEquivSo_apply_ιMulti bivectorEquivSo_apply_ιMulti_mulVec
L∃∀N

This coordinate example specializes TauCeti's extension of the characteristic-zero construction summarized in Convention [fcap-000N][fcap-000N]. Take $V=R^n$ with the standard sum-of-squares quadratic form, and let $e_i,e_j$ be distinct coordinate vectors. Under the standard-coordinate realization, \[e_i\wedge e_j\longmapsto 2(E_{ij}-E_{ji}).\] Thus its action on $x=(x_k)$ is \[x\longmapsto 2x_j e_i-2x_i e_j.\] The factor $2$ is the polar-form normalization from Convention [fcap-000N][fcap-000N]: for the sum-of-squares form, $B_Q(x,y)=2\sum _kx_ky_k$. The displayed matrix is the standard-coordinate specialization of the basis-free isomorphism in Meinrenken's proposition. Dividing the skew matrix by two would correspond to using the associated bilinear form $B_Q/2$ instead.

Remark. Infinitesimal and global Clifford symmetry [fcap-000T]

The quadratic Clifford Lie algebra is the infinitesimal part of the same conjugation action that produces reflections. Kostant proves that $\bigwedge ^2V=\operatorname {Lie}(\operatorname {Spin}(V))$, that its map to $\mathfrak {so}(V)$ is the differential of $\operatorname {Spin}(V)\to SO(V)$, and that its commutator action extends as the corresponding derivation of the exterior algebra [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]. Chevalley obtains the same two-vector Lie algebra inside the Clifford group [chevalley1954algebraic, II.2.9, pp. 67--68].

The cards above identify the algebraic Lie layer. They do not construct Lie-group structures or identify a differential of a Lie-group covering map. The next chapter instead reaches the global orthogonal group by finite products of reflections.

Theorem. An orthogonal Lie action lifts to every Clifford module [kostant1997clifford, Section 3.1, pp. 294--295] [fcap-001O]

cliffordInducedRep cliffordInducedRep_apply
L∃∀N

Let $K$ be a field in which $2$ is invertible, let $V$ be finite-dimensional, and let $Q$ be nondegenerate. Suppose a $K$-Lie algebra $L$ acts orthogonally on $V$ through \[\theta :L\longrightarrow \mathfrak {so}(V,B_Q),\] and let $\rho :\mathcal {C}\kern -2pt\ell (Q)\to \operatorname {End}_K(S)$ be any Clifford module. The equivalence of Theorem [fcap-000R][fcap-000R] lifts $\theta $ to quadratic Clifford elements; composing with $\rho $ gives a Lie representation \[\rho _{\mathcal {C}\kern -2pt\ell }:L\longrightarrow \operatorname {End}_K(S),\qquad \rho _{\mathcal {C}\kern -2pt\ell }(y)=\rho \bigl (\operatorname {soEquivQuadratic}(\theta (y))\bigr ).\] Kostant constructs this lift for a complex reductive group representation and then lets its quadratic elements act on the spin module. The formalized statement isolates the algebraic mechanism over the stated field and for an arbitrary Clifford module; it does not assert that $\theta $ is a differential of a group representation.

Differentiating smooth group homomorphisms [fcap-001Q]

The quadratic Clifford construction in the preceding section is algebraic. A different bridge starts from a smooth homomorphism of Lie groups and differentiates it at the identity. This produces the functor from Lie groups to Lie algebras and explains which part of the Spin-representation roadmap is generic differential geometry, before any Lie-group structure on the abstract Spin and special orthogonal groups has been supplied.

Definition. The differential of a smooth homomorphism [liu2016lie, Section 2.1, p. 9] [fcap-001R]

Let $G$ and $H$ be finite-dimensional real Lie groups, with identities $e_G$ and $e_H$, and let $\phi :G\to H$ be a smooth group homomorphism. Their Lie algebras are the tangent spaces \[\mathfrak g=T_{e_G}G, \qquad \mathfrak h=T_{e_H}H.\] The differential of $\phi $ at the identity is the linear map \[\operatorname {Lie}(\phi )=d\phi _{e_G}: \mathfrak g\longrightarrow \mathfrak h.\] No connectedness or simply-connectedness hypothesis is needed to define this map. Those hypotheses enter the converse problem of integrating a Lie-algebra homomorphism, not the differentiation of a given smooth homomorphism.

For $X\in \mathfrak g$, let $\widetilde X$ be its left-invariant vector field, \[\widetilde X_g=d(L_g)_{e_G}X.\] The homomorphism identity $\phi \circ L_g=L_{\phi (g)}\circ \phi $ gives \[d\phi _g(\widetilde X_g) =\widetilde {\operatorname {Lie}(\phi )(X)}_{\phi (g)}.\] Thus differentiation at the identity and transport by left translation are two descriptions of the same infinitesimal map.

Lemma. The differential preserves the Lie bracket [liu2016lie, Section 2.1, p. 9] [fcap-001S]

In the setting of Definition [fcap-001R][fcap-001R], the differential is a Lie-algebra homomorphism: \[\operatorname {Lie}(\phi )([X,Y]) =[\operatorname {Lie}(\phi )(X), \operatorname {Lie}(\phi )(Y)].\] Indeed, the left-invariant fields $\widetilde X$ and $\widetilde Y$ are $\phi $-related to the left-invariant fields determined by their images. Brackets of related vector fields are again related. Evaluating that relation at $e_G$ gives the displayed identity.

This argument is local at the identity. In particular, bracket preservation does not require $G$ to be connected or simply connected.

Theorem. The Lie functor [liu2016lie, Section 2.2, p. 10] [fcap-001T]

Differentiation at the identity is functorial. For smooth homomorphisms $G\xrightarrow {\phi }H\xrightarrow {\psi }K$, the chain rule gives \[\operatorname {Lie}(\operatorname {id}_G) =\operatorname {id}_{\mathfrak g}, \qquad \operatorname {Lie}(\psi \circ \phi ) =\operatorname {Lie}(\psi )\circ \operatorname {Lie}(\phi ).\] Together with Lemma [fcap-001S][fcap-001S], this defines a functor from Lie groups and smooth homomorphisms to Lie algebras and Lie-algebra homomorphisms.

The stronger correspondence between simply connected Lie groups and Lie algebras concerns existence and uniqueness in the reverse direction. It is not a hypothesis of these functor laws.

Theorem. Naturality of the exponential [liu2016lie, Section 2.4, pp. 12--13] [fcap-001U]

Let $\phi :G\to H$ be a smooth Lie-group homomorphism. For every $X\in \mathfrak g$, \[\phi (\exp _G X) =\exp _H\bigl (\operatorname {Lie}(\phi )(X)\bigr ).\] Equivalently, the square

$\text{[math]}$ commutes.

Proof.

The curve $t\mapsto \phi (\exp _G(tX))$ is a one-parameter subgroup of $H$. Its tangent vector at $t=0$ is $\operatorname {Lie}(\phi )(X)$. The curve $t\mapsto \exp _H(t\operatorname {Lie}(\phi )(X))$ has the same property and the same tangent vector. Uniqueness of the one-parameter subgroup with a given tangent vector identifies the curves; setting $t=1$ proves the formula.

Example. Differentiating a matrix representation [liu2016lie, Sections 2.1 and 2.4, pp. 9, 12] [fcap-001V]

Let $V$ be a finite-dimensional real vector space and let \[\rho :G\longrightarrow \operatorname {GL}(V)\] be a smooth representation. Its differential is a Lie-algebra representation \[d\rho _{e_G}:\mathfrak g\longrightarrow \mathfrak {gl}(V).\] Naturality of the exponential becomes \[\rho (\exp _G X)=\exp \bigl (d\rho _{e_G}(X)\bigr ),\] where the exponential on the right is the ordinary matrix exponential. For example, for the determinant homomorphism $\det :\operatorname {GL}_n(\mathbb R)\to \mathbb R^\times $, \[d(\det )_I(A)=\operatorname {tr}(A).\]

Remark. Why explicit smoothness changes the roadmap [liu2016lie, Sections 2.1--2.4 and 2.8, pp. 9--13, 19--20]; [isaev2018theory, Section 3.1.2, pp. 106--107] [fcap-001W]

The constructions in Definition [fcap-001R][fcap-001R]--Example [fcap-001V][fcap-001V] start with a smooth homomorphism. Their tangent map, bracket law, functor laws, and exponential naturality therefore do not require a theorem that upgrades a continuous homomorphism to a smooth one. The generic theorem does not invoke the closed-subgroup theorem; that theorem belongs to the later specialization to concrete matrix subgroups. This is the dependency split proposed in TauCetiRoadmap PR 224.

The exponential input is separate from the tangent and bracket input. Likewise, the Baker--Campbell--Hausdorff calculation can first be made in a matrix or general-linear group; using it inside a particular closed matrix subgroup additionally requires the subgroup's Lie structure. Liu describes the local exponential and BCH coordinates, while Isaev--Rubakov give the matrix Campbell--Hausdorff calculation.

The open TauCeti draft PR 3078 proposes the generic construction and its functor and exponential laws. It is not merged, so these cards carry no Lean markers. Even after that generic interface lands, the differential of $\operatorname {Spin}(Q)\to SO(Q)$ still needs compatible Lie-group structures on the two abstract groups. The algebraic identification in Theorem [fcap-000R][fcap-000R] does not by itself supply those structures.

Polarization and the exterior spinor model [fcap-001G]

A polarization turns Clifford generators into creation, contraction, and parity operators on an exterior algebra. The resulting Clifford action has two group restrictions and receives every orthogonal Lie action through the quadratic Clifford realization.

Write $S=\bigwedge _K W$ for the exterior carrier and $\rho :\mathcal {C}\kern -2pt\ell (Q)\to \operatorname {End}(S)$ for its Clifford action. Let $\mathfrak g$ be an external Lie algebra with an orthogonal action $\theta :\mathfrak g\to \mathfrak {so}(V,Q)$. The diagram records the induced Lie action at the top and the Pin and Spin restrictions of $\rho $ below.

$\text{[math]}$

Definition. Polarization data and its carrier [chevalley1954algebraic, II.2.1--II.2.2, pp. 42--44] [fcap-001H]

SpinPolarizationData
L∃∀N

Let $K$ be a commutative ring, let $V$ be a $K$-module, and let $Q$ be a quadratic form. Polarization data consists of isotropic submodules $W,W'\subseteq V$, an orthogonal remainder $L$, and a linear equivalence \[(W\oplus W')\oplus L\simeq V.\] The polar form identifies $W'$ with $W^*$; the pairing is separating in both variables. A coordinate $\ell :L\to K$ is injective and satisfies $\ell (z)^2=Q(z)$. Thus $L$ is an orthogonal remainder equipped with an injective coordinate. Over a field it is at most one-dimensional; it vanishes in the classical even split model. The carrier of the exterior spinor model is \[S=\bigwedge _K W.\]

Chevalley treats complementary totally singular subspaces in the split, even-dimensional field case. Meinrenken uses the equivalent Lagrangian model $V=F^*\oplus F$ [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, pp. 56--57]. The packaged remainder and commutative-ring hypotheses are TauCeti's stated generalization.

Definition. Creation, contraction, and the line operator [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001I]

wedge contract lineOperator
L∃∀N

For $x\in W$, creation is exterior multiplication \[\varepsilon _x(s)=x\wedge s.\] For $y\in W'$, contraction is the degree-$-1$ operator $\iota _y$ associated with the functional $x\mapsto B_Q(x,y)$. Finally, if $z\in L$, its operator is \[\lambda _z=\ell (z)\,\alpha ,\] where $\alpha $ is parity: it is $+1$ on even exterior degree and $-1$ on odd exterior degree. Chevalley's formulas identify the first two operators as left Clifford multiplication on the minimal ideal model [chevalley1954algebraic, II.2.2, pp. 43--44].

Lemma. The polarized Clifford relation [meinrenken2013clifford, Section 3.2.1, pp. 54--55] [fcap-001J]

contract_wedge cliffordOperator_sq
L∃∀N

Creation and contraction satisfy \[\iota _y\varepsilon _x+\varepsilon _x\iota _y =B_Q(x,y)\operatorname {id}_S.\] Creation and contraction each square to zero. Parity anticommutes with both, while $\lambda _z^2=Q(z)\operatorname {id}_S$. Consequently the operator $c(v)$ assembled from the three polarization coordinates obeys \[c(v)^2=Q(v)\operatorname {id}_S.\] This is the quadratic form of the usual polarized anticommutation relation $c(v)c(w)+c(w)c(v)=B_Q(v,w)$. Meinrenken states the latter as the defining condition for a Clifford module.

Theorem. The exterior Clifford action [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001K]

spinAction
L∃∀N

The square relation of Lemma [fcap-001J][fcap-001J] extends uniquely to an algebra homomorphism \[\rho :\mathcal {C}\kern -2pt\ell (Q)\longrightarrow \operatorname {End}_K(S).\] On the three summands it is determined by \[\rho (\iota (x))s=x\wedge s,\qquad \rho (\iota (y))s=\iota _y(s),\qquad \rho (\iota (z))s=\ell (z)\alpha (s).\] The corresponding formalized equations are TauCeti.spinAction_ι_wedge, TauCeti.spinAction_ι_contract, and TauCeti.spinAction_ι_lineOperator. Chevalley's split even-dimensional model has no remainder term; the third formula is TauCeti's odd-line extension of that construction.

Theorem. Creation and contraction generate all endomorphisms [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60] [fcap-001L]

creation_contraction_adjoin_eq_top spinAction_surjective
L∃∀N

Assume that $W$ is finite and free over the commutative ring $K$. The subalgebra of $\operatorname {End}_K(\bigwedge W)$ generated by all creation operators and all contractions is the whole endomorphism algebra. Since the polar pairing identifies $W'$ with $W^*$, these generators lie in the image of the exterior Clifford action. Hence \[\rho :\mathcal {C}\kern -2pt\ell (Q)\twoheadrightarrow \operatorname {End}_K(\bigwedge W)\] is surjective.

Meinrenken proves generation first in rank one by four matrix units and then by tensor decomposition. Over a split field he combines surjectivity with a dimension calculation to obtain an isomorphism and irreducibility. TauCeti formalizes the generation and surjectivity statements over a finite free module. This card does not claim that $S$ is irreducible, or that $\rho $ is injective.

Definition. The Spin and Pin representations [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001M]

spinRep pinRep
L∃∀N

The groups $\operatorname {Spin}(Q)$ and $\operatorname {Pin}(Q)$ consist of units in the Clifford algebra. Restricting the action $\rho $ of Theorem [fcap-001K][fcap-001K] along these two inclusions gives representations on the same exterior carrier: \[\operatorname {spinRep}:\operatorname {Spin}(Q)\longrightarrow \operatorname {Aut}_K(S), \qquad \operatorname {pinRep}:\operatorname {Pin}(Q)\longrightarrow \operatorname {Aut}_K(S).\] Meinrenken calls the restriction of a Clifford module to the Clifford group the spin representation. The definitions here require only the commutative ring, module, quadratic form, and polarization data already used for $\rho $; no nondegeneracy or finite-dimensionality is added.

Lemma. The restricted actions are the Clifford action [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001N]

spinRep_apply pinRep_apply
L∃∀N

For every $g\in \operatorname {Spin}(Q)$ and $h\in \operatorname {Pin}(Q)$, the two representations act through their underlying Clifford units: \[\operatorname {spinRep}(g)=\rho (g),\qquad \operatorname {pinRep}(h)=\rho (h).\] Thus the group actions introduce no new formula on $S$; they are the same Clifford action with a smaller domain. In particular, any equation proved for the action of the underlying Clifford element applies to its Spin or Pin restriction.

Example. The rank-one polarized model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, p. 59] [fcap-001P]

Let $W=Ke$ and choose $e'\in W'$ with $B_Q(e,e')=1$. In the ordered basis $(1,e)$ of $S=\bigwedge W$, creation and contraction are \[\varepsilon _e= \begin {pmatrix}0&0\\1&0\end {pmatrix}, \qquad \iota _{e'}= \begin {pmatrix}0&1\\0&0\end {pmatrix}.\] Both are nilpotent, and \[\varepsilon _e\iota _{e'}+\iota _{e'}\varepsilon _e=I_2.\] Together with their products they give the four matrix units of $\operatorname {End}_K(S)$. This is the rank-one calculation in Meinrenken's generation proof and a specialization of the general relation in Lemma [fcap-001J][fcap-001J]. The formalized ingredients are TauCeti.SpinPolarizationData.contract_wedge and TauCeti.ExteriorAlgebra.creation_contraction_adjoin_eq_top; neither declaration formalizes this displayed choice of basis.

Remark. Horizons beyond the exterior model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60]; [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]; [lawson2016spin, I.2, pp. 13--19] [fcap-0017]

The exterior action constructed above stops before several classical consequences in representation theory. Over a split field, irreducibility and the decomposition into two half-spin modules require further hypotheses and arguments; Meinrenken proves these results after establishing that the Clifford action is an isomorphism. The currently open TauCeti half-spin work is therefore not represented by a Lean marker here.

The generic mathematics of differentiating a smooth Lie-group homomorphism is developed in § [fcap-001Q][fcap-001Q]. What remains missing for the Spin cover is more specific: compatible Lie-group structures on TauCeti's abstract $\operatorname {Spin}(V)$ and $SO(V)$, followed by the identification of their specialized differential with the algebraic quadratic action above. The open TauCeti PR linked in Remark [fcap-001W][fcap-001W] proposes only the generic Lie functor.

Highest weights, triality, and the Bott-periodic real table also belong to later layers. Kostant supplies the differential in the classical complex setting, and Lawson--Michelsohn treat the real Pin and Spin groups. None of these horizons follows merely from the algebraic restrictions $\operatorname {spinRep}$ and $\operatorname {pinRep}$.

Hyperbolic recurrence and real signatures [fcap-0010]

A positive and a negative generator form a hyperbolic plane. Adjoining that plane tensors the Clifford algebra with two-by-two real matrices. Iteration removes the common part of a real signature, while a sign switch gives a complementary one-sided recurrence. These are algebraic steps toward the real classification; the real Pin and Spin groups follow a separate branch through the double-cover theory.

Convention. Real signature and Clifford signs [chevalley1954algebraic, II.2.9, pp. 65--66] [fcap-0011]

realCliffordForm realCliffordForm_apply
L∃∀N

For $p,q\ge 0$, put \[Q_{p,q}(x)=\sum _{i<p}x_i^2-\sum _{p\le i<p+q}x_i^2\] on $\mathbb {R}^{p+q}$, and write $\mathcal {C}\kern -2pt\ell _{p,q}$ for $\mathcal {C}\kern -2pt\ell (Q_{p,q})$. Thus the first $p$ Clifford generators square to $+1$, and the last $q$ square to $-1$. This agrees with Chevalley's convention for the quadratic form and with his positive/negative inertia indices.

Lawson and Michelsohn use the same signature $q_{r,s}$ but impose $v^2=-q_{r,s}(v)1$ [lawson2016spin, I.3, Proposition 3.1, p. 21]. Therefore the algebras are related by the exact index swap \[\mathcal {C}\kern -2pt\ell _{p,q}=\mathcal {C}\kern -2pt\ell ^{\mathrm {Lawson}}_{q,p}.\] The recurrence below adds one index of each sign, so it is invariant under this swap.

Definition. The hyperbolic plane [lawson2016spin, I.4, Theorem 4.1 and (4.3), pp. 25--26] [fcap-0012]

realCliffordForm_one_one_apply realBottSplitIsometry
L∃∀N

The real hyperbolic plane is \[H=(\mathbb {R}^2,Q_{1,1}),\qquad Q_{1,1}(s,t)=s^2-t^2.\] Its coordinate generators $e_+$ and $e_-$ satisfy \[e_+^2=1,\qquad e_-^2=-1,\qquad e_+e_-=-e_-e_+.\] For every signature, separating the last positive and negative coordinates gives an isometry \[(\mathbb {R}^{p+q+2},Q_{p+1,q+1}) \simeq (\mathbb {R}^{p+q},Q_{p,q})\perp H.\] The coordinate order is fixed: the retained $p$ positive and $q$ negative axes form the first factor, and the last positive and last negative axes form $H$.

Theorem. The hyperbolic matrix recurrence [lawson2016spin, I.4, Theorem 4.1, (4.3), pp. 25--26] [fcap-0013]

hyperbolicEquivTensor realCliffordBottEquiv_ι
L∃∀N

For finite-dimensional quadratic spaces, Lawson--Michelsohn state the signature recurrence \[\mathcal {C}\kern -2pt\ell _{p+1,q+1}\simeq _{\mathbb {R}\text {-alg}} \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb {R}}M_2(\mathbb {R}).\] TauCeti extends the recurrence to any real quadratic module $(M,Q)$ and supplies an explicit formula on generators: \[\mathcal {C}\kern -2pt\ell (Q\perp Q_{1,1})\simeq \mathcal {C}\kern -2pt\ell (Q)\otimes _{\mathbb {R}}M_2(\mathbb {R}).\] With \[\sigma _x=\begin {pmatrix}0&1\\1&0\end {pmatrix},\] the equivalence sends a generator $(m,(s,t))$ to \[\iota _Q(m)\otimes \sigma _x +1\otimes \begin {pmatrix}s&t\\-t&-s\end {pmatrix}.\] The first summand squares to $Q(m)$, the second to $s^2-t^2$, and the two anticommute. The universal property therefore gives the forward algebra map. In the other direction, the original Clifford algebra and the matrix algebra act through commuting algebra maps on the hyperbolic Clifford algebra; their tensor lift is inverse to the forward map. The two composites are checked on Clifford generators and pure tensors, which is why TauCeti's extension needs no finite-dimensional hypothesis. Chevalley's split-matrix theorem and orthogonal-sum calculation supply the classical structural mechanism [chevalley1954algebraic, II.2.1 and II.2.5, pp. 42--46].

Writing the displayed generator formula as $f$, its universal extension is summarized by the commuting diagram

$\text{[math]}$

Lemma. Finite hyperbolic reduction [chevalley1954algebraic, II.2.9, pp. 65--66] [fcap-0014]

realCliffordBottIterEquiv realCliffordSignatureReductionEquiv
L∃∀N

Chevalley splits a finite-dimensional real quadratic space into hyperbolic planes and a definite remainder. TauCeti combines that classical reduction with iteration of Theorem [fcap-0013][fcap-0013] and Kronecker equivalences to synthesize the explicit tensor and matrix packaging below. Iterating $n$ times gives \[\mathcal {C}\kern -2pt\ell _{p+n,q+n}\simeq \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb {R}}M_{2^n}(\mathbb {R}).\] Taking $n=\min (p,q)$ removes the common positive and negative part: \[\mathcal {C}\kern -2pt\ell _{p,q}\simeq \mathcal {C}\kern -2pt\ell _{p-n,q-n}\otimes _{\mathbb {R}}M_{2^n}(\mathbb {R}), \qquad n=\min (p,q).\] Thus if $p\le q$, the residual algebra is $\mathcal {C}\kern -2pt\ell _{0,q-p}$; if $q\le p$, it is $\mathcal {C}\kern -2pt\ell _{p-q,0}$. The matrix factors combine through the Kronecker equivalence \[M_{2^a}(\mathbb {R})\otimes M_{2^b}(\mathbb {R}) \simeq M_{2^{a+b}}(\mathbb {R}).\] Chevalley supplies the quadratic-space decomposition. The displayed $M_{2^n}$ packaging and its named equivalences are TauCeti's formalized synthesis.

Theorem. The signature-switch recurrence [lawson2016spin, I.4, Theorem 4.1 and (4.1), pp. 25--26] [fcap-001X]

realCliffordSignatureSwitchRecurrenceEquiv
L∃∀N

With the TauCeti signature convention of Convention [fcap-0011][fcap-0011], there is an algebra equivalence \[\mathcal {C}\kern -2pt\ell _{p+2,q}\simeq _{\mathbb R\text {-alg}} \mathcal {C}\kern -2pt\ell _{q,p}\otimes _{\mathbb R}M_2(\mathbb R).\] The construction first separates the last positive coordinate from $Q_{p+2,q}$. Adjoining that positive line permits a Clifford sign switch; negating $Q_{p+1,q}$ exchanges its positive and negative coordinate blocks. The resulting form is $Q_{q+1,p+1}$, to which the hyperbolic recurrence of Theorem [fcap-0013][fcap-0013] applies.

The accompanying generator theorem SignatureSwitchRecurrenceEquiv_ι records this composition through the positive-coordinate splitter, the sign-switch isometry, and the generator formula for the hyperbolic equivalence. It fixes the equivalence on the canonical Clifford generators rather than asserting only that some algebra isomorphism exists.

After converting between the two signature conventions, inverting Lawson--Michelsohn's equation (4.1), using $\mathcal {C}\kern -2pt\ell ^{\mathrm {Lawson}}_{0,2}\cong M_2(\mathbb R)$, and swapping the indices yields the displayed algebra isomorphism. Their equation (4.3) is instead the mixed $(1,1)$ recurrence used in Theorem [fcap-0013][fcap-0013]. Chevalley's split-matrix and orthogonal-sum constructions give the same structural ingredients [chevalley1954algebraic, II.2.1 and II.2.5, pp. 42--46]. The exact splitter composition and generator formula are additional data recorded by TauCeti.

Remark. Why algebraic periodicity is a separate branch [chevalley1954algebraic, II.2.1, II.2.5, and II.2.9, pp. 42--46, 65--66]; [lawson2016spin, I.4, Theorems 4.1 and 4.3, pp. 25--29] [fcap-001Y]

The recurrences in Theorem [fcap-0013][fcap-0013], Lemma [fcap-0014][fcap-0014], and Theorem [fcap-001X][fcap-001X] use Clifford universal properties, orthogonal sums, tensor products, coordinate isometries, and the real base entries. They do not use the Spin representation, the structure theorem obtained from a spinor module, or the Pin and Spin double covers. This is the algebraic branch of Layer 7.

The real groups $\operatorname {Pin}(p,q)$ and $\operatorname {Spin}(p,q)$ form a different branch. Their actions, kernels, and algebraic extensions specialize the group theory developed in § [fcap-0007][fcap-0007], and therefore genuinely consume the Layer-2 Pin/Spin work. The distinction between these branches is the dependency correction proposed in TauCetiRoadmap PR 225. It changes the order in which the mathematics can be built; it does not turn the roadmap proposal itself into a formal theorem.

Example. Four real Clifford base entries [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29] [fcap-0015]

realCliffordOneZeroEquivProd realCliffordZeroOneEquivComplex realCliffordZeroTwoEquivQuaternion realCliffordOneOneEquivMatrix
L∃∀N

With $\mathcal {C}\kern -2pt\ell _{0,0}\simeq \mathbb {R}$ as the scalar anchor, the signature convention of Convention [fcap-0011][fcap-0011] gives four nontrivial base entries: \[\begin {aligned} \mathcal {C}\kern -2pt\ell _{0,0}&\simeq \mathbb {R}, & \mathcal {C}\kern -2pt\ell _{1,0}&\simeq \mathbb {R}\times \mathbb {R}, & \mathcal {C}\kern -2pt\ell _{0,1}&\simeq \mathbb {C},\\ \mathcal {C}\kern -2pt\ell _{0,2}&\simeq \mathbb {H}, & \mathcal {C}\kern -2pt\ell _{1,1}&\simeq M_2(\mathbb {R}). \end {aligned}\] For $\mathcal {C}\kern -2pt\ell _{0,2}$, the two negative generators map to the quaternion units $i$ and $j$; their product maps to $k$. Thus they square to $-1$ and anticommute, as required by the Clifford relations. The exact generator map is recorded by TauCeti.realCliffordZeroTwoEquivQuaternion_ι.

For $\mathcal {C}\kern -2pt\ell _{1,1}$, the positive and negative generators may be represented by \[e_+\longmapsto \begin {pmatrix}1&0\\0&-1\end {pmatrix}, \qquad e_-\longmapsto \begin {pmatrix}0&1\\-1&0\end {pmatrix}.\] Their squares are $+I$ and $-I$, and they anticommute. The last equivalence is also the case $p=q=0$ of Theorem [fcap-0013][fcap-0013]. The index swap in Convention [fcap-0011][fcap-0011] explains why Lawson's one-generator table lists $\mathbb {C}$ and $\mathbb {R}\times \mathbb {R}$ in the opposite order.

Remark. What the recurrence does not classify [fcap-0016]

Hyperbolic reduction determines the matrix factor coming from matched positive and negative axes. It leaves a one-sided algebra $\mathcal {C}\kern -2pt\ell _{r,0}$ or $\mathcal {C}\kern -2pt\ell _{0,r}$. The signature-switch recurrence of Theorem [fcap-001X][fcap-001X] provides a second move, and Example [fcap-0015][fcap-0015] fixes the first real, complex, quaternionic, and matrix entries. These facts still have to be assembled into recurrences that close on each one-sided axis.

A reviewed local candidate called SPINREP-050 establishes the quaternion recurrence \[\mathcal {C}\kern -2pt\ell _{p,q+2}\simeq \mathcal {C}\kern -2pt\ell _{q,p}\otimes _{\mathbb R}\mathbb H,\] and another local candidate, SPINREP-053, iterates the recurrence chain to \[\mathcal {C}\kern -2pt\ell _{p+8,q}\simeq \mathcal {C}\kern -2pt\ell _{p,q}\otimes _{\mathbb R}M_{16}(\mathbb R).\] Neither candidate is a merged TauCeti declaration or a public TauCeti pull request, so neither receives a Lean marker here.

The residue-indexed mod-eight classification table remains unformalized. In particular, the mixed $(1,1)$ recurrence alone only removes matched axes; it cannot classify the one-sided remainder. Lawson--Michelsohn give the full classical periodicity and table in [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29].

Coordinate representations [fcap-0002]

Definition. Transported exterior-basis coordinates [wieser2024formalizing, 9.3.5] [fcap-0003]

The exterior equivalence is treated in [wieser2024formalizing, 9.3.5].

For subsets with several elements, a coordinate formula additionally needs an ordering convention and its attendant signs. No such convention is implicit in the transported basis.

Lemma. Orthogonal pair transport [wieser2024formalizing, 8.4] [fcap-0004]

Thus orthogonality removes precisely the scalar correction in the two-generator change-of-form identity. No basis or reordering convention is needed.

Lemma. Orthogonal pair transport [wieser2024formalizing, 8.4] [fcap-0004]

Thus orthogonality removes precisely the scalar correction in the two-generator change-of-form identity. No basis or reordering convention is needed.

Theorem. Pairwise orthogonal list transport [wieser2024formalizing, 8.4, (8.55)] [fcap-0006]

The order of the list is fixed throughout. Reordering would require an additional permutation-sign calculation and is not a consequence of this theorem.

Spin-representation roadmap [fcap-0019]

The exterior shadow of a Clifford algebra [fcap-000F]

Definition. Word-length filtration [chevalley1954algebraic, II.1.2 and II.1.6, pp. 40--42] [fcap-000G]

filtration filtration_mul
L∃∀N

Lemma. The leading symbol is exterior [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000H]

changeForm_prod_map_ι_sub_prod_map_ι_mem_filtration filtrationLeadingTerm_apply_ιMulti
L∃∀N

Proof.

Theorem. The graded pieces are exterior powers [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000I]

filtrationGradedPieceEquivExteriorPower filtrationLeadingTerm_eq_filtrationGradedEquiv_symm
L∃∀N

Theorem. PBW equivalence with the exterior algebra [meinrenken2013clifford, Proposition 2.6, pp. 33--34] [fcap-000J]

filtrationAssociatedGradedEquivExterior
L∃∀N

Example. The degree-two symbol [chevalley1954algebraic, II.1.6, pp. 41--42] [fcap-000K]

filtrationAssociatedGradedEquivExterior_apply_of_succ
L∃∀N

Remark. Basis proof and quotient proof [fcap-000L]

Reflections and square-normalized Clifford lifts [fcap-0007]

Convention. Quadratic-form sign [lawson2016spin, I.1, (1.3)--(1.4), p. 8] [fcap-0008]

Definition. Reflection in a nonisotropic vector [lawson2016spin, I.2, (2.12), p. 14] [fcap-0009]

reflection
L∃∀N

Lemma. Twisted Clifford conjugation is a reflection [lawson2016spin, I.2, Proposition 2.2 and (2.8), p. 13; (2.11)--(2.12), p. 14] [fcap-000A]

Proof.

Lemma. Square-normalized Pin lift [lawson2016spin, I.2, Definition 2.3 and (2.26), pp. 14, 18] [fcap-000B]

reflection_mem_range_pinToOrthogonal_of_isSquare
L∃∀N

Theorem. Paired reflections have a product-square Spin lift [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000C]

reflection_mul_reflection_mem_range_spinToOrthogonal_of_isSquare
L∃∀N

Proof.

Example. A Euclidean unit normal [lawson2016spin, I.2, (2.12), p. 14; (2.24)--(2.26), p. 18] [fcap-000D]

Remark. From individual lifts to generation [lawson2016spin, I.2, Proposition 2.2, Definition 2.3, and (2.24)--(2.26), pp. 13--18] [fcap-000E]

From reflection generation to Pin and Spin [fcap-000U]

Lemma. Fixed-subspace correction by reflections [cartan1981theory, Section 10, pp. 10--12] [fcap-000V]

exists_mem_subgroup_mul_eqOn_sup_span_singleton_of_reflection_mem
L∃∀N

Proof.

Lemma. Pin-range refinement of the correction [cartan1981theory, Section 10, pp. 10--12]; [lawson2016spin, I.2, (2.26) and Theorem 2.9, pp. 18--19] [fcap-0018]

exists_mem_range_pinToOrthogonal_mul_eqOn_sup_span_singleton
L∃∀N

Theorem. Cartan--Dieudonne generation [lawson2016spin, I.2, Theorem 2.7, p. 17] [fcap-000W]

subgroup_eq_top_of_reflection_mem
L∃∀N

Proof.

Theorem. Surjectivity of the Pin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-000X]

pinToOrthogonal_surjective_of_isSquare pinToOrthogonal_surjective
L∃∀N

Example. A planar rotation as two reflections [lawson2016spin, I.2, (2.24)--(2.26), p. 18] [fcap-000Y]

Lemma. Determinant parity detects the even lift [lawson2016spin, I.2, Theorems 2.7 and 2.9, pp. 17--19] [fcap-001A]

det_reflection mem_even_of_det_pinToOrthogonal_eq_one
L∃∀N

Proof.

Theorem. Surjectivity of the Spin action [lawson2016spin, I.2, Theorem 2.9, pp. 18--19] [fcap-001B]

spinToSpecialOrthogonal_surjective_of_isSquare spinToSpecialOrthogonal_surjective
L∃∀N

Lemma. The real Spin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001C]

zmodTwoMulEquivKerSpinToSpecialOrthogonal
L∃∀N

Theorem. The algebraic Spin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001D]

spinDoubleCoverOfSurjective spinDoubleCover
L∃∀N

Lemma. The real Pin kernel is the scalar pair [gallier2014clifford, Section 1.8, Proposition 1.21, pp. 39--40] [fcap-001E]

zmodTwoMulEquivKerPinToOrthogonal
L∃∀N

Theorem. The algebraic Pin extension [meinrenken2013clifford, Definition 3.2, pp. 51--52] [fcap-001F]

pinDoubleCoverOfSurjective pinDoubleCover
L∃∀N

Remark. Algebraic extension versus topological cover [fcap-000Z]

Bivectors and the orthogonal Lie algebra [fcap-000M]

Convention. Bivector normalizations [meinrenken2013clifford, Section 2.2.5, Proposition 2.5, p. 33] [fcap-000N]

bivector_def bivector_lie_ι
L∃∀N

Meinrenken starts with a symmetric bilinear form $B$ and the relation \[uv+vu=2B(u,v)1.\] For the associated quadratic form $Q(v)=B(v,v)$, the polar form used here is $B_Q=2B$.

Definition. Clifford bivector [meinrenken2013clifford, Section 2.2.5, Proposition 2.5, p. 33] [fcap-000O]

bivectorExterior equivExterior_bivectorExterior
L∃∀N

Lemma. A bivector acts by an infinitesimal rotation [meinrenken2013clifford, Section 2.2.10, Theorem 2.1, pp. 39--40] [fcap-000P]

bivector_lie_ι
L∃∀N

Proof.

Theorem. Exterior bivectors are the quadratic Clifford Lie algebra [meinrenken2013clifford, Section 2.2.10, Theorem 2.1, pp. 39--40] [fcap-000Q]

bivectorExteriorEquivQuadraticLieSubalgebra bivectorLieEquiv
L∃∀N

Theorem. Quadratic elements realize the orthogonal Lie algebra [meinrenken2013clifford, Section 2.2.10, Proposition 2.12, p. 40] [fcap-000R]

soEquivQuadratic soEquivQuadratic_lie_ι
L∃∀N

Example. An elementary skew matrix [meinrenken2013clifford, Section 2.2.10, Proposition 2.12, p. 40] [fcap-000S]

bivectorEquivSo_apply_ιMulti bivectorEquivSo_apply_ιMulti_mulVec
L∃∀N

Remark. Infinitesimal and global Clifford symmetry [fcap-000T]

Theorem. An orthogonal Lie action lifts to every Clifford module [kostant1997clifford, Section 3.1, pp. 294--295] [fcap-001O]

cliffordInducedRep cliffordInducedRep_apply
L∃∀N

Differentiating smooth group homomorphisms [fcap-001Q]

Definition. The differential of a smooth homomorphism [liu2016lie, Section 2.1, p. 9] [fcap-001R]

Lemma. The differential preserves the Lie bracket [liu2016lie, Section 2.1, p. 9] [fcap-001S]

This argument is local at the identity. In particular, bracket preservation does not require $G$ to be connected or simply connected.

Theorem. The Lie functor [liu2016lie, Section 2.2, p. 10] [fcap-001T]

The stronger correspondence between simply connected Lie groups and Lie algebras concerns existence and uniqueness in the reverse direction. It is not a hypothesis of these functor laws.

Theorem. Naturality of the exponential [liu2016lie, Section 2.4, pp. 12--13] [fcap-001U]

Let $\phi :G\to H$ be a smooth Lie-group homomorphism. For every $X\in \mathfrak g$, \[\phi (\exp _G X) =\exp _H\bigl (\operatorname {Lie}(\phi )(X)\bigr ).\] Equivalently, the square

$\text{[math]}$ commutes.

Proof.

Example. Differentiating a matrix representation [liu2016lie, Sections 2.1 and 2.4, pp. 9, 12] [fcap-001V]

Remark. Why explicit smoothness changes the roadmap [liu2016lie, Sections 2.1--2.4 and 2.8, pp. 9--13, 19--20]; [isaev2018theory, Section 3.1.2, pp. 106--107] [fcap-001W]

Polarization and the exterior spinor model [fcap-001G]

$\text{[math]}$

Definition. Polarization data and its carrier [chevalley1954algebraic, II.2.1--II.2.2, pp. 42--44] [fcap-001H]

SpinPolarizationData
L∃∀N

Definition. Creation, contraction, and the line operator [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001I]

wedge contract lineOperator
L∃∀N

Lemma. The polarized Clifford relation [meinrenken2013clifford, Section 3.2.1, pp. 54--55] [fcap-001J]

contract_wedge cliffordOperator_sq
L∃∀N

Theorem. The exterior Clifford action [meinrenken2013clifford, Section 3.2.2, Proposition 3.5, p. 57] [fcap-001K]

spinAction
L∃∀N

Theorem. Creation and contraction generate all endomorphisms [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60] [fcap-001L]

creation_contraction_adjoin_eq_top spinAction_surjective
L∃∀N

Definition. The Spin and Pin representations [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001M]

spinRep pinRep
L∃∀N

Lemma. The restricted actions are the Clifford action [meinrenken2013clifford, Section 3.2.1, pp. 55--56] [fcap-001N]

spinRep_apply pinRep_apply
L∃∀N

Example. The rank-one polarized model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, p. 59] [fcap-001P]

Remark. Horizons beyond the exterior model [meinrenken2013clifford, Section 3.2.4, Theorem 3.3, pp. 59--60]; [kostant1997clifford, Section 2.4, Theorem 8, pp. 286--287]; [lawson2016spin, I.2, pp. 13--19] [fcap-0017]

Hyperbolic recurrence and real signatures [fcap-0010]

Convention. Real signature and Clifford signs [chevalley1954algebraic, II.2.9, pp. 65--66] [fcap-0011]

realCliffordForm realCliffordForm_apply
L∃∀N

Definition. The hyperbolic plane [lawson2016spin, I.4, Theorem 4.1 and (4.3), pp. 25--26] [fcap-0012]

realCliffordForm_one_one_apply realBottSplitIsometry
L∃∀N

Theorem. The hyperbolic matrix recurrence [lawson2016spin, I.4, Theorem 4.1, (4.3), pp. 25--26] [fcap-0013]

hyperbolicEquivTensor realCliffordBottEquiv_ι
L∃∀N

Writing the displayed generator formula as $f$, its universal extension is summarized by the commuting diagram

$\text{[math]}$

Lemma. Finite hyperbolic reduction [chevalley1954algebraic, II.2.9, pp. 65--66] [fcap-0014]

realCliffordBottIterEquiv realCliffordSignatureReductionEquiv
L∃∀N

Theorem. The signature-switch recurrence [lawson2016spin, I.4, Theorem 4.1 and (4.1), pp. 25--26] [fcap-001X]

realCliffordSignatureSwitchRecurrenceEquiv
L∃∀N

Remark. Why algebraic periodicity is a separate branch [chevalley1954algebraic, II.2.1, II.2.5, and II.2.9, pp. 42--46, 65--66]; [lawson2016spin, I.4, Theorems 4.1 and 4.3, pp. 25--29] [fcap-001Y]

Example. Four real Clifford base entries [lawson2016spin, I.4, Theorem 4.3 and Tables I--II, pp. 27--29] [fcap-0015]

realCliffordOneZeroEquivProd realCliffordZeroOneEquivComplex realCliffordZeroTwoEquivQuaternion realCliffordOneOneEquivMatrix
L∃∀N

Remark. What the recurrence does not classify [fcap-0016]

Definition. Transported exterior-basis coordinates [wieser2024formalizing, 9.3.5] [fcap-0003]

The exterior equivalence is treated in [wieser2024formalizing, 9.3.5].

For subsets with several elements, a coordinate formula additionally needs an ordering convention and its attendant signs. No such convention is implicit in the transported basis.

Lemma. Vanishing list contraction [wieser2024formalizing, 8.4, (8.54)] [fcap-0005]

The conclusion depends only on the ordered recurrence and pointwise vanishing of $d$ on the list. In particular, it is independent of a basis or any reordering convention.

Definition. dual module [ca-0012]
Module.Dual
L∃∀N

The dual module $M^* : M \to _{l[R]} R$ is the $R$-module of all linear maps from $M$ to $R$.

Definition. even subalgebra of Clifford algebra [wieser2022computing] [ca-001J]
CliffordAlgebra.even
L∃∀N

The even subalgebra of the Clifford algebra is defined as the submodule of the Clifford algebra \[ \mathcal {C}\kern -2pt\ell ^{+}(Q) \equiv \left \{ x_1 \cdots x_k \in \mathcal {C}\kern -2pt\ell \mid x \in V, k \text { is even} \right \} \] which also forms a subalgebra. Its elements are called even elements, as they can be expressed as the geometric product of an even number of 1-vectors.

Definition. ring homomorphism [chen2016infinitely, 4.5.1] [ca-0014]
RingHom RingHomClass algebraMap
L∃∀N

Let $(\alpha , +_\alpha , *_\alpha )$ and $(\beta , +_\beta , *_\beta )$ be rings. A ring homomorphism from $\alpha $ to $\beta $ is a map $\mathit {1} : \alpha \to _{+*} \beta $ such that

$\mathit {1}(x +_{\alpha } y) = \mathit {1}(x) +_{\beta } \mathit {1}(y)$ for each $x,y \in \alpha $.
$\mathit {1}(x *_{\alpha } y) = \mathit {1}(x) *_{\beta } \mathit {1}(y)$ for each $x,y \in \alpha $.
$\mathit {1}(1_{\alpha }) = 1_{\beta }$.

2. other draft notes

Formalization notes for Zhou's rigidity construction [connes-0001]
📄PDF

August 12, 2026
Utensil Song

Introduction [connes-0010]

with contributions from Utensil Song

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]

August 12, 2026
Utensil Song

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.

$\text{[math]}$

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.

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

Tensor retraction in characteristic two [connes-001E]

Lemma. Characteristic-two tensor retraction [connes-000C]

delta_diagonal concreteSquareSpanData
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_diagonal concreteSquareSpanData
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]

SpatialWitness isNormal tracialEquiv_of_spatialWitness paperGroupFactors_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]

EquivariantHaarHomeomorph paperHaarHomeomorph
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]

HasKazhdanPropertyT HasRelativePropertyT
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]

HasKazhdanPropertyT HasRelativePropertyT elementaryGroup
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_top elementaryEquivSL3
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_top elementaryEquivSL3
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_quotient paper_gammaOne_icc paper_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:

every nonidentity $a\in N$ has an infinite $S$-orbit; and
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_quotient paper_gammaOne_icc paper_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_semisimple paperCharacteristicModuleEquiv paperGroups_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 polynomial-matrix argument paperSL3NoNontrivialAbelianNormalSubgroup for the polynomial-matrix factor handles the $\mathrm {SL}_3$ image.
The stronger finite result Sp4.no_nontrivial_normal_abelian_subgroup handles the symplectic image through a kernel-checked certificate.

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]

theoremA elementaryGroup
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:

$\text{[math]}$

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]

theoremA theoremA
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_spectralData paperSpatialWitness ActionData
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:

the dual topology instances paperKernelTopology and paperKernelDiscreteTopology;
the Borel instances paperCharacterMeasurableSpace and paperCharacterBorelSpace; and
the representation-module carrier instance representationAsModuleAddCommGroup.

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.

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]

EquivariantHaarHomeomorph continuousCrossedClosure_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]

IsProjectionSupremum isNormal
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]

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

OpenAI proof architecture [connes-0018]

Changing the kernel while preserving the measured action [connes-000M]

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

$\text{[math]}$

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

$\text{[math]}$

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:

quantitative Kazhdan subsets, constants, and relative ratios, with a bridge to the current qualitative predicate; our internal allocation is 2–3.5 thousand lines;
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;
fixed-space angles, codistance, and the class-two nilpotent estimate; our internal allocation is 5–9 thousand;
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;
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
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.lapMatrix SimpleGraph.posSemidef_lapMatrix
L∃∀N

The pinned Connes project uses Mathlib revision 062f1e3d with Lean 4.34.0-rc1. 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 cc6ce75 uses Mathlib de5ce8a 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, or magic-graph lane. It 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:

Zhou's exact invocation [zhou2026icc, Proposition 4.1, pp. 8–10];
the elementary-group theorem, unweighted boundary graph, and packaged six-root estimate [ershov2010noncommutative, Theorem 1.1, p. 1; Section 5.4, pp. 25–29; Proposition 6.1, pp. 34–35];
the broader root-graded theorem and arbitrary-ring relative estimate [ershov2017rootgraded, Theorem 1.1, p. 3; Appendix Theorem A.1, p. 110]; and
Kassabov's free-associative-ring estimates and Nica's exact-ring alternative.

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:

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

Agent implementation and review

reconciled the literature and public Lean sources, adapted attributed proof blocks, implemented the Lean development, and refactored its public interfaces;
ran literature, consumer-contract, provenance, semantic, and Tau Ceti reviews; built the Comparator, documentation, and rendering infrastructure; and repaired the resulting findings; and
drafted and revised 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.

Foundational Group Algebras (for) Physics [fgap-0001]
📄PDF

July 28, 2026
Utensil Song

These are the accompanying mathematical notes for the experimental research project FGAP. FGAP is read “F-gap,” for the foundational gap between established mathematical tools and open questions about physical structures, especially beyond the Standard Model. It is also a coined acronym for “Foundational Group Algebras (for) Physics.”

The project studies mathematical structures that may help us understand physical structures more deeply. It does not construct or claim a physical theory. The current storyline has been strongly shaped by agent exploration of one spike-test slice of that research domain. It follows the project's approach: turn a structural hypothesis into a small, source-grounded vertical slice, then use explicit calculations and formalization to expose its assumptions.

This slice begins with Hamilton's Quaternions and the quaternionic realization of the binary tetrahedral group, because they give a small and explicit route into finite real Group Algebras. For the human-curated storyline of the notes, see § [spin-0010].

For the mathematics, we follow the Hurwitz-unit treatment in [voight2021quaternion, ch. 11]. We keep the mathematics and the physical suggestions separate.

Remark. why begin with 2T? [fgap-0018]

The binary tetrahedral group $2T$ is small enough for explicit calculations, yet it connects finite symmetry, representations, real Group Algebras, and the quaternionic structures familiar from spin mathematics. Its concrete realization by Hurwitz units, and their identification with $2T$, are described in [voight2021quaternion, sec. 11.2, pp. 166--168], while the relation between representations and Group-Algebra modules is developed in [sengupta2010representations, secs. 3.1--3.3, pp. 39--42]. Wilson uses order-3 automorphisms of $Q_8$ to discuss possible physical interpretations in [wilson2021finite, sec. 4.3, pp. 12--13, v5]. He later adjoins an abstract generator $f$ of order 3 to $Q_8$ to form $2T$ in [wilson2021finite, sec. 6.1, p. 18, v5].

Any physical identification remains a hypothesis. A proposed correspondence must specify an action and representation, an algebra map, any preserved structure or form, a unit-group choice where applicable, and the intended physical meaning. Resemblance alone is not a model.

Quaternion and Hurwitz foundations [fgap-0019]

We first introduce Hamilton's Quaternions, the Hurwitz order, and a distinguished unit. Its order and conjugation action provide the concrete calculations used by the group constructions in the next two sections.

Definition. Hamilton's Quaternions [fgap-0006]

July 28, 2026

The algebra of real quaternions is the 4-dimensional real vector space \[ \mathbb {H} =\mathbb {R}1\oplus \mathbb {R}i\oplus \mathbb {R}j\oplus \mathbb {R}k. \] Thus every quaternion can be written uniquely as \[ q=a+bi+cj+dk,\qquad a,b,c,d\in \mathbb {R}. \] Addition and real scalar multiplication are coordinatewise. Multiplication is extended bilinearly from $1$ as the multiplicative identity and the table \[ \begin {gathered} i^2=j^2=k^2=ijk=-1,\\ ij=k,\quad jk=i,\quad ki=j,\\ ji=-k,\quad kj=-i,\quad ik=-j. \end {gathered} \] This makes $\mathbb {H}$ an associative, noncommutative real algebra. In Voight's notation, $\mathbb {H}=(-1,-1\mid \mathbb {R})$; see [voight2021quaternion, def. 2.2.1 and ex. 2.2.3].

More generally, when $F$ is a field of characteristic different from $2$ and $a,b\in F^\times $, the symbol \[ (a,b\mid F) \] denotes the quaternion algebra over $F$ generated by elements $i,j$ with \[ i^2=a,\qquad j^2=b,\qquad ji=-ij. \] The two slots record the scalars assigned to the squares of the two generators. With $k=ij$, the elements $1,i,j,k$ form an $F$-basis. Thus the two entries $-1,-1$ in $(-1,-1\mid \mathbb {R})$ say precisely that $i^2=-1$ and $j^2=-1$; the anticommutation relation then gives $k^2=-1$.

For $q=a+bi+cj+dk$, its quaternion conjugate and reduced norm are \[ \overline {q}=a-bi-cj-dk,\qquad \operatorname {nrd}(q)=q\overline {q} =a^2+b^2+c^2+d^2. \] We also have $\overline {q}q=\operatorname {nrd}(q)$. If $q\ne 0$, then $\operatorname {nrd}(q)>0$ and \[ q^{-1}=\frac {\overline {q}}{\operatorname {nrd}(q)}. \] So every nonzero quaternion is invertible. This is the standard involution and reduced norm specialized to Hamilton's Quaternions; see [voight2021quaternion, secs. 3.1--3.3].

The corresponding Mathlib type is Quaternion.

Definition. the Hurwitz order and its units [fgap-0016]

July 29, 2026

Inside the rational quaternion algebra $B=(-1,-1\mid \mathbb {Q})$, let $k=ij$ and \[ \omega =\frac {-1+i+j+k}{2}. \] The Lipschitz order and Hurwitz order are the $\mathbb {Z}$-lattices \[ \begin {aligned} L&=\mathbb {Z}+\mathbb {Z}i+\mathbb {Z}j+\mathbb {Z}k,\\ \mathcal {O} &=\mathbb {Z}+\mathbb {Z}i+\mathbb {Z}j+\mathbb {Z}\omega . \end {aligned} \] Both are subrings containing $1$. The order $\mathcal {O}$ contains $L$ with index $2$; it is the unique order properly containing $L$, and it is maximal. See [voight2021quaternion, sec. 11.1, esp. lem. 11.1.2].

A Hurwitz unit is a unit of $\mathcal {O}$. Equivalently, it is an element $q\in \mathcal {O}$ whose reduced norm is $1$. Voight calculates that $\mathcal {O}^{\times }$ has $24$ elements in [voight2021quaternion, sec. 11.2, pp. 166--168]. The particular unit $\omega $ will give the cyclic factor used below.

Remark. why the Hurwitz order is introduced [fgap-0017]

July 29, 2026

Hurwitz developed integral quaternions in 1919. Starting from the Lipschitz order $L$, the question is not merely which quaternions have integral coordinates, but which order has the better arithmetic structure. The Lipschitz order is not maximal. Voight compares this with enlarging $\mathbb {Z}[\sqrt {-3}]$ to the Eisenstein integers. Since $a=i+j+k$ satisfies $a^2=-3$, the analogous element \[ \omega =\frac {-1+a}{2} \] satisfies $\omega ^2+\omega +1=0$. Adjoining it enlarges $L$ to the maximal Hurwitz order $\mathcal {O}$. See [voight2021quaternion, sec. 11.1, pp. 165--166].

This enlargement supplies more than a convenient lattice. Its $24$ units form the binary tetrahedral group, and conjugation by $\omega $ cyclically permutes the quaternion units $i,j,k$. The same order also supports a norm-Euclidean algorithm. These features make the Hurwitz order a small meeting point of quaternion arithmetic, finite-group structure, and explicit calculation; see [voight2021quaternion, secs. 11.2--11.3, pp. 166--169].

Lemma. a Hurwitz unit of order $3$ [fgap-0003]

Let \[ a=i+j+k,\qquad \omega =\frac {-1+i+j+k}{2}=\frac {-1+a}{2}. \] Then $\omega $ is a Hurwitz unit of order $3$. This choice appears in [voight2021quaternion, p. 165].

The mixed terms in $a^2$ cancel in pairs: \[ \begin {aligned} a^2 &=i^2+j^2+k^2+(ij+ji)+(jk+kj)+(ki+ik)\\ &=-3. \end {aligned} \] It follows that \[ \begin {aligned} \omega ^2 &=\frac {(-1+a)^2}{4}\\ &=\frac {1-2a+a^2}{4}\\ &=\frac {-1-a}{2}. \end {aligned} \] Hence $\omega ^2+\omega +1=0$, and multiplication by $\omega -1$ gives \[ \omega ^3=1. \] Thus $\omega $ is invertible, has inverse $\omega ^{-1}=\omega ^2=(-1-i-j-k)/2$, and has order $3$ because $\omega \ne 1$.

Convention. left conjugation [fgap-0002]

For a nonzero quaternion $q$, we use left conjugation to mean \[ q\mathbin {\triangleright }x=qxq^{-1}. \] See the remark on the conjugation calculation for why the direction is recorded explicitly.

Quaternions can also be obtained from suitable Clifford Algebras; see Notes on Clifford Algebras. Here we use the multiplication in Hamilton's Quaternions directly.

Example. conjugation by a Hurwitz unit [fgap-0004]

Consider left conjugation by the Hurwitz unit $\omega =(-1+i+j+k)/2$. We have \[ \omega i\omega ^{-1}=k,\qquad \omega j\omega ^{-1}=i,\qquad \omega k\omega ^{-1}=j. \] Thus the cycle is $i\mapsto k\mapsto j\mapsto i$. Voight says that conjugation cyclically rotates these units in [voight2021quaternion, sec. 11.2.4, p. 168]; the calculation here fixes the direction. Wilson discusses an abstract order-3 automorphism cycling the quaternion generators in [wilson2021finite, sec. 4.3, pp. 12--13, v5]. That discussion does not select the exact quaternion or fix the oriented cycle calculated here.

It is enough to calculate \[ \omega i=k\omega ,\qquad \omega j=i\omega ,\qquad \omega k=j\omega . \] For example, \[ \omega i =\frac {-1-i+j-k}{2} =k\omega . \] Right multiplication by $\omega ^{-1}$ proves the three conjugation equations.

Remark. what the conjugation calculation gives [fgap-0005]

July 28, 2026

Saying that conjugation cyclically permutes $i,j,k$ does not by itself tell us which cycle is meant. Left conjugation by $\omega $ gives the cycle in the conjugation example. Conjugation by $\omega ^{-1}$ gives the inverse cycle. This is why we record the three equations instead of only saying "cyclically permutes."

The calculation supplies the first concrete group action used for the binary tetrahedral group. The next notes restrict this action to the quaternion subgroup and then use it in the semidirect-product construction. The three equations alone do not identify the complete set of $24$ Hurwitz units with that group.

In Lean, the three equations give the computational interface to Mathlib's Quaternion type. The abstract action is then recovered from this concrete calculation.

Quaternion and order-three subgroups [fgap-0007]

July 28, 2026

We now separate two small groups inside the nonzero quaternions. The first is the quaternion group generated by $i$ and $j$. The second is generated by the Hurwitz unit $\omega $. Conjugation by $\omega $ then tells us how the second group acts on the first.

This is the concrete input for a later construction of the binary tetrahedral group. We stop before that construction here: the present notes only define the two factors and calculate their action.

Definition. group action [fgap-0008]

A left action of a group $G$ on a set $X$ is a map \[ G\times X\longrightarrow X,\qquad (g,x)\longmapsto g\mathbin {\cdot }x \] such that \[ 1\mathbin {\cdot }x=x,\qquad g_1\mathbin {\cdot }(g_2\mathbin {\cdot }x) =(g_1g_2)\mathbin {\cdot }x. \] Equivalently, an action is a group homomorphism \[ \alpha :G\longrightarrow \operatorname {Sym}(X), \] where $\operatorname {Sym}(X)$ is the group of permutations of $X$. We use left actions throughout these notes. See [woit2024quantum, sec. 1.3.2, pp. 7--9].

If $X=H$ is a group and each permutation preserves multiplication, the action is a homomorphism \[ \alpha :G\longrightarrow \operatorname {Aut}(H). \] Its kernel is $\ker \alpha $. The action is faithful when $\alpha $ is injective.

Suppose $G$ acts on both $X$ and $Y$. A map $f:X\to Y$ is equivariant if \[ f(g\mathbin {\cdot }x)=g\mathbin {\cdot }f(x) \] for every $g\in G$ and $x\in X$. Equivariance is how an action passes between two different models of the same object.

Definition. the quaternion group inside Hamilton's Quaternions [fgap-0009]

July 28, 2026

Inside the group $\mathbb {H}^{\times }$ of nonzero quaternions, let \[ Q=\{\pm 1,\pm i,\pm j,\pm k\}. \] The multiplication table for Hamilton's Quaternions shows that this set is closed under multiplication and inverses. It is therefore a subgroup of $\mathbb {H}^{\times }$.

The elements $i$ and $j$ satisfy \[ i^4=1,\qquad i^2=j^2=-1,\qquad ji=i^{-1}j. \] These are the usual relations for the quaternion group. Hence $Q$ is a concrete copy of $Q_8$. Voight identifies the same 8 units in [voight2021quaternion, sec. 11.2, p. 166].

Here $Q$ always means this particular subgroup of the quaternions. An abstract quaternion group will be introduced only when a distinction between models is useful.

Lemma. normal forms in the quaternion subgroup [fgap-000A]

Every element of $Q$ has a unique normal form \[ i^a j^b,\qquad 0\leq a<4,\quad 0\leq b<2. \] Consequently, \[ Q=\langle i,j\rangle =\{i^a j^b:0\leq a<4,\ 0\leq b<2\} \] and $Q$ has 8 elements.

Proof.

The relation $ji=i^{-1}j$ moves each occurrence of $j$ to the right. The relations $i^4=1$ and $j^2=i^2$ then reduce every word in $i,j$ to the stated form. The 8 resulting quaternions are

\[ \begin {array}{cccc} 1&i&-1&-i\\ j&k&-j&-k. \end {array} \]

Their coordinates in $\mathbb {H}=\mathbb {R}1\oplus \mathbb {R}i\oplus \mathbb {R}j\oplus \mathbb {R}k$ are distinct, so the normal forms are unique.

The two-row display will also be useful when the concrete subgroup is compared with an abstract presentation of $Q_8$. See [voight2021quaternion, sec. 11.2, p. 166].

Lemma. the cyclic subgroup generated by the Hurwitz unit [fgap-000B]

Let \[ \omega =\frac {-1+i+j+k}{2}. \] The calculation in a Hurwitz unit of order $3$ gives $\omega ^3=1$ and $\omega \neq 1$. It follows that \[ C=\langle \omega \rangle =\{1,\omega ,\omega ^2\} \] is a cyclic subgroup of $\mathbb {H}^{\times }$ of order 3. In particular, $C\cong \mathbb {Z}/3\mathbb {Z}$. This subgroup appears in [voight2021quaternion, sec. 11.2.4, p. 168].

Proof.

Every power of $\omega $ reduces modulo 3, so $C\subseteq \{1,\omega ,\omega ^2\}$. The reverse inclusion is immediate. If $\omega ^2=1$, multiplying by $\omega $ would give $\omega =1$, contrary to the coordinate formula. Thus the 3 displayed elements are distinct.

Example. the Hurwitz action on the quaternion group [fgap-000C]

The subgroup $C$ acts on $Q$ by left conjugation: \[ C\longrightarrow \operatorname {Aut}(Q),\qquad c\longmapsto (q\longmapsto cqc^{-1}). \] Indeed, conjugation by a Hurwitz unit gives \[ \omega i\omega ^{-1}=k,\qquad \omega k\omega ^{-1}=j,\qquad \omega j\omega ^{-1}=i. \] Thus conjugation by the generator preserves all 8 elements of $Q$. Its conjugation powers preserve $Q$ as well, so every $c\in C$ gives the stated automorphism. The generator's action can be read from the two oriented cycles \[ i\longmapsto k\longmapsto j\longmapsto i, \qquad -i\longmapsto -k\longmapsto -j\longmapsto -i, \] while $1$ and $-1$ are fixed.

Conjugation preserves products: \[ c(q_1q_2)c^{-1}=(cq_1c^{-1})(cq_2c^{-1}). \] It is therefore an automorphism of $Q$; its inverse is conjugation by $c^{-1}$. The action law follows from \[ (c_1c_2)q(c_1c_2)^{-1} =c_1(c_2qc_2^{-1})c_1^{-1}. \] This verifies the action directly rather than inferring it from the picture. Voight records the normality of $Q$ and the cyclic rotation in [voight2021quaternion, sec. 11.2.4, p. 168].

Remark. concrete and abstract factor models [fgap-000D]

The subgroups $Q,C\leq \mathbb {H}^{\times }$ are concrete: their elements are quaternions, and the Hurwitz action is quaternion conjugation. The abstract groups \[ Q_8,\qquad \mathbb {Z}/3\mathbb {Z} \] remember the same group structures without remembering their quaternion coordinates.

Matching names and cardinalities does not identify these models. We need explicit isomorphisms \[ Q_8\mathbin {\cong }Q,\qquad \mathbb {Z}/3\mathbb {Z}\mathbin {\cong }C. \] The action must then be transported through these isomorphisms and proved equivariant. This keeps later abstract calculations connected to the quaternion realization that supplied them.

In Lean, QuaternionGroup at parameter $2$ models the abstract quaternion factor, and Multiplicative applied to ZMod at modulus $3$ models the abstract cyclic factor. The concrete subgroups remain the main computational model. Explicit isomorphisms recover the abstract interface from that model, and equivariance connects the transported action to quaternion conjugation. Formalization therefore keeps these bridges as results rather than treating them as definitions.

From the Hurwitz action to the binary tetrahedral group [fgap-000E]

July 28, 2026

The action calculated in the Hurwitz action on the quaternion group now lets us combine the quaternion group $Q$ and the cyclic group $C$. We first recall the general steps: normalization makes a set product into a subgroup, complementarity gives unique factorization, and unique factorization produces an internal semidirect product.

Applying these steps inside $\mathbb {H}^{\times }$ gives a concrete group with 24 elements: \[ Q,\ C \longrightarrow T=Q\vee C=QC \longrightarrow T\cong Q\rtimes C. \] The last isomorphism compares two models; it does not identify their elements.

Definition. normalizer of a subgroup [fgap-000F]

July 28, 2026

Let $N$ be a subgroup of $G$. The normalizer of $N$ in $G$ is \[ N_G(N)=\{g\in G:gNg^{-1}=N\}. \] It is the largest subgroup of $G$ in which $N$ is normal. In particular, a subgroup $H\leq G$ acts on $N$ by conjugation precisely when \[ H\leq N_G(N). \] See [fre2023discrete, sec. 4.2.6, pp. 56--57].

The ambient group matters. If $H$ normalizes $N$, then $N$ is normal in the subgroup generated by $N$ and $H$. This does not imply that $N$ is normal in all of $G$.

For the quaternion subgroups in Quaternion and order-three subgroups, the three conjugation calculations in the Hurwitz action on the quaternion group give \[ C\leq N_{\mathbb {H}^{\times }}(Q). \] They do not claim that $Q$ is normal in $\mathbb {H}^{\times }$.

Lemma. a normalized product is the generated subgroup [fgap-000G]

July 28, 2026

Let $N,H\leq G$. If $H\leq N_G(N)$, then the set product \[ NH=\{nh:n\in N,\ h\in H\} \] is a subgroup and \[ N\vee H=NH. \] Moreover, $N$ is normal in $N\vee H$.

Proof.

July 28, 2026

Normalization gives the calculation needed for closure: \[ (n_1h_1)(n_2h_2) =n_1(h_1n_2h_1^{-1})h_1h_2\in NH. \] It also gives $(nh)^{-1}=(h^{-1}n^{-1}h)h^{-1}\in NH$. Thus $NH$ is a subgroup containing both $N$ and $H$, while every subgroup containing $N$ and $H$ contains every product $nh$. This proves $N\vee H=NH$. Finally, conjugation by generators from $N$ and $H$ preserves $N$, so $N$ is normal in their generated subgroup.

This is the small bridge between an action by conjugation and an internal product. Compare the normalizer and internal-product discussion in [fre2023discrete, secs. 4.2.6 and 4.2.13, pp. 56--57 and 62--63].

Definition. complementary subgroups [fgap-000H]

July 28, 2026

Subgroups $N,H\leq G$ are complementary, in this ordered sense, when multiplication \[ N\times H\longrightarrow G,\qquad (n,h)\longmapsto nh \] is a bijection. Equivalently, every $g\in G$ has a unique factorization $g=nh$.

For subgroups, the two conditions \[ N\cap H=\{1\},\qquad NH=G \] give complementarity. Existence follows from $NH=G$. For uniqueness, if $n_1h_1=n_2h_2$, then \[ n_2^{-1}n_1=h_2h_1^{-1}\in N\cap H, \] so both sides are $1$.

Trivial intersection alone is not enough: a complement must also provide the factorization of the ambient group. Fré uses these ingredients for an internal semidirect product in [fre2023discrete, sec. 4.2.13, pp. 62--63].

Theorem. the internal semidirect-product theorem [fgap-000I]

July 28, 2026

Let $N,H\leq G$. Suppose $N$ is normal in $G$ and $N,H$ are complementary. Conjugation defines an action \[ \alpha :H\longrightarrow \operatorname {Aut}(N),\qquad \alpha (h)(n)=hnh^{-1}. \] Give $N\times H$ the multiplication \[ (n_1,h_1)(n_2,h_2) =\bigl (n_1\alpha (h_1)(n_2),h_1h_2\bigr ). \] The resulting external semidirect product is denoted $N\rtimes _{\alpha }H$. Multiplication induces an isomorphism \[ N\rtimes _{\alpha }H\xrightarrow {\ \cong \ }G, \qquad (n,h)\longmapsto nh. \]

Proof.

July 28, 2026

The displayed multiplication is chosen so that \[ (n_1h_1)(n_2h_2) =n_1(h_1n_2h_1^{-1})h_1h_2. \] Thus the multiplication map preserves products. Complementarity makes it bijective, so it is an isomorphism.

Conversely, the canonical copies of $N$ and $H$ in $N\rtimes _{\alpha }H$ are complementary, and the copy of $N$ is normal. The external multiplication and its split exact sequence are developed in [isaev2018theory, sec. 1.4.2, pp. 58--61]; compare [fre2023discrete, sec. 4.2.13, pp. 62--63]. An arbitrary extension by a normal subgroup need not split: the complement is extra structure.

Example. the binary tetrahedral subgroup of the quaternions [fgap-000J]

July 28, 2026

Inside $\mathbb {H}^{\times }$, let \[ T=Q\vee C. \] The Hurwitz action in the Hurwitz action on the quaternion group says that $C$ normalizes $Q$. Hence a normalized product is the generated subgroup gives \[ T=QC,\qquad Q\mathrel {\trianglelefteq }T. \]

The groups $Q$ and $C$ have orders 8 and 3. The order of their intersection divides both, so \[ Q\cap C=\{1\}. \] They are therefore complementary in $T$. Every element has a unique normal form \[ q\omega ^r,\qquad q\in Q,\quad 0\leq r<3, \] and the internal semidirect-product theorem gives \[ Q\rtimes _{\alpha }C\cong T,\qquad \alpha (c)(q)=cqc^{-1}. \]

The action orientation is fixed by the quaternion calculation: \[ i\longmapsto k\longmapsto j\longmapsto i. \] Voight identifies this semidirect product with the Hurwitz unit group and the binary tetrahedral group in [voight2021quaternion, sec. 11.2.4, p. 168].

Example. the twenty-four Hurwitz units [fgap-000K]

July 28, 2026

The unique normal forms divide $T$ into three disjoint rows: \[ \begin {array}{c|c|c} Q&Q\omega &Q\omega ^2\\ \hline 8\text { elements}&8\text { elements}&8\text { elements}. \end {array} \] Therefore $|T|=8\cdot 3=24$.

The first row is \[ Q=\{\pm 1,\pm i,\pm j,\pm k\}. \] Since \[ \omega =\frac {-1+i+j+k}{2},\qquad \omega ^2=\frac {-1-i-j-k}{2}, \] left multiplication by the 8 elements of $Q$ gives \[ Q\omega \sqcup Q\omega ^2 = \left \{ \frac {\epsilon _0+\epsilon _1i+\epsilon _2j+\epsilon _3k}{2}: \epsilon _r\in \{\pm 1\} \right \}. \] The coordinates are distinct, so these are the 16 half-integral units. Together with $Q$, they are exactly the 24 Hurwitz units listed in [voight2021quaternion, sec. 11.2, p. 166]. Thus the subgroup $T$ is the unit group of the Hurwitz order, not merely another group of the same cardinality.

Remark. internal, external, and abstract models [fgap-000L]

July 28, 2026

Three related objects have appeared. The internal model $T\leq \mathbb {H}^{\times }$ has quaternions as its elements. The external semidirect product $Q\rtimes _{\alpha }C$ has pairs $(q,c)$ as its elements. An abstract binary tetrahedral group can instead be specified without quaternion coordinates.

The isomorphism $(q,c)\mapsto qc$ compares the first two models. It is not an equality of their elements.

The next note transports the distinguished central involution and cardinality to an abstract binary tetrahedral model. Transporting the full factorization to factors such as QuaternionGroup 2 and Multiplicative (ZMod 3) also needs explicit isomorphisms and equivariance proofs. None of this follows from the order computation $|T|=24$ alone.

Definition. the distinguished involution of abstract 2T [fgap-0014]

Let $T\leq \mathbb {H}^{\times }$ be the binary tetrahedral group of Hurwitz units from the binary tetrahedral subgroup of the quaternions, and let $B$ be the abstract semidirect-product model obtained from the same Hurwitz action. Choose the group isomorphism \[ \rho :B\mathbin {\cong }T \] that compares these two models. Voight identifies $T$ with the Hurwitz unit group and with $Q_8\rtimes \mathbb {Z}/3\mathbb {Z}$ in [voight2021quaternion, sec. 11.2.4, p. 168].

The quaternion $-1$ belongs to $T$; it is central, its square is 1, and it is not 1. Define the distinguished central involution of $B$ by \[ z=\rho ^{-1}(-1). \] Since an isomorphism preserves multiplication and reflects equality, \[ z\in Z(B),\qquad z^2=1,\qquad z\neq 1. \] Thus the abstract group retains the central involution supplied by its quaternionic realization. The element $z$ is not identified with the quaternion $-1$; the isomorphism $\rho $ relates them.

The same isomorphism transports cardinality. Since the calculation in the twenty-four Hurwitz units gives $|T|=24$, \[ |B|=|T|=24. \] The corresponding Lean theorem uses Mathlib's Nat.card; its statement is Nat.card BinaryTetrahedral.Abstract = 24.

The occurrence of $-1$ among the 24 Hurwitz units is explicit in [voight2021quaternion, sec. 11.2, p. 166].

Central involutions and complementary summands [fgap-000V]

A central element whose square is one produces two complementary idempotents whenever two is invertible. The construction separates a module into the two eigenspaces of that element and separates the algebra itself into two algebra factors. No semisimplicity or representation classification is needed.

The reading order follows the implications \[ \begin {array}{ccccc} z^2=1,\ z\in Z(A)&\longrightarrow &e_+,e_-& \longrightarrow &M=e_+M\oplus e_-M\\ &&\big \downarrow &&\\ &&A\cong e_+A\times e_-A.&& \end {array} \] Centrality is needed for the lower algebra statement. The upper module decomposition is an additive direct sum from the complementary-idempotent equations; centrality makes its summands $A$-submodules.

Definition. central involution in an algebra [fgap-000W]

Let $R$ be a commutative ring, let $A$ be an associative unital $R$-algebra, and suppose $2\cdot 1_R$ is invertible. Write \[ h=(2\cdot 1_R)^{-1}. \] A central involution for this construction is an element $z\in A$ such that \[ z^2=1_A,\qquad za=az\quad \text {for every }a\in A. \] We then define \[ e_+=h(1_A+z),\qquad e_-=h(1_A-z), \] using the structural map $R\to A$ for the scalar $h$.

Only the equation $z^2=1_A$ is used. The element need not have exact order 2: the extra condition $z\neq 1_A$ merely excludes the degenerate case $e_-=0$. The algebra $A$ need not be commutative.

Example. a central group element inside a Group Algebra [fgap-000X]

Let $G$ be a group and let $z_G\in G$ satisfy \[ z_G^2=1_G,\qquad z_Gg=gz_G\quad \text {for every }g\in G. \] In the Group Algebra $R[G]$, write $[z_G]$ for the basis element indexed by $z_G$. Then \[ [z_G]^2=[1_G]=1_{R[G]}, \] and $[z_G]$ commutes with every basis element $[g]$. By linearity it is a central involution in the algebra. The Group Algebra and the passage from group representations to its modules are developed in [sengupta2010representations, secs. 3.1--3.3, pp. 39--42]; compare [webb2007finite, pp. 1--4].

The brackets matter. Assume $R$ is nontrivial. Then $[z_G]\neq -1_{R[G]}$: their supports differ when $z_G\neq 1_G$; when $z_G=1_G$, this is $1_{R[G]}\neq -1_{R[G]}$, since 2 is invertible.

Lemma. the two idempotents of a central involution [fgap-000Y]

For the elements $e_+$ and $e_-$ associated with a central involution, \[ e_+^2=e_+,\qquad e_-^2=e_-,\qquad e_+e_-=e_-e_+=0,\qquad e_++e_-=1_A. \] Both idempotents are central.

Proof.

First, \[ e_++e_-=h(1+z)+h(1-z)=2h=1_A, \] so $e_-=1_A-e_+$. Since $2h=1_R$ and $z^2=1_A$, \[ e_+^2 =h^2(1+2z+z^2) =2h^2(1+z) =e_+. \] The remaining identities now follow from this one idempotence calculation: \[ \begin {aligned} e_-^2&=(1_A-e_+)^2=1_A-e_+=e_-,\\ e_+e_-&=e_+(1_A-e_+)=0,\\ e_-e_+&=(1_A-e_+)e_+=0. \end {aligned} \] Finally, each $e_\pm $ is a scalar linear combination of the central elements $1_A$ and $z$, so it is central.

These equations are the elementary two-idempotent instance of the projection calculus discussed in [sengupta2010representations, sec. 4.5, pp. 63--68].

Example. the central split of the real Group Algebra of 2T [fgap-0015]

Let $B$ be the abstract binary tetrahedral group, let $z\in B$ be its distinguished central involution, and put \[ A=\mathbb {R}[B]. \] The group element $z$, its basis image $[z]\in A$, and the scalar $-1_A$ are different kinds of objects. The image $[z]$ is central in $A$ and satisfies $[z]^2=1_A$, by a central group element inside a Group Algebra.

The two elements \[ e_+=\frac {1_A+[z]}2,\qquad e_-=\frac {1_A-[z]}2 \] therefore satisfy \[ e_+^2=e_+,\qquad e_-^2=e_-,\qquad e_+e_-=e_-e_+=0,\qquad e_++e_-=1_A. \] They are central by the two idempotents of a central involution. Hence left multiplication by $e_+$ and $e_-$ gives two complementary projections on the regular $A$-module. This specializes the generic central-involution split to $\mathbb {R}[B]$; no representation-theoretic classification is used.

The Group Algebra convention is developed in [sengupta2010representations, secs. 3.1--3.3, pp. 39--42]. The projection interpretation of complementary idempotents is compared with [webb2007finite, exercise 2.7, p. 15].

Theorem. the eigenspace decomposition of a module [fgap-000Z]

Let $z$ be a central involution in $A$, let $e_+,e_-$ be its associated idempotents, and let $M$ be a left $A$-module. Left multiplication defines $A$-linear projections \[ p_\pm :M\longrightarrow M,\qquad p_\pm (m)=e_\pm m. \] They satisfy \[ p_\pm ^2=p_\pm ,\qquad p_++p_-=\mathrm {id}_M,\qquad p_+p_-=p_-p_+=0. \] Their ranges and kernels are \[ \begin {aligned} \operatorname {range}(p_+)&=e_+M,& \ker (p_+)&=\operatorname {range}(p_-)=e_-M,\\ \operatorname {range}(p_-)&=e_-M,& \ker (p_-)&=\operatorname {range}(p_+)=e_+M. \end {aligned} \] Consequently, if \[ M_+=e_+M,\qquad M_-=e_-M, \] then \[ M=M_+\oplus M_-. \] These summands are precisely the two eigenspaces for the action of $z$: \[ M_+=\{m\in M:zm=m\},\qquad M_-=\{m\in M:zm=-m\}. \]

Proof.

The idempotent and mixed-product identities from the two idempotents of a central involution give the displayed projection identities after acting on $M$. Centrality of $e_\pm $ makes $p_\pm $ $A$-linear. Their ranges are $e_\pm M$ by definition. If $p_+(m)=0$, then \[ m=(p_++p_-)(m)=p_-(m), \] so $m$ lies in the range of $p_-$. Conversely, $p_+p_-=0$ shows that every element in that range lies in $\ker (p_+)$. This proves the first kernel-range equality; the second is symmetric. The identity $p_++p_-=\mathrm {id}_M$ now gives the displayed direct sum.

Direct calculation gives $ze_+=e_+$ and $ze_-=-e_-$, proving one eigenspace inclusion in each case. Conversely, if $zm=m$, then \[ e_+m=h(m+zm)=2hm=m. \] If $zm=-m$, the analogous calculation gives $e_-m=m$.

Idempotents as projections and complementary orthogonal idempotents as direct decompositions are recorded in [webb2007finite, exercise 2.7, p. 15]; see also [sengupta2010representations, props. 4.5.1--4.5.3, pp. 63--67].

Theorem. the central-idempotent algebra product [fgap-0010]

For a central involution $z$ and its associated idempotents, put \[ A_+=e_+A,\qquad A_-=e_-A. \] Because $e_+$ and $e_-$ are central, these are two-sided ideals and $e_\pm A=Ae_\pm $. Each is a unital $R$-algebra in its own right, with unit $e_\pm $ and structural map $r\mapsto re_\pm $. There is an $R$-algebra isomorphism \[ \begin {aligned} \Phi :A&\longrightarrow A_+\times A_-, &a&\longmapsto (e_+a,e_-a),\\ \Psi :A_+\times A_-&\longrightarrow A, &(x,y)&\longmapsto x+y. \end {aligned} \]

Proof.

For $a,b\in A$, $a(e_\pm b)=e_\pm (ab)$ and $(e_\pm b)a=e_\pm (ba)$, so $A_\pm $ are two-sided ideals. If $x=e_+a\in A_+$, then $e_+x=x$; thus $e_+$ is the unit of $A_+$, and similarly for $A_-$.

Mixed products vanish: \[ (e_+a)(e_-b)=e_+e_-ab=0, \] and likewise in the reverse order. It follows that $\Phi $ and $\Psi $ preserve multiplication. Finally, \[ \Psi \Phi (a)=(e_++e_-)a=a, \] while $\Phi \Psi (x,y)=(x,y)$ because the matching idempotent fixes each factor and the other annihilates it.

The use of local units on idempotent-generated ideals follows the standard discussion in [sengupta2010representations, secs. 4.5--4.6, pp. 63--73].

Example. splitting the Group Algebra of C₂ [fgap-0011]

Let $C_2=\{1,s\}$ with $s^2=1$, and suppose 2 is invertible in the nonzero commutative ring $R$. The basis element $[s]$ is central, and \[ e_+=\frac {[1]+[s]}2,\qquad e_-=\frac {[1]-[s]}2. \] The algebra-product theorem becomes \[ R[C_2]\cong R\times R. \]

The isomorphism and its inverse are explicit: \[ \begin {aligned} a[1]+b[s]&\longmapsto (a+b,a-b),\\ (x,y)&\longmapsto \frac {x+y}{2}[1]+\frac {x-y}{2}[s]. \end {aligned} \] Under this map, $e_+$ goes to $(1,0)$ and $e_-$ goes to $(0,1)$. Thus the two idempotents are the coordinate projections, not merely a dimension count.

Remark. three levels of splitting [fgap-0012]

The same formulas support three conclusions, but their structures should not be conflated: \[ \begin {array}{c|c|c} \text {level}&\text {conclusion}&\text {input}\\ \hline \text {additive}&M=e_+M\oplus e_-M& e_++e_-=1,\ e_+e_-=e_-e_+=0\\ \text {module}&M_\pm \text { are eigensubmodules}& \text {central action of }z\\ \text {algebra}&A\cong e_+A\times e_-A& e_+,e_-\text { central}. \end {array} \]

For an arbitrary idempotent $e\in A$, left multiplication by $e$ and $1-e$ gives a split of the underlying $R$-module, \[ A=eA\oplus (1-e)A, \] and therefore also of the underlying additive group. Without centrality, these projections need not be homomorphisms of the left regular $A$-module: $eA$ and $(1-e)A$ are right ideals, but need not be left ideals or two-sided ideals. The two summands therefore need not be algebra factors. The product theorem is stronger than this $R$-module direct-sum statement.

Remark. mathematical summands and physical readings [fgap-0013]

A central involution canonically separates the algebra and its modules into two mathematical summands. This alone does not identify either summand with particles, interactions, chirality, or any other physical sector. Such an interpretation requires additional data: a representation, selected observables or forms, dynamics, and a map from the mathematics to measurable quantities.

The split is useful precisely because it can be calculated before those choices are made. Later notes may test proposed physical correspondences against it, but the algebra decomposition remains valid independently of whether any such proposal succeeds.

Real blocks of the quaternion Group Algebra [fgap-001C]

July 30, 2026
Utensil Song

The preceding central-involution construction isolates algebra factors without classifying all representations. For the quaternion group, the following direct coefficient calculation goes further and makes every real block explicit.

proposition. the real Group Algebra of the quaternion group [fgap-001B]

Let $Q_8=\{\pm 1,\pm i,\pm j,\pm k\}$ be the concrete quaternion group from the quaternion group inside Hamilton's Quaternions, and put \[ \mathcal {E}=\{-1,1\}\subset \mathbb {R}^{\times }, \qquad \mathcal {X}=\mathcal {E}\times \mathcal {E}. \] For $(\epsilon ,\delta )\in \mathcal {X}$, there is a real character \[ \chi _{\epsilon ,\delta }:Q_8\longrightarrow \mathbb {R}^{\times } \] determined by \[ \chi _{\epsilon ,\delta }(-1)=1,\qquad \chi _{\epsilon ,\delta }(i)=\epsilon ,\qquad \chi _{\epsilon ,\delta }(j)=\delta ,\qquad \chi _{\epsilon ,\delta }(k)=\epsilon \delta . \] These are the four characters pulled back from $Q_8/\{\pm 1\}\cong C_2\times C_2$; compare [etingof2024introduction, sec. 4.3, pp. 63--64 and ex. 4.8.1, p. 73].

Write $\mathbb {R}^{\mathcal {X}}$ for the algebra of functions $\mathcal {X}\to \mathbb {R}$, with pointwise operations. Extending the four characters and the inclusion $Q_8\subset \mathbb {H}^{\times }$ linearly gives an algebra homomorphism \[ \Phi :\mathbb {R}[Q_8]\longrightarrow \mathbb {R}^{\mathcal {X}}\times \mathbb {H}. \] Then $\Phi $ is an isomorphism of real algebras. The displayed map retains the chosen character index and quaternionic realization as part of its data.

Proof.

Let $u_q$ be the Group-Algebra basis element indexed by $q\in Q_8$.

Write a general element in the form \[ x=\sum _{q\in Q_8}a_qu_q. \] For $q\in \{1,i,j,k\}$, set \[ s_q=a_q+a_{-q},\qquad d_q=a_q-a_{-q}. \] The quaternion coordinate of $\Phi (x)$ is \[ d_1+d_i i+d_j j+d_k k. \] It therefore recovers the four differences $d_q$.

The coordinate indexed by $(\epsilon ,\delta )\in \mathcal {X}$ is \[ y_{\epsilon ,\delta } =s_1+\epsilon s_i+\delta s_j+\epsilon \delta s_k. \] The inverse Hadamard calculation gives \[ \begin {aligned} s_1&=\frac 14\sum _{(\epsilon ,\delta )\in \mathcal {X}}y_{\epsilon ,\delta },& s_i&=\frac 14\sum _{(\epsilon ,\delta )\in \mathcal {X}} \epsilon y_{\epsilon ,\delta },\\ s_j&=\frac 14\sum _{(\epsilon ,\delta )\in \mathcal {X}} \delta y_{\epsilon ,\delta },& s_k&=\frac 14\sum _{(\epsilon ,\delta )\in \mathcal {X}}\epsilon \delta y_{\epsilon ,\delta }. \end {aligned} \] Thus the four real coordinates recover the four sums $s_q$. Finally, \[ a_q=\frac {s_q+d_q}{2},\qquad a_{-q}=\frac {s_q-d_q}{2}, \] so $\Phi (x)$ recovers all eight coefficients of $x$. Hence $\Phi $ is injective. Its domain and codomain both have real dimension 8, so it is bijective.

The quaternion coordinate alone is surjective, because its basis values include $1,i,j,k$. It vanishes exactly when $d_1=d_i=d_j=d_k=0$, or equivalently when $a_q=a_{-q}$ for $q\in \{1,i,j,k\}$. Its kernel is therefore the 4-dimensional span of \[ u_1+u_{-1},\quad u_i+u_{-i},\quad u_j+u_{-j},\quad u_k+u_{-k}. \] It therefore induces \[ \mathbb {R}[Q_8]/\ker (\Phi _{\mathbb {H}}) \cong _{\mathbb {R}\text {-alg}}\mathbb {H}. \] This quotient depends on the chosen quaternionic realization. The combined map $\Phi $ is what exhibits the selected quotient as the quaternion factor of the displayed product; a quotient map by itself does not supply that direct-factor statement.

The quaternion model is grounded in [voight2021quaternion, sec. 11.2, p. 166]. The extension of group representations to Group-Algebra maps follows [sengupta2010representations, secs. 3.1--3.2, pp. 39--41]. The coefficient recovery above is direct and does not assume a general classification theorem. No physical meaning is assigned to a factor merely from its dimension or familiar algebra.

Appendix [fgap-001A]

with contributions from Utensil Song

The appendix first supplies the general Group-Algebra route behind the finite examples. It then records exploratory structures that are not needed for the quaternionic and Group-Algebra spine.

The human-curated Group-Algebra route [fgap-001G]
📄PDF

August 12, 2026
Utensil Song

A finite group becomes linear once its elements are used as a basis. This route starts with that construction, passes through modules, semisimple blocks, and characters, and then follows normal subgroups, computation, and twisted multiplication. The explicit quaternion calculations earlier in these notes are test cases for this general route, not substitutes for it.

Definition. the Group Algebra and its universal extension [fgap-001H]

MonoidAlgebra.lift MonoidAlgebra.lift_single
L∃∀N

Let $k$ be a commutative ring and $G$ a group. The Group Algebra $k[G]$ is the free $k$-module with basis $[g]$ indexed by $g\in G$, equipped with \[ [g][h]=[gh],\qquad 1=[1_G],\qquad (\sum _g a_g[g])(\sum _h b_h[h])=\sum _{g,h}a_gb_h[gh]. \] The scalar embedding sends $a$ to $a[1_G]$. Thus each group element is a unit of $k[G]$, with inverse $[g^{-1}]$.

If $A$ is a $k$-algebra and $u:G\to A^\times $ is a group homomorphism, there is a unique $k$-algebra homomorphism \[ \widetilde u:k[G]\longrightarrow A, \qquad \widetilde u\left (\sum _g a_g[g]\right )=\sum _g a_g u(g). \] This universal property extends representations and concrete group maps from basis elements to the whole Group Algebra. See [sengupta2010representations, secs. 3.1--3.2, pp. 39--41].

Theorem. representations are Group-Algebra modules [fgap-001I]

Representation.asModule Representation.ofModule Rep.equivalenceModuleMonoidAlgebra
L∃∀N

Let $k$ be a field, $G$ a group, and $V$ a $k$-vector space. Giving a linear representation $\rho :G\to \operatorname {GL}_k(V)$ is equivalent to giving a unital left $k[G]$-module structure on $V$, up to the identity type synonyms used to keep the 2 scalar actions distinct. The action associated to $\rho $ is \[ (\sum _g a_g[g])\cdot v=\sum _g a_g\rho (g)v. \] Conversely, restriction of a unital $k[G]$-action to the units $[g]$ recovers $\rho $. Invariant subspaces are submodules and intertwining linear maps are $k[G]$-linear maps.

Proof.

The extension in the Group Algebra and its universal extension supplies the algebra homomorphism $k[G]\to \operatorname {End}_k(V)$. Associativity and the unit law give a module. In the other direction, multiplication by each $[g]$ is invertible, and the module law gives the group law. These operations are inverse. See [sengupta2010representations, sec. 3.2, pp. 40--41].

Example. the regular representation reads the basis [fgap-001J]

Let $G$ act on $k[G]$ by left multiplication. In the basis $\{[h]:h\in G\}$, an element $g$ sends $[h]$ to $[gh]$; hence its matrix is the permutation matrix of left translation. This is the left regular representation. It is faithful because the image of $[1_G]$ records $g$.

The same basis underlies the coefficient calculations in the real Group Algebra of the quaternion group: there, the quaternion coordinate recovers antisymmetric coefficient pairs and the character coordinates recover symmetric pairs. The regular module is the linear carrier for both the abstract Group Algebra and the explicit 8-coordinate computation. Compare [james2001representations, ch. 6, pp. 53--58].

Theorem. Maschke averaging [fgap-001K]

MonoidAlgebra.Submodule.exists_isCompl
L∃∀N

Let $G$ be finite and $k$ a field in which $|G|$ is invertible. Every subrepresentation $W\subseteq V$ has a $G$-stable complement. Consequently every finite-dimensional $k[G]$-module, and $k[G]$ itself, is semisimple.

Proof.

Choose a $k$-linear projection $P:V\to W$ and average its conjugates: \[ P_G=\frac 1{|G|}\sum _{g\in G}\rho (g)P\rho (g)^{-1}. \] Then $P_G$ remains the identity on $W$ and commutes with $G$. Its kernel is a $G$-stable complement. Division by $|G|$ requires the stated invertibility hypothesis. This is Maschke's theorem as proved in [sengupta2010representations, thm. 3.5.1, pp. 44--46].

Theorem. Wedderburn blocks over an algebraically closed field [fgap-001L]

exists_algEquiv_pi_matrix_conjClasses
L∃∀N

Let $G$ be finite and $k$ an algebraically closed field whose characteristic does not divide $|G|$. There are positive integers $d_C$, indexed by the conjugacy classes $C$ of $G$, such that \[ k[G]\cong _{k\text {-alg}} \prod _{C\in \operatorname {Conj}(G)}M_{d_C}(k), \qquad \sum _C d_C^2=|G|. \] The class labels are an indexing choice: the statement does not canonically pair a particular conjugacy class with a particular irreducible module.

Maschke semisimplicity followed by Artin--Wedderburn gives the stated product. Lux and Pahlings state the results in [lux2010representations, thms. 1.5.5--1.5.6, pp. 56--57].

The dimension identity can also be read from the regular representation, where an irreducible module occurs with multiplicity equal to its dimension; compare [james2001representations, thms. 11.9 and 11.12, pp. 100--101].

Definition. characters, class functions, and the character table [fgap-001M]

basisOfIrreducibleCharacters characterTable card_inv_mul_sum_characterTable_mul_characterTable_inv card_conjClass_mul_sum_characterTable_mul_characterTable_inv
L∃∀N

For a finite-dimensional representation $\rho $ over a characteristic-zero field, its character is $\chi _\rho (g)=\operatorname {tr}(\rho (g))$. Trace is unchanged by conjugation, so $\chi _\rho $ is a class function. A character table places the irreducible characters in rows and the conjugacy classes in columns. Tau Ceti identifies class functions with functions on conjugacy classes in TauCeti.ClassFunction.equivConjClasses.

Over $\mathbb C$, the irreducible characters form an orthonormal basis of the class functions. Thus the table is square: the number of irreducible characters equals the number of conjugacy classes. This also counts the Wedderburn blocks and gives the dimension of the center. See [james2001representations, thm. 16.4, pp. 159--166].

Theorem. primitive central idempotents as block projectors [fgap-001N]

primitiveCentralIdempotent asAlgebraHom_primitiveCentralIdempotent primitiveCentralIdempotent_mul_primitiveCentralIdempotent
L∃∀N

Over a splitting field of characteristic not dividing $|G|$, an irreducible character $\chi $ defines the central element \[ e_\chi =\frac {\chi (1)}{|G|}\sum _{g\in G}\chi (g^{-1})[g]. \] It is a nonzero primitive central idempotent. On a simple module with character $\psi $, it acts as the identity if $\psi =\chi $ and as zero otherwise. Distinct $e_\chi $ are therefore orthogonal block projectors. See [lux2010representations, thm. 2.1.6 and cor. 2.1.7, pp. 88--90]. A constructed family of such projectors does not yield a complete block decomposition until a sum-to-1 statement is also known.

Theorem. the Frobenius--Schur trichotomy [fgap-0021]

frobeniusSchurIndicator_eq_one_or_eq_zero_or_eq_neg_one frobeniusSchurIndicator_eq_one_iff frobeniusSchurIndicator_eq_neg_one_iff frobeniusSchurIndicator_eq_zero_iff
L∃∀N

Let $\rho $ be an irreducible finite-dimensional representation of a finite group over an algebraically closed field of characteristic 0. Its Frobenius--Schur indicator \[ \nu _2(\rho )=\frac 1{|G|}\sum _{g\in G}\chi _\rho (g^2) \] takes exactly 1 of the values $1$, $0$, and $-1$. The value $1$ is equivalent to the existence of a nondegenerate invariant symmetric bilinear form; $-1$ is equivalent to a nondegenerate invariant alternating form; and $0$ is equivalent to the absence of a nonzero invariant bilinear form. See [james2001representations, def. 23.13, the proof of thm. 23.14, and thm. 23.16, pp. 273--277]. James and Liebeck state the alternatives using nonzero invariant forms; for an irreducible representation, a nonzero invariant symmetric or alternating form has zero radical and is therefore nondegenerate.

This trichotomy classifies the invariant-form behavior of the complex irreducible representation. It does not by itself compute a Schur index or a complete decomposition after descent to $\mathbb R$.

Remark. real types are not Schur indices [fgap-001Y]

Over $\mathbb R$, a simple finite-dimensional block may instead have division algebra $\mathbb R$, $\mathbb C$, or $\mathbb H$. The Frobenius--Schur trichotomy in the Frobenius--Schur trichotomy detects invariant-form type, but it is not a complete theorem about a character's field of values or Schur index. The explicit decomposition \[ \mathbb R[Q_8]\cong \mathbb R^4\times \mathbb H \] in the real Group Algebra of the quaternion group is a complete real example, not an application of the algebraically closed formula. For Schur indices and invariant forms, see [lux2010representations, sec. 2.9, pp. 164--172].

Definition. conjugate constituents and the inertia subgroup [fgap-001O]

Let $N\trianglelefteq G$, let $V$ be a $G$-representation, and let $W\subseteq V|_N$ be an irreducible $N$-subrepresentation. For $g\in G$, the conjugate representation $,{}^gW$ has the same vector space and action \[ n\cdot _g w=(g^{-1}ng)\cdot w. \] The inertia subgroup of $W$ is \[ I_G(W)=\{g\in G:{}^gW\cong W\}. \] The isomorphism classes of conjugates form a $G$-orbit, with stabilizer $I_G(W)$. See [lux2010representations, sec. 3.6, pp. 222--225].

Theorem. the single orbit in Clifford restriction [fgap-001P]

isSemisimpleRepresentation_comp_subtype exists_isAtom_forall_nonempty_linearEquiv_conjSubrep
L∃∀N

Let $N\trianglelefteq G$ be finite, and work over a field for which the relevant finite-group modules are semisimple. If $V$ is an irreducible $G$-representation, then the irreducible constituents of $V|_N$ lie in 1 $G$-orbit under conjugation. Equivalently, after choosing 1 constituent $W$, every other constituent is isomorphic to some $,{}^gW$.

This is the orbit assertion in Clifford theory. It does not by itself say that all constituents occur with the same multiplicity, nor does it construct extensions across the inertia subgroup. Compare [lux2010representations, thm. 3.6.2(a), pp. 223--225].

Theorem. Clifford homogeneity and the semidirect route [fgap-001Q]

Let $N\trianglelefteq G$ and let $V$ be an irreducible complex representation of $G$. If $W_1,\ldots ,W_r$ represent the distinct conjugates of an irreducible constituent of $V|_N$, then for 1 positive integer $e$, \[ V|_N\cong e(W_1\oplus \cdots \oplus W_r). \] Thus restriction is homogeneous along a single orbit. The common multiplicity is an additional assertion beyond the single orbit in Clifford restriction. This is Clifford's theorem, [james2001representations, thm. 20.8, pp. 216--217].

The inertia subgroup is the intermediate group where one studies whether $W$ extends, possibly projectively, before inducing to $G$. For semidirect products, this reduces the problem to the action of the complement. For $Q_8\rtimes C_3\cong 2T$, it connects the normal quaternion subgroup to the skew-Group-Algebra model in two routes from binary tetrahedral symmetry. This theorem does not supply the full character table of $2T$.

Example. semidirect products make Clifford theory concrete [fgap-0020]

Suppose $G=N\rtimes H$. Conjugation by $H$ permutes the irreducible constituents of $V|_N$. Their stabilizers are the inertia subgroups, so the orbit and homogeneity statements in the single orbit in Clifford restriction and Clifford homogeneity and the semidirect route reduce the search for irreducible $G$-representations to stabilizer data, projective extension, and induction. Clifford theory thereby gives a character-theoretic route for semidirect products.

For $Q_8\rtimes C_3\cong 2T$, the action and ordinary skew-Group-Algebra realization are recorded in the central split of the real Group Algebra of 2T and two routes from binary tetrahedral symmetry. They supply the normal-subgroup and algebraic input to this route, but do not give the full character table of $2T$.

Remark. from a presentation to checked representation data [fgap-001R]

A finite presentation $\langle x_1,\ldots ,x_m\mid r_1,\ldots ,r_s\rangle $ gives a compact input for algorithms that enumerate cosets, compute conjugacy classes, and build character data. Sims develops the algorithms and the conditions under which such computations terminate; Lux and Pahlings place them inside computational representation theory.

The output has 3 possible evidential strengths. A transcript with versioned inputs is reproducible. A compact certificate, such as matrices satisfying the relations together with independently checked completeness identities, can be verified without trusting the search. An unrecorded software answer is neither. GAP is therefore a discovery and calculation tool; its output becomes mathematics here only when the decisive relations and completeness checks are visible. See [sims1994computation, ch. 1] and [lux2010representations, secs. 1.1 and 4.2].

The route is \[ \begin {aligned} \text {finite presentation}&\longrightarrow \text {computed candidates}\\ &\longrightarrow \text {checked relations and completeness}. \end {aligned} \] The arrows distinguish generation from certification rather than describing a project workflow.

Definition. factor sets and twisted Group Algebras [fgap-001S]

of_mul_of lift isProjectiveRepEquivAlgHom
L∃∀N

Let $k$ be a field, $G$ a group, and $\alpha :G\times G\to k^\times $ a normalized 2-cocycle: \[ \alpha (1,g)=\alpha (g,1)=1, \qquad \alpha (g,h)\alpha (gh,\ell )= \alpha (h,\ell )\alpha (g,h\ell ). \] The twisted Group Algebra $k_\alpha [G]$ has basis $u_g$ and multiplication \[ u_gu_h=\alpha (g,h)u_{gh}. \] The cocycle equation is exactly the associativity condition.

A projective representation with factor set $\alpha $, namely operators $T_g$ satisfying $T_gT_h=\alpha (g,h)T_{gh}$, extends uniquely to an algebra map $k_\alpha [G]\to \operatorname {End}_k(V)$; conversely an algebra map gives such a projective representation on its basis operators. Cohomologous cocycles rescale the basis and give isomorphic twisted algebras. See [conlon1964twisted, the introduction and sec. 1, pp. 152--155].

Remark. the qualified Clifford bridge [fgap-001Z]

A generalized Clifford algebra becomes a twisted group algebra only after its parameters are fixed. Let $k$ contain a primitive $n$-th root of unity $\omega $, assume $\operatorname {char}k\nmid n$, and choose $q_1,\ldots ,q_m\in k^\times $. The algebra generated by $e_1,\ldots ,e_m$ with \[ e_i^n=q_i, \qquad e_i e_j=\omega e_j e_i\quad (j<i) \] is isomorphic to a twisted group algebra of $(\mathbb Z/n\mathbb Z)^m$ for an explicit 2-cocycle. The monomials in the $e_i$ correspond to its twisted basis. See [cheng2019new, sec. 2.3 and prop. 2.1, pp. 3--4].

This is a qualified bridge, not an identification of every Clifford algebra with an ordinary Group Algebra. The field, root of unity, grading, parameters, and twisting are part of the theorem. It is also different from Clifford theory in the single orbit in Clifford restriction and Clifford homogeneity and the semidirect route, which concerns restriction of representations to normal subgroups.

Remark. the inertia obstruction is projective [fgap-001T]

For a constituent $W$ with inertia subgroup $I=I_G(W)$, choose intertwiners $T_i:W\to {}^iW$. Their composites need not satisfy the group law strictly. Instead one obtains scalars \[ T_iT_j=\alpha (i,j)T_{ij}. \] Associativity makes $\alpha $ a factor set. Changing the intertwiners changes $\alpha $ by a coboundary. The resulting cohomology class measures the obstruction to replacing the projective action by an ordinary action.

Twisted Group Algebras therefore enter the Clifford-theory route. The ordinary skew Group Algebra in two routes from binary tetrahedral symmetry corresponds to trivial twisting; it should not be identified with a general $k_\alpha [G]$. The extension and induction analysis is developed in [lux2010representations, secs. 3.6--3.7, pp. 222--240].

proposition. the canonical grading of a Group Algebra [fgap-001U]

AddMonoidAlgebra.grade.isInternal AddMonoidAlgebra.grade.gradedAlgebra AddMonoidAlgebra.single_mem_grade
L∃∀N

For each $g\in G$, let $A_g=k[g]$ be the 1-dimensional subspace spanned by the basis element $[g]$. Then \[ k[G]=\bigoplus _{g\in G}A_g, \qquad A_gA_h\subseteq A_{gh}. \] Thus $k[G]$ is canonically graded by the group $G$. In Lean's additive graded-algebra interface this statement is expressed after passing from the multiplicative index $G$ to its additive copy; each single basis element lies in its corresponding grade.

The basis and multiplication law in the Group Algebra and its universal extension give the decomposition and product containment directly; compare the construction in [sengupta2010representations, secs. 3.1--3.2, pp. 39--41]. It is distinct from the Hopf structure in the standard Hopf structure on a Group Algebra: the grading records where products land, while the coalgebra maps record how a basis element is copied and inverted.

proposition. the standard Hopf structure on a Group Algebra [fgap-001V]

MonoidAlgebra.instHopfAlgebra MonoidAlgebra.counit_single MonoidAlgebra.comul_single MonoidAlgebra.antipode_single
L∃∀N

Let $k$ be a commutative ring and $G$ a group. The Group Algebra $k[G]$ is a Hopf algebra with structure determined on basis elements by \[ \Delta ([g])=[g]\otimes [g],\qquad \epsilon ([g])=1,\qquad S([g])=[g^{-1}]. \] The comultiplication and counit are algebra homomorphisms; the antipode extends inversion and satisfies the 2 convolution identities.

Proof.

Each formula respects multiplication on basis elements. For example, $\Delta ([gh])=[gh]\otimes [gh]=([g]\otimes [g])([h]\otimes [h])$. The counit calculation is similar. Finally $[g][g^{-1}]=[1]=[g^{-1}][g]$, which gives both antipode identities on the basis and hence by linearity on all of $k[G]$. This group-algebra Hopf structure appears, for example, in [broue2024rings, ex. 18.3.3(1), pp. 500--501].

Remark. what the real quaternion example settles [fgap-001W]

The general route has several distinct endpoints. Over an algebraically closed field, Wedderburn blocks and the character table organize all simple representations. Over $\mathbb R$, division-algebra type and descent data enter. For a normal subgroup, Clifford theory organizes restriction and induction. With a nontrivial factor set, projective representations are modules over a twisted algebra.

The quaternion calculation in the real Group Algebra of the quaternion group closes 1 bounded endpoint: it gives an explicit real-algebra equivalence $\mathbb R[Q_8]\cong \mathbb R^4\times \mathbb H$, and Real blocks of the quaternion Group Algebra identifies its center. It does not prove a general real Wedderburn theorem, the characters of $2T$, or the Clifford-theory extension step. Those are separate statements and do not follow from the worked example.

Remark. the Hessian-group outlook [fgap-001X]

Wilson's proposed route begins with \[ Q_8\rtimes C_3\cong 2T \] and then studies the iterated semidirect product $(G_{27}\rtimes Q_8)\rtimes C_3$, with the indicated actions part of the data. Its central scalar subgroup $C_3\leq G_{27}$ has quotient the Hessian group of order 216, so the larger group is a triple cover of that quotient. The name alone would not choose either semidirect action. See [wilson2024discrete, sec. 2.2, pp. 4--5].

The comparison with $U(1)\times SU(2)\times SU(3)$ is an attributed finite-model proposal, not an isomorphism or a canonical physical interpretation. To become a mathematical correspondence it would need typed representations and homomorphisms, the preserved forms or observables, and a rule connecting them to physical data. Hamilton's geometric-algebra models in [hamilton2023supergeometric] and [hamilton2023unification] provide a comparison motivation, not independent confirmation of this finite-group construction.

Finite tests for a topos layer [fgap-000M]

Group Actions, Group Algebras, and action groupoids already describe much of the finite symmetry data needed in these notes. The question here is narrower: does passing to a topos add universal classification, a common inverse-image language, or internal reasoning that is not already present below the topos level?

Five finite tests give a guarded answer. Ordinary actions and action groupoids do not need topoi. Torsor classification, inverse-image constructions, and internal inhabitation do add something, but only when their extra structure is actually used. Questions about local and global symmetry motivate these tests; they do not decide them.

Example. the real Group Algebra of a cyclic group of order three [fgap-000N]

Let $C_3=\langle g\mid g^3=1\rangle $. Sending $g$ to $x$ gives \[ \mathbb {R}[C_3]\cong \mathbb {R}[x]/(x^3-1). \] Over the real numbers, \[ x^3-1=(x-1)(x^2+x+1), \] and the two factors are coprime. The Chinese remainder theorem and the identification $\mathbb {R}[x]/(x^2+x+1)\cong \mathbb {C}$ therefore give \[ \mathbb {R}[C_3]\cong \mathbb {R}\times \mathbb {C}. \]

More concretely, if $\zeta $ is a primitive complex cube root of unity, the isomorphism is \[ a+bg+cg^2\longmapsto \bigl (a+b+c,\ a+b\zeta +c\zeta ^2\bigr ). \] The two factors can be read in three compatible ways: \[ \begin {array}{c|c|c} \text {factor of }x^3-1& \text {real algebra block}& \text {real representation}\\ \hline x-1&\mathbb {R}&\text {trivial line}\\ x^2+x+1&\mathbb {C}&\text {rotation plane}. \end {array} \] The rotation plane is the linearization of the nontrivial part of the regular Group Action. More explicitly, the generator cyclically permutes the basis $1,g,g^2$. The averaging element \[ e_0=\frac {1+g+g^2}{3} \] projects onto the fixed line $\mathbb {R}(1+g+g^2)$, while its complementary kernel is the augmentation plane \[ \{a+bg+cg^2:a+b+c=0\}. \] Orbits, freeness, and transitivity belong to the action; the projector and invariant subspaces appear only after linearization.

Since the spectrum of a product is the disjoint union of the spectra, \[ \operatorname {Spec}\mathbb {R}[C_3] \cong \operatorname {Spec}\mathbb {R} \sqcup \operatorname {Spec}\mathbb {C}. \] This is a useful commutative picture. It is not yet a reason to introduce a topos, and it does not extend without choices to noncommutative Group Algebras.

Remark. the center is a commutative shadow [fgap-000O]

The quaternion group $Q_8$ has a real Group Algebra decomposition \[ \mathbb {R}[Q_8]\cong \mathbb {R}^4\times \mathbb {H}. \] This can be seen directly from the concrete copy $Q_8\subset \mathbb {H}^{\times }$ in the quaternion group inside Hamilton's Quaternions, rather than assumed from a classification theorem.

Let $u_q$ denote the basis element of the Group Algebra indexed by $q\in Q_8$, and write a general element as $x=\sum _{q\in Q_8}a_qu_q$. The four characters of $Q_8/\{\pm 1\}\cong C_2\times C_2$ and the quaternionic map $u_q\mapsto q$ combine to an algebra homomorphism \[ \Phi :\mathbb {R}[Q_8]\longrightarrow \mathbb {R}^4\times \mathbb {H}. \] For $q\in \{1,i,j,k\}$, put $s_q=a_q+a_{-q}$ and $d_q=a_q-a_{-q}$. The quaternion coordinate of $\Phi $ recovers \[ d_1+d_i i+d_j j+d_k k. \] The four real coordinates recover the Hadamard transform \[ s_1+\epsilon s_i+\delta s_j+\epsilon \delta s_k, \qquad \epsilon ,\delta \in \{\pm 1\}. \] The Hadamard matrix is invertible, so these four values recover every $s_q$. Together with the four differences, they recover every coefficient. Thus $\Phi $ has zero kernel. Both sides have real dimension 8, so $\Phi $ is an isomorphism. The quaternionic realization and multiplication used here are developed in Hamilton's Quaternions and [voight2021quaternion, sec. 11.2, p. 166].

Taking centers now gives \[ Z\bigl (\mathbb {R}[Q_8]\bigr ) \cong Z\bigl (\mathbb {R}^4\times \mathbb {H}\bigr ) \cong \mathbb {R}^5. \] The comparison is: \[ \begin {array}{c|c|c} \text {object}&\text {retained data}&\text {forgotten data}\\ \hline \mathbb {R}[Q_8]&4\mathbb {R}\text { and }\mathbb {H}&\text {none here}\\ Z(\mathbb {R}[Q_8])&\text {five central factors}& \mathbb {H}\text { and block size or type}. \end {array} \] For a real-centered simple block, the center alone cannot distinguish matrix size or real from quaternionic type. A complex block still has complex center. Hence $\operatorname {Spec}Z(\mathbb {R}[Q_8])$ is a selected commutative shadow, not a lossless localization of the noncommutative algebra.

Example. isotropy survives the coarse quotient [fgap-000P]

Let $C_2=\{1,s\}$ act on $X=\{-1,0,1\}$ by $s\mathbin {\cdot }x=-x$. The action groupoid $C_2\ltimes X$ has the points of $X$ as objects and an arrow $(h,x):x\to h\mathbin {\cdot }x$ for every $h\in C_2$. Omitting identity arrows, its shape is

$\text{[math]}$ Thus \[ \operatorname {Aut}(0)\cong C_2,\qquad \operatorname {Aut}(1)=\operatorname {Aut}(-1)=1. \]

The coarse quotient remembers only the two orbits:

$\text{[math]}$ It has forgotten the nonidentity automorphism at $0$. By contrast, the action groupoid has one component equivalent to the terminal groupoid and one component equivalent to $BC_2$. Therefore \[ \mathsf {Set}^{(C_2\ltimes X)^{\mathrm {op}}} \simeq \mathsf {Set}\times \mathsf {B}C_2, \] while sheaves on the discrete coarse quotient form $\mathsf {Set}\times \mathsf {Set}$.

The retained information is already the isotropy arrow in the action groupoid. Passing to its presheaf category organizes families of such data, but does not create that arrow. This test supports the groupoid bridge and does not, by itself, admit a topos layer.

Definition. torsors and the universal torsor [fgap-000Q]

Let $G$ be a group object in a topos $\mathcal {E}$. A left $G$-object $T$ is a torsor when $T\to 1$ is an epimorphism and \[ (\mu ,\pi _2):G\times T\longrightarrow T\times T, \qquad (g,t)\longmapsto (g\mathbin {\cdot }t,t) \] is an isomorphism. The second condition is the internal form of freeness and transitivity. See [maclane1992sheaves, sec. VIII.2, pp. 429--430].

For an ordinary group $G$, write \[ \mathsf {B}G=\mathsf {Set}^{BG^{\mathrm {op}}} \] for the topos of right $G$-sets, regarded as presheafs on the one-object category $BG$. Its universal torsor $U_G$ has underlying right $G$-set $G$ with regular right multiplication. The constant group object $\underline {G}$, whose right $G$-action is trivial, acts on $U_G$ by left multiplication. This supplies the torsor action; the left and right actions commute.

For $C_2$, the regular left action is a torsor in $\mathsf {Set}$: \[ C_2\times C_2\longrightarrow C_2\times C_2, \qquad (g,h)\longmapsto (gh,h) \] is a bijection. The trivial action on a 2-point set $D$, despite $D\to 1$ being onto, is not a torsor. Its corresponding map sends $(g,d)$ to $(d,d)$, so it is neither injective nor surjective. Inhabitation and cardinality alone do not supply a torsor.

Theorem. the classifying property of BG [fgap-000R]

Let $G$ be a group and $\mathcal {E}$ a topos over $\mathsf {Set}$. There is a natural equivalence \[ \operatorname {Geom}_{/\mathsf {Set}}(\mathcal {E},\mathsf {B}G) \simeq \operatorname {Tor}(\mathcal {E},G) \] between geometric morphisms over $\mathsf {Set}$ to $\mathsf {B}G$ and $G$-torsors in $\mathcal {E}$. Under this equivalence, a geometric morphism \[ f:\mathcal {E}\longrightarrow \mathsf {B}G \] classifies the torsor $f^*U_G$.

This is Theorem VIII.2.7 of [maclane1992sheaves]; its theorem and proof are on printed pp. 431--433.

The two directions are visible in the diagram

$\text{[math]}$ The geometric morphism points toward the classifying topos. Its inverse-image functor carries the universal torsor back to the topos in which the classified torsor lives.

Proof.

Inverse image preserves finite limits and, as a left adjoint, colimits. Every epimorphism in a topos is regular, so inverse image carries the universal torsor equations, including the epimorphic map to $1$, to torsor equations in $\mathcal {E}$. Conversely, the cited theorem constructs a geometric morphism from a torsor and proves that the two constructions are naturally inverse. The complete construction belongs to the classifying theorem; the point used here is its variance and universal property.

For a single finite action, freeness and transitivity can be checked without topoi. The added value here is one universal object classifying torsors in every topos over $\mathsf {Set}$ and carrying them along inverse image.

Convention. geometric morphisms and inverse image [fgap-000S]

For a geometric morphism \[ f:\mathcal {E}\longrightarrow \mathcal {F}, \] we write \[ f^*:\mathcal {F}\longrightarrow \mathcal {E}, \qquad f_*:\mathcal {E}\longrightarrow \mathcal {F}, \qquad f^*\dashv f_*. \] Thus the morphism and its inverse-image functor point in opposite directions. The functor $f^*$ preserves finite limits.

Two examples fix the convention: \[ \begin {array}{c|c|c} \text {input map}&\text {geometric morphism}&\text {inverse image}\\ \hline i:\{x\}\hookrightarrow X& \mathsf {Set}\to \mathsf {Sh}(X)& i^*F=F_x=\displaystyle \varinjlim _{x\in U}F(U)\\[3pt] \varphi :H\to G& \mathsf {B}H\to \mathsf {B}G& \operatorname {Res}^G_H:\mathsf {B}G\to \mathsf {B}H. \end {array} \] In the first row, the stalk is the filtered colimit of all neighborhood sections, not the value on one chosen neighborhood.

Mac Lane and Moerdijk construct inverse-image sheaves through pulled-back étale spaces in [maclane1992sheaves, sec. II.9], especially printed pp. 99--101.

In the second row, right actions are presheaves. Precomposition with $B\varphi ^{\mathrm {op}}$ is restriction of actions. It has both Kan-extension adjoints, so it is the inverse-image part of the displayed geometric morphism. The homomorphism and geometric morphism point from $H$ to $G$; restriction points from $G$-objects to $H$-objects.

Example. internal inhabitation without a global point [fgap-000T]

Work in $\mathsf {B}C_2$, the topos of right $C_2$-sets, and let $U=C_2$ carry the regular right action. The unique equivariant map $U\to 1$ is an epimorphism because its underlying function is surjective. In the internal language, this says that $U$ is inhabited. Internal Group Actions are developed in [maclane1992sheaves, sec. V.2, pp. 237--240].

A global element would be an equivariant map $1\to U$. Its value would have to satisfy $u\mathbin {\cdot }s=u$, but the regular action has no fixed point. Hence \[ \operatorname {Hom}_{\mathsf {B}C_2}(1,U)=\varnothing . \] The two external tests are: \[ \begin {array}{c|c} \text {internal statement}&\text {external test}\\ \hline U\text { is inhabited}&U\to 1\text { is epi}\\ U\text { has a global point}&U^{C_2}\neq \varnothing . \end {array} \]

More generally, for a nontrivial group $G$, the regular right $G$-object $U_G=G$ satisfies \[ U_G\to 1\text { is epi}, \qquad \Gamma (U_G)=U_G^G=\varnothing . \] Indeed, if $xg=x$ for every $g$, cancellation forces every $g$ to be $1$. Internal existence is therefore generalized or local existence; it does not choose a global invariant element. This distinction is not a physical existence claim.

Remark. where the topos layer begins [fgap-000U]

The finite tests separate calculations that merely take place in a topos from calculations that use topos-level structure: \[ \begin {array}{c|c|c|c} \text {test}&\text {lower level}&\text {topos value}&\text {verdict}\\ \hline C_3\text { action}&\text {linear action}&\text {none}&\text {fail}\\ C_2\ltimes X&\text {isotropy}&\text {none}&\text {fail}\\ C_2\text { torsor}&\text {free/transitive}&\text {classification}&\text {conditional}\\ \text {context}&\text {pullback/restriction}&\text {inverse image}&\text {conditional}\\ U_G&\text {no fixed point}&\text {internal inhabitation}&\text {strict}. \end {array} \]

Topoi enter these notes only when a result uses universal torsor classification, organizes several constructions as inverse image or base change, or relies on internal reasoning that differs from global sections. Ordinary Group Actions, Group Algebra calculations, and action groupoids stay below that layer.

This boundary also excludes several stronger claims. The spectrum of a center is not the original noncommutative Group Algebra. The action-groupoid example does not require a quotient stack. No site, descent theorem, or physical correspondence has been supplied by these finite tests. Each of those would need its own mathematical construction before extending the present layer.

Models and routes from binary tetrahedral structure [fgap-001F]
📄PDF

July 30, 2026
Utensil Song

The concrete, internal, external, and abstract models of $2T$ retain different data. Their comparison opens a Group-Algebra route through the semidirect factors and a representation-theoretic route through the McKay correspondence.

Remark. what the models of 2T retain [fgap-001D]

The same binary tetrahedral symmetry now has several models. They answer different questions.

The concrete model $T\leq \mathbb {H}^{\times }$ retains quaternion coordinates, multiplication, conjugation, and norm. It is the model for explicit calculations.
The internal semidirect-product structure retains the same group $T$, but also marks the subgroups $Q,C\leq T$. The facts \[ T=QC,\qquad Q\mathrel {\trianglelefteq }T,\qquad Q\cap C=\{1\} \] say that every element of $T$ has a unique factorization $qc$. They expose how the two parts fit inside the concrete group.
The external model $Q\rtimes _{\alpha }C$ replaces a quaternion by a pair $(q,c)$. It retains the factors and records their interaction in the conjugation action $\alpha (c)(q)=cqc^{-1}$. Its multiplication is \[ (q,c)(q',c') =\bigl (q\alpha (c)(q'),cc'\bigr ). \]
An abstract model can specify the binary tetrahedral group without quaternion coordinates. This is convenient when only its group structure is needed, but coordinates and named factors must be restored by additional maps.

The multiplication map \[ \mu :Q\rtimes _{\alpha }C\longrightarrow T,\qquad (q,c)\longmapsto qc \] is an isomorphism by the internal semidirect-product theorem. Indeed, \[ \mu \bigl ((q,c)(q',c')\bigr ) =q(cq'c^{-1})cc' =qcq'c' =\mu (q,c)\mu (q',c'). \] Thus the external multiplication is not an analogy: it is exactly the concrete multiplication written in factor coordinates. The two carriers are still different, so a theorem or construction passes between them only through an explicit isomorphism. If it refers to the named factors or their action, the transport must also record the corresponding compatibility.

The internal and external constructions are developed in [fre2023discrete, sec. 4.2.13, pp. 62--63] and [isaev2018theory, sec. 1.4.2, pp. 58--61]. The concrete identification of $2T$ with the Hurwitz unit group and $Q_8\rtimes \mathbb {Z}/3\mathbb {Z}$ is given in [voight2021quaternion, sec. 11.2.4, p. 168].

Remark. two routes from binary tetrahedral symmetry [fgap-001E]

The semidirect-product model and the quaternion model open two different routes from the same group. One rewrites the Group Algebra in interacting factor data. The other places the group inside $\mathrm {SU}(2)$ and leads to the McKay graph.

The Group-Algebra route

Extend the conjugation action $\alpha :C\to \operatorname {Aut}(Q)$ linearly to real-algebra automorphisms \[ \overline {\alpha }_c:\mathbb {R}[Q]\longrightarrow \mathbb {R}[Q]. \] On the vector space $\mathbb {R}[Q]\otimes _{\mathbb {R}}\mathbb {R}[C]$, write a pure tensor as $a\mathbin {\#}c$ and define \[ (a\mathbin {\#}c)(b\mathbin {\#}d) =a\,\overline {\alpha }_c(b)\mathbin {\#}cd, \] extending bilinearly. This convention defines the skew Group Algebra $\mathbb {R}[Q]\rtimes _{\overline {\alpha }}C$; it is also a crossed product with trivial twisting cocycle.

The basis map \[ [q]\mathbin {\#}c\longmapsto [qc] \] respects multiplication by the calculation in what the models of 2T retain, and unique factorization makes it a bijection. Hence \[ \mathbb {R}[Q]\rtimes _{\overline {\alpha }}C \mathbin {\cong _{\mathbb {R}\text {-alg}}}\mathbb {R}[T]. \] This is the Group-Algebra form of $T\cong Q\rtimes _{\alpha }C$. The extension of group maps to Group-Algebra maps follows the convention in [sengupta2010representations, secs. 3.1--3.2, pp. 39--41].

A module over this skew Group Algebra can be read as an $\mathbb {R}[Q]$-module $M$ together with a linear action of $C$ satisfying \[ c\mathbin {\cdot }(a\mathbin {\cdot }m) =\overline {\alpha }_c(a)\mathbin {\cdot } (c\mathbin {\cdot }m). \] The external model therefore exposes the compatibility needed to assemble representations from the two factors. It does not by itself decompose $\mathbb {R}[T]$ into simple blocks. That requires further representation-theoretic input.

The McKay route

Under the standard matrix realization of the unit quaternions as $\mathrm {SU}(2)$, the concrete group $T$ becomes a finite subgroup of $\mathrm {SU}(2)$. Let $\tau _3$ be its faithful 2-dimensional complex representation. The McKay graph has one vertex for each irreducible complex representation $\tau _i$; the number of edges from $\tau _i$ to $\tau _j$ is the multiplicity of $\tau _j$ in \[ \tau _3\otimes \tau _i. \] For the binary tetrahedral group this graph is the affine Dynkin diagram $\widetilde {E}_6$. The character table, the seven irreducible representations, and the tensor-product calculation are given in [stekolshchik2008notes, table A.12, prop. A.10, and ex. A.11, pp. 172--174].

This graph connects the representation theory of $2T$ with quivers and the ADE classification. The same source relates a binary polyhedral subgroup $G\leq \mathrm {SU}(2)$ to the quotient $\mathbb {C}^2/G$, its invariant algebra, and its Kleinian singularity in [stekolshchik2008notes, secs. A.3--A.4, pp. 158--161]. These are routes toward quotient geometry and related orbifold constructions. They are not consequences of the semidirect-product theorem alone.

Neither route assigns physical meaning to $Q$, $C$, an algebra block, or a vertex of $\widetilde {E}_6$. They supply mathematical structures on which a physical correspondence could be stated and tested. A proposed correspondence must still identify the action, representation, preserved structure, and physical interpretation.

some HF papers worth skimming [uts-016E]

May 25, 2025

- multimodal, diffusion
    - Scaling Diffusion Transformers Efficiently via μP
        - establish μP as a principled and efficient scaling strategy for diffusion Transformers
        - with appendix on Theoretical Background of μP
    - Neurosymbolic Diffusion Models
        - the first method to integrate masked diffusion models as the neural network extractor in neurosymbolic predictors
        - with a very long appendix on math background
    - Diffusion vs. Autoregressive Language Models: A Text Embedding Perspective
        - propose adopting diffusion language models for text embeddings, motivated by their inherent bidirectional architecture and recent success in matching or surpassing LLMs especially on reasoning tasks
        - focus on Dream 7b: Introducing dream 7b, the most powerful open diffusion large language model to date
            - consistently outperforms existing diffusion language models by a large margin
            - matches or exceeds top-tier Autoregressive (AR) language models of similar size on the general, math, and coding abilities
            - demonstrates strong planning ability and inference flexibility that naturally benefits from the diffusion modeling
            - virtually all leading LLMs relying on this same sequential left-to-right architecture
            - Discrete diffusion models (DMs) have gained attention as a promising alternative for sequence generation since their introduction to the text domain, which dynamically refine the full sequence in parallel starting from a fully noised state
    - MMaDA: Multimodal Large Diffusion Language Models
        - unified diffusion architecture
        - superior performance across diverse domains such as textual reasoning, multimodal understanding, and text-to-image generation
        - rich and impressive examples
        - with appendix on Preliminaries of Discrete Diffusion, PPO and GRPO
    - LaViDa: A Large Diffusion Language Model for Multimodal Understanding
        - Large Vision-Language Diffusion Model with Masking
        - follows a similar design to common AR VLMs like LLaVa
    - GRIT: Teaching MLLMs to Think with Images
        - generate visually grounded reasoning chains by interleaving natural language with explicit bounding box coordinates referencing relevant image regions
    - Dimple: Discrete Diffusion Multimodal Large Language Model with Parallel Decoding
        - trained using a novel two-phase paradigm–Autoregressive-then-Diffusion
    - dKV-Cache: The Cache for Diffusion Language Models
        - diffusion language models have long been constrained by slow inference
        - motivated by the observation that different tokens have distinct representation dynamics throughout the diffusion process
        - propose a delayed and conditioned caching strategy for key and value states
    - Understanding Generative AI Capabilities in Everyday Image Editing Tasks
        - analyzing 83k requests with their associated 305k edits from the recent 12 years on the `/r/PhotoshopRequest` Reddit community
        - new dataset: PSR
    - Hunyuan-Game: Industrial-grade Intelligent Game Creation Model
        - lots of examples of game creation
- efficiency
    - Scaling Law for Quantization-Aware Training
        - a comprehensive scaling law for 4-bit QAT of LLMs, integrating model size, training dataset size, and quantization granularity
        - previous methods do not account for quantization granularity G
        - weight and activation quantization errors tend to contribute almost equally to the total error
    - Fine-tuning Quantized Neural Networks with Zeroth-order Optimization
        - push the limits of memory-efficient training by minimizing memory usage on model weights, gradients, and optimizer states, within a unified framework
        - perturbs the continuous quantization scale for gradient estimation and uses a directional derivative clipping method to stabilize training
        - Zeroth-order optimization (ZO) methods are often used in cases where gradients and higher-order derivatives of the objective cannot be directly computed or are unreliable
        - successfully fine-tune Stable Diffusion 3.5 Large quantized by BitsAndBytes on stylized images using a single Nvidia RTX 4090 24GB GPU
    - A Token is Worth over 1,000 Tokens: Efficient Knowledge Distillation through Low-Rank Clone
        - trains a set of low-rank projection matrices that jointly enable soft pruning by compressing teacher weights, and activation clone by aligning student activations, including FFN signals, with those of the teacher
        - remarkable distillation efficiency, achieving superior performance with more than 1000× fewer training tokens
        - LRC w/o FFN produces a substantial performance degradation that persists throughout training, further confirming the critical importance of FFN activations
        - LRC’s projection-based alignment is not only sufficient for effective knowledge transfer but also more efficient and stable
- agents, reasoning, RL
    - NovelSeek: When Agent Becomes the Scientist -- Building Closed-Loop System from Hypothesis to Verification
    - Reinforcement Learning Finetunes Small Subnetworks in Large Language Models
    - Tool-Star: Empowering LLM-Brained Multi-Tool Reasoner via Reinforcement Learning
    - AceReason-Nemotron: Advancing Math and Code Reasoning through Reinforcement Learning
    - Training-Free Reasoning and Reflection in MLLMs
    - Date Fragments: A Hidden Bottleneck of Tokenization for Temporal Reasoning
    - RLVR-World: Training World Models with Reinforcement Learning
    - SPhyR: Spatial-Physical Reasoning Benchmark on Material Distribution
    - Risk-Averse Reinforcement Learning with Itakura-Saito Loss
- safety
    - Phare: A Safety Probe for Large Language Models
    - Audio Jailbreak: An Open Comprehensive Benchmark for Jailbreaking Large Audio-Language Models
    - Are Vision-Language Models Safe in the Wild? A Meme-Based Benchmark Study
- application
    - Steering Large Language Models for Machine Translation Personalization
    - This Time is Different: An Observability Perspective on Time Series Foundation Models
    - Prior Prompt Engineering for Reinforcement Fine-Tuning
    - Using Large Language Models for Commit Message Generation: A Preliminary Study
    - The Distracting Effect: Understanding Irrelevant Passages in RAG
- more
    - Distilling LLM Agent into Small Models with Retrieval and Code Tools
    - CLEVER: A Curated Benchmark for Formally Verified Code Generation
    - DiSA: Diffusion Step Annealing in Autoregressive Image Generation
    - Capability-Based Scaling Laws for LLM Red-Teaming
    - FinTagging: An LLM-ready Benchmark for Extracting and Structuring Financial Information
    - GSO: Challenging Software Optimization Tasks for Evaluating SWE-Agents
    - watch The 3D Gaussian Splatting Adventure: Past, Present, Future
    - DCM: Dual-Expert Consistency Model for Efficient and High-Quality Video Generation
    - GUI-Actor: Coordinate-Free Visual Grounding for GUI Agents
    - Agentic Neural Networks: Self-Evolving Multi-Agent Systems via Textual Backpropagation
    - Large Language Models Often Know When They Are Being Evaluated
    - Tiny-diffusion: A minimal implementation of probabilistic diffusion models
    - AgentDistill: Training-Free Agent Distillation with Generalizable MCP Boxes
    - Time Series Forecasting with Graph Transformers
    - The Effect of State Representation on LLM Agent Behavior in Dynamic Routing Games
    - Compiling LLMs into a MegaKernel: A path to low-latency inference
    - Magenta RealTime: An Open-Weights Live Music Model
    - Audit & Repair: An Agentic Framework for Consistent Story Visualization in Text-to-Image Diffusion Models
    - Let Your Video Listen to Your Music!
    - Vision as a Dialect: Unifying Visual Understanding and Generation via Text-Aligned Representations
    - Bridging Cinematic Principles and Generative AI for Automated Film Generation
    - Show HN: PILF, The ultimate solution to catastrophic oblivion on AI models
    - Qwen VLo: From “Understanding” the World to “Depicting” It
    - WorldVLA: Towards Autoregressive Action World Model (on HN)
    - Small language models are the future of agentic AI (on HN)
    - Overclocking LLM Reasoning: Monitoring and Controlling LLM Thinking Path Lengths (on HN)
    - Reinforcement Learning from Human Feedback (RLHF) in Notebooks
    - LLMs should not replace therapists (on HN)
    - Mercury: Ultra-fast language models based on diffusion (on HN)
    - Biomni: A General-Purpose Biomedical AI Agent (on HN)
    - Distributed AI Agents for Cognitive Underwater Robot Autonomy
    - GEPA: Reflective prompt evolution can outperform reinforcement learning (on HN)
    - Hijacking multi-agent systems in your PajaMAS
    - Core Safety Values for Provably Corrigible Agents
    - Flow Matching Policy Gradients
    - Fine-tuned small LLMs can beat large ones with programmatic data curation (on HN)
        - the chosen task is considered not challenging
    - Persona vectors: Monitoring and controlling character traits in language models (on HN)
    - Qwen-Image: Crafting with native text rendering (on HN)
    - Exploring Autonomous Agents: A Closer Look at Why They Fail When...
    - Kimina-Prover: Applying Test-time RL Search on Large Formal Reasoning Models
    - Emergent Misalignment: Narrow finetuning can produce broadly misaligned LLMs (on HN)
    - Context Rot: How Increasing Input Tokens Impacts LLM Performance (on HN) (on lobste.rs)
    - All AI models might be the same (on HN)
    - LLM Economist: Large Population Models and Mechanism Design in Multi-Agent Generative Simulacra
    - Subliminal learning: Models transmit behaviors via hidden signals in data (on HN)
        - Simon Willison | Subliminal Learning: Language Models Transmit Behavioral Traits via Hidden Signals in Data
    - Flow Matching Meets Biology and Life Science: A Survey
    - Seed-Prover/SeedProver at main · ByteDance-Seed/Seed-Prover
    - Transformers Without Normalization (on HN)
    - Embedding-Aware Quantum-Classical SVMs for Scalable Quantum Machine Learning

Agent-assisted work and human examination [connes-000T]

This draft expands the examination method summarized in § [connes-000Z].

An agent-authored formalization is easier to examine when the code comes with a route back to the literature, an executable verification record, and an audit of the questions that technical checks cannot settle. This project tests that combined method.

Grounding: mathematical claims tied to the literature and external inputs identified at their exact Lean boundary.
Technical verification: statement and axiom comparison, Landlock and network isolation, and replay through the Lean kernel and nanoda, as recorded in the Comparator note.
Mathematical audit: source correspondence, definitions, hypotheses, concrete consumers, literature claims, and proof architecture tracked in the audit ledger.
Traceability: declarations and transferred proof material connected to their sources by the provenance ledger.
Exposition: mathematical arguments, implementation choices, and unresolved boundaries collected in these notes.

Together these layers let a reader follow a claim from the literature to its Lean declaration, downstream consumer, audit status, and executable check. The resulting draft includes the material a human needs to examine and digest the work.

Comments on [dereli2010degenerate] [uts-0007]

This paper is found because it's cited by [filimoshina2023some].

Comments on [fauser2004grade] [uts-0006]

Some restrictions in Clifford algebra to geometric calculus: A unified language for mathematics and physics are relaxed in this paper.
This paper cites A treatise on quantum clifford algebras for the foundation of Clifford algebra, and the use of Kuperberg graphical calculi over commutative diagrams.

Comments on [weber2013lie] [uts-0005]

Particularly, we cite:

Lecture 18 - Clifford Algebras and Spin Groups
Lecture 19 - Clifford and Spin Representations
Lecture 20 - Duality and Triality

These lecture notes are based on Spin geometry (pms-38).

Comments on [woit2012lie] [uts-0004]

Particularly, we cite:

Clifford Algebras and Spin Groups
The Spinor Representation

Formalization motivation [connes-000S]

This draft expands the formalization motivation summarized in § [connes-000Z].

The mathematical comparison identifies where information is lost. The formalization asks whether that loss can be exposed as an explicit proof interface. Lean turns the claim that a factor forgets structure into an auditable dependency map.

Expose hidden interfaces: square-span, Fourier shear, measurable transport, continuous closure, spectral detection, characteristic kernels, and quotient-twisted modules.
Separate routine translation from proof design: the concrete boundaries are summarized in § [connes-000K].
Make forgetting auditable: each change of structure crosses a named Lean interface.

Library consumer. The project uses Mathlib and TauCeti algebraic, analytic, and representation-theoretic infrastructure. Its missing or bespoke interfaces indicate where contributions to those libraries could support later formalizations. The present library boundary is recorded in § [connes-000G].

Fulltext Search with Pathfind [uts-016D]

> For now, this page only works if the forest site is started with `just pathfind`.

Definition. Implicit surface [hart1996sphere, sec. 1] [ag-000K]

If an SDF $f$ is a continuous mapping, the subset $\Omega $ can be implicitly described as the locus of points \[ \Omega = \{ p : f(p) \le 0 \} \]

By continuety, $f$ is zero on $\partial \Omega $ which forms the implicit surface of $f$.

Definition. Kronecker delta [wiki2024dirac] [uts-0002]

Kronecker delta \[\delta _{i j}= \begin {cases}0 & \text { if } i \neq j \\ 1 & \text { if } i=j\end {cases}\] or with use of Iverson bracket: \[ \delta _{i j}=[i=j] . \] where $[P]$ is defined as: \[ [P]=\begin {cases}1 & \text { if } P \text { is true } \\ 0 & \text { if } P \text { is false }\end {cases} \]

In Lean 4, the Kronecker delta could be defined as:


def δ (i j : I) : R := (Pi.single i 1 : _ → R) j

Mathematical motivation [connes-000Q]

This draft expands the mathematical motivation summarized in § [connes-000Z].

The counterexample is not merely a negative answer to Connes' conjecture. Its richer content is a controlled experiment in nonfaithfulness. The three proof families vary different algebraic inputs while preserving the analytic output.

The group distinction survives algebraically but disappears after measurable crossed-product transport.

OpenAI: vary the abelian kernel. [openai2026tenadvances, Chapter 4];
Zhou: fix the kernel; vary the action and module structure. [zhou2026icc, Sections 1 and 3]; and
Anthropic: fix both; vary the extension class. [anthropic2026icc, Sections 3–5].

Three kinds of information loss stand out:

Cocycle: algebraically nontrivial, measurably removable;
Action: Fourier–Pontryagin transport conjugates distinct module actions; and
Extension data: characteristic-two data distinguish groups while their factors remain isomorphic.

Property (T) acts as a control condition: these are rigid groups, not examples explained by group-theoretic flexibility. The comparison asks which algebraic distinctions survive representation, twisting, duality, and analytic completion, and at which step the others disappear.

Test PDF [uts-000A]

Test equation tagging and referencing [uts-000B]

Inspired by thosgood/fga.

The following is an equation:

Eq. [math-eq-1.1]

\[E = m c^2 \tag{math-eq-1.1}\]

Eq. [eqid]

\[E = m c^2 \tag{1.2}\]

Eq. [eqid2]

\[E = m c^2 \tag{1.3}\]

Eq. [math-eq-1.4]

\[E = m c^2 \tag{math-eq-1.4}\]

Now we refer to Eq [math-eq-1.1], Eq [eqid].

games I really enjoyed [uts-001G]

## Flash games

### Pipol Destinations

It's a simple game from my youth, where you need to guide people safely to their destinations by excavating or backfilling tunnels.

It took me quite some effort to find it again, and it can be played using the Ruffle emulator nowadays.

## PC Games

- Prince of Persia Series from Ubisoft, particularly
  - Prince of Persia: The Sands of Time (2003)
  - Prince of Persia: Warrior Within (2004)
  - Prince of Persia: The Two Thrones (2005)
  - Prince of Persia: The Forgotten Sands (2010)
  - I also played Prince of Persia (2008), but not so enjoyable as the others
- Tomb Raider Series, particularly
  - One of Tomb Raider I/II/III (1996-1998)
  - Tomb Raider (2013)
  - Rise of the Tomb Raider (2015)
- Sentimental Graffiti (1998)
- Devil May Cry 4 (2008)
- Homeworld 2 (2003)
- Assassin's Creed Unity (2014)
- Blades of Time (2012)
- Prototype (2009)
- Portal 2 (2011)
- Ballance (2004)
- Kerbal Space Program (2015)
- FAR: Changing Tides (2022)
- Black Myth: Wukong (2024)

## iOS Games

- Mekorama (2016)
- Fancade (2020)
- Geostorm (2017)
- Monument Valley (2014)
- Monument Valley 2 (2017)

## Desktop Games

- Ah!Ha Hedgehog Escape from Eureka
- Jump IN' from SmartGames: Help the rabbits jump and hide!
- Cytosis: An Animal Cell Biology Game from Genius Games

some links about Star Trek [uts-001K]

I've long wished to note down memorable quotes from Star Trek. Particularly the Discovery, Picard, Orville and Strange New Worlds series in recent years.

I have tried to look for high quality transcripts of these series, and selected quotes.

Here are some good resources:

- OpenSubtitles.org has subtitles organized by episode and season, e.g. Star Trek: Discovery (2017) but there is no easy way to bulk download and review the quality of the subtitles. Many subtitles from various sources are provided for each episode, and good subtitles might not be available for all episodes e.g. filtering by the title and the uploader
- Memory Alpha on Fandom has detailed articles on each episode, with "Summary" for the plot and "Memorable quotes"
    - e.g. Star Trek: Discovery
    - full list of TV and films
- a few websites from China:
    - https://www.startrekchina.org/ (also on Github)
    - https://docs.startrekcn.cn/ (also on Github)
- Star Trek TrueType Font Collection

test graphviz transcludes [uts-001M]

test typst [uts-000R]

Note: The Typst files and their imports must be placed under typst, as it's set up as the root directory for Typst imports.

rendering a Typst file with imports

rendering a Typst code block with imports

#import "config.typ" : setup #let fulltext = [ // #set page(width: 595.28pt, height: auto, margin: (x: 0.5cm, y: 0.5cm)) // #set text(size: 16pt) // #set heading(numbering: "1.") = Fibonacci sequence The Fibonacci sequence is defined through the recurrence relation $F_n = F_(n-1) + F_(n-2)$. It can also be expressed in _closed form:_ $ F_n = round(1 / sqrt(5) phi.alt^n), quad phi.alt = (1 + sqrt(5)) / 2 $ #let count = 8 #let nums = range(1, count + 1) #let fib(n) = ( if n <= 2 { 1 } else { fib(n - 1) + fib(n - 2) } ) The first #count numbers of the sequence are: #align(center, table( columns: count, ..nums.map(n => $F_#n$), ..nums.map(n => str(fib(n))), )) ] #show : setup(fulltext)

hybrid typst with forester markup

This is native forester markup:

external link: typst docs
wiki link: test tikz drawing
citations: [nakahira2023diagrammatic]
cross-references: § [uts-000E]

This is the same markup rendered in Typst:

#import "config.typ" : setup #let fulltext = [ We wish to use - external link: #link("https://typst.app/docs", underline(text(black)[typst docs])) - wiki link: #link("/forest/uts-000E/", underline(stroke: (dash: "dotted"), text(black)[test tikz drawing])) - citations: #link("/forest/nakahira2023diagrammatic/", text(rgb("#10731d"))[[nakahira2023diagrammatic]]) - cross-references: #link("/forest/uts-000E/", underline(stroke: (dash: "dotted"), text(black)[§ ])) ] #show : setup(fulltext)

render a complicated Typst file

Adapted from ⧉, removed figures and bib for now, due to depending on external non-Typst files.

// This is for adjusting the size so it can fit into the blog post #import "config.typ" : setup #let fulltext = [ = Examples Paragraph 1. Paragraph 2. Paragraph 3 \ with line break. == Simple content - *bold* - _emphasis_ - `code` - "quotes" - Indented + numbered + #lorem(10) + #underline[underline] + #text(orange, size: 0.8em)[orange smaller text] - #link("https://typst.app/docs/reference/")[link] - #[[]] ```typ _fenced code block_ with *syntax highlighting* ``` #quote(block: true, attribution: "Me")[ We are not born to be doomed on one planet. ] #quote(block: false, attribution: "Me")[ Never lose hope. ] inline math: $a + b/c = sum_i x^i$ display math: $ 7.32 beta + sum_(i=0)^nabla (Q_i (a_i - epsilon)) / 2 $ #set heading(numbering: "I.1:") == Figure #set heading(numbering: "1.1.") == Tables #set rect(height: 1em) #table( columns: 2, [Points], rect(width: 72pt), [Millimeters], rect(width: 25.4mm), [Centimeters], rect(width: 2.54cm), [Inches], rect(width: 1in), [Relative to font size], rect(width: 6.5em) ) == Show rules #show "green text": text(green)[text] Here is some green text. #show emph: set text(blue) _emphasized_ text is now blue. #block[ #show heading.where(level: 3): set align(center) === centered heading #show heading.where(level: 4): it => { set align(right) set text(red) // set heading(numbering: "1.I:") // not working block(it.body) //it } ==== red heading #let apply-template(body, name: "My document") = { show heading.where(level: 4): emph set heading(numbering: "1.1") align(center, text(name, size: 2em)) body } #show: apply-template.with(name: "Report") #lorem(20) ] #box(stroke: red, inset: 1em)[Box text] #block(stroke: red, inset: 1em)[Block text] #set rect(height: auto) // without auto, would be affected by the rect height #rect[Rect text] #figure( text(size: 5em)[I], caption: [I'm cool, right?], ) Horizontal #h(1cm) spacing. #v(1cm) And some vertical too! Double font size: #box(stroke: red, baseline: 40%, height: 2em, width: 2em) This line width is 50% of the box width: #box(stroke: red, width: 4em, inset: (y: 0.5em), line(length: 50%)) Single fraction length just takes maximum size possible to fill the parent: Left #h(1fr) Right #rect(height: 1em)[ #h(1fr) ] If you use several fractions inside one parent, they will take all remaining space proportional to their number: Left #h(1fr) Left-ish #h(2fr) Right #block( fill: luma(230), inset: 8pt, radius: 4pt, width: 100%, height: 200pt, [ #place( top + right, // place at the page right and top square( width: 20pt, stroke: 2pt + blue ), ) #let note(where, body) = place( center + where, float: true, clearance: 6pt, rect(body), ) #lorem(10) #note(bottom)[Bottom 1] #note(bottom)[Bottom 2] #lorem(10) #note(top)[Top] #lorem(10) #for i in range(16) { let amount = i * 6pt place(center, dx: 2*amount - 32pt, dy: -0.2*amount)[A] } #rect(inset: 0pt, move( dx: 6pt, dy: 6pt, rect( inset: 8pt, fill: white, stroke: black, [Abra cadabra] ) )) ] ) This is mirrored. #scale(y: -100%)[This is mirrored.] #scale(200%, origin: bottom + left)[This is enlarged.] #scale(200%, origin: top + left, text(blue)[This is enlarged \ and eats what follows.]) #lorem(20) #hide(lorem(20)) Something is hidden before this but occupies space. The rest are shown in two columns except for this paragraph. #lorem(10) #block[ #show: rest => columns(2, rest) #lorem(20) #colbreak() #lorem(20) #colbreak() // #show: rest => columns(1, rest) // not working ] == Scripting #table( columns: 2, fill: (x, y) => if x+y == 2 { yellow } else if x + y == 3 { red } else { blue.lighten(50%) }, ..for i in range(5) { for j in range(2) { (text(str(i + j)),) } } ) #let f = (name) => "Hello, " + name #f("Typst function!") #let g(name) = "Hello, " + name #g("Typst function shorthand!") By default braces return anything that "returns" into them. #let h() = { "Str1" [Str2] lorem(5) } #h() #let i() = { "Str1" return "Str" } #i() #let j(name: "Typst function with default value") = "Hello, " + name + "." #j() #j(name: "Typst function with named argument") #(type([content]) == content) #repr([It is _content_!]) #repr(none) === String #let s = "another small string" #s.replace("a", sym.alpha) \ #s.split(" ") // split by space #(2 - 5) \ #0xff \ #0o10 \ #0b1001 #calc.pow(2, 10) === List #let values = (1, 7, 4, -3, 2) #repr(values) #values.at(-1) #values.find(calc.even) #values.filter(calc.odd) #() === Dict #let dict = ( name: "Typst", born: 2019, ) #repr(dict) #dict.at("born") #dict.insert("city", "Berlin ") #("name" in dict) #(:) === Conditions & loops #let a = 5 #if (a > 1 and a <= 4) or a == 5 [ `a` matches the condition ] #let s = 0 #for i in range(3, 6) { s += i [Number #i is added to sum. Now sum is #s.] } #let people = (Alice: 3, Bob: 5) #for (name, value) in people [ #name has #value apples. ] #let text-params = (fill: blue, size: 0.8em) Some #text(..text-params)[text]. #let f(..args) = [ #args.pos()\ #args.named() ] #f(1, "a", width: 50%, block: false) === State #let s = state("x", 0) #let compute(expr) = [ #s.update(x => eval(expr.replace("x", str(x))) ) New value is #context s.get(). ] #compute("10") \ #compute("x + 3") \ #compute("x * 2") \ #compute("x - 5") Value at `<here>` is #context s.at(<here>) #compute("10") \ #compute("x + 3") \ *Here.* <here> \ #compute("x * 2") \ #compute("x - 5") === Math <math> $ forall v, w in V, alpha in KK: alpha dot (v + w) = alpha v + alpha w \ // cont — contour integral, integral.cont, integral.double, integral.square, sum.integral \ // lt — less than, gt — greater than lt, lt.circle, lt.curly, lt.eq, lt.eq.curly, lt.not, lt.eq.not, lt.eq.not.curly, gt, lt.gt.eq, lt.gt.not \ gt.nequiv, gt.napprox, gt.ntilde, gt.tilde.not \ arrow.b, triangle.r, angle.l \ plus.circle.big plus.circle, times.circle.big plus.circle \ square, square.filled, diamond.filled, arrow.filled \ alpha, Alpha, beta, Beta, beta.alt, gamma, pi, Pi,\ pi.alt, phi, phi.alt, Phi, omicron, kappa, kappa.alt, Psi,\ theta, theta.alt, xi, zeta, rho, rho.alt, kai, Kai,\ bb(A), AA, bb(1) \ nothing, nothing.rev, diameter \ $ #show math.equation: set text(features: ("cv01",)) $ nothing, nothing.rev, diameter $ #show math.nothing: math.diameter $ nothing, nothing.rev, diameter $ $ (a^2 + b^2)/2 \ {[((a + b)/2) + 1]_0} \ lr([a/2, b), size: #150%) \ abs(a + b), norm(a + b), floor(a + b), ceil(a + b), round(a + b) \ $ // #block[ // #show math.equation: set align(right) // $ // (a + b)/2 // $ // ] // the above is not working #align(center, block($ x = 5 $)) $ (3x + y) / 7 &= 9 && "given" \ 3x + y &= 63 && "multiply by 7" \ 3x &= 63 - y && "subtract y" \ x &= 21 - y/3 && "divide by 3" $ #show math.integral: math.limits #show math.sum: math.limits $ sum_a^b \ integral_a^b \ scripts(sum)_a^b \ a =_"By lemme 1" b, a scripts(=)_+ b \ arccos, arcsin, arctan, arg, cos, cosh, cot, coth, csc,\ csch, ctg, deg, det, dim, exp, gcd, hom, id, im, inf, ker,\ lg, lim, liminf, limsup, ln, log, max, min, mod, Pr, sec,\ sech, sin, sinc, sinh, sup, tan, tanh, tg "and" tr \ $ #let arcsinh = math.op("arcsinh") $ arcsinh x $ #let liminf = math.op(math.underline(math.lim), limits: true) #let limsup = math.op(math.overline(math.lim), limits: true) #let integrate = math.op($integral dif x$) $ liminf_(x->oo)\ limsup_(x->oo)\ integrate x^2 $ Inline, but like true display: $display(sum_0^oo e^x^a)$ $ vec(a, b, c) + vec(1, 2, 3) = vec(a + 1, b + 2, c + 3) \ vec(1, 2, 3, delim: "{") \ vec(1, 2, 3, delim: "||") \ vec(1, 2, 3, delim: #none) \ vec(a, b, c) vec(a, b, c, gap:#0em) vec(a, b, c, gap:#1em) \ mat( 1, 2, ..., 10; 2, 2, ..., 10; dots.v, dots.v, dots.down, dots.v; 10, 10, ..., 10; // `;` in the end is optional ) \ mat( delim: "|", 1, 2, ..., 10; 2, 2, ..., 10; dots.v, dots.v, dots.down, dots.v; 10, 10, ..., 10; gap: #0.3em ) \ $' #set math.equation(numbering: "(1)") #for klass in ("normal", "punctuation", "opening", "closing", "fence", "large", "relation", "unary", "binary", "vary" ) { align(center, block[ #show math.circle: math.class.with(klass) $ text(#klass : ) class("normal", a) class(#klass, b) class("normal", c) quad square circle square $ ]) } #align(center, block(width: 7em)[ // Cruel and world are separated. // Imagine this is a phrase that can't be split, what to do then? Hello cruel world // Let's connect them with a special space! // No usual spacing is allowed, so either use semicolumn... Hello cruel#sym.space.nobreak;world // ...parentheses... Hello cruel#(sym.space.nobreak)world // ...or unicode code Hello cruel\u{00a0}world // Well, to achieve the same effect I recommend using box: Hello #box[cruel world] ]) #align(center, block(width: 5em)[ This is an $i$-th element. This is an $i$\u{2011}th element. // the best way would be #show "-th": "\u{2011}th" This is an $i$-th element. ]) == Bibliography and Citation Style Goes back to @math . ] #show : setup(fulltext)

test graphviz [uts-001L]

Adapted from ⧉:

strict digraph "" { graph [bgcolor=transparent]; node [label="\N", penwidth=1.8 ]; edge [arrowhead=vee]; QuadraticForm [color=green, fillcolor="#B0ECA3", label=QuadraticForm, shape=box, style=filled]; LinearMap [color=green, fillcolor="#B0ECA3", label=LinearMap, shape=box, style=filled]; Dual [color=green, fillcolor="#B0ECA3", label=Dual, shape=box, style=filled]; LinearMap -> Dual [style=dashed]; TensorAlgebra [color=green, fillcolor="#B0ECA3", label=TensorAlgebra, shape=box, style=filled]; LinearMap -> TensorAlgebra [style=dashed]; Group [color=green, fillcolor="#B0ECA3", label=Group, shape=box, style=filled]; Ring [color=green, fillcolor="#B0ECA3", label=Ring, shape=box, style=filled]; Group -> Ring [style=dashed]; Module [color=green, fillcolor="#B0ECA3", label=Module, shape=box, style=filled]; Ring -> Module [style=dashed]; DivisionRing [color=green, fillcolor="#B0ECA3", label=DivisionRing, shape=box, style=filled]; Ring -> DivisionRing [style=dashed]; RingHom [color=green, fillcolor="#B0ECA3", label=RingHom, shape=box, style=filled]; Ring -> RingHom [style=dashed]; Module -> LinearMap [style=dashed]; VectorSpace [color=green, fillcolor="#B0ECA3", label=VectorSpace, shape=box, style=filled]; Module -> VectorSpace [style=dashed]; Algebra [color=green, fillcolor="#B0ECA3", label=Algebra, shape=box, style=filled]; Module -> Algebra [style=dashed]; RingQuot [color=green, fillcolor="#B0ECA3", label=RingQuot, shape=box, style=filled]; Module -> RingQuot [style=dashed]; BilinForm [color=green, fillcolor="#B0ECA3", label=BilinForm, shape=box, style=filled]; Module -> BilinForm [style=dashed]; FreeAlgebra [color=green, fillcolor="#B0ECA3", label=FreeAlgebra, shape=box, style=filled]; Algebra -> FreeAlgebra [style=dashed]; RingQuot -> FreeAlgebra [style=dashed]; BilinForm -> QuadraticForm [style=dashed]; DivisionRing -> VectorSpace [style=dashed]; RingHom -> LinearMap [style=dashed]; RingHom -> Algebra [style=dashed]; RingHom -> RingQuot [style=dashed]; AlgHom [color=green, fillcolor="#B0ECA3", label=AlgHom, shape=box, style=filled]; RingHom -> AlgHom [style=dashed]; FreeAlgebra -> TensorAlgebra [style=dashed]; Monoid [color=green, fillcolor="#B0ECA3", label=Monoid, shape=box, style=filled]; Monoid -> Ring [style=dashed];}

Adapted from ⧉:

digraph { graph [rankdir=LR]; node [shape=record]; 0 [label="0 | [• S, $]\n[S → • a S b, $]\n[S → •, $]"]; 1 [label="1 | [S •, $]"]; 2 [label="2 | [S → a • S b, $]\n[S → • a S b, b]\n[S → •, b]"]; 3 [label="3 | [S → a S • b, $]"]; 4 [label="4 | [S → a • S b, b]\n[S → • a S b, b]\n[S → •, b]"]; 5 [label="5 | [S → a S b •, $]"]; 6 [label="6 | [S → a S • b, b]"]; 7 [label="7 | [S → a S b •, b]"]; 0 -> 1 [label=S]; 0 -> 2 [label=a]; 2 -> 3 [label=S]; 2 -> 4 [label=a]; 3 -> 5 [label=b]; 4 -> 6 [label=S]; 4 -> 4 [label=a]; 6 -> 7 [label=b]; }

Adapted from ⧉:

digraph G { node [shape=plaintext fontname="Arial"]; 0 -> 1 [arrowhead=none]; 1 -> 2 [arrowhead=none]; 2 -> 7 [arrowhead=none]; 7 -> 8 [arrowhead=none]; 8 -> 9 [arrowhead=none]; 8 -> 10 [arrowhead=none]; 9 -> 10 [color="#aaaaaa" constraint=false]; 10 -> 11 [arrowhead=none]; 10 -> 12 [arrowhead=none]; 11 -> 12 [color="#aaaaaa" constraint=false]; 7 -> 13 [arrowhead=none]; 8 -> 13 [color="#aaaaaa" constraint=false]; 13 -> 14 [arrowhead=none]; 7 -> 15 [arrowhead=none]; 13 -> 15 [color="#aaaaaa" constraint=false]; 15 -> 16 [arrowhead=none]; 15 -> 17 [arrowhead=none]; 16 -> 17 [color="#aaaaaa" constraint=false]; 2 -> 3 [arrowhead=none]; 7 -> 3 [color="#aaaaaa" constraint=false]; 3 -> 4 [arrowhead=none]; 2 -> 5 [arrowhead=none]; 3 -> 5 [color="#aaaaaa" constraint=false]; 5 -> 6 [arrowhead=none]; 2 -> 18 [arrowhead=none]; 5 -> 18 [color="#aaaaaa" constraint=false]; 18 -> 19 [arrowhead=none]; 19 -> 20 [arrowhead=none]; 19 -> 21 [arrowhead=none]; 20 -> 21 [color="#aaaaaa" constraint=false]; 18 -> 22 [arrowhead=none]; 19 -> 22 [color="#aaaaaa" constraint=false]; }

The same, but randomly choose a layout from one of 'circo', 'dot', 'fdp', 'sfdp', 'neato', 'osage', 'patchwork', 'twopi':