Expand roadmap: Integral quadratic forms and lattices

[roed-math]

Dependencies. This roadmap extends the one merged in Integral Lattices #200. Its direct dependencies are exactly the six roadmaps Suggested.lean imports: Quadratic Form Invariants #252, Global Quadratic Forms #254, Global Number Fields #245, Class Field Theory #250, Adelic Algebraic Groups #246, and Orthogonal and Spin Groups #255, plus merged Root Systems and Mathlib. The inherited supplier order is #192; #188 → #244 → #189 → #191 → #245 → #246+#250 → #252 → #254 → #255 → this.

Summary

This expands the IntegralLattices roadmap merged in #200 to the arithmetic of integral
lattices over ℤ and ℤ_p: Gram and discriminant data, dual lattices and discriminant forms,
localizations and Jordan theory, Conway–Sloane genus symbols, classes and spinor genera, binary
lattices and quadratic-order ideal classes, Nikulin's existence/uniqueness/embedding theory,
unimodular lattices in low rank, the local ingredients of a mass, theta series, and the
assertion semantics of the LMFDB lattice records.

It extends #200 rather than adding a second lattice roadmap. The embedded IntegralLattice
stays the sole public carrier, and #200's reviewed radical/signature, dual-lattice,
discriminant-module, gluing, ADE, and D₈⁺ ≅ E₈ routes all survive into the expanded
programme.

What this revision changes: the mass formula moves out

The reviewed scopes of #246 and #255 deliberately export no generic strong approximation,
reduction theory, Tamagawa measure, or central-isogeny volume comparison. This roadmap was
still resting on all four, which is a prose reference to a removed milestone rather than a
closed dependency. The affected results now have one exact owner — the successor roadmap
OrthogonalTamagawaAndLatticeMass, which #255 and #246 name from their side:

Moved out	Was	Why it cannot stay
Eichler's theorem cls⁺ L = spn⁺ L, and the class-number finiteness in rank ≥ 3 that follows	4D, and the rank-≥ 3 half of 4E	needs strong approximation for Spin, which no accepted roadmap proves
the adelic decomposition of SO(V)(ℚ) \ SO(V)(𝔸) into class-indexed pieces	7B	needs a Tamagawa measure
the identity vol(K_p(L)) = α_p(L) in the Tamagawa normalization	one bullet of 7C	the gauge-form measure is undefined without that normalization
the volume theorem vol(SO(V)(ℚ) \ SO(V)(𝔸)) = 2	7F	#255 states that only the successor may export it
the Smith–Minkowski–Siegel formula and its checks	7H	assembled from 7B and 7F
rank-16 completeness: the genus of E₈² has exactly two classes	7I	needs 7H

Everything the successor will need from the lattice side stays here, so the split leaves no
gap between the two documents: the class/genus/proper-genus sets and the stabilizer dictionary
(4A, 4B), spinor genera and the proper-spinor-genus class group (4C), the automorphism-group
infiniteness argument (4F), Kneser neighbours (4G), the two masses and the relation m⁺ = 2m
(7A), the local densities at odd p (7C) and Cho's dyadic density at 2 (7D), the archimedean
factor (7E), and the low-rank values in ranks 0, 1 and 2 (7G). Those are lattice arithmetic and
use no adelic volume. Rank 2 of 4E likewise stays, since it runs through the binary
correspondence B2/B5 and the Picard group, not through strong approximation.

Suggested.lean follows: it no longer #checks
OrthogonalSpinGroups.strongApproximation_finiteAdelicSpin, a name #255 does not export and
has said only the successor may. In its place it checks four declarations #255 does export and
this roadmap does consume — OrthogonalCompactOpens, finiteAdelicOrthogonal, transvection,
transvectionLiftHom. Every remaining #check names a declaration its supplier actually
exports.

A second commit: the dependency-complete build did not actually pass

An earlier revision of this description said a dependency-complete build of this target passes.
It did not. With every supplier branch merged locally, Suggested.lean reported 25 errors, which
GitHub's build check cannot see because it fails earlier on the seven unmerged imports. They are
repaired here, and none of them changes a statement:

• formTwist is a sorry-bodied def whose type does not mention L, so Lean dropped the
  section variable and every L.formTwist a failed. L is now bound explicitly.
• discriminantBilinearModule and discriminantQuadraticModule were sorry-bodied records,
  which makes their carrier A opaque — and then AddSubgroup L.DiscriminantGroup does not match
  AddSubgroup (…).A, so the isotropic, Lagrangian and overlattice statements of Layer 1, and the
  D₈⁺ ≅ E₈ artifact, could not be written at all. The carrier and the pairing are now data:
  the bilinear module is built on L.DiscriminantGroup with discriminantPairing, the quadratic
  module on it with discriminantQuadraticForm. Only symmetric and polar stay milestones.
• LocalCarrier and CompletedAmbient use ℤ_[p] and ℚ_[p] and were missing [Fact p.Prime],
  so the whole Layer 3 localization block failed to elaborate.
