feat: roadmap for theta series of lattice

[seewoo5]

The main goal of this formalization is to define theta series of lattices and prove Hecke-Schoeneberg, i.e. theta series of (even-dimensional) even lattice is a modular form of suitable weight (=dim/2) and level. When the lattice is unimodular, the level becomes 1. Using this, one can prove formulas for the number of lattices points with given length for small dimensions (notably 2, 8, 24).

Note that this may overlap with integral lattice project and modular form project. At least, this project will use some part of these projects' formalizations. Also, the project idea arose from sphere packing project; Math Inc.'s 24-dimensional sphere packing formalization includes theta series of Leech lattice (as a function, not as a modular form), which is used to prove uniqueness.

README.md and Suggested.lean file are written with Claude with small guidance.

[CBirkbeck]

Head reviewed: b6c95b203b054319abeeafda1cb01d7da14a1f1c

I reviewed the current head, including both the 640-line roadmap README and the 469-line Suggested.lean.

Verdict: changes requested.

This is a worthwhile roadmap. The exponent convention

$$ \Theta_L(\tau)=\sum_{x\in L}e^{\pi i\lVert x\rVert^2\tau}, $$

the separation between the real analytic lattice and the rational integral-lattice carrier, and the applications to $E_8$, rank $16$, and the Leech lattice are all sensible. The intended summit—Hecke–Schoeneberg for an even lattice of even rank—is also exactly the right theorem.

There are, however, three kinds of problem:

1. a serious ownership conflict with two other roadmaps;
2. several statements which are actually false;
3. a major gap in the proposed route through finite quadratic modules and the Weil representation.

1. The same mathematics currently has three owners

Roadmap #286 claims general-dimensional lattice Poisson summation, the analytic theta function, its convergence and $q$-expansion, direct sums and scaling, the dual-lattice transformation, and modularity.

But the current L-functions roadmap already claims general lattice Poisson summation and the Gaussian theta transformation. The expanded Integral Lattices roadmap also has a complete Layer 8 owning the analytic theta series, convergence, $q$-expansion, sums and twists, the rank-one comparison, dual/covolume comparison, and the $S$-transformation.

This needs resolving before #286 can merge. I would use the following split:

• #286 owns the generic lattice Poisson theorem, theta and coset-theta functions, transformation laws, modularity, and applications.
• L-functions consumes the generic Poisson theorem and owns only the number-field theta/Mellin construction needed for zeta and Hecke $L$-functions.
• Integral Lattices owns the rational lattice, discriminant group and discriminant form, but consumes #286 for theta series and modularity.

The $D_{16}^{+}$ application would then either be explicitly stacked after the expanded Integral Lattices roadmap or postponed to a later application PR. The same ownership decision must be recorded in all three roadmaps.

2. Positive scaling does not preserve the lattice predicates

Layer 0 says that integrality, evenness and unimodularity are invariant under positive scaling. This is false.

For $c>0$,

$$ (cL)^\vee=c^{-1}L^\vee,\qquad \det(cL)=c^{2n}\det L. $$

Thus arbitrary positive scaling usually destroys integrality and unimodularity. For example, $\sqrt2,E_8$ is even and integral, but it is not unimodular. A generic positive real scaling will not even remain integral.

The roadmap should distinguish:

• invariance under isometry;
• preservation under orthogonal direct sum;
• exact arithmetic criteria for preservation under scaling.

The determinant and theta scaling formulas are valid, but the predicates themselves are not invariant.

3. The claimed level of the Fricke partner is false

The roadmap asserts that if $N=\operatorname{level}(L)$, then

$$ \sqrt N,L^\vee $$

is an even lattice of level $N$.

Evenness and the determinant formula are correct, but the exact level need not be $N$. Take

$$ L=\sqrt2,E_8. $$

Then $L$ is even and has level $2$, whereas

$$ \sqrt2,L^\vee=E_8 $$

has level $1$.

