HEXAGONbeta

The Chaise Longue Theorem: Conjecture 1.2 of Degtyarev–Shimada for the Fermat varieties of every degree in every even dimension, and the integral Hodge conjecture for those whose degree is prime, equal to 4, or prime to (n+1)!

A mix of human-written and AI-generated textHuman understanding: some partsmath.AG — Algebraic Geometrymath.AC — Commutative Algebramath.CO — Combinatorics

Contributed by Rafael Amichis Luengo ↗

Version 1 / Oct 13, 2026 / CC BY 4.0

Abstract

Let X⊂Pn+1X \subset \mathbb{P}^{n+1} be the complex Fermat variety of degree m≥3m \ge 3 and even dimension n=2kn = 2k, and let L(X)⊆Hn(X;Z)L(X) \subseteq H_n(X; \mathbb{Z}) be the subgroup generated by the classes of its standard kk-dimensional linear subspaces. Degtyarev and Shimada conjectured that Hn(X;Z)/L(X)H_n(X; \mathbb{Z})/L(X) is torsion free [DS, Conjecture 1.2]. We prove this conjecture for every degree m≥3m \ge 3 in every even dimension, modulo two topological results used by [DS]: Pham's theorem on the homology of the affine Fermat variety, and their intersection numbers. Its algebraic form — the quotient Z[G]/(ψJ)\mathbb{Z}[G]/(\psi_J) of the group ring of [DS] is free abelian of rank m2k+1−Qk(m)m^{2k+1} - Q_k(m) — is proved with no topology, and it has been verified for every degree by a complete proof in the proof assistant Lean 4 with the Mathlib library, with no gap and no axiom beyond the three standard ones. The proof reduces the conjecture, prime by prime, to dimension counts in truncated polynomial rings, proved by peeling off one variable at a time. Consequences: the integral Hodge conjecture for XX whenever mm is prime, or m=4m = 4, or mm is prime to (n+1)!(n+1)!, with the integral Hodge classes of middle degree generated by the standard linear subspaces — in particular for the Fermat quartic of every even dimension; and the primitivity of the sublattices spanned by the linear subspaces that [DS] exhibit on the partial Fermat varieties, which [DS] proved conditionally on the conjecture. This work has not been refereed by a human expert.

Provenance statement

