canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in the RS DNA-storage density module is strictly positive. Anyone citing positivity of that threshold (for certificates or density bounds) can point here. The proof is a one-line wrapper: unfold the definition and apply linear arithmetic to the bound φ > 1.5.
Claim. The canonical threshold constant of the DNA-storage density module satisfies $0 < \mathrm{canonical\,threshold}$.
background
This module treats DNA storage density in Recognition Science units. Empirically, Church et al. (2012) report about $2.15 \times 10^{17}$ bytes per gram; RS frames densities as powers of the golden ratio $\varphi$ on a structural ladder (module status: structural theorem, zero sorry, zero axiom).
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced in the RS chain (T6). The only upstream fact used here is the tighter lower bound $\varphi > 1.5$, which follows from $\sqrt{5} > 2$. The canonical threshold is a named real constant in this module, defined from $\varphi$; positivity is the elementary sanity check before density certificates.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \ldots$ by linarith using the lemma $\varphi > 1.5$. No case splits or further RS structure.
why it matters
Keeps the DNA-storage density certificate stack free of floating non-positivity. The module pairs this with nonnegativity of the domain cost and an inhabited certificate (DNAStorageCert / cert_inhabited). Downstream use count is currently zero in the graph, so the lemma is local hygiene rather than a forcing-chain step.
It sits in the information domain, not in T0–T8, but it inherits $\varphi$ from Constants and Cost. It does not itself match the Church et al. figure to a specific $\varphi^k$; that comparison remains structural commentary in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.