canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used for crystal-structure configuration costs is strictly positive. Materials workers in the RS Bravais-count development cite it whenever a positive cutoff built from φ is required. The proof is a one-line wrapper: unfold the definition, then finish by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the real constant defined in this module by a simple expression in the golden ratio $\varphi$.
background
This module develops a structural account of the 14 Bravais lattices in three dimensions from configuration dimension, under the Recognition Science forcing chain (in particular $D=3$ and the self-similar fixed point $\varphi$). Status is a structural theorem with no sorry and no extra axioms.
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the unique positive self-similar fixed point forced at T6. The upstream lemma used here records the elementary tightening $\varphi>1.5$ (from $\sqrt{5}>2$). The canonical threshold is a module-local real constant built from $\varphi$; sibling facts also record a domain cost, its non-negativity, and a Bravais-3 certificate package that consumes such cutoffs.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then close by linarith using the lemma $\varphi>1.5$. No further case splits or Recognition-Composition identities are required; positivity is pure real arithmetic once the definition is expanded.
why it matters
Gives the positivity side-condition for the canonical cutoff that sits beside domain-cost non-negativity in the ConfigDim materials development. The parent setting is the structural claim that the 14 Bravais classes in $D=3$ arise from an RS counting law (module framing: doubled count law $2(2^3-1)$ for dual lattice structure, with $D=3$ from T8 and $\varphi$ from T6). No downstream edges are recorded yet; the lemma is infrastructure for certificate inhabitation and cost comparisons rather than a terminal physics identity. It does not itself compute the integer 14.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.