pith. machine review for the scientific record. sign in
theorem proved term proof high

lambda_positive

show as:
view Lean formalization →

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.

claimIn 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 106theorem lambda_positive : cosmologicalConstant > 0 := by

proof body

Term-mode proof.

 107  unfold cosmologicalConstant H0
 108  norm_num
 109
 110/-! ## The Dark Energy Density -/
 111
 112/-- Critical density of the universe. -/

depends on (9)

Lean names referenced from this declaration's body.