`IndisputableMonolith.Relativity.GW`

IndisputableMonolith/Relativity/GW.lean · 16 lines · 0 declarations

Explainer status: pending

   1-- Gravitational Waves Module Aggregator
   2import IndisputableMonolith.Relativity.GW.TensorDecomposition
   3import IndisputableMonolith.Relativity.GW.ActionExpansion
   4import IndisputableMonolith.Relativity.GW.PropagationSpeed
   5import IndisputableMonolith.Relativity.GW.Constraints
   6
   7/-!
   8# Gravitational Waves Module
   9
  10Provides tensor perturbation theory for gravitational wave propagation:
  11- `TensorDecomposition` - TT gauge decomposition h_ij^TT
  12- `ActionExpansion` - Quadratic action for tensor modes
  13- `PropagationSpeed` - c_T² = 1 + O(αC) modification
  14- `Constraints` - GW170817 bounds on scalar coupling
  15-/
  16

source mirrored from github.com/jonwashburn/shape-of-logic