canonicalThreshold
plain-language theorem explainer
Canonical cosmological threshold fixed as φ − 3/2 in RS-native units. Cosmology certificates and domain-cost comparisons cite this cutoff when testing vacuum structure against a positive scale. The declaration is a one-line arithmetic definition in the golden ratio; positivity is proved separately.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio (the unique positive self-similar fixed point of the Recognition forcing chain).
background
This module develops Recognition Science cosmology as a structural theorem package: the vacuum equation of state is forced to $w = -1$ exactly, so a sustained DESI Y3 deviation from $w=-1$ at $2\sigma$ would falsify the framework. Present DESI BAO values ($w_0\approx -0.95$, $w_a\approx -0.27$) show only mild tension.
The constant $\varphi$ is imported from Constants (T6: the unique positive fixed point of the self-similarity relation forced by the J-cost). Domain costs in the same file are built from the Recognition cost functional $J$, so a fixed positive real threshold is needed to separate negligible vacuum defects from reportable cosmological signals. The value $\varphi - 3/2$ is that working cutoff.
proof idea
Pure definition: the symbol is bound to the real expression $\varphi - 3/2$. No lemmas, tactics, or hypotheses. Downstream positivity (canonicalThreshold_pos) and certificate constructions treat the value as an ordinary positive real constant.
why it matters
Gives cosmology proofs a single named scale against which domain costs and EOS certificates are compared. The parent module asserts $w=-1$ exactly from the RS vacuum; any certified comparison of vacuum cost to this threshold inherits that structural claim. In the broader chain, $\varphi$ is the T6 fixed point, so the threshold is not an external fit parameter but a pure function of the forced self-similar constant. Sibling certificates (EOSDeep4Cert, cert) sit in the same file and are the natural consumers when the graph is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.