canonicalThreshold
plain-language theorem explainer
Defines the canonical materials threshold as the golden ratio minus three halves, a fixed real used as a comparison level for domain costs in the copper FCC lattice module. Materials theorists working the RS lattice match would cite it when checking positivity or cost bounds. The body is a pure definitional abbreviation, not a derived equality.
Claim. The canonical threshold is the real number $\varphi - \tfrac{3}{2}$, where $\varphi$ is the golden ratio fixed by the Recognition self-similarity equation.
background
Recognition Science forces a unique dimensionless cost $J$ and a unique self-similar scale $\varphi$ (forcing chain T5–T6). In RS-native units many material and mass scales sit on the $\varphi$-ladder. This module treats the copper FCC lattice spacing against that ladder: the structural claim is $\varphi^4 a_0 \approx 3.626,\mathrm{\AA}$ versus the experimental $3.615,\mathrm{\AA}$ (about $0.3%$ relative error), recorded as a match with no sorry and no extra axioms.
The threshold itself is a fixed real cut built from $\varphi$. Sibling definitions in the same file introduce a domain cost functional and prove it is nonnegative; the threshold is the natural comparison value against which those costs are judged. Imports pull in Mathlib reals, the global Constants module (where $\varphi$ lives), and the Cost module (where $J$ and related defect measures live).
proof idea
No proof. The declaration is a one-line definitional abbreviation: the real constant is set equal to $\varphi - 3/2$ by def. Downstream positivity or comparison lemmas (for example the sibling that asserts the threshold is positive) unfold this equality and use elementary arithmetic on $\varphi > 1$.
why it matters
Gives the module a single named cut for cost comparisons in the copper FCC structural match. The module doc frames the work as a structural theorem with zero sorry and zero axioms, tying lattice geometry to the forced scale $\varphi$ from T6. Even with no recorded downstream edges in the graph, the constant is the natural reference for any later certificate that domain cost stays below or above a fixed level, and for the inhabited certificate objects listed as siblings. It does not itself encode the angstrom match; it only supplies the dimensionless threshold those arguments can quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.