The unconditional conclusion is that $\sqrt N,L^\vee$ is even and its level divides $N$. Equality requires an additional primitivity or content condition. This error occurs in the conventions and in Layer 0, and will also affect the later Fricke statement.

4. The coset $q_N$-expansion is described incorrectly

The roadmap says that $\theta_{\gamma+L}$ has a $q_N$-expansion "with leading exponent $q_L(\gamma)$."

There are two problems:

• $q_L(\gamma)$ lies in $\mathbf Q/\mathbf Z$, whereas an exponent of

  $$
  q_N=e^{2\pi i\tau/N}
  $$

  is an integer.

• The discriminant value does not determine the first nonzero exponent.

What it determines is the congruence class of all exponents:

$$ r\equiv Nq_L(\gamma)\pmod N. $$

The first exponent is controlled by the minimum norm in the coset $\gamma+L$.

The roadmap should define the coset representation numbers explicitly and prove the support congruence. This is also the exact input needed for boundedness at the cusps.

5. A theta identity is reversed

Layer 2 writes

$$ \Theta_L=\sum_{\gamma\in A_L}\theta_\gamma $$

and says that this recovers $\Theta_{L^\vee}$.

The correct identity is

$$ \Theta_{L^\vee} =\sum_{\gamma\in L^\vee/L}\theta_{\gamma+L}. $$

This should be corrected in the prose and represented by an exact theorem in Suggested.lean.

6. "Rank is even throughout" conflicts with the rank-one test

The roadmap repeatedly says that rank is even throughout and that Complex.cpow must never appear. But it also asks the rank-one case to reproduce jacobiTheta_S_smul.

The function identity

$$ \Theta_{\mathbf Z}=\vartheta $$

is a good convention check. The $S$-transformation of $\vartheta$, however, is a half-integral-weight statement and necessarily involves square-root or metaplectic branch data. It is outside the integral-weight, no-cpow framework.

The scope should instead say:

• Layers 0–2 and Poisson summation permit arbitrary rank.
• The integral-weight modularity layers assume even rank.
• The rank-one acceptance test compares only the functions and $q$-expansions.

A suitable $S$-transformation check inside the stated scope would be $\mathbf Z^2$, or the square of the Jacobi theta transformation.

7. The proposed Weil representation uses data that a finite quadratic module does not have

For a general finite quadratic module $(A,q)$, Layer 5 proposes

$$
\rho(S)e_\gamma

|A|^{-1/2}(-i)^{n/2}
\sum_{\delta\in A}e\bigl(b(\gamma,\delta)\bigr)e_\delta.
$$

A bare finite quadratic module has no ambient dimension $n$. It has a signature or Brown invariant in $\mathbf Z/8\mathbf Z$. For the discriminant form of a lattice, this agrees with the lattice signature modulo $8$, but that agreement is a theorem.

The coefficient should therefore be expressed using

$$ e!\left(-\frac{\operatorname{sig}(A,q)}8\right), $$

or the construction should be restricted to discriminant forms equipped with a lattice-signature witness.

This is not a presentational issue: as written, the central scalar is not defined by the advertised input. The literature likewise distinguishes whether the finite quadratic module gives a representation of $\mathrm{SL}_2(\mathbf Z)$ or of its metaplectic cover by its signature. (arXiv)

8. Primary decomposition is not enough for Layer 5

The roadmap appears to assume that primary decomposition of the discriminant form is sufficient to evaluate the Gauss sums, prove Milgram's formula, and derive the explicit $\Gamma_0(N)$ action.

It is not. The standard arithmetic theory uses the Jordan decomposition of a finite quadratic module:

• at odd primes, local signs and $p$-excess;
• at $2$, odd and even components, often called type I and type II, and their oddities;
• a signature in $\mathbf Z/8\mathbf Z$ assembled from these local invariants.

Strömberg's treatment explicitly introduces this refined Jordan decomposition, including the two distinct $2$-adic types, before giving the local Gauss-sum and Weil-representation formulae. The general matrix coefficients involve precisely these $p$-adic invariants. (arXiv)

