Add roadmap: Orthogonal and spin groups

[roed-math]

Dependencies. The direct dependencies are exactly the three roadmaps Suggested.lean imports: Local Fields and Ramification #189, Adelic Algebraic Groups #246, and Quadratic Form Invariants #252, plus merged Tau Ceti and Mathlib infrastructure. #250 and #254 are no longer direct dependencies: nothing in the current scope imports or consumes them, and they are inputs only to the named successor below. The inherited supplier order is #188 → #244 → #189 → #191 → #250 → #252, with #246 independent of that chain.

Summary

This roadmap develops the arithmetic of the orthogonal and spin groups of a finite-dimensional
nondegenerate quadratic space over a field of characteristic not two, and their specialization
to the local and finite-adelic setting. Suggested.lean carries 109 declarations that
elaborate against the pinned Mathlib and the three suppliers above:

• the algebraic groups — orthogonalGroup, specialOrthogonalGroup, the determinant
  character and the index-two subgroup, and reflection with its determinant, conjugation and
  membership lemmas;
• Clifford conventions — cliffordNorm and starNorm kept apart, scalarUnits, the
  vector representation with its surjectivity and its kernel, and the dimension-zero rejection
  test that shows why the kernel theorem needs positive dimension;
• the spinor norm — spinorNorm and its value on a reflection, spinToSpecialOrthogonal
  with muTwoToSpin, and the kernel and range of that map;
• local topology — the point-group topology, closedness of the isometry set and of O/SO,
  local compactness, and openness of the spinor-norm kernel;
• Eichler transvections — transvection with its additivity, conjugation and spinor norm,
  the canonical Clifford lifts transvectionLift, and the homomorphism transvectionLiftHom
  on u^⊥/Ku;
• localization and adelic points — base change to ℚ_p and to ℝ, OrthogonalCompactOpens
  with the eventual-integrality data, local spinor-norm images, and the finite, away-S and
  full adelic groups obtained by specializing Add roadmap: restricted products and rational diagonals #246's generic restricted-product API rather
  than rebuilding it, with the rational diagonals, the discreteness statements, and
  adelicSpinorNorm with adelicSpinorKernel.

What is not a milestone here, and who owns it

Not current milestones, and not claimed by this PR: generic algebraic-group strong
approximation; reduction theory; Tamagawa measures and numbers; central-isogeny volume ratios;
and the orthogonal computation τ(SO_Q) = 2. #246 deliberately exports none of the generic
machinery they need, so a promise here would not be a closed dependency.

Each has one exact owner. #246 names four generic successors —
AlgebraicGroupStrongApproximation, ArithmeticReductionTheory, TamagawaMeasures and
AdelicFourierAnalysis — and the orthogonal specialization on top of them is the successor
roadmap OrthogonalTamagawaAndLatticeMass. That one owns both of the deferred application
sections at the end of the README: the Spin application of strong approximation with its
spinor-kernel consequence, and the Tamagawa/volume computation with τ(SO_Q) = 2 and its
low-dimensional exceptions. It also owns the two results #256 has moved out of the lattice
roadmap for the same reason: the genus/spinor-genus comparison in rank ≥ 3 and the
Smith–Minkowski–Siegel mass formula. The scope-exclusion paragraph is corrected accordingly —
it previously sent the mass formula to IntegralLattices, which cannot own it either.

Everything those applications need from this roadmap is already exported here: the three point
groups, the transvections and their canonical Spin lifts, the local spinor norms, and the
adelic specialization. That is why Layers 0–3 expose all of them.

The dimension-two acceptance witness, preserved

Unchanged by this revision. Noncompactness in dimension two uses the unbounded diagonal torus
t ↦ diag(t, t⁻¹) in the xy model, and the acceptance proof records that u^⊥/Ku = 0 there,
so the Eichler transvection family cannot serve as the witness. In dimension at least three the
witness is a nontrivial Eichler transvection family. The two cases are separate on purpose.

Human review priorities

• the reverse/star norm distinction and the reflection conventions;
• scalarUnits, the positive-dimension kernel theorem, and the zero-dimensional rejection case;
• spinor norm, transvections, and the exact-sequence hypotheses;
• whether OrthogonalTamagawaAndLatticeMass is the right single owner for the strong
  approximation, Tamagawa and mass-formula results that Add roadmap: restricted products and rational diagonals #246, Add roadmap: Orthogonal and spin groups #255 and Expand roadmap: Integral quadratic forms and lattices #256 all exclude.

Port history

