costDensity
plain-language theorem explainer
The average J-cost per unit volume within a spacetime region supplies the local energy density for dark energy derivations. Researchers deriving the cosmological constant from ledger tension in Recognition Science would reference this quantity. It is obtained by dividing the region's total ledger cost by its proper volume.
Claim. For a spacetime region $R$ with total J-cost $C$ and proper volume $V > 0$, the cost density is given by $C / V$.
background
The Cosmology.DarkEnergy module derives the cosmological constant from ledger tension: the ledger must balance globally while expansion creates new volume that requires fresh entries. A spacetime region is a structure holding positive proper volume in Planck units, a count of ledger entries, and the total J-cost of those entries. Upstream, the total cost functional is defined as the sum of normalized bit cost and curvature cost, with the balance residual vanishing at the optimal scale. J-cost primitives are supplied by the multiplicative recognizer comparator and by the cost of recognition events.
proof idea
This is a one-line definition that divides the totalCost field of the input region structure by its volume field.
why it matters
This definition supplies the local energy density that enters the module's definitions of expansion tension and the cosmological constant. It realizes the ledger-tension origin of dark energy, consistent with the phi-ladder and the eight-tick octave from the forcing chain. The module targets a derivation of Lambda approximately equal to the square of the Hubble parameter times a small factor, yielding the observed 10^{-122} scale in Planck units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.