canonicalThreshold
plain-language theorem explainer
The canonical threshold for the Physics structural certificate at recognition rung 46 is the real number φ − 3/2. Anyone checking domain-cost positivity or the M46 certificate against the golden-ratio ladder cites this constant. It is a one-line definition in terms of the RS fixed point φ.
Claim. The canonical threshold is the real constant $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of Recognition Science.
background
Recognition Science forces a unique dimensionless cost $J$ and a unique self-similar scale $\varphi$ (forcing steps T5–T6). Masses and structural cutoffs sit on the $\varphi$-ladder; thresholds are therefore expressed as simple polynomials in $\varphi$.
This module is the structural Physics certificate at recognition rung 46 (Plan v7, 120th pass). It is marked as a structural theorem with zero sorry and zero axioms. The local objects are a domain cost, its non-negativity, and a certificate package that packages those facts.
The constant $\varphi$ is imported from IndisputableMonolith.Constants. Numerically $\varphi\approx 1.618$, so $\varphi-3/2\approx 0.118$, a small positive scale used as a comparison level for the domain cost.
proof idea
Pure definition: the real is set equal to $\varphi - 3/2$. No lemmas or tactics are involved. Downstream positivity of the threshold is proved separately by comparing $\varphi$ to $3/2$.
why it matters
Structural certificates pin RS predictions at fixed rungs without free parameters. Rung 46 is the Physics domain certificate; the threshold $\varphi-3/2$ is the comparison value against which the domain cost is measured. It sits downstream of the forcing chain that uniquely determines $\varphi$ (T6) and upstream of the certificate inhabitation and non-negativity lemmas in the same module. The value is deliberately elementary so that positivity reduces to the elementary inequality $\varphi>3/2$, which follows from the closed form of $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.