lambda_positive
plain-language theorem explainer
The cosmological constant is shown positive in the Recognition Science ledger-tension model, establishing repulsive dark energy from global balance during expansion. Cosmologists deriving acceleration from first principles in this framework would cite the result when connecting ledger costs to the Hubble scale. The proof is a direct term reduction that unfolds the definition as three times the square of the Hubble parameter and confirms the inequality by numerical normalization.
Claim. In Recognition Science the tension energy density defined by the cosmological constant satisfies $3 H_0^2 > 0$, where $H_0$ denotes the present-day Hubble parameter in natural units.
background
The module COS-006 derives dark energy from ledger tension: the requirement that total J-cost sums to zero globally conflicts with the creation of new spacetime volume during expansion, leaving a residual positive energy density. The cosmological constant is defined as this tension energy per unit volume and scales as $H_0^2$ in natural units with $c=1$. The Hubble parameter $H_0$ is given numerically as $2.2$ times $10^{-18}$ in the same units. Upstream structures supply the discrete phi-tier densities and the J-cost factorization used to calibrate the ledger.
proof idea
The term proof unfolds the definitions of cosmologicalConstant and H0, then applies norm_num to reduce the resulting arithmetic inequality to a manifestly true numerical statement.
why it matters
The result closes the sign of the cosmological constant inside the COS-006 ledger-tension derivation, confirming that expansion produces a repulsive term consistent with the Recognition Science forcing chain. It supports the module claim that Lambda emerges as the J-cost of maintaining coherence across growing volume and aligns with the eight-tick octave scaling that sets the ratio of Planck to Hubble scales. No downstream theorems are recorded yet, so the declaration stands as a terminal sign check within the dark-energy block.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.