canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in the J-cost data-compression certificate is strictly positive. Anyone citing the RS overhead bound (J(φ) bits beyond Shannon entropy) needs this positivity fact. The proof is a one-line wrapper: unfold the definition and finish by linear arithmetic from φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau$, where $\tau$ is the real constant obtained by unfolding the module's canonical-threshold definition (an expression in the golden ratio $\varphi$).
background
This module records a structural theorem on optimal data compression from the Recognition J-cost: classical Huffman coding places average code length in $[H(X), H(X)+1]$, while RS claims the optimal encoding carries $J(\varphi)$ bits of overhead per symbol beyond Shannon entropy.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced by the Recognition chain (T6). The only upstream fact used here is the tighter numerical bound $\varphi > 1.5$, proved from $\sqrt{5} > 2$. The canonical threshold is the module-local real constant built from $\varphi$ that appears in the compression certificate; positivity is the elementary gate before nonnegativity and certificate packing lemmas.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi > 1.5$ supplied by phi_gt_onePointFive. No further case splits or Recognition identities are required.
why it matters
Positivity of the canonical threshold is the first numeric gate in the J-cost compression package (siblings: domain cost nonnegativity, the compression certificate, and its inhabited instance). It underwrites the claim that RS optimal encoding adds a strictly positive but controlled overhead of order $J(\varphi)$ beyond Shannon entropy, tying information theory to the forced cost $J$ and the fixed point $\varphi$ (T5–T6). No downstream consumers are wired yet in the graph; the immediate parent objects are the local certificate constructors in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.