GiftPy provides a validated computational pipeline for constructing and analyzing G₂ holonomy metrics on twisted connected sum (TCS) manifolds. The package implements numerical methods for approximating G₂ structures, computing topological invariants, and certifying existence via Joyce’s perturbation theorem. Originally developed for a physics application (the GIFT framework), the geometric tools are general and may be of independent interest to researchers studying exceptional holonomy.
G₂ holonomy metrics are notoriously difficult to compute explicitly. Joyce’s foundational work established existence theorems for compact G₂ manifolds via resolution of orbifolds and perturbation methods, but these proofs are non-constructive. The twisted connected sum (TCS) construction of Kovalev and Corti-Haskins-Nordström-Pacini provides a more explicit path: glue two asymptotically cylindrical Calabi-Yau 3-folds along a common S¹ × K3 boundary. Yet even TCS methods yield existence rather than explicit metric coefficients.
The challenge is threefold. First, the G₂ structure equations are a coupled system of nonlinear PDEs. Second, verifying torsion-freeness (dφ = 0, d*φ = 0) requires computing exterior derivatives of a 3-form defined over a 7-dimensional space. Third, extracting physical quantities such as Betti numbers, harmonic forms, and curvature tensors demands robust numerical methods with quantified error bounds.
GiftPy addresses these challenges through a combination of physics-informed neural networks (PINNs), spectral methods for harmonic form extraction, and formal verification bridges to proof assistants.
The package implements the twisted connected sum framework for G₂ manifolds. Starting from two asymptotically cylindrical (ACyl) Calabi-Yau 3-folds Y₁ and Y₂, each with cylindrical end diffeomorphic to (0, ∞) × S¹ × K3, the construction proceeds:
For the specific construction in GIFT, the building blocks yield Betti numbers computed via Mayer-Vietoris:
| Block | Origin | b₂ | b₃ |
|---|---|---|---|
| M₁ | Quintic in P⁴ | 11 | 40 |
| M₂ | CI(2,2,2) in P⁶ | 10 | 37 |
| K₇ | TCS gluing | 21 | 77 |
Explicit G₂ metrics are approximated using physics-informed neural networks. The network parameterizes a G₂ 3-form φ on a coordinate patch:
Input: x ∈ R⁷
↓
Fourier Features: 64 frequencies → 128 dimensions
↓
Hidden Layers: 4 × 256 neurons (SiLU activation)
↓
Output: 35 independent components of φ ∈ Λ³(R⁷)
Training minimizes a composite loss:
| L = w_T | dφ | ² + w_T | d*φ | ² + w_det | det(g) - target | ² + w_pos ReLU(-λ_min(g)) |
The torsion terms drive toward the torsion-free condition. The determinant constraint fixes the volume form to a specified target (65/32 in the GIFT application). The positivity term ensures the induced metric g(φ) remains positive definite.
Training runs in 5-10 minutes on consumer hardware and achieves:
| T | = 0.00286 (well below Joyce’s threshold) |
Given the trained metric, the pipeline extracts topological invariants:
Betti numbers via spectral analysis: The Hodge Laplacian Δ_k = dd* + d*d is discretized on a mesh. Eigenvalue clustering identifies harmonic forms as zero-modes (up to numerical tolerance). For k=2, spectral analysis recovers b₂ = 21 exactly. For k=3, the spectral gap appears at position 76-77, indicating b₃ = 77 (with one mode at the numerical boundary).
Harmonic form basis: Eigenvectors corresponding to near-zero eigenvalues provide a numerical basis for H^k(K₇). These forms are used downstream for computing integrals, Yukawa couplings, and other geometric quantities.
Curvature tensors: Christoffel symbols, Riemann curvature, Ricci tensor, and scalar curvature are computed via automatic differentiation of the neural network.
A distinctive feature of GiftPy is its connection to formal proof assistants. The numerical results feed into a Lean 4 certificate that establishes existence rigorously.
What is proven: The Lean formalization verifies that Joyce’s perturbation theorem (Theorem 11.6.1 in Compact Manifolds with Special Holonomy) applies to the numerical solution. Specifically:
| Theorem | Statement | Lean Status | ||||
|---|---|---|---|---|---|---|
global_below_joyce |
T | < ε₀ | Proven | |||
joyce_margin |
Safety factor > 35× | Proven | ||||
k7_admits_torsion_free_g2 |
∃ φ_tf torsion-free | Proven |
| The core argument: Joyce’s theorem states that if a compact 7-manifold admits a G₂ structure with sufficiently small torsion, then a nearby torsion-free G₂ structure exists. The PINN solution achieves | T | = 0.00286 against a conservative threshold ε₀ = 0.1, providing a 35× safety margin. |
What remains numerical: The explicit metric coefficients are PINN weights, not closed-form expressions. The harmonic forms are numerical eigenvectors, not analytic formulae. Lean certifies existence bounds rather than computing the exact torsion-free metric.
pip install giftpy
Requirements: Python 3.10+, PyTorch 2.0+, NumPy, SciPy.
import gift_core as gc
# Run the full pipeline
config = gc.PipelineConfig(neck_length=15.0, use_pinn=True)
result = gc.run_pipeline(config)
# Access results
print(f"det(g) = {result.det_g}") # 2.03125
print(f"Torsion = {result.torsion_norm}") # 0.00286
print(f"b₂ = {result.b2}, b₃ = {result.b3}") # 21, 77
# Export Lean certificate
lean_proof = result.certificate.to_lean()
| Module | Content |
|---|---|
gift_core.geometry |
K3, ACyl CY3, TCS construction |
gift_core.g2 |
G₂ 3-form, holonomy, torsion computation |
gift_core.harmonic |
Hodge Laplacian, spectral analysis |
gift_core.nn |
PINN architecture and training |
gift_core.verification |
Lean/Coq certificate generation |
Specificity: The current implementation is tuned for the K₇ construction with b₂ = 21, b₃ = 77. Generalizing to other TCS building blocks (different Fano 3-folds, different gluing diffeomorphisms) requires adapting the topological constraints.
Standard TCS bounds: Note that typical TCS constructions yield b₂ ≤ 9. The GIFT K₇ with b₂ = 21 either employs non-standard building blocks or should be understood via the variational characterization rather than explicit TCS gluing.
Explicit metric: The PINN provides a numerical approximation, not a closed-form metric. For applications requiring analytic expressions, further work is needed.
Moduli space: The uniqueness of the G₂ metric within its moduli class is not addressed. Multiple metrics with the same topological invariants may exist.
Open invitation: Extending GiftPy to other G₂ manifolds (Joyce orbifold resolutions, other TCS examples, or the newer constructions of Foscolo-Haskins-Nordström) would be valuable contributions to the field.
Code repository: github.com/gift-framework/core
Related documentation: S2: K₇ Manifold Construction
GiftPy is part of the GIFT Framework. For the physics application, see the main paper.