canonicalThreshold
plain-language theorem explainer
Defines the canonical recognition threshold as φ − 3/2, which equals the J-cost at the golden ratio. Anyone citing the Maxwell-demon bound in Recognition Science uses this as the per-bit floor. The body is a one-line real constant, not a proof.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio. Equivalently it is $J(\varphi)$ for the cost $J(x)=(x+x^{-1})/2-1$.
background
The module recasts Maxwell's demon in Recognition Science: a demon cannot drive the J-cost below one recognition quantum per bit processed. The cost functional is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the Recognition Composition Law and the T5 step of the forcing chain.
The golden ratio $\varphi$ is the self-similar fixed point (T6). Because $\varphi^{-1}=\varphi-1$, a short calculation yields $J(\varphi)=\varphi-3/2$. That value is the minimal positive cost scale appearing in the demon argument and is therefore named the canonical threshold.
Local imports supply only Mathlib, the RS constants (including $\varphi$), and the Cost module that defines $J$.
proof idea
Pure definition: the real constant is written as the closed form $\texttt{phi} - 3/2$. No lemmas are invoked. The identity with $J(\varphi)$ is immediate from the algebraic relation $\varphi+\varphi^{-1}=2\varphi-1$ and the definition of $J$, but that identity is not proved inside this declaration.
why it matters
Supplies the numerical floor used by the Maxwell-demon certificate in the same module (siblings such as $\texttt{canonicalThreshold_pos}$ and $\texttt{MaxwellDemon2DeepCert}$). The module status line states a structural theorem with zero sorry and zero axioms: the demon cannot reduce J-cost below $J(\varphi)$ per bit. That quantum is exactly this threshold, linking the information-erasure bound to the T5–T6 forcing landmarks (unique $J$, forced $\varphi$). Downstream certificates compare domain costs against it; without the constant the positivity and inhabitation claims have nothing to measure against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.