canonicalThreshold
plain-language theorem explainer
Defines the real number φ − 3/2 as the canonical threshold used in the J-cost baryon-density module. Cosmology workers matching RS predictions for Ω_b h² cite it as the fixed comparison level against domain cost. The body is a one-line definitional assignment to the golden ratio minus three halves.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden-ratio fixed point of Recognition Science.
background
The module aims at a structural exact prediction for the baryon density parameter $\Omega_b h^2$ from the Recognition Science cost $J$. In RS units the golden ratio $\varphi$ is forced as the unique self-similar fixed point (forcing step T6), and the cost is the unique $J(x)=(x+x^{-1})/2-1$ satisfying the Recognition Composition Law.
Module status is a structural theorem with no sorry and no axioms. Earlier numerical sketches in the module header compare candidate closed forms such as $\sqrt{J(\varphi)}/\varphi^3$ or $J(\varphi)^2/\varphi$ against the observational anchor $0.0224$, noting residual factors of order a few.
The threshold $\varphi-3/2$ sits beside a non-negative domain-cost functional on the same file; positivity of the threshold itself is recorded by a sibling lemma.
proof idea
Pure definition: the identifier is bound to the real expression $\varphi - 3/2$ with no proof obligations. Downstream positivity or comparison lemmas unfold this abbreviation and reason about $\varphi>1$.
why it matters
Supplies the fixed numerical level against which domain cost is compared when building the baryon-density exact certificate in this cosmology module. It ties the observational $\Omega_b h^2$ program to the forced golden ratio $\varphi$ (T6) and the unique J-cost (T5), keeping the structural claim free of free parameters. Sibling certificates and inhabited-cert lemmas consume the same constant; the module header still flags residual numerical mismatch factors, so the threshold is scaffolding for the exact closed form rather than the final density identity itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.