Relativity and quantum mechanics. Dependently-typed structures for physics in Idris.
Feynman propagator with mass 20. (Cyp)
A set of Idris libraries for relativity and quantum physics, exploring library design for physical computations in the presence of full dependent types.
Much of the functionality is not sufficiently performant for serious work, which could be addressed by interfacing with another runtime. For now the library is to be considered a prototype.
Idris v0.19 at least is probably required.
Notes on a few constituent modules.
Data types representing the quantum operators of the n-qubit state space, and functions on them, especially implementing their algebra.
Data types for n-qubit state vectors, and functions involving both vectors and operators. In particular, we can calculate outcome probabilities and expectation values for any observables.
Writing down a field theory for fermions requires a representation of the gamma matrix algebra. In even dimensions (d = 2k + 2) this is a set of d square matrixes with size 2^(k+1). The next odd-dimensional representation is formed by adding an additional matrix of the same size, corresponding to the product of all the others. We implement functions to recursively define gamma matrices of arbitrary dimension starting with d = 2. These numerical properties are enforced by the type system.
Data type Marks representing the number of ways to choose n objects from a set of m, along with related functions and proofs. Used to make ScalarGraphs.
Data type for correct-by-construction Feynman graph topologies with a fixed interaction order, i.e. a fixed number of line-endpoints connected to each vertex.
Various constructions needed for the spinor helicity formalism for scattering amplitudes in quantum field theory.
Type-safe representations of quantum energy spectra and basis vectors, with cardinalities and degeneracies specified at the type level. Separate types for finite versus infinite dimensional systems.