feat: roadmap for complex tori and logarithmic transforms - #280
Conversation
CBirkbeck
left a comment
There was a problem hiding this comment.
Part of a deep adversarial review of the reusable-roadmap split — PRs #279–#284, reviewed 25 August 2026. This section covers #280 — Complex tori: varying lattices and logarithmic transforms.
Head reviewed: 805203145c0a3db0d14a686795fcd1bc961d601a
Verdict
Major changes requested.
The roadmap has successfully become reusable and it correctly distinguishes the orbit covering from the family projection. However, the central cyclic-affine classification is formulated on the wrong group. This affects the freeness criterion, the classification of twists, the logarithmic-transform parameter, and the claimed independence theorem.
Main mathematical error: affine translations belong to the torus, not the lattice
Let
[
T=E/\Lambda
]
and let (A) preserve (\Lambda). An affine automorphism of (T) is
[
\phi_{A,t}(x)=Ax+t
]
with (t\in T), not (t\in\Lambda). A lattice element is zero in (T), so using a translation parameter in (\Lambda) loses the geometry.
The correct formulas are
[
\phi_{A,t}^{,k}(x)=A^k x+N_{A,k}(t),\qquad
N_{A,k}(t)=\sum_{i=0}^{k-1}A^i t.
]
For (A^m=1), the order condition is
[
N_{A,m}(t)=0\quad\text{in }T.
]
Translation conjugacy changes
[
t\longmapsto t+(1-A)b,\qquad b\in T,
]
so conjugacy classes of order-(m) affine lifts are controlled by
[
H^1(C_m,T)
=\ker(N_A:T\to T)/\operatorname{im}(1-A).
]
The fixed-point criterion for the (k)-th power is
[
\phi_{A,t}^k\text{ has a fixed point}
\iff
N_{A,k}(t)\in\operatorname{im}(1-A^k:T\to T).
]
The current roadmap and Suggested.lean instead put t in Λ, take the cokernel of A-1 on Λ, and test fixed points of an affine permutation of Λ. Those are valid elementary statements about the set Λ, but they are not the classification or fixed-point criterion needed for the torus quotient.
Decisive regression test
Take (A=1). Order-(m) translations of (T) are parametrized by
[
T[m]\cong \Lambda/m\Lambda.
]
The proposed cokernel is
[
\operatorname{coker}(A-1)=\Lambda,
]
which is plainly wrong.
The normalized lattice class
If the translation is represented by (v/m), with (v\in\Lambda^A), the associated integral class is not generally
[
v\bmod (A-1)\Lambda.
]
Via
[
0\to\Lambda\to E\to T\to0
]
and the vanishing of finite-group cohomology of the real vector space (E), the relevant class lies in
[
H^2(C_m,\Lambda)
=\Lambda^A/N_A\Lambda.
]
The roadmap must use the actual norm quotient. This is the class which should feed the logarithmic transform.
Required rewrite of Milestone 4
Milestone 4 should be divided into two levels.
Torus-level affine algebra
For (T=E/\Lambda):
- define affine automorphisms with (t\in T);
- prove the iterate and norm formulas;
- define the (C_m)-action under (A^m=1) and (N_A(t)=0);
- classify translation conjugacy by (H^1(C_m,T));
- prove the fixed-point criterion in (T);
- check every nonidentity power for composite (m).
Integral connecting class
For a chosen lift (\widetilde t\in E):
- prove (N_A(\widetilde t)\in\Lambda^A);
- prove change of lift changes it by (N_A\Lambda);
- identify the resulting class in (\Lambda^A/N_A\Lambda);
- prove its equivalence with the torus (H^1)-class;
- specialize to (v/m).
The current lattice-affine lemmas may remain as auxiliary algebra, but they cannot be the public classification.
Further gaps
1. Equivariant descent needs freeness of the total action
Milestone 3 assumes a properly discontinuous action on the base and forms a quotient of the torus family. A base stabilizer can act nontrivially on the fibre. To apply the free quotient theorem from #279, the induced action on the total space must be free.
This is especially important for elliptic base points, where fibre translation is precisely what removes fixed points. State the total freeness hypothesis or prove it from the torus-level affine criterion.
2. “Local product charts” must not imply holomorphic isotriviality
A non-isotrivial family such as
[
\mathbb C/(\mathbb Z+\tau(y)\mathbb Z)
]
is not holomorphically locally a product with one fixed elliptic curve merely because the total-space projection is a submersion.
Distinguish:
- submersion coordinates around a point of the total space;
- smooth local triviality;
- holomorphic local triviality as a family with a fixed compact fibre.
Only the first is automatic here. Do not call the family a holomorphic fibre bundle unless an isotriviality theorem or stronger hypothesis is supplied.
3. Uniform proper discontinuity needs a named compact estimate
Pointwise discreteness of every lattice is not by itself the theorem used to form the total quotient. The roadmap should explicitly prove that on a compact subset of the base there is a uniform lower bound for the norm of every nonzero period, or equivalently a uniform bound on inverse period matrices. This supplies orbit-local finiteness and compact fundamental representatives.
4. State separation and countability assumptions on the base
The total-space Hausdorff and second-countability claims need the corresponding hypotheses on Y, together with continuity/holomorphy of the period data. Put them in the constructor rather than relying on the informal word “complex manifold”.
5. Exact normal and canonical orders need the correct injectivity argument
Divisibility of the order follows from the cyclic character. Exact order requires proving that the associated-character map into the Picard group is injective in the case at hand, for example from connected compactness of the covering space and constancy of invertible holomorphic functions.
6. Independence must use the correct cohomology class
The logarithmic transform is not classified by coker(A-1) on the lattice. The independence theorem must hold with the period family fixed and the correct class in (H^1(C_m,T)), equivalently its connecting class in (\Lambda^A/N_A\Lambda), fixed.
7. Expand Suggested.lean
The file currently validates affine permutations of Λ, not affine automorphisms of E/Λ. Add representative declarations for:
- the fixed torus quotient;
- the varying total-space quotient and both projections;
- torus-level affine automorphisms;
- the (H^1(C_m,T)) class;
- the integral connecting class;
- total-space freeness;
- the multiple-fibre local model.
What should remain
- use of the standard orbit quotient;
- distinction between
qandp; - pointwise full-lattice hypotheses through
IsZLattice; - retention of the varying period family;
- checking every nonidentity power for composite order;
- map-level fundamental-group and homology comparisons;
- the construction-independent scope.
Recommended disposition
The cyclic-affine core must be rewritten before the roadmap can be approved. This is not a cosmetic change: it alters the parameter space of logarithmic transforms and the proof of freeness.
Cross-roadmap notes (apply across the #279–#284 split)
- PRs #280, #282, #283, and #284 still use the Levent six-sphere PDF as the link in the PR body. These are now general-purpose roadmaps. The construction paper should be described only as a motivating consumer; each PR body should instead foreground the standard sources listed in its README.
- Every downstream roadmap should import or
#checkthe exact representative interfaces of its supplier once those suppliers land. Prose references alone are not enough to prevent incompatible carriers. - The intended merge order is:
#279 and corrected #283first;#280after both;#281after #279 and an exact algebraic toric supplier;#282after #279 and a reconciled compact-Riemann-surface degree API; and#284after corrected #283 plus its geometric-topology and Morse/transversality suppliers.
|
🤖 Addressed in 6bfc981. The cyclic-affine core now lives on T=E/Λ: its class is ker N/im(1−A), and the integral connecting class is Λ^A/NΛ. The fixed-point, freeness, independence, and A=1 regression checks use those groups. The roadmap also makes total-space freeness explicit, separates submersion charts from smooth and holomorphic local triviality, names the uniform compact period estimate, states base separation/countability, and uses the associated-character injectivity criterion for exact bundle orders. Suggested.lean now seeds the torus-level and multiple-fibre interfaces, and the PR body foregrounds the standard sources. |
CBirkbeck
left a comment
There was a problem hiding this comment.
Part of the second deep review of the reusable-roadmap split — PRs #279–#284, reviewed 26 August 2026 against the updated heads. This section covers #280 — Complex tori and logarithmic transforms.
Head reviewed: 6bfc9818e941a30c2d0696d61e7805bbc9281e3e
All six updated branches pass their current CI. The comments below concern the mathematics and the proposed public APIs, not elaboration failures.
What has been fixed
The central error from the first review has been corrected properly:
-
the affine translation parameter is now
t : T, not an element of the lattice; -
the iterate and fixed-point criteria live on the torus;
-
conjugacy classes are modeled by
$$ H^1(C_m,T)=\ker N_A/\operatorname{im}(1-A); $$ -
the integral connecting class lives in
$$
H^2(C_m,\Lambda)=\Lambda^A/N_A\Lambda;
$$ -
the
A = 1regression givesT[m] ≃ Λ/mΛ; -
total-space freeness is separated from freeness of the base action;
-
compact-uniform period separation is explicit;
-
submersion coordinates, smooth local triviality and holomorphic isotriviality are distinguished;
-
exact normal-bundle order uses the Picard-injectivity criterion.
That removes the previous major blocker.
1. A lattice automorphism need not induce a holomorphic torus automorphism
The roadmap currently says to let a lattice automorphism induce A_T : T ≃+ T. Algebraically that is fine, but the later cyclic quotient is a complex-analytic quotient.
For example, on
complex conjugation preserves the lattice and induces an additive torus automorphism, but it is antiholomorphic. A general integral automorphism can be neither complex-linear nor antiholomorphic.
The roadmap should separate:
-
the abstract additive
H¹/H²theory, which only needsA_T : T ≃+ T; and -
the analytic logarithmic-transform constructor, which needs an explicit
$$
A_E:E\simeq_{\mathbf C}E
$$preserving
Λ, or the corresponding biholomorphic torus automorphism.
Without that extra input, Milestone 5's generator need not be biholomorphic.
2. The Lean H¹ carrier is only a set quotient
AffineHOne is currently a raw Quotient of a setoid. But the roadmap promises cyclic-group cohomology, functoriality, restriction and a connecting isomorphism. Here T is abelian, so H¹(C_m,T) should be an AddCommGroup, preferably implemented as an additive subgroup quotient.
Likewise Suggested.lean currently defines only
integralConnectingClass ... (v : invariantLattice A) :
AffineHTwo A m hAwhich is just the quotient class of an already supplied invariant vector. It does not seed the actual connecting map from a torus H¹ class, nor the isomorphism obtained from
0 → Λ → E → T → 0.
Add representative declarations for:
- the additive-group structure on
AffineHOne; - the connecting homomorphism;
- the isomorphism
AffineHOne ≃+ AffineHTwounder the stated vanishing theorem.
3. “Order-m” should mean exact order only when proved
The condition
says the affine map has order dividing m. Similarly T[m] is the m-torsion subgroup, not the subset of points of exact order m.
Rename the general carrier to “m-periodic affine lifts” or “affine C_m-actions”, and keep the exact-order criterion as a separate theorem.
Verdict
Changes requested, but no longer a major redesign. The torus cohomology is now mathematically correct; the remaining work is to distinguish additive from holomorphic automorphisms and to make the cohomology carrier genuinely group-valued.
Cross-roadmap disposition (applies across #279–#284)
- #279: fix one gluing signature; then merge.
- #280: add the complex-linear analytic input and group-valued connecting API; then merge.
- #281: repair the lattice foundation and monomial-domain theorem before further review.
- #282: make cusp data primitive and resolve degree/Riemann–Hurwitz ownership.
- #283: fix the low-degree relative-homotopy carrier; then merge.
- #284: keep the revised README, but substantially rewrite
Suggested.leanaround genuine manifold orientations, tangent-bundle trivializations, collared boundary data and actual quadratic forms/formations.
|
🤖 Addressed in cd824ce. The additive H¹ theory now uses an additive-subgroup quotient with its group structure, connecting homomorphism, and H¹ ≃+ H² interface. The analytic constructor separately requires a complex-linear lift (or descended biholomorphic automorphism), and all general statements now distinguish period dividing m from exact order and m-torsion from exact-order points. |
CBirkbeck
left a comment
There was a problem hiding this comment.
Part of the third adversarial review of the reusable-roadmap split (#279–#284) and companion roadmaps (#288, #81, #250), reviewed 26 August 2026 against the current heads. This section covers #280 — Complex tori and logarithmic transforms.
Head reviewed: cd824ce9a19df1f9467a18603c71a09cff1fa825
CI status at time of posting: no workflow runs have started on this head yet; the routine build should complete before merging.
Result
Approve mathematically.
All three points from the previous review have been addressed correctly.
-
The analytic constructor now starts from a complex-linear equivalence
E ≃L[ℂ] E, and the file explicitly says that an arbitrary additive torus automorphism does not imply holomorphy. -
AffineHOneis now the additive quotient
not a raw set quotient. It has an inherited AddCommGroup, a genuine connecting homomorphism, and an additive equivalence with
under the equivariant short exact sequence.
- Period dividing
m, exact orderm, and the subgroupT[m]are now distinguished.
The fixed-point criterion checks every nonidentity power for composite m, and the total-space freeness statement remains separate from the base action. I found no new blocker.
Cross-roadmap dependency recommendation — Analytic geometry chain
Acyclic implementation order:
ComplexManifolds
├── ComplexTori
├── AnalyticToricGeometry
└── FuchsianOrbifolds core
ModularForms.LevelOne.JInputs
└── FuchsianOrbifolds.LevelOne
RiemannSurface.Degree (independent lower module)
├── FuchsianOrbifolds applications
└── ModularForms.DimensionFormula
The generic degree/genus module must not depend on the higher ModularForms Riemann–Roch module.
Sources: Birkenhake–Lange, Brown, and Barth–Hulek–Peters–Van de Ven.
Motivating consumer: Levent PDF
AI assistance: Codex (GPT-5) and Codex 5.6 Sol.