def definition def or abbrev

`decompose_perturbation`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  20def decompose_perturbation (h : Fin 3 → Fin 3 → ℝ) : Prop :=

proof body

Definition body.

  21  ∃ (tp : TensorPerturbation) (scalar : ℝ) (vector : Fin 3 → ℝ),
  22    h = (fun i j => tp.h_TT 0 i j + (if i = j then scalar else 0) + (vector i + vector j))
  23
  24/-- Existence of a TT projection operator. -/

depends on (6)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
TensorPerturbation in IndisputableMonolith.Relativity.GW.TensorDecomposition decl_use