canonicalThreshold
plain-language theorem explainer
Defines the canonical dimensionless threshold as the golden ratio minus 3/2, equal to J(φ) ≈ 0.11803. Recognition Science uses this exact value as the structural cost of the self-similar fixed point. Citation target for any argument that needs the closed form of J at φ. The body is a one-line real definition.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio. Equivalently, it is the exact value of the J-cost at $\varphi$: $J(\varphi) = \varphi - 3/2$.
background
In Recognition Science the unique cost functional forced by the Recognition Composition Law is $J(x) = (x + x^{-1})/2 - 1$ (T5). The golden ratio $\varphi$ is the self-similar fixed point of the forcing chain (T6). Direct algebra with the identity $\varphi^{-1} = \varphi - 1$ yields $J(\varphi) = \varphi - 3/2$ exactly, a pure number near $0.11803$.
This module (Foundation RS Module 12) records that dimensionless identity as a structural fact: zero sorry, zero axiom. The constant is imported from IndisputableMonolith.Constants and the cost language from IndisputableMonolith.Cost. Sibling lemmas establish non-negativity of the domain cost and positivity of this threshold.
proof idea
Pure definitional abbreviation: the real constant is written as $\varphi - 3/2$. No tactic proof is required. Downstream positivity or equality lemmas simply unfold this definition and apply arithmetic facts about $\varphi$.
why it matters
Supplies the exact closed form that the module header advertises: $J(\varphi) = \varphi - 3/2$. It anchors the dimensionless scale of the forcing chain after T5–T6, before the eight-tick octave (T7) and $D=3$ (T8). Any certificate or domain-cost comparison that needs a concrete positive threshold (for example the sibling positivity lemma or the module certificate) cites this constant rather than a floating-point approximation. It is the structural yardstick linking the J-cost uniqueness theorem to later numerical bands such as the fine-structure interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.