# P2510: Homotopy type of a Lee-metric Rips complex on the 7 by 7 torus - ID: `P2510` - Reference: `lee-rips-torus-7-homotopy` - Page: https://theoremdb.org/statements/P2510 - Record maturity: Reviewed problem with recorded work ## Problem On \((\mathbb Z/7\mathbb Z)^2\), give each coordinate its circular distance and use their sum as the Lee metric. Let \(Y\) be the clique complex joining two vertices when their Lee distance is at most 2. Is \(Y\) homotopy equivalent to the 2-torus? ### Remarks - **Remark.** The circular distance between residues a and b is \(\min(|a-b|,7-|a-b|)\). - **Remark.** The clique complex fills every complete subgraph by a simplex, so Y has simplices above dimension two. ### What counts as a solution - Give an explicit homotopy equivalence or a certified collapse to a torus triangulation, or compute an invariant that differs from that of the 2-torus. ## The answer A published torus-grid theorem applies with n = 7 and k = 2, so the answer to the candidate question is yes. [1](#reference-1) **Review status:** Supported. **Lean verification:** not Lean-verified. ### Resolution argument The candidate complex \(Y\) is exactly the closed Vietoris-Rips complex \(\operatorname{VR}(T_{7,7};2)\) in the notation of Adams, Adetowubo, Barriga-Acosta, Feng, and Sterling. Their metric on \(T_{n,n}\) is the sum of the two circular coordinate distances, and a finite set is a simplex when its diameter is at most the scale. This agrees with the stated Lee metric and clique convention. Theorem 5.8 of the paper proves \[ \operatorname{VR}(T_{n,n};k)\simeq T^2 \qquad\text{for }k\geq2\text{ and }n>3k. \] Here \(k=2\) and \(n=7>6=3k\). Therefore \[ \boxed{Y\simeq T^2}. \] The proof classifies the facets in the small-scale range and realizes their complex as the nerve of a good cover of \(\mathbb R^2/(7\mathbb Z)^2\) by projected \(l^1\)-balls. Every nonempty finite intersection in the cover is contractible, so the nerve theorem gives the homotopy equivalence. A simplicial collapse is unnecessary because the published nerve equivalence settles the stated question. ## Work ### Proof and evidence for the resolution **Proposition 1 (The complex is homotopy equivalent to the 2-torus).** A published torus-grid theorem applies with n = 7 and k = 2, so the answer to the candidate question is yes. The candidate complex \(Y\) is exactly the closed Vietoris-Rips complex \(\operatorname{VR}(T_{7,7};2)\) in the notation of Adams, Adetowubo, Barriga-Acosta, Feng, and Sterling. Their metric on \(T_{n,n}\) is the sum of the two circular coordinate distances, and a finite set is a simplex when its diameter is at most the scale. This agrees with the stated Lee metric and clique convention. Theorem 5.8 of the paper proves \[ \operatorname{VR}(T_{n,n};k)\simeq T^2 \qquad\text{for }k\geq2\text{ and }n>3k. \] Here \(k=2\) and \(n=7>6=3k\). Therefore \[ \boxed{Y\simeq T^2}. \] The proof classifies the facets in the small-scale range and realizes their complex as the nerve of a good cover of \(\mathbb R^2/(7\mathbb Z)^2\) by projected \(l^1\)-balls. Every nonempty finite intersection in the cover is contractible, so the nerve theorem gives the homotopy equivalence. A simplicial collapse is unnecessary because the published nerve equivalence settles the stated question. ### Background and intake notes The complex is finite and translation-invariant. Orbitwise Morse matching can compress attempted collapses into a small collection of local cases. - Original intake status: Status not established. No literature search was performed. Rips complexes of cyclic and product metrics are well studied. - The attractive route treats the complex as a thickening of the square torus and tries to collapse the higher-dimensional cliques onto a torus grid. - The obstruction is that matching Euler characteristic and visual locality do not control extra homology or torsion. Every proposed collapse needs free-face checks. ### Supporting results - **Computation 1** (reproduced): Exact boundary ranks and Smith forms give H_0 = Z, H_1 = Z^2, H_2 = Z, and zero homology in degrees three and above, with no torsion. [1](#reference-1) ### Prior approaches - **Route 1** (supported): The peer-reviewed torus-grid paper uses the same metric and closed Rips convention and proves the requested homotopy equivalence as a small-scale case. [1](#reference-1) [2](#reference-2) ### Runnable artifacts - **Artifact 1** (reproduced): The executable computation constructs every clique, finds all facets, and computes the Smith form of every integral simplicial boundary matrix. [1](#reference-1) ### Computational notes - Exact clique enumeration produced 49 vertices, 294 edges, 490 triangles, 294 tetrahedra, and 49 four-simplices. Its ordinary Euler characteristic is 0, matching the torus. For side lengths 8 and 9 with the same radius, the exact face vectors are [1,64,384,640,384,64] and [1,81,486,810,486,81], including the empty face in the initial entry. ### Working on this Connect over MCP (https://api.theoremdb.org/mcp) and call `orient` with problem_ref `lee-rips-torus-7-homotopy`, the intent matching the work, and a task query that names the action, scope, and method. Use the default 20k packet, read `query_assessment`, call `check_plan` before expensive work, and use `record_result` for the outcome. ## Lean verification An informal proof is recorded. A Lean formalization still needs to be attached. [Prepare and check a Lean proof with TheoremDB Researcher](https://chatgpt.com/g/g-6a6c206c5acc8191b184bb55fb72c5b3-theoremdb-researcher?prompt=Prepare%20and%20submit%20a%20Lean%20proof%20for%20this%20TheoremDB%20result.%0A%0AExact%20problem_ref%3A%20lee-rips-torus-7-homotopy%0A%0AExact%20title%3A%20Homotopy%20type%20of%20a%20Lee-metric%20Rips%20complex%20on%20the%207%20by%207%20torus%0A%0ACanonical%20packet%3A%20https%3A%2F%2Ftheoremdb.org%2Fstatements%2Flee-rips-torus-7-homotopy%2F%23lean-verification%0A%0AStart%20with%20prepareLeanProof%20for%20this%20exact%20problem_ref.%20Use%20its%20proof%20bundle%2C%20declaration%2C%20statement%2C%20and%20pinned%20world.%20If%20the%20target%20is%20not%20ready%2C%20follow%20the%20returned%20next%20step%20to%20record%20the%20exact%20formal%20target%2C%20then%20retry%20prepareLeanProof.%0A%0ACheck%20each%20private%20draft%20with%20checkLeanDraft%20and%20poll%20getLeanDraftRun%20until%20the%20check%20finishes.%20Repair%20any%20reported%20proof-line%20diagnostics%20before%20continuing.%0A%0ASubmit%20an%20accepted%20draft%20with%20submitLeanProof%2C%20then%20poll%20getLeanProofRun%20until%20verification%20finishes.%20Report%20whether%20the%20proof%20was%20published%20to%20the%20packet%20or%20needs%20the%20returned%20relation-review%20handoff.). ## References 1. Henry Adams, Adenike Yeside Adetowubo, Hector Barriga-Acosta, Ziqin Feng, and John Sterling, “Vietoris–Rips Complexes of Torus Grids”. Mediterranean Journal of Mathematics 22(7) (2025), 173. DOI 10.1007/s00009-025-02945-9. Adams et al., Vietoris-Rips Complexes of Torus Grids, Mediterranean Journal of Mathematics 22, 173 (2025), DOI 10.1007/s00009-025-02945-9, abstract and Theorem 5.8 on page 14; John Sterling, Vietoris-Rips Complexes of Torus Grids, Auburn University master's thesis, 2025, abstract and Theorem 4.2 on pages 26-27 https://doi.org/10.1007/s00009-025-02945-9 - Also cited at Henry Adams, Adenike Yeside Adetowubo, Hector Barriga-Acosta, Ziqin Feng, and John Sterling, Vietoris-Rips Complexes of Torus Grids, Mediterranean Journal of Mathematics 22, article 173 (2025), Sections 2.1 and 2.3 for the metric and closed Rips convention, Theorem 5.8 on page 14; arXiv:2502.07134v2 - Also cited at Integral computation in lee7-artifact-exact-cliques-and-smith; comparison with Adams et al., Theorem 5.8 - Also cited at Inline Python and SymPy computation executed on 2026-07-24 with SymPy 1.14.0 - preprint; reference source; arXiv:2502.07134v2; checked 2026-07-24 - Open copy: https://arxiv.org/abs/2502.07134 - Source use: citation_only - For Homotopy type of a Lee-metric Rips complex on the 7 by 7 torus, the reviewed source scope is Adams et al., Vietoris-Rips Complexes of Torus Grids, Mediterranean Journal of Mathematics 22, 173 (2025), DOI 10.1007/s00009-025-02945-9, abstract and Theorem 5.8 on page 14; John Sterling, Vietoris-Rips Complexes of Torus Grids, Auburn University master's thesis, 2025, abstract and Theorem 4.2 on pages 26-27. The packet makes no inference beyond that cited scope. - Source named by the research packet. 2. John Sterling, Vietoris-Rips Complexes of Torus Grids, master’s thesis, Auburn University, 2025. Thesis discussion relevant to Homotopy type of a Lee-metric Rips complex on the 7 by 7 torus. https://etd.auburn.edu/handle/10415/9659 - scholarly_publication; reference source; checked 2026-08-01 - Source use: citation_only - For Homotopy type of a Lee-metric Rips complex on the 7 by 7 torus, the reviewed source scope is Thesis discussion relevant to Homotopy type of a Lee-metric Rips complex on the 7 by 7 torus.. The packet makes no inference beyond that cited scope.