pith. machine review for the scientific record. sign in
def definition def or abbrev high

isBalanced

show as:
view Lean formalization →

isBalanced encodes the global ledger balance condition for any spacetime region by requiring its aggregate J-cost to vanish. Researchers deriving the cosmological constant from Recognition Science ledger tension cite this predicate to express the zero-residual constraint during cosmic expansion. The definition reduces directly to the totalCost field of the SpacetimeRegion structure.

claimA spacetime region $R$ satisfies the balance condition precisely when its total J-cost vanishes: totalCost$(R) = 0$.

background

SpacetimeRegion is the record type carrying proper volume, positive volume proof, entry count, and total J-cost for a ledger segment. The module derives dark energy as residual tension when the global ledger must remain balanced while expansion adds new volume that requires fresh entries. Upstream totalCost definitions supply the summation: QuantumLedger.totalCost sums per-entry costs, LambdaRecDerivation.totalCost combines normalized bit and curvature terms, and SMLagrangianSkeleton.totalCost aggregates sector contributions.

proof idea

One-line definition that directly projects the totalCost field of the SpacetimeRegion record and asserts equality to zero.

why it matters in Recognition Science

This predicate supplies the zero-strain anchor used by RRF.Core.Glossary.isBalanced, isConsistent, and JMinimizationLaw, and by Octave.preserves_equilibria. It implements the module's core step that the cosmological constant equals the per-volume J-cost of preserving ledger coherence across expanding space, linking to the T5 J-function and the global balance requirement in the forcing chain.

scope and limits

formal statement (Lean)

  84def isBalanced (R : SpacetimeRegion) : Prop := R.totalCost = 0

proof body

Definition body.

  85
  86/-- The ledger density: entries per unit volume. -/

used by (23)

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

depends on (9)

Lean names referenced from this declaration's body.