canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold (a φ-dependent constant in the D=3 combinatorics layer) is strictly positive. Authors of domain-cost comparisons or the D3 certification objects cite this sign fact before any threshold test. Proof is a one-line unfold-plus-linarith wrapper on the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the module's canonical threshold constant (defined from the golden ratio $\varphi$).
background
This module packages the combinatorial consequences of $D=3$: three spatial dimensions, three quark colors, three neutrino flavors, three families, three charge types, three baryon categories, and three-valued logic, all traced to $\mathrm{configDim}=D=3$. Status is structural (zero sorry, zero axiom).
The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. The upstream lemma phi_gt_onePointFive records the elementary tightening $\varphi>1.5$, obtained from $\sqrt{5}>2$.
Sibling definitions in the same file introduce a domain cost and the canonical threshold itself. Positivity of that threshold is the first arithmetic fact needed before any comparison of domain costs against it.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linear arithmetic with the single lemma $\varphi>1.5$. After unfolding, the goal is an inequality linear in $\varphi$ that is immediate from that lower bound; linarith closes it.
why it matters
Local infrastructure inside the D=3 combinatorics structural package. Sibling certification objects (D3CombinatoricsV2Cert, cert, cert_inhabited) sit in the same module and rely on a well-defined positive threshold when they assert the combinatorial package. Framework landmark T8 forces $D=3$ spatial dimensions; this file turns that dimension count into the matching list of threes. No external used_by edges are recorded yet, so the lemma is presently consumed inside the module's own cert construction rather than by a named parent theorem downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.