structure definition def or abbrev

`EdgePerturbation`

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

formal statement (Lean)

  81structure EdgePerturbation (nE : ℕ) where
  82  eta : Fin nE → ℝ
  83
  84/-- Linearization coefficients: for each (hinge, edge) pair, the partial
  85    derivative of the deficit angle with respect to the edge length,
  86    evaluated at the flat background. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

SimplicialFieldCurvatureCert in IndisputableMonolith.Foundation.SimplicialLedger.SimplicialDeficitDischarge decl_use
DeficitLinearizationCert in IndisputableMonolith.Geometry.DeficitLinearization decl_use
linearizedDeficit in IndisputableMonolith.Geometry.DeficitLinearization decl_use
linear_regge_vanishes in IndisputableMonolith.Geometry.DeficitLinearization decl_use

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
eta in IndisputableMonolith.Cosmology.Nucleosynthesis decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
deficit in IndisputableMonolith.Geometry.DihedralAngle decl_use
deficit in IndisputableMonolith.Geometry.Schlaefli decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
eta in IndisputableMonolith.Relativity.Geometry.Metric decl_use