canonicalThreshold
plain-language theorem explainer
Defines the canonical inflation threshold as the real number φ − 3/2. Cosmology workers in Recognition Science cite it when fixing the cost cutoff that separates the inflationary domain from the post-inflation regime. The body is a one-line constant abbreviation in terms of the forced self-similar scale φ.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the unique self-similar fixed point of the Recognition cost.
background
The module fixes Recognition Science inflation observables: spectral index $n_s$ and tensor-to-scalar ratio $r$. Status is structural (zero sorry, zero axiom). Reported RS values are $n_s = 1 - 2/45 = 0.9556$ (about 2.1σ from the quoted 0.9649) and $r = 2/(45\varphi^2) \approx 0.0169 < 0.036$.
Here $\varphi$ is the T6 fixed point of the forcing chain (the unique positive solution of the self-similarity relation tied to the J-cost $J(x) = (x + x^{-1})/2 - 1$). The Cost import supplies that J-cost and nonnegativity infrastructure; Constants supplies $\varphi$. Sibling domainCost is the cost functional on the inflationary domain against which this threshold is compared.
proof idea
Pure definition: the real constant is introduced by the arithmetic expression $\varphi - 3/2$. No lemma applications, tactics, or proof obligations.
why it matters
Gives a single named cutoff for the inflation-parameter certificate in this module (siblings canonicalThreshold_pos, InflationParam5Cert, cert). In the RS picture the threshold sits a fixed offset below $\varphi$, so domain-cost comparisons stay dimensionless and φ-native. It supports the structural claim that RS passes on $r$ and sits inside 3σ on $n_s$, without introducing free scales. No forcing-chain step (T0–T8) is proved here; the definition only packages the numerical gate used by the local certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.