canonicalThreshold
plain-language theorem explainer
Names the real threshold φ − 3/2 used as the comparison scale in the ISM dust-fraction module. Anyone citing the Module 9 structural MATCH (J(φ)² ≈ 1.39% vs ~1% empirical) needs this constant. It is a one-line arithmetic definition in the RS constant φ; no proof work.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the self-similar fixed point of the Recognition cost.
background
Astrophysics RS Module 9 treats the interstellar-medium dust fraction. The module headline is structural: $J(\varphi)^2 \approx 1.39%$, compared with the empirical ~1% dust fraction, and is marked MATCH with zero sorry and zero axioms.
The cost $J$ is the unique continuous solution of the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The constant $\varphi$ is forced as the self-similar fixed point at T6 of the unified forcing chain and is imported from Constants.
Sibling definitions in the same file introduce a domain cost, its nonnegativity, and a positivity lemma for this threshold; the present declaration simply freezes the numeric scale $\varphi-3/2$ for those comparisons.
proof idea
Definition only. The body is the arithmetic expression $\varphi - 3/2$ in the imported RS constant $\varphi$; there is no tactic proof and no lemma application.
why it matters
Supplies the named real scale against which the Module 9 domain cost is judged in the ISM dust-fraction certificate. The module claims a structural MATCH between $J(\varphi)^2$ and the observed ~1% dust fraction; this threshold sits next to domainCost and the positivity fact for the same constant. It is local astrophysics scaffolding, not a forcing-chain landmark (T5–T8), but it inherits $\varphi$ from T6 and $J$ from the RCL/J-uniqueness step. Downstream certificate objects in the file package the MATCH claim around this scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.