The current Integral Lattices roadmap supplies finite quadratic modules and primary components, but not this local classification. Layer 5 therefore needs a genuine new block containing:

1. odd-primary Jordan components;
2. odd and even $2$-primary Jordan components;
3. the required existence and uniqueness statements;
4. $p$-excess and oddity;
5. the finite-quadratic-module signature;
6. all local Gauss-sum evaluations;
7. multiplicativity under orthogonal sums;
8. Milgram's formula.

There is another possible route: prove Milgram analytically from the lattice theta transformation, and decline to develop the general classification of finite quadratic modules. Either route is defensible, but the roadmap must choose one.

9. The hardest part of Hecke–Schoeneberg is hidden

After defining the operators corresponding to $S$ and $T$, the roadmap asks for:

$$ \rho\text{ factors through }\mathrm{SL}_2(\mathbf Z/N\mathbf Z), $$

and, for

$$ A=\begin{pmatrix}a&b\c&d\end{pmatrix}\in\Gamma_0(N), $$

$$ \rho(A)e_0=\chi_L(d)e_0. $$

Neither follows formally from the presentation of $\mathrm{SL}_2(\mathbf Z)$. These are essentially the explicit finite Weil-representation calculations. The formula for a general matrix involves local $p$-adic invariants, and the $2$-primary calculation is the delicate part. Strömberg explicitly separates the easy projective/Gauss-sum form from the difficult evaluation of the scalar factor. (arXiv)

The roadmap should spell out a route such as:

1. calculate the action on each Jordan component;
2. combine the components at a fixed prime;
3. combine the prime-primary parts;
4. establish the congruence kernel;
5. calculate the action on $e_0$ for $\Gamma_0(N)$;
6. identify the product of local symbols with the Kronecker character.

Without this, the roadmap jumps from the definition of the representation to its most difficult explicit consequence.

10. The Milgram/Weil argument is potentially circular

The roadmap says that the $S,T$-relations are checked by a Gauss-sum computation, whose decisive evaluation is Milgram's formula. But it also presents Milgram's formula as part of the theory obtained from the Weil representation.

A dependency order must be fixed. For example:

Analytic route

1. Prove the vector-valued theta transformation by Poisson summation.
2. Apply the modular-group relation to obtain Milgram's formula for lattice discriminant forms.
3. Use Milgram to verify the abstract $S,T$-relations.
4. Construct the Weil representation.

Local arithmetic route

1. Classify the Jordan components.
2. Evaluate all local Gauss sums independently.
3. Deduce Milgram's formula.
4. Verify the presentation relations and construct the representation.

At present an implementation agent cannot tell which result may be used in which proof.

11. The discriminant character is constructed in the wrong order

The congruence

$$ D_L=(-1)^k\det L\equiv0\ \text{or}\ 1\pmod4 $$

gives a Kronecker character at a natural modulus associated with $D_L$. It does not by itself give a character modulo $N=\operatorname{level}(L)$.

To define

$$ \chi_L:(\mathbf Z/N\mathbf Z)^\times\longrightarrow\mathbf C^\times, $$

one needs the lattice-specific theorem that the conductor of the Kronecker character divides $N$, or equivalently the required periodicity modulo $N$.

The README mentions conductor divisibility, but Suggested.lean simply introduces

def discChar ... : DirichletCharacter ℂ (level L) := sorry

and then treats conductor divisibility as generic. It is not generic; it is the load-bearing lattice theorem.

The order should be:

1. construct the Kronecker character at its canonical modulus;
2. prove its conductor divides level L;
3. change level to obtain discChar L k.

This should be an exact target with a stated proof route, probably using the same local calculation needed for the $\Gamma_0(N)$ formula.

12. The multidimensional Poisson route needs intermediate theorems

Mathlib's current Poisson summation theorem is one-dimensional, on $\mathbf R$, just as the roadmap says.

But "apply it $n$ times and use Fubini" does not yet provide a formalization plan. The missing infrastructure includes:

