structure definition def or abbrev

`Hinge`

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

formal statement (Lean)

 163structure Hinge (_L : SimplicialLedger.SimplicialLedger) where
 164  deficit : ℝ
 165
 166/-- A *codimension-0 or codimension-1* stratum of the ledger: the
 167    3-simplex interior or a 2-face shared between two simplices.
 168    Neither carries curvature by the flat-interior axiom. -/

used by (2)

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

cubicDeficitFunctional in IndisputableMonolith.Foundation.SimplicialLedger.CubicDeficitDischarge decl_use
conformal_edge_length_flat in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
or in IndisputableMonolith.Constants.EulerMascheroni decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
SimplicialLedger in IndisputableMonolith.Foundation.SimplicialLedger decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
deficit in IndisputableMonolith.Geometry.DihedralAngle decl_use
deficit in IndisputableMonolith.Geometry.Schlaefli decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
two in IndisputableMonolith.QFT.SpinStatistics decl_use