canonicalThreshold
plain-language theorem explainer
Defines the real constant φ − 3/2 used as the comparison threshold in the baryon density module. Cosmologists matching RS ladder predictions to Ω_b ≈ 0.049 cite it when relating the golden-ratio cost scale to the observed baryon fraction. The body is a one-line real literal built from the forced fixed point φ.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio (self-similar fixed point of the Recognition ladder).
background
The module treats the baryon density parameter on the Recognition Science phi-ladder (Plan v7, 119th pass). It records the structural claim that the observed $\Omega_b \approx 0.049$ sits near the RS cost scale $J(\varphi)/2 \approx 0.059$, and treats the match as consistent.
Here $\varphi$ is the unique self-similar fixed point forced by the T6 step of the unified forcing chain. The cost $J$ is the unique nonnegative functional satisfying the Recognition Composition Law, normalized so $J(x)=(x+x^{-1})/2-1$. The threshold $\varphi-3/2$ is the elementary real offset used to place that cost scale against the baryon fraction window.
No external cosmological data enter the definition itself; it is pure RS arithmetic on $\varphi$.
proof idea
Pure definition: the right-hand side is the real expression $\varphi-3/2$ with $\varphi$ imported from the Constants module. No lemmas, tactics, or rewriting are required.
why it matters
Supplies the numeric cut used by the OmegaBaryon4 certificate and its positivity sibling. In the broader framework it sits on the T6-forced $\varphi$ ladder that also produces the eight-tick octave and the mass yardstick. The module status note ties the threshold to the rough numerical agreement $J(\varphi)/2\sim 0.059$ versus $\Omega_b\approx 0.049$; the definition itself does not close that comparison, but gives the constant against which later inequalities are stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.