• standard-lattice Poisson summation on $\mathbf R^n$;
• partial Schwartz or currying lemmas;
• absolute summability sufficient to rearrange iterated sums;
• product or partial-transform formulae for the Fourier transform;
• Fourier change of variables under a continuous linear equivalence;
• the transpose/adjoint-inverse description of the transformed lattice;
• the determinant/covolume normalization.

Mathlib does have the general covolume and relative-index theory needed for the final normalization.

Layer 1 should therefore be divided into:

1. the standard $\mathbf Z^n$ theorem;
2. Fourier change of variables;
3. dual-lattice transport;
4. the final general lattice theorem.

13. Suggested.lean avoids nearly every load-bearing interface

The most serious promises are currently omitted or replaced by True := sorry:

• the real/rational bridge;
• orthogonal sums;
• the rank-one comparison;
• the vector-valued inversion law;
• finite-quadratic-module signature;
• the Weil $S,T$-operators;
• the presentation relations;
• Milgram's formula;
• the congruence-kernel theorem;
• the $\Gamma_0(N)$ action on $e_0$.

The polynomial-in-$E_4,\Delta$ result is represented by

∃ c : ℕ × ℕ →₀ ℂ, True

which fixes no mathematical interface at all.

This undermines the purpose of Suggested.lean. The merged Integral Lattices roadmap already has planned names for IntegralLattice, FiniteBilinearModule, FiniteQuadraticModule and the discriminant modules.

The theta roadmap should import that supplier's Suggested.lean and write exact statements for:

• the real/rational bridge;
• $\Theta_{L^\vee}=\sum_\gamma\theta_\gamma$;
• the vector-valued $S$-law;
• the finite-quadratic-module signature;
• the Weil operators and relations;
• Milgram;
• the congruence kernel;
• the $\Gamma_0(N)$ character formula.

If it intends to depend on the open expanded Integral Lattices PR, this must be an explicit stacked dependency.

14. The shell convolution is not presently a meaningful sum

The roadmap writes

$$ r_{L\oplus M}(t)=\sum_s r_L(s)r_M(t-s) $$

while $s,t\in\mathbf R$. There is no ordinary finite sum over all real $s$.

For even integral lattices, state the coefficient convolution over $\mathbf N$. At the general real-lattice level, formulate it as convolution of discrete shell-counting measures or sum over a finite set of represented norms.

What I would keep

The following parts are good and should survive the rewrite:

• the real analytic lattice carrier and explicit bridge to the rational carrier;
• the exponent $\pi i\lVert x\rVert^2\tau$;
• the distinction between a raw theta function and a bundled modular form;
• scalar and vector-valued transformations;
• the general rank-$8$, rank-$16$, and rank-$24$ statements before named examples;
• the insistence that $240$ and $196560$ are outputs, not hypotheses;
• the warning that $\theta_\gamma=\theta_{-\gamma}$, so the theta components cannot themselves be used as a basis to manufacture the Weil representation;
• the exclusion of half-integral-weight modularity.

Recommended structure

A dependency-complete rewrite could be:

1. Generic multidimensional lattice Poisson summation.
2. Real/rational bridge, duality, shells, determinant and exact level/scaling statements.
3. Theta and coset-theta series, with precise $q_N$-support.
4. Scalar and vector-valued transformation laws.
5. Level-one modularity and the graded-ring consequences.
6. Jordan decomposition of finite quadratic modules, local Gauss sums, oddity, $p$-excess, signature, Milgram and the Weil representation.
7. Congruence kernel, $\Gamma_0(N)$ calculation, discriminant character and Hecke–Schoeneberg.
8. $E_8$, Leech and, once its supplier is available, $D_{16}^{+}$.

The summit and applications are mathematically good. The roadmap now needs a unique ownership boundary, correction of the scaling/level/coset statements, and a full account of the local finite-quadratic-module theory hidden inside Layer 5.

[seewoo5]

🤖 Drafted with Claude Code.

Thanks for the detailed review. Done in 10f2b0c: a rewrite of both files addressing every point. Here is what changed, numbered as in the review.

