structure definition def or abbrev

`LedgerDensity`

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

formal statement (Lean)

 169structure LedgerDensity where
 170  /-- Number of transactions per unit volume. -/
 171  density : ℝ
 172  /-- Density is non-negative. -/
 173  nonneg : 0 ≤ density
 174
 175/-- Mass from ledger density (the claim). -/

used by (2)

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

curvatureFromLedger in IndisputableMonolith.RRF.Foundation.Ledger decl_use
massFromLedger in IndisputableMonolith.RRF.Foundation.Ledger decl_use

depends on (13)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
Mass in IndisputableMonolith.Constants.RSNativeUnits decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
from in IndisputableMonolith.Foundation.PrimitiveDistinction decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
volume in IndisputableMonolith.Papers.GCIC.BrainHolography decl_use
density in IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS decl_use