Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Normalized Pin products and Clifford norm

Statement

Let Γ, Pin, Spin⁡full, N(x)=xxˉ, and ρ have the definitions in Real Clifford group, Pin, and the two Spin subgroups and Clifford involutions and the norm of a vector product. Then N is scalar-valued and multiplicative on Γ. For x=u1⋯uk with anisotropic uj,

N(x)=∏j=1k(−Q(uj)).

Pin is exactly {x∈Γ:N(x)∈{1,−1}}. If dim⁡V>0, it is the subgroup generated by ∣Q(u)∣=1 vectors and consists of normalized anisotropic-vector products; its even part consists of the even products and is Spin⁡full. For V=0, Pin⁡(0)=Spin⁡full(0)=Spin⁡N=1(0)={1,−1}. In every dimension, Spin⁡N=1 is the norm-one subgroup of the full even group.

Facts & Assumptions

Given: The real quadratic space and group definitions above.

[F1]

The norm of a product of anisotropic vectors is the product of the scalar norms −Q(uj) (Clifford involutions and the norm of a vector product).

[F2]

In positive dimension, Pin is generated by vectors with ∣Q(u)∣=1; in dimension zero, Pin is {1,−1}. Full Spin is its even subgroup (Real Clifford group, Pin, and the two Spin subgroups).

[F3]

Γ is a group acting orthogonally; an anisotropic vector acts by its reflection. The action has scalar kernel and every element of Γ is scalar times a product of anisotropic vectors (Twisted Clifford action, reflections, and scalar kernel).

[F4]

Every orthogonal map factors into anisotropic reflections (Cartan–Dieudonné factorization over a real quadratic space).

Proof

technique · direct
1.1F1F3algebra

For a vector product, [F1] makes N(x) a real scalar. By [F3], every x∈Γ is λu1⋯uk for λ∈R× and anisotropic uj; N(λ)=λ2, so N(x) is scalar. For scalar-valued norms, N(xy)=xyyˉxˉ=xN(y)xˉ=N(y)N(x), which proves multiplicativity.

2.1F1F2F3step 1.1algebra

The empty product has norm N(1)=1. Every normalized vector belongs to Γ by [F3], has inverse u/Q(u)=±u, and has norm N(u)=−Q(u)∈{1,−1}. Thus subgroup words are normalized-vector products, and multiplicativity in step 1.1 shows that they have norm ±1. In dimension zero Pin is {1,−1}, and both scalars belong to Γ and have norm 1. Hence Pin is contained in the asserted norm locus in every dimension.

3.1F2F3F4step 1.1step 2.1construct

Conversely, take x∈Γ with N(x)=±1. By [F4], factor ρx into reflections and lift them by normalized vectors to a product y with ρy=ρx. By [F3], xy−1=λ is a nonzero scalar, and step 1.1 gives N(x)=λ2N(y). Since both norms are ±1 and λ2>0, λ2=1, so λ=±1. If dim⁡V>0, −1 is itself a product of normalized vectors: for Q(u)=1, u(−u)=−1, and for Q(u)=−1, u2=−1. If V=0, it is included by definition. Thus every norm-±1 element lies in Pin.

4.1F1F2F3step 1.1step 3.1algebra∎

The grading parity of a vector product is its number of factors modulo two, and nonzero scalars are even. In positive dimension, the even elements of Pin are therefore exactly the even normalized products, which are Spin⁡full by [F2]. In dimension zero every Clifford element is scalar by [F3], so both signs are even and have norm 1, giving all three groups {1,−1}. In every dimension the definition of Spin⁡N=1 selects the norm-one subgroup; multiplicativity in step 1.1 ensures that it is a subgroup.

Remarks

The norm of an even product can be −1 in mixed signature; “full even Spin” and “norm-one Spin” are intentionally distinct definitions.

Depends on

Used by

Cited to discharge well-definedness by Real Clifford group, Pin, and the two Spin subgroups.

Dependency tree · two levels

8 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources