expansionTension
plain-language theorem explainer
Expansion tension quantifies the residual J-cost incurred when new spacetime volume requires fresh ledger entries to preserve global balance. Cosmologists working in Recognition Science would cite this when tracing the cosmological constant to ledger dynamics under expansion. The definition is a direct product of the volume increment, entry density, and J-cost evaluated at the golden ratio.
Claim. Let $V$ denote spacetime volume and $e$ the entry density (entries per unit volume). The expansion tension is $(V_2 - V_1) e J(phi)$, where $J$ is the J-cost function satisfying the Recognition Composition Law.
background
The module derives dark energy from ledger tension: global J-cost balance must hold, yet expansion creates new volume that demands additional entries. Entry density is the ratio of ledger entries to volume in a given spacetime region. J-cost is the function $J(x) = (x + x^{-1})/2 - 1$ that appears throughout the forcing chain and satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ (imported from the Cost module).
proof idea
One-line definition that multiplies the volume difference by entry density and by the J-cost evaluated at the golden ratio. No auxiliary lemmas or tactics are invoked beyond the arithmetic operations and the imported Jcost constant.
why it matters
The definition supplies the explicit tension energy density that the module equates with the cosmological constant. It fills the quantitative step in the COS-006 ledger-tension derivation of Lambda and connects directly to the phi-ladder and eight-tick structure of the forcing chain. No downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.