canonicalThreshold
plain-language theorem explainer
Defines the canonical ecological threshold as $\varphi - 3/2$ in RS-native units. Ecologists and RS foundation workers cite it when comparing domain costs against a fixed positive cutoff for biotic interaction certificates. The body is a pure definitional constant, not a derived equality.
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 Ecology module treats the five classical biotic interaction types (competition, mutualism, predation, amensalism, commensalism) as the five axes of the recognition configuration space, matching configDim $D = 5$. Costs on those axes are measured with the RS cost functional imported from Cost, and compared against fixed real cutoffs.
$\varphi$ is the unique positive self-similar fixed point forced at T6 of the unified forcing chain; it is the base of the RS ladder and appears throughout Constants. Subtracting $3/2$ places the threshold slightly above zero ($\varphi - 3/2 \approx 0.118$), so it sits between the Berry creation scale $\varphi^{-1}$ and ordinary $O(1)$ costs.
Sibling lemmas such as nonnegativity of domain cost and positivity of this threshold turn the constant into a usable comparison value for certificates.
proof idea
Definitional constant: the right-hand side is the literal real expression $\varphi - 3/2$ with no proof obligations, tactics, or lemmas. Downstream positivity is proved separately.
why it matters
Gives Ecology a single named cutoff against which domain costs are scored when building biotic-interaction certificates (four-type and inhabited certs in the same module). Anchors the structural claim that the five ecological interaction types arise from five-axis recognition geometry rather than from ad-hoc biology. Uses the forced constant $\varphi$ (T6) so the threshold is not a free parameter. Does not itself close the ecology story; it only supplies the numeric gate those certificates compare against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.