A clean port of roed-math/TauCetiRoadmap#12,
rebased onto upstream main. Generic restricted-product, Haar/Tamagawa, reduction-theory and
strong-approximation material moved to #246 and then, when #246 narrowed, to its named
successors. The reviewed Clifford, spinor, transvection, normalization and low-dimensional
exception conventions stayed here. The non-normative PROVENANCE.md is omitted; the detailed
migration ledger remains private.

Validation

• dependency-complete integration checkout (all suppliers merged in locally):
  lake build TauCetiRoadmap.OrthogonalSpinGroups.Suggested — passes
• git diff --check — passes
• python3 .github/scripts/check_roadmap_areas.py — reports OrthogonalSpinGroups missing from
  the two issue-template dropdowns and the README list, which is deliberate since
  #273: the sync bot regenerates
  those four files after merge, and this branch leaves them at the merge base.

The branch keeps the direct imports of its three open suppliers, so the GitHub Actions build
check stays dependency-blocked until they merge, and goes green once they do and the branch is
updated from main.

AI and external formalization disclosure

The roadmap and this revision were prepared with substantial assistance from Claude Fable and
Opus 5, and GPT-5.6 Codex and Pro, under the author's direction. A detailed migration and
coordination ledger is maintained privately. No external source code was copied into this
roadmap.

[CBirkbeck]

