isBalanced
plain-language theorem explainer
A spacetime region counts as balanced exactly when its total J-cost vanishes. Cosmologists deriving the cosmological constant from Recognition Science ledger tension cite this predicate as the global balance constraint in the COS-006 derivation. The definition is introduced by direct equality on the totalCost field of the region structure.
Claim. A spacetime region $R$ is balanced when its total J-cost satisfies $R.totalCost = 0$.
background
The COS-006 module derives dark energy from ledger tension: the ledger must balance globally while expansion creates new volume that requires fresh entries, producing residual tension energy identified with Lambda. The SpacetimeRegion structure records proper volume (in Planck units), a positivity proof, the number of ledger entries, and the total J-cost of those entries. Upstream totalCost definitions compute this quantity as a sum of per-entry J-costs (QuantumLedger), sector sums without cross terms (SMLagrangianSkeleton), or normalized bit-plus-curvature terms (LambdaRecDerivation), with the balance residual stated to vanish at the optimal scale.
proof idea
Direct definition that equates the balance predicate to the equality of the totalCost field to zero on the SpacetimeRegion structure.
why it matters
This supplies the zero-strain predicate consumed by Glossary.isBalanced, isConsistent, JMinimizationLaw, and the Octave wellPosed and preserves_equilibria results. It encodes the ledger balance constraint step of the COS-006 derivation that identifies Lambda with the J-cost per unit volume of maintaining coherence across expanding space. The definition therefore sits at the interface between the J-cost functional (T5 uniqueness) and the cosmological constant extraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.