pith. machine review for the scientific record. sign in
theorem other other high

equilibrium

show as:
view Lean formalization →

The equilibrium condition states that the recognition cost vanishes exactly when the scale ratio equals unity. Researchers modeling baryogenesis or climate attractors cite this to anchor their J-cost calculations at the balanced point. The proof reduces directly to the unit lemma for the squared-ratio cost function.

claim$J(1) = 0$, where $J(x) = (x-1)^2/(2x)$ is the recognition cost function.

background

In the Recognition Science framework the J-cost function quantifies recognition cost for a scale ratio x via the explicit squared-ratio form J(x) = (x-1)^2/(2x). This module derives nonlinear dynamics and chaos from RS by equating chaos with J growth once the cost exceeds the J(φ) threshold; five bifurcation types arise from configDim D = 5 and period-doubling reaches the eight-tick octave 2^3. The upstream Jcost_unit0 lemma supplies the base case by direct simplification of the cost definition.

proof idea

One-line wrapper that applies the Jcost_unit0 lemma from the Cost module, which itself simplifies the definition of Jcost.

why it matters in Recognition Science

This anchors the zero-cost reference point in the nonlinear-dynamics setup and feeds directly into BaryogenesisCert (where it certifies matter_balance_equilibrium) and climateJCost_nonneg (where it supports non-negativity). It realizes the fixed-point case of T5 J-uniqueness in the forcing chain, supplying the equilibrium reference for all downstream cost-based derivations in astrophysics, chemistry, and cosmology.

scope and limits

Lean usage

theorem baryoEquil : Jcost 1 = 0 := equilibrium

formal statement (Lean)

  35theorem equilibrium : Jcost 1 = 0 := Jcost_unit0

proof body

  36

used by (40)

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

… and 10 more

depends on (2)

Lean names referenced from this declaration's body.