canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold as φ − 3/2 in real numbers. Elastic-modulus and domain-cost arguments on the phi-ladder cite this constant as the comparison level. The body is a pure definitional abbreviation; no proof work is required.
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 module derives a structural elastic-modulus estimate from the phi-ladder (Plan v7, 119th pass). Status is zero-sorry, zero-axiom. The target scale is steel-like stiffness: empirical $E \sim 200$ GPa versus the RS estimate $\varphi^{10}\cdot 2,\mathrm{GPa}\approx 246$ GPa ($\varphi^{10}\approx 123$).
$\varphi$ is imported from Constants as the unique positive fixed point of the self-similarity relation forced at T6. The Cost import supplies the J-cost and related non-negativity infrastructure used by sibling domain-cost lemmas. The threshold $\varphi-3/2$ sits just above zero ($\varphi\approx 1.618$) and serves as the comparison value against which domain costs are measured.
proof idea
Pure definition. The right-hand side is the arithmetic expression $\varphi - 3/2$ with no further lemmas or tactics.
why it matters
Supplies the numeric cut-off used by the ElasticMod4 certificate and the positivity lemma for the same constant. In the broader RS chain it is a local physics-scale constant built from the T6 value of $\varphi$, not a new forcing step. It lets the module compare domain costs to a fixed positive level while keeping the elastic-modulus claim structural (no axioms). Downstream certificate inhabitants rely on this name rather than inlining the arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.