canonicalThreshold
plain-language theorem explainer
Defines the canonical recognition threshold as φ − 3/2 in RS-native units. Gravity structural arguments in this module use it as the fixed cutoff for domain-cost comparisons. The body is a one-line real definition from the golden ratio constant.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio.
background
This module records structural gravity predictions of Recognition Science: the unique cost $J(x)=\frac12(x+1/x)-1$, the golden ratio $\varphi$ as the self-similar fixed point, and spatial dimension $D=3$ forced by the forcing chain.
The constant $\varphi$ is imported from the Constants layer (T6 landmark: fixed point of the self-similarity relation tied to $J$). Domain cost is the non-negative real obtained by evaluating $J$ on a positive scale ratio; thresholds on that cost separate regimes in the structural gravity statements.
No upstream lemmas are required: the declaration only names a real built from $\varphi$.
proof idea
Not a proof. One-line definition: bind the real phi - 3/2 (Mathlib arithmetic on the imported golden-ratio constant).
why it matters
Supplies the numerical cutoff used by the structural gravity certificate in this file (siblings such as positivity of the threshold and the inhabited certificate package). It sits under the RS gravity structural claim that $J$, $\varphi$, and $D=3$ are forced (module status: structural theorem, zero sorry). Numerically $\varphi-3/2\approx0.118$, a small positive scale consistent with near-unity recognition ratios. No paper proposition number is attached in the source; the landmark link is T5–T6 ($J$-uniqueness and $\varphi$) rather than a dynamical GR derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.