cdt-rs

Causal Dynamical Triangulations using Constrained Delaunay Triangulations in Rust

Introduction

For an introduction to Causal Dynamical Triangulations, see this paper.

Roadmap

• Use Kani to verify correctness
• Use an existing Rust Delaunay triangulation library (e.g. Spade), or write one that can be verified by Kani?
• 2D Delaunay triangulation
• 1+1 foliation
• 2D ergodic moves
• 2D Metropolis-Hastings
• Diffusion-accelerated MCMC?
• Visual output
• 3D Delaunay triangulation
• 2+1 foliation
• 3D ergodic moves
• 3D Metropolis-Hastings
• Visual output
• 4D Delaunay triangulation
• 3+1 foliation
• 4D ergodic moves
• 4D Metropolis-Hastings
• Initialize masses in 3D with Constrained Delaunay Triangulation
• Initialize masses in 4D with Constrained Delaunay Triangulation
• Shortest path
• Geodesic distance
• Einstein tensor
• Quantize spacetime!

Issues

• Spade 2.3.0 is broken - Fixed with Spade 2.3.1