canonicalThreshold
plain-language theorem explainer
Defines the canonical cost threshold as φ − 3/2 in RS-native units. Materials and crystal-structure arguments cite it when comparing domain costs against a fixed cutoff for 3D Bravais classification. The body is a one-line real constant built from the golden ratio.
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 aims at a structural count of 3D Bravais lattices from configuration dimension (Plan v7), with status claimed as a structural theorem (no sorry, no axiom). The informal count sketch is $14 = 2\cdot(2^3-1)$, doubling the $D=3$ octave count for dual lattice structure.
Recognition Science forces $\varphi$ at T6 as the unique self-similar fixed point tied to the J-cost $J(x)=(x+x^{-1})/2-1$. The Cost import supplies the cost language used by sibling definitions such as domain cost and its nonnegativity. This constant sits beside those cost objects as the fixed numerical cutoff against which domain costs are compared in the crystal-structure certificates.
proof idea
Pure definition: the real is introduced by the closed form $\varphi - 3/2$. No lemmas, tactics, or proof obligations.
why it matters
Gives a single named cutoff for the materials layer that classifies 3D crystal configurations via cost. Sibling positivity (canonicalThreshold_pos) and the Bravais certificate objects (Bravais3Cert, cert, cert_inhabited) are the natural consumers: they need a concrete positive scale built from $\varphi$ rather than an ad hoc real. Ties the materials count to the forcing-chain landmarks T6 ($\varphi$) and T8 ($D=3$), and to the eight-tick octave that underlies the informal $2\cdot(2^3-1)$ Bravais sketch in the module doc. Does not itself close the lattice enumeration; it only standardizes the threshold those certificates use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.