canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold is strictly positive. Anyone using the Maxwell-demon J-cost floor cites this to guarantee a genuine per-bit lower bound rather than a vacuous zero. The argument is a one-line wrapper: unfold the threshold and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold equals $J(\varphi)=\varphi-\tfrac{3}{2}$ and satisfies $0<J(\varphi)$, where $\varphi=(1+\sqrt{5})/2$ is the golden ratio and $J(x)=(x+x^{-1})/2-1$ is the unique recognition cost.
background
This module reformulates Maxwell's demon in Recognition Science: a demon cannot drive the J-cost of a processed bit below $J(\varphi)$. The quantity $J(\varphi)$ is the recognition quantum per bit (demon information gain equals that quantum times bits erased).
The cost $J$ is the unique continuous solution of the Recognition Composition Law forced at T5; $\varphi$ is the self-similar fixed point forced at T6. Direct evaluation gives $J(\varphi)=\varphi-3/2$. The sibling definition canonicalThreshold packages exactly that value.
The sole upstream fact used here is the elementary bound $\varphi>1.5$ (from $\sqrt{5}>2$), which immediately forces the threshold above zero.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (exposing an expression equivalent to $\varphi-3/2$), then invoke linear arithmetic with the lemma $\varphi>1.5$. No further case splits or algebraic identities are required.
why it matters
Positivity turns the Maxwell-demon floor into a genuine strict lower bound rather than a non-negative placeholder. The module status line records a structural theorem (zero sorry, zero axiom) whose certificate siblings (MaxwellDemon2DeepCert, cert, cert_inhabited) rest on a positive recognition quantum per bit.
Framework landmarks: T5 J-uniqueness supplies the cost shape; T6 forces $\varphi$ as the fixed point at which the quantum is evaluated. The result is local bookkeeping inside the Foundation layer; it does not itself close the full demon impossibility argument, but every later citation of the per-bit floor needs this inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.