• the Layer 3G Hilbert-reciprocity check passed no field to ClassFieldTheory's
  finiteHilbertSupport, finiteHilbertInvariantAt and infiniteHilbertInvariantAt, which take
  it explicitly, nor to QuadraticFormInvariants.hilbertSymbol_productFormula, which now binds
  its own field at universe 0 because Class Field Theory pins its cohomology there.

Ownership

One canonical owner per prerequisite: local forms from #252; global rational classification
from #254; number-field orders, the ideal class monoid, Pic and NarrowPic from #245;
nonsplit ring class fields from #250; generic restricted products and rational diagonals from
#246; the orthogonal groups, the spinor norm and the finite-adelic point groups from #255;
Poisson summation and the real-parameter Gaussian transform from #248; ADE from merged Root
Systems. The LFunctions dependency is one-way: it supplies the analytic Gaussian identity,
this roadmap owns the arithmetic theta series and its transformation, and no L-functions
milestone imports a lattice theorem. Modularity and half-integral weight stay outside.

Corrections preserved from earlier rounds

Unchanged by this revision, and listed so a re-review can confirm no regression: raw proper
fractional ideals versus invertible proper fractional ideals, with Pic/NarrowPic only on
the invertible carrier and a separate ideal class monoid for the noninvertible ones; the
square-discriminant split branch treated separately from the nonsplit one; formTwist versus
carrier dilation; full-submodule versus rational-span restriction; the half-norm
discriminant-form convention in ℚ/ℤ with Nikulin's ℚ/2ℤ reached only through an explicit
dictionary; the nondegeneracy hypothesis in the Nikulin decomposition; and the rank-one and
D₈⁺ ≅ E₈ acceptance artifacts.

Human review priorities

• the successor split above — whether the line between 7A/7C/7D/7E/7G and 7B/7F/7H/7I is in the
  right place, and whether OrthogonalTamagawaAndLatticeMass is the right single owner for the
  far side;
• that nothing in Layers 0–6, 8 and 9 still leans on a removed supplier;
• preservation of Add roadmap: integral lattices and discriminant forms #200's embedded carrier and half-norm discriminant-form convention;
• the dyadic Jordan/genus-symbol boundary and Cho's normalization in 7D;
• theta-series ownership and the one-way LFunctions dependency.

Validation

• dependency-complete integration checkout (all seven suppliers merged in locally):
  lake build TauCetiRoadmap.IntegralLattices.Suggested and a whole-repository lake build
