canonicalThreshold
plain-language theorem explainer
Defines the real scalar threshold φ − 3/2 used in the J-cost derivation of the matter density parameter. Cosmologists working the RS Omega_m structural identity cite it as the cut separating the domain-cost regime from the vacuum piece. The body is a one-line constant abbreviation in terms of the forced golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the unique self-similar fixed point of the Recognition cost (the golden ratio).
background
The module derives the matter density parameter from the J-cost functional. In RS units the structural claim is $\Omega_m/\Omega_\Lambda=(D+1)/(D-1)$; with the forced spatial dimension $D=3$ this ratio equals 2, so $\Omega_m=1-\Omega_\Lambda$ once the vacuum piece is fixed.
$J$ is the unique nonnegative cost satisfying the Recognition Composition Law; $\varphi$ is forced as its self-similar fixed point (forcing chain T5–T6). The sibling domainCost evaluates a nonnegative cost on a real argument; the present constant supplies the numerical cut against which that cost is compared when certifying the matter fraction.
Planck 2018 reports $\Omega_m\approx 0.315$. The module notes that naive substitution of RS-native constants can flip sign relative to laboratory units; the structural ratio, not the raw numerical plug-in, is the theorem content.
proof idea
Pure definition: the real constant is introduced by the single equation $\varphi-3/2$. No tactics, no lemmas. Positivity is discharged separately by the sibling canonicalThreshold_pos.
why it matters
Gives the explicit numerical gate used by the Omega-matter certification bundle in this module (OmegaMatter3Cert, cert). It sits downstream of the forcing chain that produces $\varphi$ (T6) and $D=3$ (T8), and upstream of the structural identity $\Omega_m/\Omega_\Lambda=2$ advertised in the module header. Without a fixed positive threshold the domain-cost comparison that isolates the matter piece has no canonical cut. The definition itself closes no open question; it only names the cut that the surrounding certificates apply.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.