canonicalThreshold
plain-language theorem explainer
The canonical threshold used in the Recognition Science Alcock–Paczynski analysis is the real constant φ − 3/2. That value is exactly the J-cost at the golden-ratio fixed point, J(φ). Cosmologists citing the RS geometric-distortion prediction take it as the numerator of the exponent J(φ)/D. The declaration is a one-line numeric definition.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the self-similar fixed point of Recognition Science (the golden ratio).
background
The module treats the Alcock–Paczynski (AP) test as a pure geometric distortion: the ratio of perpendicular to parallel scale factors $\alpha_\perp/\alpha_\parallel$. In Recognition Science that ratio is forced to $\varphi^{J(\varphi)/D}$, with $D=3$ spatial dimensions from the forcing chain (T8).
The cost functional is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), unique by T5. Because $\varphi$ satisfies $\varphi=1+1/\varphi$, one has $J(\varphi)=\varphi-3/2$. Numerically $J(\varphi)\approx 0.118$, so the AP exponent is $J(\varphi)/3\approx 0.039$ and the predicted ratio is $\varphi^{0.039}\approx 1.064$.
The constant $\varphi$ itself is imported from IndisputableMonolith.Constants (T6 fixed point). No further hypotheses are required for the definition.
proof idea
Pure definition: the real is bound to the closed-form expression $\varphi-3/2$. There is no proof body, no tactic, and no lemma application. Downstream positivity and certificate lemmas simply unfold this abbreviation.
why it matters
This constant is the structural numerator of the RS Alcock–Paczynski exponent. The module status line records a structural theorem (0 sorry, 0 axiom) whose predicted distortion is $\varphi^{J(\varphi)/D}=\varphi^{0.039}\sim 1.064$. Sibling lemmas (canonicalThreshold_pos, Alcock5Cert, cert) package the same number into a non-negativity fact and an inhabited certificate for the AP claim.
Within the broader framework it sits on T5 (J-uniqueness), T6 ($\varphi$ forced), and T8 ($D=3$). It does not itself close any open forcing step; it only names the concrete real that those steps already determine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.