canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold as the real number φ − 3/2. Domain-coverage and milestone certificates in this physics module treat it as the fixed comparison level for domain cost. The body is a one-line arithmetic definition from the golden ratio constant; no proof obligations.
Claim. The canonical threshold is the real constant $\varphi - 3/2$, where $\varphi$ denotes the golden ratio (the self-similar fixed point of Recognition Science).
background
This module is a structural milestone certificate (FinalModule_1399): zero sorry, zero axioms, aimed at domain-coverage bookkeeping in the Recognition Physics layer.
The golden ratio $\varphi$ is imported from the Constants stack. In the forcing chain it is the unique self-similar fixed point (T6). Sibling definitions in the same file introduce a domain cost functional and a positivity lemma for this threshold, then package them into a MilestoneCert.
The numerical value is small and positive: $\varphi \approx 1.618$, so $\varphi - 3/2 \approx 0.118$. It sits in the same family of φ-native cutoffs as the Berry creation threshold $\varphi^{-1}$, but is a distinct linear shift used for domain-cost comparison rather than creation energetics.
proof idea
Pure definition: the real is assigned by the closed form phi - 3/2. No tactics, no lemmas, no reduction. Downstream positivity or comparison facts (e.g. the sibling that the threshold is positive) must be proved separately from properties of $\varphi$.
why it matters
Gives a single named cutoff that domain-cost and milestone-certificate constructions can cite without re-inlining $\varphi - 3/2$. In the Recognition framework it is local scaffolding for the domain-coverage milestone, not a forcing-chain step (T0–T8) and not the mass-ladder or α-band machinery. It keeps the certificate module’s comparison level φ-native and auditable. No parent theorems are recorded on the depends/used-by edges for this declaration itself; its role is to feed sibling positivity and MilestoneCert packaging in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.