The author, Rafael Amichis Luengo, does not write mathematics. He chose the problem, directed the work for more than two and a half months, and gave ideas in plain words — images — each translated into a precise statement before anything was measured. For the even degrees the image of a light aeroplane set the direction and two «wings» carried weight (the step for the prime 2, and «the odd comes before the even», which became a recursion used in §8). According to the author, the whole route (the Hodge–Fermat campaign, the cases k = 2 and k = 3, and this paper) took more than a thousand hours, and this paper alone 76 days of almost full-time work. Three attached files tell how the work was done and say what belongs to whom: THE_STORY_AND_THE_NUMBERS.md (the team and its roles, the method of images and what each image produced, the archive, the dead routes, the announcement of 23 September that was retracted the same day, and the numbers); ON_AI_AND_MATHEMATICS.md (the division of the work, in the author's voice and then the auditor's); and HOW_THE_EVEN_DEGREES_WERE_CLOSED.md (the even degrees, 2–4 October). The proofs and the text were written by instances of Claude (Anthropic), working in separate roles from written missions: constructors that proposed and wrote proofs; auditors that re-derived every step and ran checks with their own code; and cold readers with no access to the audits. Earlier versions were also read by AI systems of two other providers (ChatGPT, OpenAI; Gemini, Google). Computations were used as checks, never as steps of a proof. The algebraic form of the main theorem (Main Theorem′, every degree) and Theorem O were formalized in Lean 4 with Mathlib (233 files, 41 243 lines, 1 859 theorems and lemmas, no sorry, standard axioms only); the topology of [DS] (Pham's theorem and their intersection numbers) is cited, not formalized. The Lean proofs were written by Aristotle (Harmonic) from pieces written from the paper, compiled on the author's machine and audited; the Lean certificate was read cold before release. No human expert has refereed this work. Paper, version 12: https://doi.org/10.5281/zenodo.23129698. Lean certificate: https://doi.org/10.5281/zenodo.23129677. Repository with the full record (missions, reports, audits, cold readings, engines, logs and the Lean project): https://github.com/tretoef-estrella/chaise-longue-theorem. This TeX source was generated from the version-12 text by a script (md2tex_chaise.py) and checked against it word by word.
AI provenance filesHOW_THE_EVEN_DEGREES_WERE_CLOSED.md · 15 KBON_AI_AND_MATHEMATICS.md · 7 KBTHE_STORY_AND_THE_NUMBERS.md · 20 KB

Tools used

Anthropic
Claude Code
Harmonic
Aristotle
Lean
LeanVersion v4.28.0
Lean
Mathlib
Python
Python
Singular
Singular
Macaulay2
Macaulay2

References

  1. M. F. Atiyah, F. Hirzebruch, Analytic cycles on complex manifolds , Topology 1 (1962), 25--45. ( 1.3 only.)
  2. E. Aljovin, H. Movasati, R. Villaflor Loyola, Integral Hodge conjecture for Fermat varieties , J. Symbolic Comput. 95 (2019), 177--184. doi:10.1016/j.jsc.2019.02.006; arXiv:1711.02628.arXivDOI
  3. A. Degtyarev, I. Shimada, On the topology of projective subspaces in complex Fermat varieties , J. Math. Soc. Japan 68 (2016), no. 3, 975--996. doi:10.2969/jmsj/06830975; arXiv:1405.4683 (v3, 14 July 2015). Theorems 1.1, 1.4, 2.1, 2.2, Conjecture 1.2, Definition 1.3, Corollaries 1.5--1.7, Claim 4.3, Remark 4.4, Lemma 4.5 and 4-- 5 (including 4.6) were read in the original.arXivDOI
  4. L. de Moura, S. Ullrich, The Lean 4 theorem prover and programming language , in: Automated Deduction -- CADE 28, Lecture Notes in Computer Science 12699 , Springer, 2021, 625--635. doi:10.1007/978-3-030-79876-5_37. ( 14.8 only.)DOI
  5. A. Degtyarev, Lines generate the Picard groups of certain Fermat surfaces , J. Number Theory 147 (2015), 454--477. doi:10.1016/j.jnt.2014.07.020; arXiv:1305.3073. (Cited in [DS] as reference [3], under a slightly different title.)arXivDOI
  6. A. Degtyarev, Projective spaces in Fermat varieties , arXiv:1512.06199 (19 December 2015). Conjecture 4.4, (4.5)--(4.6) and Corollaries 4.7--4.8 were read in the original.arXiv
  7. N. Aoki, On some arithmetic problems related to the Hodge cycles on the Fermat varieties , Math. Ann. 266 (1983), 23--54; erratum Math. Ann. 267 (1984), 572. doi:10.1007/BF01458703. ( 1.3, 12.1 (H5). Theorem A (p. 24), its proof ( 7, pp. 41--43) and the definitions of 0 were read in the original; the erratum concerns only Theorem B.)DOI
  8. R. Bezrukavnikov, S. Riche, L. Rider, Modular affine Hecke category and regular unipotent centralizer , arXiv:2005.05583 (v2, 4 July 2024; the first version carried , I in the title). ( 1.6, 1.8, 10, 11.1, 14.6, 15 and 16; 2.1-- 2.6 were read in the arXiv source, in particular Proposition 2.12 and the proof of Lemma 2.13.)arXiv
  9. R. K. Brylinski, Limits of weight spaces, Lusztig's qq-analogs, and fiberings of adjoint orbits , J. Amer. Math. Soc. 2 (1989), no. 3, 517--533. (Remark 10.4(5) only; not read in the original.)
  10. D. Cox, J. Little, D. O'Shea, Ideals, Varieties, and Algorithms , Undergraduate Texts in Mathematics, Springer, 2nd ed., 1997. (Macaulay's basis theorem: the standard monomials of an ideal form a basis of the quotient.)
  11. L. Cerlienco, M. Mureddu, From algebraic sets to monomial linear bases by means of combinatorial algorithms , Discrete Math. 139 (1995), 73--87. (Remark 5.10(4) only.)
  12. C. De Concini, C. Procesi, A characteristic free approach to invariant theory , Adv. Math. 21 (1976), 330--354. (Remark 10.3(2) only.)
  13. D. Favero, T. L. Kelly, The Chern character of a coherent sheaf on a smooth projective hypersurface , arXiv:2609.12759 (11 September 2026). ( 1.3 and 1.10 only; the abstract and 1 were read in the arXiv version.)arXiv
  14. V. Ginzburg, Loop Grassmannian cohomology, the principal nilpotent and Kostant theorem , arXiv:math/9803141 (v2). (Remark 10.4 only; 4 was read in the arXiv source.)arXiv
  15. A. M. Garsia, C. Procesi, On certain graded SnS_ n -modules and the qq-Kostka polynomials , Adv. Math. 94 (1992), 82--138. (Remark 10.4(4); Appendix A, remark after Definition A.11; Complement to Theorem 5.9.)
  16. R. Amichis Luengo, The Hammock Theorem , Zenodo (2026). doi:10.5281/zenodo.21382543. ( 1.8 only.)DOI
  17. R. Jumagulov, The Hodge conjecture for Fermat fourfolds of odd degree at most 199 , arXiv:2608.18134 (28 July 2026). ( 1.3 and 15 only; cited for the statement in its abstract.)arXiv
  18. G. D. James, The Representation Theory of the Symmetric Groups , Lecture Notes in Mathematics 682 , Springer, 1978. (Remark 4.2(3) only.)
  19. J. C. Jantzen, Representations of Algebraic Groups , 2nd ed., Mathematical Surveys and Monographs 107 , American Mathematical Society, 2003. (Remarks 10.3(2) and 10.4(3) only.)
  20. N. Koblitz, A. Ogus, Algebraicity of some products of values of the function , Proc. Sympos. Pure Math. 33 , Part 2, Amer. Math. Soc., 1979, 343--345. (Quoted through [Ran]; not read in the original.)
  21. J. Kollár, Trento examples , in: Classification of irregular varieties (Trento, 1990), Lecture Notes in Math. 1515 , Springer, 1992, 134--139. ( 1.3 only.)
  22. S. Kumar, N. Lauritzen, J. F. Thomsen, Frobenius splitting of cotangent bundles of flag varieties , Invent. Math. 136 (1999), 603--621. (Remark 10.4(3) only; quoted through [BRR]; not read in the original.)
  23. D. E. Knuth, Overlapping Pfaffians , Electron. J. Combin. 3 (1996), no. 2, #R5; arXiv:math/9503234. ( 8.3 and 1.10; 0-- 3 and 6 were read in the arXiv version.)arXiv
  24. B. Kostant, Lie group representations on polynomial rings , Amer. J. Math. 85 (1963), 327--404. ( 1.6, 10, 14.6 and 16; quoted through [Gin]; not read in the original.)
  25. R. Amichis Luengo, The Chaise Longue Theorem --- Lean certificate , version 2 (3 October 2026, every degree, and Theorem O), doi:10.5281/zenodo.23129677, and in [Rep], folder lean/ ; version 1 (29 September 2026, odd degrees) is doi:10.5281/zenodo.23045371. Both versions were read cold before release. ( 1.0, 14.6 and 14.8 only.)DOI
  26. L. Liu, Filtrations of tilting modules and costalks of parity sheaves , arXiv:2007.12444 (24 July 2020). (Remark 10.4(5) only; the introduction was read.)arXiv
  27. G. Lusztig, Singularities, character formulas, and a qq-analog of weight multiplicities , Astérisque 101--102 (1983), 208--229. (Remark 10.4(5) only; not read in the original.)
  28. O. Mathieu, Filtrations of G-modules , Ann. Sci. École Norm. Sup. (4) 23 (1990), no. 4, 625--644. (Remarks 10.3(2) and 10.4(3) only.)
  29. R. Amichis Luengo, The Chaise Longue Theorem and the centralizer of a regular unipotent element (supplementary note, version 1, 1 October 2026), deposited with this version of the paper in the same Zenodo record, and in [Rep], paper/ . ( 1.8 and 14.6 only; not refereed.)
  30. The mathlib Community, The Lean mathematical library , in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 367--381. doi:10.1145/3372885.3373824. ( 14.8 only.)DOI
  31. J. Milnor, Morse Theory , Annals of Mathematics Studies 51 , Princeton University Press, 1963. ( 7, the Lefschetz theorem on hyperplane sections; used in 12.1 and Appendix B.)
  32. M. Mizukami, Birational mappings from quartic surfaces to Kummer surfaces (in Japanese), Master's thesis, University of Tokyo, 1975. ( 1.3 and 1.10 only; quoted from [SSvL, 3 and 6]; not read.)
  33. M. Miranda, H. Movasati, L. Rufino, R. Villaflor, Lengths of Hodge characters in Fermat varieties , arXiv:2609.27301 (v2, 26 September 2026). ( 1.3 and 1.10 only; the abstract and 1 were read in the arXiv version.)arXiv
  34. S. Okada, Pfaffian formulas and Schur Q-function identities , Adv. Math. 353 (2019), 446--470. doi:10.1016/j.aim.2019.07.006; arXiv:1706.01029. ( 8.3 and 1.10; 2, in particular Proposition 2.3 and its proof, was read in the arXiv version.)arXivDOI
  35. R. Amichis Luengo, The Chaise Longue Theorem --- working record , github.com/tretoef-estrella/chaise-longue-theorem (2026). Contains, among the author's earlier documents, The Localization Theorem and The Block Decomposition (the splitting of the group ring over FpF_ p into blocks, June 2026), The Watermark Theorem (4 June 2026) and The Double Ladder Theorem (5 June 2026), the machine verdicts of The Hodge--Fermat Campaign , and every engine and log of 14. These documents have not been refereed. The repository is public since 26 September 2026; it also contains the Lean 4 project of 14.8 (folder lean/ ).
  36. F. Pham, Formules de Picard--Lefschetz généralisées et ramification des intégrales , Bull. Soc. Math. France 93 (1965), 333--367. (Appendix B only.)
  37. Z. Ran, Cycles on Fermat hypersurfaces , Compositio Math. 42 (1980/81), no. 1, 121--142. (Numdam CM_1980__42_1_121_0. Proposition 1.7, Proposition 1.8(i) and Theorem 4.9 were read in the original.)
  38. S. Riche, Kostant section, universal centralizer, and a modular derived Satake equivalence , arXiv:1411.3112 (v4, 19 May 2015). (Remark 10.4(3) only; the introduction and 2.2 were read in the arXiv source.)arXiv
  39. T. Shioda, The Hodge conjecture for Fermat varieties , Math. Ann. 245 (1979), no. 2, 175--184. doi:10.1007/BF01428804. (Quoted as in [DS] and [Ran]; not read in the original.)DOI
  40. T. Shioda, T. Katsura, On Fermat varieties , Tôhoku Math. J. (2) 31 (1979), no. 1, 97--115. (Quoted as in [DS] and [Ran]; not read in the original.)
  41. R. Amichis Luengo, The Sofa Theorem , Zenodo (2026). doi:10.5281/zenodo.21288551. ( 1.8 only.)DOI
  42. M. Schütt, T. Shioda, R. van Luijk, Lines on Fermat surfaces , J. Number Theory 130 (2010), no. 9, 1939--1963. ( 1.3 and 1.10; 3 and 6 were read in the arXiv source.)
  43. T. Tanisaki, Defining ideals of the closures of the conjugacy classes and representations of the Weyl groups , Tôhoku Math. J. (2) 34 (1982), no. 4, 575--585. (Appendix A, remark after Definition A.11; Complement to Theorem 5.9.)
  44. C. Voisin, Abel--Jacobi map, integral Hodge classes and decomposition of the diagonal , J. Algebraic Geom. 22 (2013), no. 1, 141--174. ( 1.3 only; Theorem 2.11 is quoted as in [AMV, 1]; not read in the original.)
  45. R. Amichis Luengo, The Watermark and Double Ladder Theorems (Verified in Lean) , Zenodo (2026). doi:10.5281/zenodo.23062529. (Remark 12.2, 15 and 16 only; not refereed.)DOI
  46. R. Amichis Luengo, The Watermark in Every Even Dimension , Zenodo (2026). doi:10.5281/zenodo.23091046. (Remark 12.2 and 15 only; not refereed.)DOI
  47. L. C. Washington, Introduction to Cyclotomic Fields , 2nd ed., Graduate Texts in Mathematics 83 , Springer, 1997. ( 12.1 only; not read in the original.)

Version history

  1. v1Submitted by Rafael Amichis LuengoInitial depositCurrentOct 13, 2026