canonicalThreshold
plain-language theorem explainer
The canonical BIT dark-energy threshold is the real number φ − 3/2 (numerically ≈ 0.118). It is the upper endpoint of the allowed δw₀ interval in the BIT kernel family. Cosmologists and RS foundation work cite it as the maximum equation-of-state drift. The body is a one-line arithmetic definition in the RS constant φ.
Claim. Define the canonical threshold by $T := \varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
The module builds the BIT kernel family v3 from the J-cost. The Recognition cost is $J(x) = (x + x^{-1})/2 - 1$. Because $\varphi$ obeys $\varphi = 1 + 1/\varphi$, one has $J(\varphi) = \varphi - 3/2$ exactly. The module sets the BIT dark-energy drift $\delta w_0$ in the closed interval $[0, J(\varphi)]$.
The canonical kernel is $K(z) = 1/(1+z)$. At best fit $\delta w_0 = 0$ one recovers pure $\Lambda$; at the upper endpoint $\delta w_0 = J(\varphi)$ the equation-of-state drift reaches its maximum value $\approx 0.118$. The constant $\varphi$ itself is forced at step T6 of the unified forcing chain; $c=1$ and related RS units come from the Constants import.
Sibling material in the same file treats a domain cost built from $J$ and a positivity certificate for this threshold.
proof idea
Pure definition: the real is introduced by the arithmetic expression $\varphi - 3/2$. No tactic proof, no lemmas. Downstream positivity (the sibling that asserts the threshold is positive) is the natural first consumer.
why it matters
Pins the numerical upper bound that the module doc quotes as maximum BIT drift $0.118$. In the Recognition framework this value is not free: it equals $J(\varphi)$, so the dark-energy window is fixed by the same J-uniqueness (T5) and $\varphi$-forcing (T6) that generate the rest of the ladder. The definition therefore sits at the interface between the foundation cost calculus and the BIT cosmological kernel $K(z)=1/(1+z)$. It supplies the concrete constant that certificates and domain-cost comparisons in this file are written against. No open sorry is involved; the object is structural scaffolding for the zero-sorry BITKernel3 certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.