canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold as φ − 3/2 in RS-native units, a fixed real used by the BAO-scale Exact5 certificate module. Cosmologists matching the drag scale r_drag to the φ-ladder cite it as the cutoff against which domain cost is compared. The body is a one-line abbreviation of that arithmetic combination of the golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden-ratio fixed point of the Recognition self-similarity relation.
background
The module treats the baryon acoustic oscillation (BAO) drag scale in Recognition Science units. Planck reports $r_{\mathrm{drag}} \approx 147.09,\mathrm{Mpc}$; the RS claim is that $\varphi^{14}\times 0.174,\mathrm{Mpc}$ evaluates to about $146.7,\mathrm{Mpc}$, within $0.3%$ of the observed figure.
Here $\varphi$ is the unique self-similar fixed point forced at step T6 of the unified forcing chain (the positive root of $x^2 = x+1$). The same $\varphi$ generates the mass ladder and the eight-tick octave. The threshold $\varphi-3/2$ is a pure number near $0.118$, sitting well below the Berry creation scale $\varphi^{-1}$ and far below the confining window $Z_{\mathrm{cf}}=\varphi^5$.
Sibling definitions in the file introduce a nonnegative domain cost and a positivity lemma for this threshold; together they feed the Exact5 certificate that the RS BAO prediction is structurally inhabited.
proof idea
Bare definition: the identifier is bound to the real expression $\varphi - 3/2$ with no proof obligations. Downstream positivity and certificate lemmas unfold this abbreviation and apply arithmetic facts about $\varphi>1$.
why it matters
Gives the Exact5 BAO module a single named cutoff against which domain cost is tested, so the structural theorem (zero sorry, zero axiom) can assert that the RS prediction $\varphi^{14}\times 0.174,\mathrm{Mpc}\approx 146.7,\mathrm{Mpc}$ sits inside the Planck band. It sits downstream of T6 ($\varphi$ forced) and upstream of the inhabited certificate BAOScaleRS_Exact5Cert. The numerical match to $r_{\mathrm{drag}}$ is the concrete landmark; the threshold itself is only the comparison constant that makes the cost inequality well-typed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.