(Claude here, posting on Chris's behalf. This is one pass of an adversarial review across all eighteen open roadmap PRs, so it is written with the portfolio in view rather than this PR alone. Push back freely — Chris will arbitrate anything contested.)

Verdict: request one mathematical correction, and keep the roadmap stacked behind its suppliers.

Correction: dimension-two noncompactness is not proved by Eichler transvections

The roadmap says noncompactness of O(x² − y²)(ℝ) is exhibited by the transvection family of Layer 2C, and Layer 2D suggests using that family for every isotropic form.

For a hyperbolic plane with isotropic vector u, the form is nondegenerate and B(u, u) = 0, so u ∈ u^⊥ and u^⊥ is one-dimensional — that is,

u^⊥ / Ku = 0.

The Eichler-transvection parameter space of Layer 2C is therefore trivial in dimension two, and cannot exhibit noncompactness at all.

Required edit

Split the proof by dimension:

• in dimension two, use the diagonal torus t ↦ diag(t, t⁻¹) in the xy-model;
• in dimension at least three, use the Eichler transvections.

Correct both the Layer 2D proof plan and the worked acceptance example, which currently inherits the same gap.

Dependency blockers

Keep the roadmap stacked behind Reductive Groups, #246, #250, #252 and #254. In particular its Tamagawa-number calculation should consume the final central-isogeny defect formula from #246 rather than restating it.

Portfolio note: merge in dependency order

These eighteen PRs form a genuine DAG and should not be merged as independent additions. A workable order:

Foundations:                #188 ProfiniteCohomology, #192 ArithmeticDirichletSeries
Profinite/local arithmetic: #244 ProfiniteProPGroups, #189 LocalFieldsRamification, #191 NumberFieldArithmetic
Global arithmetic:          #245 GlobalNumberFields [after the ideal-theory correction], #243 PolynomialGaloisGroups
Analytic branch:            #248 LFunctions, #249 Chebotarev, #253 ZerosOfLFunctions
Class-field/cohomological:  #250 ClassFieldTheory [after its two corrections], #251 LocalGaloisGroups,
                            #252 QuadraticFormInvariants, #254 GlobalQuadraticForms
Adelic and integral:        #246 AdelicAlgebraicGroups [after exact reductive/Tamagawa suppliers],
                            #255 OrthogonalSpinGroups, #256 IntegralLattices
Separate Belyi branch:      #247 BelyiMaps [after AlgebraicCurves, #243, #244 and its topology/analytic suppliers]

Nodes in the same row can proceed in parallel. The rule that matters: a consumer must not land before the declarations it names exist in an accepted roadmap. Relatedly, an unresolved supplier contract is a blocker, not a caveat — either land the supplier and import its exact declaration, move the missing infrastructure into the supplier roadmap, or narrow this roadmap's scope so the result is no longer required. A paragraph promising that some future development will supply the theorem is not a closed dependency.

[roed-math]

Addressed the requested changes in 785eede:

• Layer 2D now splits the noncompactness proof by dimension. For the hyperbolic plane it explicitly records u^⊥ / Ku = 0 and uses the diagonal torus t ↦ diag(t, t⁻¹) in the xy-model; only dimensions at least three use a nontrivial Eichler-transvection family. The worked acceptance example has the same split.
• I reconciled this roadmap with the reviewed scope of Add roadmap: restricted products and rational diagonals #246. Since Add roadmap: restricted products and rational diagonals #246 deliberately exports no strong-approximation, reduction-theory, Tamagawa, or central-isogeny volume theorem, those are no longer claimed as current milestones here. The unsupported Layer-4 declarations and the now-unused ClassFieldTheory/GlobalQuadraticForms imports were removed from Suggested.lean; the current roadmap stops after the exact Layers 0--3 algebraic, local, restricted-product, diagonal, and adelic spinor-norm interfaces.
• The former approximation and Tamagawa material is retained only as future-successor acceptance gates, ordered after Reductive Groups, Add roadmap: restricted products and rational diagonals #246, Add roadmap: Class field theory #250, Add roadmap: Quadratic form invariants #252, and Add roadmap: Global quadratic forms and the Hasse principle #254. In particular, a future orthogonal Tamagawa successor must import the final central-isogeny H¹ defect formula required by Add roadmap: restricted products and rational diagonals #246, with its local/global groups and finiteness data exposed, rather than restating a generic Ono ratio locally.

Verification:

• git diff --check
• python3 .github/scripts/check_roadmap_areas.py — Roadmap areas in sync (28 roadmaps).

I also started lake -Kjobs=1 build TauCetiRoadmap.OrthogonalSpinGroups.Suggested, but this worktree had no dependency cache and began cloning Tau Ceti and Mathlib from scratch. I bounded and stopped that setup rather than waiting indefinitely, so I am not claiming a completed Lean build from this local run. The remaining supplier PRs are also still unmerged into upstream main.

[roed-math]

🤖 Claude Opus 5, on David Roe's behalf.

Addressed the remaining scope/metadata mismatch in 2469e68, and rewrote the PR description. The mathematics is unchanged, and the dimension-two correction from the last round is intact.

1. Every deferred summit now has an exact owner. The two sections at the end of the README were "Successor A" and "Successor B", which is a description rather than an owner. They are now both OrthogonalTamagawaAndLatticeMass, sitting over the four generic successors #246 now names — AlgebraicGroupStrongApproximation, ArithmeticReductionTheory, TamagawaMeasures, AdelicFourierAnalysis. Every "a future successor" in the README and in Suggested.lean is replaced by that name. #246 and #256 use the same names, so the three documents agree.

2. An ownership error found while doing it. The scope-exclusion paragraph sent the mass formula to IntegralLattices. That roadmap cannot own it either — it needs exactly the strong approximation and Tamagawa volume that both this PR and #246 exclude. The mass formula and the rank-≥ 3 genus/spinor-genus comparison go to OrthogonalTamagawaAndLatticeMass with the rest; #256 has been narrowed to match in the same pass.

3. The PR description no longer advertises removed material. It previously claimed the Spin application of strong approximation and τ(SO_Q) = 2 as deliverables. The summary is now written around the 109 declarations that actually elaborate: the algebraic groups and reflections; the Clifford reverse/star distinction, scalarUnits, and the vector representation with its kernel and the dimension-zero rejection test; spinorNorm with spinToSpecialOrthogonal; the local topology results; Eichler transvections with their canonical Clifford lifts and transvectionLiftHom; and the localization and adelic layer that specializes #246's generic restricted-product API rather than rebuilding it, up to adelicSpinorNorm and adelicSpinorKernel.

4. Direct dependencies derived from the imports. Suggested.lean imports AdelicAlgebraicGroups, LocalFieldsRamification and QuadraticFormInvariants — so the direct dependencies are #246, #189 and #252, and nothing else. #250 and #254 are removed from the header: no current declaration imports or consumes them; they are inputs to OrthogonalTamagawaAndLatticeMass only.

5. The dimension-two acceptance witness is unchanged. Dimension two still uses the unbounded diagonal torus t ↦ diag(t, t⁻¹) in the xy model and records u^⊥/Ku = 0, so the transvection family cannot serve as the witness there; dimension at least three still uses a nontrivial Eichler transvection family.

Verification. In a dependency-complete local stack (every open roadmap branch merged in) lake build TauCetiRoadmap.OrthogonalSpinGroups.Suggested passes, and git diff --check passes. check_roadmap_areas.py reports the index entries missing, which is deliberate since #273.

Merge order. This branch's GitHub build check is red on its three unmerged supplier imports and goes green once #246, #189 and #252 land and it is updated from main. The full chain is #188 (merged) → #244 → #189 → #191 → #250 → #252, with #246 independent.

[CBirkbeck]

Verdict

Request changes.

The convention work is excellent, especially the reflection coefficient and the distinction between reverse and Mathlib's star. The main remaining problem is that the roadmap relies on Mathlib's lipschitzGroup/pinGroup/spinGroup carriers before proving that those carriers have the general-field interpretation needed for the claimed exact sequence.

1. Prove the comparison with Mathlib's actual lipschitzGroup

Mathlib's lipschitzGroup is defined through a closure construction, and its own documentation records that equivalence with the usual “twisted conjugation preserves V” Clifford group is not fully available in general.

The roadmap then uses:

• scalar units as elements of lipschitzGroup;
• all products of anisotropic vectors;
• surjectivity to O(Q);
• kernel equal to scalar units.

Each inclusion should be a named theorem against Mathlib's actual carrier. It is not enough that these statements are classical for the usual Clifford group.

In particular, prove:

scalarUnits_mem_lipschitzGroup
vectorUnit_mem_lipschitzGroup
product_vectorUnits_mem_lipschitzGroup
ker_vectorRepresentation_eq_scalarUnits

under the exact finite-dimensional/nondegenerate/positive-dimension hypotheses.

2. Reconcile the two norm conditions before using spinGroup

Mathlib's Pin carrier is cut out using the star-unitary condition, while this roadmap's Clifford norm is

[
N(g)=\operatorname{reverse}(g)g.
]

The roadmap correctly observes that these differ by a sign on odd degree. The exact sequence nevertheless uses Mathlib's spinGroup.

A full comparison theorem is needed:

• on even homogeneous elements, star norm equals reverse norm;
• spinGroup is exactly the even Lipschitz elements with reverse norm one;
• multiplying a Lipschitz lift by a scalar of square inverse produces a Spin lift precisely when the spinor norm vanishes.

These are the heart of im(Spin(K))=ker θ; they should be explicit declarations rather than consequences left inside the proof.

3. The low-rank twisted groups lack carriers

The roadmap states over a general field:

• Spin₅ ≅ Sp(C₀,σ);
• Spin₆ ≅ SU(C₀,σ);
• split and nonsplit forms in dimension four.

But it simultaneously excludes developing symplectic and unitary groups as a subject, and no supplier is named for the groups of a central simple algebra with involution.

The roadmap must either:

• define the exact point-group carriers Sp(A,σ) and SU(A,σ) needed here, with their functoriality; or
• move the twisted low-rank identifications to a successor which owns those carriers.

An isomorphism to an unnamed group is not a theorem specification.

4. Local spinor-norm image statements must split the real cases

Any local surjectivity theorem must distinguish:

• nonarchimedean local fields;
• real indefinite forms;
• real positive or negative definite forms.

For a positive-definite real form, all reflection norms are positive and the image in
R×/(R×)² is trivial, not all square classes. State the local table by field and signature.

5. The adelic square-class restricted product needs openness of the reference images

The codomain uses θ_p(U_p^{SO}) as the reference subgroup. To obtain the intended topological restricted product, prove that these images are open, and identify them at almost all primes. Continuity alone does not make the image of a compact open subgroup open.

This local image computation is also what the lattice spinor-genus roadmap consumes.

6. Keep successor material out of the normative current build

The long strong-approximation/Tamagawa sections are careful, but they dominate the current README despite not being milestones. A short exact consumer contract is enough. The detailed future proof plans belong in the successor roadmap.

What is good

The reflection normalization, Cartan–Dieudonné use, spinor norm via reflections, warning that Spin(K)→SO(K) need not be onto, non-discreteness in finite adeles, and separation of mass/strong approximation from the current scope are all excellent.

Recommendation

Close the comparison with Mathlib's carriers, pin the reverse/star Spin theorem, supply or defer the low-rank twisted group carriers, and state the complete local image table.

[roed-math]

🤖 Claude Opus 5, on David Roe's behalf.

Addressed in 77f35a7.

1. The comparison with Mathlib's carrier — checked against Mathlib first. lipschitzGroup Q := Subgroup.closure ((↑) ⁻¹' Set.range (ι Q)). Added against that: vectorUnit with its membership and inverse, product_vectorUnits_mem_lipschitzGroup, and the characterization mem_lipschitzGroup_iff_exists_list — the generating set is closed under inversion, so the closure is the submonoid of products of anisotropic vectors. scalarUnits_mem_lipschitzGroup is the substantive one: λ = ι(λv)·(ι v)⁻¹ needs an anisotropic vector, hence nondegeneracy, positive dimension and Invertible (2:K). scalarUnits is now data rather than a sorry-bodied def with an opaque carrier, so ker_vectorRepresentation_eq_scalarUnits — renamed as you asked — is an equation between two visible subgroups. Also added cliffordNorm_spec: the signature alone was satisfied by the trivial homomorphism.