1. Ownership. New Scope and ownership section adopting exactly the split you proposed: this roadmap owns generic lattice Poisson summation, Θ_L and the coset series, the transformation laws, Gauss sums, modularity and the applications; L-functions consumes Layer 1 and owns only the number-field theta/Mellin material; Integral Lattices owns the rational carrier and discriminant forms and consumes theta from here. D₁₆⁺ (8E) is stated as consuming the integral-lattices gluing construction and sequenced last. The same boundary needs to be recorded in #248 and #256; I'll open the matching edits there (or comment on those PRs) once the wording here is agreed.

2. Scaling. Fixed. 2B now states the scaling laws ((cL)^∨ = c⁻¹L^∨, det(cL) = c^{2n} det L), the exact criterion for c • L to be integral, the √m-scalings that actually occur, and explicitly that none of integral/even/unimodular is scaling-invariant (with √2 E₈).

3. Fricke partner. Fixed. 2F: √N L^∨ is even, det = N^n/det L, and its level divides N, with the exact value N / gcd(N, c_L) (c_L the gcd of the half-norms) and √2 E₈ ↦ E₈ recorded as a required test.

4. Coset expansions. Fixed. Coset representation numbers r_{γ+L} are defined (2G), the q_N-expansion is ∑ r_{γ+L}(2m/N) q_N^m with the support congruence m ≡ N q_L(γ) (mod N) (3C, cosetRepNum_eq_zero_of_not_modEq in Lean), and the leading exponent is explicitly attributed to the minimal norm of the coset.

5. Fixed: Θ_{L^∨} = ∑_{γ ∈ A_L} θ_{γ+L} (3B, thetaSeries_dual_eq_sum).

6. Rank. Layers 1–3 are now stated for arbitrary rank; even rank starts with the automorphy factors in Layer 4. The rank-one test compares functions and q-expansions only; the in-scope S-check is ℤ², the square of jacobiTheta_S_smul (4D, thetaSeries_stdLattice_two_neg_inv).

7–10. The Weil representation route. Rather than repair it, I removed it: the Weil representation and the SL(2,ℤ) presentation are no longer targets, and Hecke–Schoeneberg is routed through Schoeneberg's coset splitting (Layer 7) with the Gauss-sum input isolated in a new Layer 6. That layer chooses the analytic route you offered: the reciprocity law G_L(a,c) = (c/a)^k (det L)^{-1/2} e(n/8) ∑_{L^∨/aL} e(-c‖y‖²/2a) is proved by theta asymptotics (the only analytic input); Milgram is its a = c = 1 case; the dual side is evaluated at an odd modulus a coprime to N, where the form is unimodular mod a, so only CRT, a p^e → p^{e-2} reduction, diagonalisation over 𝔽_p and g_p² = (-1/p)p are needed — no Jordan decomposition and nothing 2-adic. The dependency order is now linear (4 → 6B → 6C/6D → 6E → 6F → 7). The Γ(N)-statement for the coset series (7E) comes from the same splitting applied to a coset. The scope section records what a future Weil-representation roadmap would need (the finite-quadratic-module signature from #256, and the Scheithauer/Strömberg local formulas).

11. χ_L. Reordered: kroneckerChar D_L at modulus |D_L| (2H) → the lattice theorem conductor ∣ level L (6F, proved from G_L(a, N) = G_L(1, N) for a ≡ 1 mod N and the closed form 6E) → discChar := changeLevel _ (primitiveCharacter _). The Lean file follows this order exactly.

12. Poisson. Layer 1 split into 1A–1F: standard lattice via iterated one-dimensional Poisson with the partial-Schwartz/partial-transform lemmas named, Fourier change of variables, dual-lattice transport, the general theorem, summability, Gaussians.

