canonicalThreshold
plain-language theorem explainer
Defines the canonical recognition threshold as the real number φ − 3/2, with φ the golden-ratio fixed point of the RS cost. Cited wherever relational-QM domain costs are compared against a fixed cutoff in a J-cost frame. The body is a one-line abbreviation; no proof obligations.
Claim. The canonical threshold is the real constant $\varphi - 3/2$, where $\varphi$ denotes the golden-ratio self-similar fixed point of the Recognition cost.
background
The module develops Relational Quantum Mechanics in the Recognition Science sense: each observer carries a J-cost frame, so absolute scale is frame-dependent while ratios of the form J(observable/reference) are shared. The cost J is the unique symmetric generator fixed by the Recognition Composition Law (T5), and φ is its self-similar fixed point (T6).
In that setting one needs a fixed real cutoff against which domain costs are tested. This declaration simply names that cutoff as φ − 3/2. Sibling facts in the same file establish non-negativity of the domain cost and positivity of this threshold; the present item only introduces the constant.
proof idea
Bare definition: the identifier is bound to the real expression φ − 3/2 drawn from the Constants import. No tactics, no lemmas, no proof term beyond the arithmetic expression itself.
why it matters
Supplies the numerical gate used by the Relational QM3 certificate in this module (siblings RelationalQM3Cert, cert, cert_inhabited). In the RS forcing chain, φ is forced at T6; subtracting 3/2 places the cutoff just below the unit scale of the cost, consistent with treating small J-defects as “same domain” for observer agreement. The module claims a structural theorem (0 sorry, 0 axiom) linking Rovelli-style observer dependence to J-cost frames; this constant is the concrete threshold those comparisons invoke. It is not itself a forcing step, but a named parameter of the relational-QM layer built on T5–T6.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.