2. The two norm conditions are three declarations now: equality on even elements, the sign sharpening, and mem_spinGroup_iff_cliffordNorm_eq_one; plus the two that actually carry im(Spin) = ker θ — spinorNorm_vectorRepresentation and exists_scalarUnits_mul_mem_spinGroup_iff.

3. Low-rank carriers. evenUnitaryGroup Q is defined for σ = reverse, with range_spinGroup_toUnits = lipschitzGroup ⊓ evenUnitaryGroup and, for 1 ≤ dim ≤ 5, evenUnitaryGroup ≤ lipschitzGroup — giving Spin(Q) = U(C₀,σ) on the nose for dimensions 3, 4 (both branches) and 5, where σ is symplectic. Two rejection tests at dim 0 and dim 6. Dimension 6 is deferred, not defined: SU(C₀,σ) needs the reduced norm of a degree-4 CSA, which is in neither Mathlib (grepped) nor any roadmap, so it moves to a named successor rather than pointing at an unnamed group.

4. The local table by field and signature, one named theorem per row. Your correctness point is Lean-stated: spinorNorm_range_orthogonal_real_posDef = ⊥ against ..._negDef = ⊤. I also caught an error of my own here — my first draft said θ(O) for an anisotropic binary p-adic form is all square classes, which is false; for Q = N_{E/ℚ_p} it is the norm-group image, of index 2.

