canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold equals φ − 3/2 and is strictly positive. Anyone citing the golden-ratio J-cost minimum (J(φ) ≈ 0.118) needs this positivity fact. The proof unfolds the definition and closes by linear arithmetic from the elementary bound φ > 1.5.
Claim. The canonical threshold, equal to the J-cost at the golden ratio $J(\varphi)=\varphi-\tfrac{3}{2}$, is strictly positive: $0<\varphi-\tfrac{3}{2}$.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$ (T5 uniqueness). At the golden ratio $\varphi=(1+\sqrt{5})/2$, forced as the self-similar fixed point (T6), the identity $\varphi+1/\varphi=2\varphi-1$ collapses the cost to $J(\varphi)=\varphi-3/2\approx 0.118$.
This module records structural facts about that minimum value, called the canonical threshold. The local status line is a structural theorem: zero sorry, zero axioms.
The sole upstream input is the elementary lower bound $\varphi>1.5$, obtained from $\sqrt{5}>2$ so that $(1+\sqrt{5})/2>3/2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (which is $\varphi-3/2$), then finish with linarith on the imported lemma $\varphi>1.5$. No further case splits or algebraic identities are required.
why it matters
Puts the golden-ratio recognition cost on a strictly positive footing inside the foundation layer. The same module packages this fact into the structural certificate RSFDNStructural002Cert, so any consumer of that certificate inherits positivity of $J(\varphi)$.
Framework landmarks: T5 (J-uniqueness) supplies the cost functional; T6 forces $\varphi$ as the fixed point at which the cost is evaluated. The numerical value $\varphi-3/2$ sits well below the Berry creation threshold $\varphi^{-1}$ and is the natural floor for cost comparisons on the $\varphi$-ladder.
No external downstream theorems yet (used-by list empty); the lemma is presently a local gate for the module certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.