entryDensity
plain-language theorem explainer
entryDensity computes the average ledger entries per unit volume for any spacetime region. Researchers deriving the cosmological constant from ledger tension in the COS-006 framework cite this quantity when quantifying the deficit created by cosmic expansion. The definition is a direct quotient of the two fields supplied by the SpacetimeRegion structure.
Claim. For a spacetime region $R$ equipped with ledger entry count $n$ and proper volume $V>0$, the entry density is defined by $d(R) := n/V$.
background
The module COS-006 treats dark energy as residual ledger tension arising when global J-cost balance must be maintained while new spacetime volume appears. SpacetimeRegion is the basic data structure carrying a positive real volume (in Planck units) together with a natural-number count of ledger entries and their total J-cost. Upstream cost functions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost values that populate the totalCost field, while the volume definition imported from BrainHolography supplies the geometric measure.
proof idea
This is a one-line definition that extracts the entries and volume fields of the input SpacetimeRegion and returns their quotient.
why it matters
The definition supplies the density argument required by the downstream expansionTension function, which identifies the resulting tension energy density with the cosmological constant. It therefore operationalizes the ledger-balance constraint stated in the module doc-comment and connects directly to the Recognition Science forcing chain in which expansion creates new volume that must be populated by entries whose J-cost yields the observed dark-energy scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.