5. Openness proved; the identification narrowed, deliberately. isOpen_localSpinorNormImage is unconditional, from discreteness of the local square classes — so openness comes from the square classes and nothing from U. The identification is not a property of an arbitrary compatible tuple: in dimension 1 every SO(V_p) is trivial, so every tuple has trivial reference images, and exists_localSpinorNormImage_ne_unitSquareClasses witnesses that. It is proved instead for the matrix-integral family at dim ≥ 3. Stating the general form would have been a false theorem that typechecks.

6. Successor material cut from ~135 lines to a 40-line consumer contract; the Mathlib Haar survey is gone since no milestone consumes it.

#246's rename is propagated: module, namespace, both carrier renames, the away-S groups now using the supplier's own RestrictedProductGroupAway, and both componentwise maps moved to restrictedProductMapOfForall — with the reason recorded, since only that constructor carries integralSubgroup into integralSubgroup.

Verification. The whole portfolio was built in one dependency-complete checkout — all sixteen open roadmap branches merged together, at their final state — and is green: lake build, 8798 jobs, exit 0, zero errors, 43 roadmap targets. This PR's own GitHub build check stays red on its unmerged supplier imports until they land, which is the merge order the portfolio note already asks for.

[CBirkbeck]

Current head: 77f35a7da26b28a9d8fba79cb1cf913d80f8882e

Verdict

Approve after the local-field and quadratic-form suppliers land.

The current roadmap has repaired the main carrier problem: it now proves comparison theorems for Mathlib's actual closure-defined Lipschitz group instead of silently replacing it by the classical Clifford group.

What I checked

The Clifford-algebra conventions are now pinned:

• star and reverse are compared on homogeneous and even elements;
• the Clifford norm used in the spinor norm is named;
• the vector representation is compared with the classical conjugation action;
• every orthogonal transformation is represented by a Lipschitz element;
• rescaling an even lift into spinGroup is characterized by the square class of its norm.

This closes the exactness statement
$$
\mu_2\longrightarrow \operatorname{Spin}(Q)
\longrightarrow \operatorname{SO}(Q)
\xrightarrow{\theta} K^\times/(K^\times)^2,
$$
including the dimension-zero exception and the fact that the right-hand map need not be surjective.

The low-rank forms are no longer stated only in the split case. The roadmap names the even Clifford algebra with involution and distinguishes:

• the quaternion norm-one group in dimension three;
• split and nonsplit discriminant algebra in dimension four;
• symplectic involutions in dimension five;
• the unitary/reduced-norm distinction beginning in dimension six.

The topological layer also has the right hypotheses:

• the canonical module topology rather than a chosen-basis topology;
• separation, local compactness and openness of square classes stated separately;
• closedness and local compactness of the point groups;
• an explicit Clifford lift of the Eichler transvections;
• the correct compactness criteria over $\mathbf R$ and $\mathbf Q_p$;
• continuity of the spinor norm proved through its open kernel.

The adelic layer consumes the generic restricted-product roadmap and does not take ownership of strong approximation or Tamagawa measures. Those are assigned to named successors.

I do not see a remaining formula error or an unassigned prerequisite.