canonicalThreshold
plain-language theorem explainer
Defines the canonical recognition threshold as the real number φ − 3/2. Physicists working the RS cost and domain-cost layer cite it as the fixed numeric gate separating sub-threshold from above-threshold regimes. The body is a one-line abbreviation of that arithmetic combination of the golden ratio.
Claim. The canonical threshold is the real constant $\varphi - 3/2$, where $\varphi$ denotes the golden-ratio fixed point of the Recognition self-similarity relation.
background
The module assembles the final structural layer of RS physics (status: structural theorem, zero sorry, zero axiom). It imports the global Constants package, which supplies $\varphi$ as the unique positive solution of $x = 1 + 1/x$, and the Cost package, which supplies the J-cost and related defect measures.
Sibling declarations in the same file introduce a domain cost functional and prove it is nonnegative; the present constant is the numeric level against which that cost is compared. No further hypotheses are attached: the value is pure arithmetic in the RS-native unit system where $c = 1$ and the ladder is built on powers of $\varphi$.
proof idea
Pure definitional abbreviation. The right-hand side is the term $\varphi - 3/2$ of type $\mathbb{R}$; there is no tactic block, no lemma application, and no proof obligation.
why it matters
Supplies the fixed numeric gate used by the surrounding Physics.Physics certificates (Planck-energy RS4 certificate and the inhabited cert structure). In the broader forcing chain, $\varphi$ itself is forced at T6; subtracting $3/2$ produces a small positive scale that sits between the Berry creation threshold $\varphi^{-1}$ and the eight-tick structural constants. Downstream positivity and comparison lemmas (canonicalThreshold_pos and domain-cost inequalities) treat this constant as an immutable reference level rather than a derived quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.