canonicalThreshold
plain-language theorem explainer
Defines the real constant φ − 3/2 as the canonical numerical threshold used in the short-GRB duration module. Astrophysicists working the RS duration ladder cite it when comparing domain costs or positivity bounds against a fixed RS-native cutoff. The body is a one-line arithmetic definition in terms of the golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio fixed by the self-similarity axiom of Recognition Science.
background
Recognition Science forces the golden ratio $\varphi$ as the unique self-similar fixed point of the cost functional (forcing step T6). In RS-native units many dimensionless cutoffs are simple polynomials in $\varphi$.
This module treats short gamma-ray burst durations. The structural claim is that the observed short-GRB window sits between $\varphi^{-2}$ and $\varphi^{-1}$ seconds (approximately 0.382–0.618 s), inside the broader observational band 0.1–2 s. The module is marked structural (zero sorry, zero axiom).
Sibling definitions introduce a non-negative domain cost on the same real line; the constant defined here supplies the fixed comparison value against which that cost is measured.
proof idea
Pure definition: the real constant is introduced by the arithmetic expression $\varphi - 3/2$. No proof obligations arise at the definition site; positivity and downstream comparisons are handled by sibling lemmas.
why it matters
Supplies the fixed RS-native cutoff that the short-GRB module uses when it asserts structural agreement between the $\varphi$-ladder duration window and observation. It sits beside the domain-cost family and the module certificate, giving a single named real against which non-negativity and matching statements can be stated without repeating the arithmetic. The value is downstream of T6 ($\varphi$ forced) and is local scaffolding for the GRB duration MATCH claim recorded in the module header; it does not itself encode the duration bounds $\varphi^{-2}$–$\varphi^{-1}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.