canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as $\varphi - 3/2$, the golden-ratio offset used as a comparison level for domain costs in the RS physics stack. Anyone checking positivity or barrier arguments against the eight-tick QCD structural solution would cite it. The body is a one-line arithmetic definition from the forced constant $\varphi$.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
Recognition Science forces $\varphi$ as the unique self-similar scale (forcing step T6) and the eight-tick octave as the discrete period $2^3$ (T7). Module 8 packages the structural claim that QCD $\theta = 0$ follows from that eight-tick uniqueness, solving the strong CP problem without a dynamical axion.
Costs in the stack are measured by the J-cost $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$). Sibling definitions in this module introduce a domain cost and prove it is nonnegative; the present constant supplies a fixed real barrier against which those costs are compared.
Numerically $\varphi \approx 1.618$, so $\varphi - 3/2 \approx 0.118 > 0$. The definition lives in RS-native units imported from Constants and Cost.
proof idea
Pure definition: the real constant is written as the difference $\varphi - 3/2$. No lemmas, tactics, or hypotheses. Downstream positivity (sibling canonicalThreshold_pos) is the natural next check that this offset is strictly positive.
why it matters
Gives a single named barrier level for cost comparisons inside the Module 8 structural theorem that QCD $\theta = 0$ follows from eight-tick uniqueness. That theorem is marked structural (zero sorry, zero axiom) and is the RS answer to the strong CP problem.
The offset is built from $\varphi$, already forced by T5–T6 (J-uniqueness and the self-similar fixed point), so the threshold inherits the same uniqueness rather than being an adjustable parameter. It sits beside domain-cost nonnegativity in the same file and is the natural scale against which those costs are tested when closing the eight-tick argument.
No open scaffold is attached: the declaration is a closed arithmetic definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.