• python3 .github/scripts/check_roadmap_areas.py — passes (this roadmap already has its README
  line and dropdown entries from Add roadmap: integral lattices and discriminant forms #200)
• git diff --check — passes

The PR branch keeps the direct imports of its seven open suppliers, so the GitHub Actions
build check stays dependency-blocked until those PRs merge; it goes green as soon as they do
and the branch is updated from main. This PR is not a draft — an earlier revision of this
description said it was, which was wrong.

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 changes inherited from #245, and keep the late layers stacked behind their suppliers.

Required mathematical correction

The binary quadratic-form / order correspondence must use the Picard group of invertible proper ideals, not all proper ideals — for a general number-field order, proper does not imply invertible (see #245). If noninvertible ideals are to be classified, they form a separate ideal class monoid and do not parameterise the Picard group.

Audit every binary-form milestone consuming

NumberFieldOrder.properIdeals
Pic O
NarrowPic O

once #245 is repaired.

Dependency changes

The early lattice, discriminant-form and Jordan layers may be reviewed independently. The later parts are not ready to land before #245 (orders and Picard groups), #246 (adelic measure carriers), #252 and #254 (local/global quadratic forms), and #255 (spinor genera and strong approximation). The mass formula and spinor-genus applications should import those final declarations rather than recording prose contracts.

Structural recommendation

The internal boundaries are good enough that this may remain one broad roadmap, but the implementation should be staged in at least three PRs: (1) integral and p-adic lattices, discriminant forms and genera; (2) binary forms/orders and Nikulin embeddings; (3) spinor genera, mass formula and theta series.

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]

Authorship disclosure: This update was prepared and posted by GPT-5.6 Codex on behalf of David Roe.

Addressed the required binary-form/Picard correction in e9a006a, against the corrected Global Number Fields contract from #245 (1035a24):

• replaced the obsolete NumberFieldOrder.properIdeals group contract with the exact split between raw properFractionalIdeals and group-valued invertibleProperFractionalIdeals;
• made B2 first prove that the binary-form ideal is proper and then use isProper_iff_isUnit_of_finrank_eq_two at the quadratic-field boundary before passing it to mkPic or NarrowPic;
• recorded that noninvertible proper ideals belong to IdealClassMonoid, with picEquivUnitsIdealClassMonoid identifying only its units with Pic;
• audited the B1--B5 supplier table, B2--B5 narrative, the rank-two class-number application, and the representative Lean contracts so that every group-valued use is explicitly invertible;
• added direct checks for the corrected Add roadmap: Global number fields, ray classes, adeles, and Hecke characters #245 declarations, including the raw and invertible carriers, the quadratic specialization, the ideal class monoid, and the narrow-to-wide map.

The dependency feedback remains enforced: the later spinor-genus and mass layers directly import their supplier roadmaps, introduce no local substitute carriers, and PR #256 remains sequenced after #245, #246, #252, #254, and #255. README-only supplier milestones are still identified as such and must be replaced by accepted declarations before this consumer lands.

Verification:

• python3 .github/scripts/check_roadmap_areas.py — passes on the PR branch;
• git diff --check — passes;
• a disposable integration stack was assembled through Add roadmap: Orthogonal and spin groups #255 with corrected Add roadmap: Global number fields, ray classes, adeles, and Hecke characters #245 layered in.

The Lean target build was not completed in this run: the disposable checkout started without a dependency cache, and the bounded lake exe cache get attempt was stopped while fetching caches. This is a validation limitation, not a claimed pass; the branch remains intentionally supplier-dependent until the upstream PRs land.

The recommendation to split implementation into three future PRs is staging guidance rather than a correction to this roadmap PR; the roadmap already exposes the corresponding early/local, binary/Nikulin, and spinor/mass/theta boundaries.

[roed-math]

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

Addressed the architectural blocker in cda777f, repaired the targets a dependency-complete build rejects in 428d1b3, and rewrote the PR description. The mathematical corrections from the earlier rounds are all intact.

The blocker was: "the README still relies on strong-approximation and Tamagawa results that the final scopes of #246 and #255 explicitly no longer own. A prose reference to removed supplier milestones is not a closed dependency."

Response: narrow, and give the removed summit one exact owner. That owner is OrthogonalTamagawaAndLatticeMass, the orthogonal specialization #255 and #246 now name from their side, sitting over #246's generic AlgebraicGroupStrongApproximation, ArithmeticReductionTheory and TamagawaMeasures. Moved out:

Moved out	Was	Why it could not stay
Eichler's theorem cls⁺ L = spn⁺ L, and the rank-≥ 3 class-number finiteness that follows	4D, half of 4E	needs strong approximation for Spin
the adelic decomposition of SO(V)(ℚ) \ SO(V)(𝔸)	7B	needs a Tamagawa measure
vol(K_p(L)) = α_p(L) in the Tamagawa normalization	one bullet of 7C	the gauge-form measure is undefined without it
the volume theorem vol(SO(V)(ℚ) \ SO(V)(𝔸)) = 2	7F	#255 says only the successor may export it
the Conway–Sloane mass formula and its checks	7H	assembled from 7B and 7F
rank-16 completeness	7I	needs 7H

What stayed, and why the split leaves no gap. Everything the successor consumes from the lattice side is still a milestone here: 4A class/genus sets, 4B the stabilizer dictionary and the two double-coset correspondences, 4C spinor genera with the proper-spinor-genus class group, 4F, 4G, rank 2 of 4E through B2/B5, 7A the two masses with m⁺ = 2m, 7C's local density at odd p, 7D Cho's dyadic density, 7E the archimedean factor, and 7G the low-rank values in ranks 0, 1 and 2. None of those uses an adelic volume. Layer 7 is retitled "masses, local densities, and the archimedean factor" accordingly, and each moved milestone carries an Owner: line so a reader who opens the file in the middle cannot mistake a specification for a claim.

A concrete supplier defect this exposed. Suggested.lean contained

#check OrthogonalSpinGroups.strongApproximation_finiteAdelicSpin

and #255 does not export that declaration — its README says explicitly that only the successor may. So the file could not have elaborated even in a fully merged stack. It is removed, and in its place are four names #255 does export and this roadmap does consume: OrthogonalCompactOpens, finiteAdelicOrthogonal, transvection, transvectionLiftHom. Every remaining #check names a declaration its supplier actually exports.

Scope and dependency tables rewritten. The out-of-scope table drops the claim that #255 owns "the orthogonal Tamagawa theorem" and that #246 owns "strong approximation and Tamagawa measures", and gains rows for the generic and orthogonal successors. The supplier table's #246 and #255 rows now list only exported declarations. The ordering section, the API checklists, the hard-theorem table, and the worked examples follow.

Stale metadata fixed. The description said the PR was a draft; it is not, and the new description says so. The dependency-chain link labelled #255 pointed at /pull/254; corrected. The summary no longer claims the mass-formula summit.

Corrections preserved from earlier rounds, listed so a re-review can confirm no regression: raw proper fractional ideals versus invertible proper fractional ideals, with Pic/NarrowPic only on the invertible carrier and a separate ideal class monoid for the noninvertible ones; the square-discriminant split branch; formTwist versus carrier dilation; full-submodule versus rational-span restriction; the half-norm discriminant-form convention in ℚ/ℤ, with Nikulin's ℚ/2ℤ reached only through the explicit dictionary; the nondegeneracy hypothesis in the Nikulin decomposition; and the rank-one and D₈⁺ ≅ E₈ acceptance artifacts.

Verification. In a dependency-complete local stack (every open roadmap branch merged in) lake build TauCetiRoadmap.IntegralLattices.Suggested and a whole-repository lake build both pass. check_roadmap_areas.py and git diff --check pass.

Merge order. This is the last node of the arithmetic portfolio: its build check is red on its seven unmerged supplier imports and goes green once #252, #254, #245, #250, #246, #255 and #248 land and the branch is updated from main.

[CBirkbeck]

Verdict

Request changes.

This is one of the strongest roadmaps in the collection. It has corrected several subtle errors in binary masses, dyadic symbols and Nikulin's hypotheses. The remaining problems are mostly dependency closure: the dyadic local-density layer and the certificate layer claim objects for which no current algebraic-group or mass supplier exists.

1. The dyadic local-density milestone is a roadmap-sized algebraic-group construction

Layer 7D asks for Cho's smooth affine group scheme 𝒢_L, its special fibre, unipotent radical and reductive quotient, for a general unramified extension of Z₂.

No current roadmap supplies:

• smoothening of the orthogonal group scheme;
• special fibres and reductive quotients of affine group schemes;
• dimensions and point counts of the unipotent radical;
• the comparison of the smooth-model density with the congruence-count limit.

This is not a small lattice calculation. Either:

• expand 7D into an exact construction chain with an algebraic-group-scheme supplier; or
• move it to OrthogonalTamagawaAndLatticeMass, which already owns the measure comparison.

It is inconsistent to say that all algebraic-group measure infrastructure is out of scope while constructing the most delicate smooth integral model locally inside this roadmap.

2. The Nikulin existence predicate must be a typed object, not only a table in prose

Nikulin's boundary-rank conditions at p=2 are the highest-risk part of the roadmap. The exact predicate should be represented in Suggested.lean, including:

• l(A_{q_p});
• determinant square-class conditions at equality;
• the special dyadic alternatives;
• the signature/Brown-invariant congruence.

Then the theorem should literally say that the predicate is necessary and sufficient.

A generic field named localConditions would not be enough. The point of the roadmap's careful source audit is to prevent one omitted boundary clause.

The same applies to the 2-elementary admissibility predicate.

3. Separate certificate semantics from completeness proofs

The LMFDB-facing StoredGenusCertificate may safely assert:

• Gram matrix;
• local symbols;
• minima and shell counts;
• automorphism order;
• membership in a genus;
• pairwise nonisometry.

It cannot internally certify a complete class list unless it imports either:

• the mass formula;
• a proved connected neighbor graph in the exact regime;
• or another independent completeness theorem.

Those were deliberately moved to OrthogonalTamagawaAndLatticeMass. Make completeness a separate downstream certificate whose assumptions include an imported exact mass or connectivity theorem. Do not leave a class_number field suggesting that the current roadmap proves exhaustiveness.

4. The finite class-number statements need their proof owner visible

For positive-definite lattices, finiteness follows from reduction/bounded Gram matrices and can remain here. For indefinite rank at least three, the roadmap correctly moves Eichler/strong approximation out.

Ensure that no generic finite_genusClassSet theorem in this roadmap silently covers the indefinite high-rank case. The statement should branch:

• positive definite: proved here by reduction;
• indefinite rank two: proved here by ideal classes;
• indefinite rank at least three: successor.

5. The binary ring-class comparison should be restricted to the nonsplit quadratic branch

The roadmap mostly does this correctly. Make it impossible in the API to ask for a ring class field of the split quadratic algebra Q×Q. The split branch has an elementary ideal/class description and no quadratic field ring class field.

6. The theta-series endpoint should be described as a transformation law, not modularity

The roadmap correctly moves modularity out. Ensure the exported theorem says precisely:

• convergence and holomorphy;
• Poisson transformation under S;
• parity/translation under T;
• vector-valued transformation for discriminant cosets where developed.

Do not call this isModularForm until a modular-forms carrier and cusp-holomorphy theorem are imported.

What is good

The single embedded lattice carrier, bilinear-first convention over Z, discriminant-form and gluing theory, correction of the proper/full binary mass relation, Conway–Sloane dyadic calculus, exact Nikulin boundary warnings, and removal of the unsupported mass formula are all excellent.

Recommendation

Either provide a real algebraic-group supplier for 7D or move that construction, type the Nikulin condition tables, and split semantic records from downstream completeness certificates. After that the roadmap will have a clean and trustworthy boundary.

[roed-math]

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

Addressed in 12ce6e4.

1. Cho's dyadic density moved out — after checking there is no supplier. Reductive Groups works over a field and its integral group schemes are the split Chevalley–Demazure ones, which 𝒢_L is not; nothing anywhere supplies smoothening, integral models of orthogonal group schemes, or unipotent-radical point counts. 7D is now owned by OrthogonalTamagawaAndLatticeMass, with a paragraph saying why its reason differs from 7B/7F/7H/7I. To keep the split gapless, new milestone 3I stays here and holds the lattice-side data: type I/II, bound/free, Cho's N_M, N_Q and the identity N = t + ∑_{i<j} i·n_i·n_j + ∑_i d_i − b + c, with well-definedness from O'Meara 93:28/93:29. 7C is rescoped rather than moved: its limit and stabilization already covered p = 2, so α_2 is still constructed here and the successor only evaluates it.

2. The Nikulin conditions are typed. NikulinExistenceConditions has one field per clause of Thm 1.10.1 — the signature congruence, l(A_{q_p}), the odd boundary at equality with sign (−1)^{t₋}, and the dyadic boundary with its no-q_θ^{(2)}(2)-summand alternative — stated as a literal ↔. TwoElementaryAdmissible likewise for Thm 3.6.2, with twoElementaryAdmissible_independence pinning four witness tuples that show clauses 4–7 are independent. A localConditions-style field is named as an explicit rejection test, since that is what would defeat the exercise.

3. Certificate split. StoredGenusCertificate loses reps_complete, classNumber and classNumber_eq; StoredClassNumberCertificate extends it with a mass and the named import mass_isGenusMass, so completeness is a theorem whose assumption names the imported result rather than a field implying exhaustiveness.

4. Finiteness branches are three named theorems — positive definite by reduction, indefinite rank 2 by ideal classes — with a ⚠ block forbidding a generic statement that would silently cover indefinite rank ≥ 3, and naming 4D and the rank-≥3 half of 4E as the successor's.

5. The split branch is unaskable: binaryRingClassField carries ¬ IsSquare Δ in its type, with not_isField_splitQuadraticAlgebra as the rejection test.

6. Theta gains 8F and 8G — the T and S laws, the coset theta and its vector-valued transformation — and nothing is called isModularForm; both the scope section and the Lean section say what an import would have to supply first.

Two notes. B7 cited two supplier layers that no longer exist ("Restricted Products Layers 3, 6, 7" and "Orthogonal and Spin Groups Layer 5"); both are repaired to name exact declarations. And a latent trap I found but deliberately did not change: discriminantQuadraticForm and discriminantPairing are sorry-bodied defs whose types do not mention [L.IsNondegenerate], so the section instance is silently dropped and both apply to degenerate lattices. Nothing is false — the formulas need no nondegeneracy — but if you want the convention visible in those two types, say so and it is a one-line change each.

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.

[roed-math]

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

Follow-up in b74954e, resolving the one open note from my previous comment. The nondegeneracy convention is now visible in the types: discriminantPairing and discriminantQuadraticForm carry [L.IsNondegenerate] written inline — inline rather than as a section variable, because a sorry-bodied def whose type does not mention the instance silently drops it, which is exactly how the convention went invisible in the first place. A comment on each records the reason so the binder is not "simplified" away later. discriminantBilinearModule and discriminantQuadraticModule pick the instance up from the section as before.

[mrdouglasny]

🤖 Claude Opus 5, supervised by Michael Douglas.

A review from the applications side rather than the formalization side: what this roadmap
gives mathematical physics, and where the boundary as drawn would leave a physics consumer
stranded. I have not checked the Nikulin or Conway–Sloane statements against their sources —
other reviewers are doing that — so nothing below is a correctness claim. The concern is
coverage and ownership, and it bears directly on two of the listed human review priorities:
the successor split, and theta-series ownership.

Summary. The framing of this roadmap is LMFDB plus the K3 pipeline, and that framing
undersells it. Layers 1 and 5 and milestone 6A are, close to line for line, the mathematics
of charge lattices, defect groups, and string compactification. Three gaps matter for that
audience; two of them are cheap and sit inside layers that already exist, and the third is a
naming action rather than a scope addition.

What is already here

Milestone	What it is, on the physics side
1C, 1D — A_L = L⋆/L, b_L : A_L × A_L → ℚ/ℤ, q_L(x̄) = B(x,x)/2	the defect group of a charge lattice, the Dirac pairing mod 1, and the topological spin of a line operator
1E, 1F — isotropic subgroups ↔ integral and even overlattices, with A_M ≅ H^⊥/H	the choices of global form of a gauge theory, that is the maximal mutually local sets of line operators; H^⊥/H is the anyon-condensation formula for what survives gauging
1F — the glued lattice is unimodular exactly when H is Lagrangian	an absolute theory, as opposed to a relative one, exists exactly for a Lagrangian subgroup
1H, 1I — the Gauss-sum invariant sign q ∈ ℤ/8, and Milgram	Gauss–Milgram: the chiral central charge mod 8 of the associated abelian anyon theory, equivalently the framing anomaly of the Chern–Simons theory with K-matrix G
5A — the genus of an even lattice is determined by (t₊, t₋, q_L)	a K-matrix theory is determined by signature, defect group and spins, and by nothing else
5D — U ⊕ T and E₈(−1) ⊕ T stabilization	adding invertible sectors does not change the anomaly
5E and 5J — O(T) → O(q_T) is surjective for indefinite T	every duality action on the one-form symmetry is realized by an honest lattice isometry; this is the input to the statement that S-duality permutes the global forms of N = 4 super Yang–Mills
6A — the indefinite unimodular classification	the Narain theorem: II_{d,d} ≅ U^d is the uniqueness of the Narain lattice and hence of the T-duality moduli space, and II_{16+d,d} ≅ U^d ⊕ E₈² for d ≥ 1 is why the two ten-dimensional heterotic strings become one theory on a circle. It also covers II_{25,1}
6E — the 24 Niemeier lattices	heterotic on T²⁴, CHL orbifolds, moonshine
8G — the vector-valued law on discriminant cosets	the characters of a lattice conformal field theory, with their S and T matrices

One convention decision is worth endorsing explicitly, since the discriminant-form convention
is on the review-priority list. Choosing q_L : A_L → ℚ/ℤ with q_L(x̄) = B(x,x)/2, rather
than Nikulin's ℚ/2ℤ, is the convention physics uses: q_L(μ) is the topological spin mod
one, and 8G's characters e^{2πi q_L(μ)} are then the T-matrix of the conformal field
theory with no factor to insert. The roadmap notes that the half-norm convention is what makes
8G come out clean; it is also what makes the resulting Lean statements directly quotable
outside mathematics. Keep it, and keep Nikulin's convention reachable only through the
dictionary, exactly as written.

Three gaps

1. The duality groups themselves have no owner. The scope section lists "automorphism
groups of indefinite lattices, and Borcherds' method" among the subjects with no owner. But
O(Γ^{d,d}; ℤ) is the T-duality group, O(Γ^{16+d,d}; ℤ) the heterotic duality group, and
O⁺(II_{25,1}) the object behind the fake monster algebra and the one-loop heterotic
amplitude. What this roadmap proves about them is 4F, that O(L) is infinite.

Deferring them is the right call for this PR; leaving them unowned is not. The revision's own
standard — a prose reference to a removed milestone is not a closed dependency — applies to
consumers as well as to suppliers, and an unowned subject on the boundary list is
indistinguishable from an oversight. I would ask that the boundary list name a successor here
the way the adelic material was given OrthogonalTamagawaAndLatticeMass; something like
IndefiniteLatticeAutomorphisms, owning reflection subgroups, the Eichler criterion for
O(L)-orbits, and Borcherds' fundamental domains. That is one row in a table, not a scope
increase, and it converts "nobody has thought about this" into "deliberately deferred to a
named place".

2. Layer 8 cannot express a Narain partition function. Every theta milestone assumes
PosDef, and the conventions section gives the right reason: for an indefinite form the
series diverges. The physics object is the Siegel–Narain theta, which is defined for
indefinite L given a point of the Grassmannian — a maximal positive definite subspace
v ⊆ L ⊗ ℝ, that is a point of O(p,q)/(O(p) × O(q)), which is the compactification moduli
space. No Grassmannian appears anywhere in the roadmap, so at present Layer 8 covers lattice
CFT characters but not the partition function of the compactified string.

The proposed addition is one milestone:

8H. The Siegel–Narain theta. For nondegenerate L of signature (p,q) and a maximal
positive definite v ⊆ L ⊗ ℝ, define
Θ_{L,v}(τ) = ∑_{x ∈ L} exp(πiτ·β(x_v, x_v) + πi τ̄·β(x_{v^⊥}, x_{v^⊥})).
Prove convergence and the S and T laws, the coset refinement over A_L, and
equivariance in v under O(L).

This needs no supplier that is not already imported: it runs on the same Poisson summation
Layer 8 takes from L-functions, and it keeps that dependency one-way, since nothing analytic
is imported back. It also subsumes 8B, 8E and 8G as the q = 0 case, so it is a
generalization of the existing milestones rather than a parallel track, and it is the natural
later home for theta lifts. If it is judged out of scope, the same treatment as gap 1 would
do: name the owner.

3. Two cheap additions to Layer 1.

• Van der Blij. For integral nondegenerate L and a characteristic vector w, meaning
  β(w,x) ≡ β(x,x) (mod 2) for all x ∈ L, one has τ(L) ≡ β(w,w) (mod 8). Characteristic
  vectors already appear in the roadmap, but only inside the proof of 6C; they are not an
  exported object. This is the odd-lattice twin of 1I, which is already a milestone, and on
  the physics side it is the spin-structure and Wu-class statement underlying fermionic
  abelian topological field theories and spin Chern–Simons. Since 5A already carries the odd
  analogue through b_L (Corollary 1.16.3), the odd branch is half built; this completes it
  at low cost.
• Witt triviality and the existence of a Lagrangian subgroup. A nondegenerate finite
  quadratic module (A,q) admits a Lagrangian subgroup exactly when it is Witt-trivial, and
  sign q = 0 is then necessary but not sufficient. 1G defines Lagrangian and 1F already
  proves that gluing along a Lagrangian subgroup yields a unimodular lattice; what is missing
  is the existence criterion in the other direction. This is the gapped-boundary criterion for
  an abelian anyon theory, and the reason a chiral theory admits no gapped boundary. Naming
  sign as a homomorphism W(q) → ℤ/8 on the Witt group would additionally give 5D and 5E a
  common invariant-theoretic frame; 5E already refers to "Witt-type statements" without a Witt
  group in the document.

On the split, from the applications side

The split is architecturally right and I would not argue against it. Two remarks on what it
costs, both bearing on the first review priority.

The moved-out 7I, that the genus of E₈² has exactly two classes, is the statement that
there are exactly two heterotic strings in ten dimensions. It is the one theorem in this
roadmap an outside physicist is most likely to ask for by name. 6D stays here and proves
everything except exhaustion, which is the correct place to cut, but 6D and 7I should be
tracked as a pair in OrthogonalTamagawaAndLatticeMass's charter so that the completeness
half does not fall between the two documents.

Second, the mass formula is Siegel–Weil, and Siegel–Weil is the backbone of the Narain
averaging and ensemble holography programme of the last few years. It is worth recording in
the boundary list that even the successor does not reach that application: the successor's
masses are positive definite by construction, whereas the Narain average is the indefinite
Siegel–Weil, which needs 8H above together with the Eisenstein series. As the list reads now,
"the analytic proof of the mass formula, which uses Siegel Eisenstein series, the Weil
representation and Siegel–Weil" sounds as though Siegel–Weil lands next door. It is two
roadmaps away, and saying so costs one clause.

One thing that should be an explicit non-goal

The Dirac pairing on a four-dimensional electric–magnetic charge lattice is antisymmetric,
and this roadmap is symmetric-bilinear throughout. Integral symplectic lattices, Sp(2n, ℤ),
and Siegel modular forms — the electric–magnetic duality and intermediate-Jacobian story — are
a different roadmap, not a gap in this one. I would add a line to the boundary list saying so,
so that a future contributor does not try to graft the symplectic case onto this carrier. The
symmetric case, which is Chern–Simons K-matrices, six-dimensional defect groups and the
Narain lattice, is the right and complete target for this document.

The asks

1. Name an owner for automorphism groups of indefinite lattices, rather than leaving the
   subject on the unowned list.
2. Add 8H, the Siegel–Narain theta, or name its owner. It requires no new supplier and keeps
   the L-functions dependency one-way.
3. Add van der Blij and the Lagrangian-existence criterion to Layer 1.
4. Record integral symplectic lattices as an explicit non-goal.
5. Track 6D and 7I as a pair in the successor's charter, and note that indefinite Siegel–Weil
   is not the successor's either.

Items 1, 3, 4 and 5 are edits to lists this document already maintains. Only item 2 is new
mathematical content.

[roed-math]

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

The applications-side review is addressed in 41fead8. Thank you — it is unusual and useful to see the consumer readings written down. The five asks, in order:

1. Named. IndefiniteLatticeAutomorphisms is now an owner-table row (reflection subgroups, Eichler criteria for O(L)-orbits, arithmeticity and fundamental domains, Borcherds' method), and the subject is off the unowned list.

2. Named rather than added. IndefiniteThetaAndSiegelWeil owns the Siegel–Narain theta with its Grassmannian parameter, the coset refinement, S/T laws, O(L)-equivariance, theta lifts, and indefinite Siegel–Weil. Your exact worry — that the current wording makes Siegel–Weil sound one door away — is answered in the charter paragraph, the analytic-mass boundary bullet, and both Layer-8 end blocks: OrthogonalTamagawaAndLatticeMass is positive definite throughout, and Siegel–Weil is two boundaries away, not one.

3. Both additions made — each with a correction to the proposed statement. Van der Blij is milestone 1L with IsCharacteristicVector and an integer-signature Int.ModEq 8 congruence — with unimodularity in the hypotheses, because the nondegenerate-only statement is false: for ⟨2⟩ every vector is characteristic (all form values are even), the signature is 1, and β(w,w) is always even. The witness is a Lean rejection test, a hard-theorems row, and a worked example; 6C now cites 1L instead of an unexported notion. The Lagrangian half: FiniteQuadraticModule.IsMetabolic and gaussSign_eq_zero_of_isMetabolic are added, and the full equivalence "Witt class zero ↔ metabolic" goes to the named successor FiniteQuadraticModuleWittTheory rather than a tautological local Witt group. Here too a proposed shape was false: Lagrangian through the bilinear form alone fails — the discriminant form of A₁ ⊕ A₁ has a subgroup with H = H^⊥ and vanishing bilinear restriction whose quadratic form takes the value ½, Gauss sum 2i, sign = 2. Lagrangian is therefore q-isotropic ∧ self-orthogonal, with that trap pinned by its own rejection test.

4. Added as a boundary row: alternating integral lattices, Sp(2n, ℤ), the alternating Dirac pairing, and Siegel modular forms are a different subject, not to be grafted onto this symmetric carrier.

5. Paired. The OrthogonalTamagawaAndLatticeMass charter now states that 6D constructs and distinguishes the two rank-16 candidates, its 7I proves exhaustion, and only the pair classifies rank 16 — with your heterotic reading in one clause — plus the explicit note that the successor's masses never reach the indefinite Siegel–Weil.

Build green in the dependency-complete stack; nothing from the named successors is imported.

[CBirkbeck]

Reviewed head: b74954eb74c98b287036a1a1a068a077db184f1f; re-checked against the current head 41fead8 (note at the end).

Verdict

Request changes to resolve the theta-series boundary.

The difficult lattice arithmetic is now in very good shape. The mass formula, dyadic smooth group scheme and Eichler/strong-approximation results have been moved to a genuine successor; Nikulin's boundary conditions and the certificate semantics have been made explicit. I do not see a new error in those parts.

The remaining problem was introduced by the new Theta Series roadmap #286.

The current ownership statement is now false

This roadmap's §Scope lists modularity of theta series among the subjects that "have no owner and are not part of this roadmap" — "Calling that endpoint modularity would need two things this portfolio does not have" — and Layer 8 closes with "§Scope records that none of the three has an owner."

That is no longer accurate: PR #286 is precisely a roadmap for the modularity of lattice theta series, and it is mentioned nowhere here.

More importantly, Layer 8 here currently owns:

• the analytic theta series;
• convergence and holomorphy;
• its $q$-expansion;
• direct sums and twists;
• the rank-one comparison;
• the dual/covolume comparison;
• the scalar $S$-transformation;
• the $T$-translation;
• the vector-valued discriminant-coset transformation.

PR #286 owns the same objects and transformations, and PR #248 also owns generic lattice Poisson summation and the Gaussian theta transform.

These are not merely three applications of one theorem. They would produce competing definitions and public APIs for the same theta function and the same Poisson formula.

Required resolution

Choose one canonical owner before merging this layer. My preferred division is:

• Integral Lattices: the rational lattice carrier, dual lattice, discriminant group and form, shells and representation numbers, together with the rational-to-real comparison;
• Theta Series #286: the real analytic theta and coset-theta functions, Poisson summation, transformations and modularity;
• L-functions #248: the mixed-embedding and Mellin specializations used in number-field $L$-functions.

Under that split, replace Layer 8 here by a short imported contract:

1. construct the real realization of a positive-definite integral lattice;
2. prove its dual, covolume and discriminant data agree with the algebraic carrier;
3. apply the theta-series supplier;
4. transport the coefficients back to the shell counts of this roadmap.

This also resolves the two $q$-parameter conventions cleanly. The general integral-lattice theta can use
$$
q=e^{\pi i\tau},\qquad
\Theta_L=\sum_k r_L(k)q^k,
$$
while the even-lattice modular form uses
$$
Q=e^{2\pi i\tau},\qquad
\Theta_L=\sum_m r_L(2m)Q^m;
$$
the supplier should state the conversion rather than the two roadmaps defining separate theta objects.

What is otherwise now satisfactory

The current roadmap has correctly:

• one embedded rational lattice carrier;
• a bilinear-first integral convention which does not divide by $2$;
• duality, discriminant forms and overlattice gluing;
• local Jordan and dyadic symbol theory;
• separate class, genus and spinor-genus carriers;
• a precise division between positive-definite finiteness, binary indefinite theory and the successor's high-rank strong-approximation results;
• lattice-side local density inputs without claiming the mass formula;
• typed Nikulin existence and embedding conditions;
• semantic LMFDB records separated from completeness certificates;
• the $E_8$, $D_{16}^{+}$, Niemeier and K3-facing applications assigned to the correct layers.

Once the theta-series ownership is synchronized with #286 and #248, I would approve subject to the declared supplier order.

---

Re-check at 41fead8. The commit after the reviewed head names three successors (IndefiniteLatticeAutomorphisms, IndefiniteThetaAndSiegelWeil, FiniteQuadraticModuleWittTheory), adds characteristic vectors with van der Blij's congruence (1L) and Lagrangian/metabolic finite quadratic modules with the Gauss-sign vanishing (1G/1H), and pins the symplectic boundary. I checked the new witnesses — ⟨2⟩ against dropping unimodularity, the discriminant form of A₁ ⊕ A₁ against bilinear-only isotropy, and q_θ^{(5)}(5) with (θ|5) = −1 against the converse — and they are correct. The theta-series boundary is unchanged: the owner table still sends Poisson summation and the Gaussian theta to L-functions, Layer 8 still owns the transformation laws, and #286 is mentioned nowhere, so the request above stands.