canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as φ − 3/2, the golden-ratio offset used as the comparison level in the Gap-45 exact certificate. Anyone citing the structural Gap-45 identities (45 = D²(D+2) from D = 3) or the domain-cost nonnegativity lemmas will pull this constant. It is a bare definitional abbreviation, not a proved inequality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
The module Gap45_Exact_v2 packages the structural identity gap-45 = 45 = D²(D+2) = 9·5 that follows once spatial dimension is fixed at D = 3 (forcing step T8). The same integer 45 appears as a classical angle (π/4), a mechanical optimum, and the human chromosome count offset, all traced to that dimensional forcing.
The golden ratio φ is the unique positive fixed point forced by self-similarity (T6) after J-cost uniqueness (T5). Constants and Cost are imported so that φ and the J-cost are available in RS-native units. Sibling definitions introduce a domain cost and prove it is nonnegative; the present constant supplies the numerical cut against which that cost is compared.
proof idea
Pure definitional abbreviation: the real constant is declared equal to φ − 3/2 by unfolding. No tactics, no lemmas, no proof obligations.
why it matters
Supplies the fixed real level used by the Gap-45 exact certificate and by the positivity lemma for the canonical threshold itself. In the Recognition chain it sits downstream of T6 (φ forced) and T8 (D = 3), converting those forcing results into a concrete numeric gate for the structural 45-count. The module claims a structural theorem with zero sorry and zero axioms; this constant is the numeric hinge of that certificate. It does not itself prove the 45-identity, but every comparison that certifies domain cost against the gap uses it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.