SpacetimeRegion
plain-language theorem explainer
SpacetimeRegion packages a positive proper volume in Planck units together with a count of ledger entries and their aggregate J-cost. Cosmologists deriving the cosmological constant from ledger tension in expanding space cite this structure when forming cost densities or checking balance. The declaration is a direct structure definition that introduces the four fields with no further computation or lemmas.
Claim. A spacetime region is a tuple $(V, n, C)$ where $V > 0$ is proper volume in Planck units, $n$ is the number of ledger entries, and $C$ is their total J-cost.
background
Recognition Science defines the J-cost of a recognition event via the functional $J(x) = (x + x^{-1})/2 - 1$ on positive ratios, with global ledger balance requiring the sum of all such costs to vanish. The module COS-006 treats dark energy as the residual tension that appears when cosmic expansion creates new volume that must be populated by fresh entries while the ledger constraint is maintained. Upstream results supply the totalCost functional from LambdaRecDerivation and the cost map from ObserverForcing that feed the fields of this structure.
proof idea
The declaration is a structure definition that directly introduces the four fields volume with its positivity witness, entries, and totalCost. No lemmas or tactics are invoked; the object is the basic data carrier for the downstream density and balance predicates.
why it matters
This structure supplies the basic object for the ledger-tension account of the cosmological constant in the COS-006 module. It is used to define costDensity as totalCost divided by volume and isBalanced as the predicate totalCost = 0. The construction links the global zero-cost constraint to the expanding volume, producing the observed small value of Λ from the Planck-to-Hubble ratio mediated by the golden-ratio ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.