canonicalThreshold
plain-language theorem explainer
Defines the canonical dark-energy threshold as φ − 3/2 in RS-native units. Cosmology certificates and equation-of-state arguments cite this constant when comparing domain cost against the vacuum floor. The body is a one-line real abbreviation of the golden ratio minus three-halves.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition ladder).
background
The module treats the dark-energy equation of state in Recognition Science. Its structural claim is that $w = -1$ exactly in RS; a DESI measurement of $w \neq -1$ at $2\sigma$ would falsify the framework.
Constants are imported from the RS constants layer: $\varphi$ is the unique positive fixed point forced by self-similarity (forcing step T6). The cost layer supplies the J-cost $J(x) = (x + x^{-1})/2 - 1$ used to score domain defects. Sibling definitions in this file introduce a domain cost and prove it is nonnegative, then compare that cost to the present threshold.
Numerically $\varphi \approx 1.618$, so $\varphi - 3/2 \approx 0.118$. The threshold sits between the Berry creation scale $\varphi^{-1}$ and the dream fraction $\varphi^{-3}$ on the same ladder.
proof idea
Pure definition: the real constant is introduced by abbreviation as $\varphi - 3/2$. No proof obligations. Downstream positivity is handled by the sibling lemma that this value is strictly positive.
why it matters
Gives a named RS-native scale against which dark-energy domain cost is measured in the v5 equation-of-state certificate. The module status is structural (zero sorry, zero axiom) and asserts $w = -1$ exactly; this threshold is the comparison constant that makes that certificate well-typed.
It sits in the cosmology domain of the monolith and inherits $\varphi$ from the forcing chain (T6). Parent certificates such as the DEoS5 certificate and its inhabited instance are expected to reference it when stating that vacuum cost lies below or at the canonical floor. Open empirical pressure comes only from external DESI-style $w$ measurements, not from the definition itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.