canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold φ − 3/2 used in the J-cost treatment of the reionization endpoint. Cosmologists working the RS redshift ladder cite it as the fixed comparison value against domain cost. It is a bare constant abbreviation, not a proved inequality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio fixed by the Recognition self-similarity equation.
background
The module derives the end of cosmic reionization from the Recognition J-cost. Status is structural: zero sorry, zero axioms. Observationally reionization finishes near $z\sim 5.5$–6; the RS side matches powers of $\varphi$ (roughly $\varphi^3\approx 4.24$, $\varphi^4\approx 6.85$).
Here $\varphi$ is the unique self-similar fixed point forced at T6 of the unified forcing chain. The J-cost is the unique symmetric cost $J(x)=(x+x^{-1})/2-1$ from T5. Sibling definitions package a domain cost on the reionization side and certificates that compare that cost to a fixed real cutoff.
This declaration simply names that cutoff: $\varphi-3/2$. Numerically $\varphi\approx 1.618$, so the threshold sits near $0.118$, a small positive scale natural for late-time residual cost.
proof idea
No proof. The declaration is a one-line real abbreviation: subtract $3/2$ from the imported constant $\varphi$. Downstream positivity and certificate lemmas treat the name as that literal value.
why it matters
Gives a single named real against which the reionization domain cost is measured, so endpoint certificates stay free of magic numbers. It sits in the cosmology layer that ties the J-cost (T5) and $\varphi$ (T6) to the observed end of reionization near $z\sim 5.5$–6, consistent with the module’s $\varphi$-power ladder. Parent certificates in the same file (endpoint cert and inhabitedness) are the immediate consumers; the broader forcing chain is only background.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.