13. Suggested.lean. Now imports TauCetiRoadmap.IntegralLattices.Suggested and states exactly: the bridge ratModel : IntegralLattice (ℚ ⊗[ℤ] L) with the discriminant-group equivalence carrying pairing and quadratic form; orthogonal sums in WithLp 2 (E × F); the rank-one and rank-n comparisons with jacobiTheta; the general-v and vector-valued S-laws; Gauss sums, reciprocity, Milgram, the odd-modulus evaluation, the closed form, the conductor theorem and discChar; the coset splitting identity; Hecke–Schoeneberg in both spellings; and the polynomial identity as ∃! c : ℕ × ℕ →₀ ℂ with the weight constraint. No True := sorry remains. The dependency is on the merged Integral Lattices roadmap only, not on #256.

14. Convolution. Stated over ℕ for even lattices (repNum_orthSum) and over the finite set of represented norms in general.

[roed-math]

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

Coordination rather than review: your Scope and ownership section says each of the three roadmaps records the same boundary, so this is notice that the other two are being changed to match it, with the exact names we consume.

L-functions #248 (fb5d3c3) has dropped its own generic development. Layer 1 previously opened "For a full ℤ-lattice in a finite-dimensional real inner-product space, develop the Fourier transform of a Gaussian and prove Poisson summation for Schwartz functions" — that claim is gone, and the layer now consumes, by name: poissonSummation, summable_poisson_left, summable_poisson_right, dual, dual_dual, covolume_dual, gaussian, gaussian_apply, fourier_gaussian. It keeps only what is specific to number fields: the mixed-embedding conventions, the Euclidean-vs-trace-dual comparison with its 4^{r₂} determinant, the N(I)·2^{-r₂}√|d_K| covolume consumed from Mathlib, the partial-zeta theta kernels, the Mellin transforms, and the single normalization theorem. Its holomorphic upper-half-plane pointer now routes to this roadmap rather than to Integral Lattices.

Integral Lattices #256 is having its own theta/latticeTheta/cosetTheta and their T/S and vector-valued laws removed, replaced by a consumption contract naming yours — matching your "states no theta series of its own". It remains your supplier for the rational carrier, the discriminant group and forms, finite quadratic modules, the overlattice correspondence and the ADE lattices, so the dependency runs both ways across the Layer-2 bridge and neither direction is circular at the level of declarations.

Two things worth your attention, both small:

1. Your ownership note promises L-functions "the generic Poisson theorem of Layer 1", but two of the declarations that consumption actually needs — dual_dual and covolume_dual — are in your Layer 2. If the Layer-1 wording is meant to be exhaustive, it is slightly too narrow; widening it to name the dual/covolume lemmas would make the contract exact.

2. poissonSummation is stated for an InnerProductSpace ℝ E, and the number-field mixed space is not one — NumberField.mixedEmbedding.mixedSpace K carries a product sup norm. Consuming your theorem therefore needs a transport, which Add roadmap: L-functions: completions and functional equations #248 now states as mixedInner_toMixed (through Mathlib's NumberField.mixedEmbedding.euclidean.toMixed) together with euclideanIdealLattice, whose DiscreteTopology and IsZLattice instances close by infer_instance; the measure half is Mathlib's euclidean.volumePreserving_toMixed. That transport is properly ours, not yours — flagging it only so you know the generic statement is being applied through a change of model rather than directly, in case it affects how you phrase Layer 1's hypotheses.

Neither of our roadmaps adds import TauCetiRoadmap.ThetaSeries.Suggested: the repo's rule is that no milestone waits on a pull request, so both cite your declarations by name and the imports land when this roadmap does. Nothing here asks you to change anything — if you would rather draw a line differently, say so and we will follow yours, since this is your subject.

[roed-math]

🤖 Claude Opus 5, on David Roe's behalf — follow-up to the note above, now that both sides have landed.

• L-functions #248: fb5d3c3, generic development removed, your nine declarations consumed by name.
• Integral Lattices #256: 1dde7cf, its theta/latticeTheta/cosetTheta and the T/S and vector-valued laws deleted, replaced by a contract naming thetaSeries, thetaCoset, thetaCosetClass, thetaSeries_add_one, thetaSeries_add_two, thetaCoset_add_one, thetaSeries_neg_inv, thetaCosetClass_neg_inv, thetaSeries_dual_eq_sum and friends. It now also carries an explicit list of what it supplies you, so the bridge has a named contract from both ends.

Three small things found while doing it, all in your favour to fix rather than ours:

1. Two layer labels in your README point at the wrong layers of Integral Lattices. You cite "integral-lattices Layer 3 for q_L and b_L" — those are 1D there — and "Layer 5 for the construction of D₁₆⁺", which is 6D. Expand roadmap: Integral quadratic forms and lattices #256's new supply table names the labels from its side if you want to copy them.

2. Your ownership note promises L-functions "the generic Poisson theorem of Layer 1", but the consumption also needs dual_dual and covolume_dual, which are in your Layer 2.

3. Milgram is deliberately not deduplicated. Expand roadmap: Integral quadratic forms and lattices #256 keeps its 1I (any signature, via the arithmetic route) and records your milgram (positive definite, via theta asymptotics) as a separate wanted theorem that the bridge identifies — collapsing them would drop the indefinite case, which your roadmap explicitly does not cover.

One consequence you may care about: #256 no longer imports L-functions at all. That dependency existed only to state its theta layer, so handing the theta series to you removed an edge from the graph rather than moving one.

[seewoo5]

🤖 Drafted with Claude Code.

Thanks — done in d78b813, and I've taken your line rather than drawing a different one.

1. Layer labels. Fixed, and I fixed the four others of the same kind while I was in there. The
citations now read: 1D for q_L and b_L; 6D (through the gluing of 1F) for D₁₆⁺ and its
non-isometry; 0A with 1B, 1C and 1D for the carrier the bridge lands in; 0A, 1B–1G, 1J, 1K and 6D
for the dependency of Layers 2, 4 and 8; 1K for the rank-one and ADE acceptance values; and 1H for
the finite-quadratic-module signature the Weil-representation note points at. Consumed, not
redefined now carries a label per item, copied from your new supply table, and 2G records that its
shells are your 2B's counts read in E, with the bridge identifying them.

2. The L-functions contract. Widened, and made exact rather than by-layer: it now names
poissonSummation, summable_poisson_left, summable_poisson_right, gaussian, gaussian_apply
and fourier_gaussian of Layer 1 together with dual, dual_dual (2A) and covolume_dual (2C).
Suggested.lean's header lists both consumption contracts — your nine and #256's eighteen — so a
rename here is visibly an edit to someone else's specification. All twenty-seven names are declared
in the file, in TauCetiRoadmap.ThetaSeries.

On the transport. Agreed that it is yours, and I've taken the flag as a reason to pin Layer 1's
hypotheses rather than to soften them: Not owned here and the poissonSummation docstring now say
the statement quantifies over a real inner product space, that a consumer whose own model is not one
(mixedSpace K and its product sup norm, named) applies it after transporting along a linear
isometry, and that Layer 1 is not weakened to avoid that. So mixedInner_toMixed and
euclideanIdealLattice are exactly the right shape from this side.

3. Milgram. Recorded from this end too, in the scope section, at 6C and on the milgram
docstring: your 1I is every signature by finite arithmetic from 1H, 6C here is the positive definite
instance by theta asymptotics, both are wanted, the bridge of 2D identifies them, neither is derived
from the other, and collapsing them would drop the indefinite case. 6C now ends "Do not replace this
milestone by a citation of that one."

One thing your correction surfaced. Following the pointer to 6D showed a real overlap rather than
a stale label: 6D constructs both lattices and separates them by their root systems, while 8E here
described reproving the non-isometry by a root-sublattice index. That is the duplication the split
exists to remove, so 8E now consumes the non-isometry from 6D and owns only
Θ_{E₈ ⊕ E₈} = Θ_{D₁₆⁺} = E₄² and the statement that the theta series does not determine the
lattice, with an explicit instruction not to reprove the non-isometry by that index, by a vector
count, or by any other route. exists_thetaSeries_eq_not_isometric keeps its statement — it is the
combined fact — and its docstring now attributes the two halves separately.

lake build is green.