canonicalThreshold
plain-language theorem explainer
The canonical compression threshold is the real number φ − 3/2, equal to the J-cost at the golden ratio. Recognition Science information theory cites it as the forced per-symbol overhead (in bits) of optimal RS encoding above Shannon entropy. The declaration is a one-line arithmetic definition in the RS constant φ.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden-ratio fixed point of the Recognition self-similarity relation.
background
The module treats optimal data compression under the Recognition cost. Classical Huffman coding places average code length between the Shannon entropy $H(X)$ and $H(X)+1$. In RS units the analogous overhead is fixed by the J-cost rather than by an integer bit budget.
The cost functional is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain. The golden ratio $\varphi$ is the self-similar fixed point forced at T6. Direct algebra gives $J(\varphi)=\varphi-3/2$, so the named threshold is simply that value.
Local constants come from IndisputableMonolith.Constants and the cost API from IndisputableMonolith.Cost. Sibling lemmas record non-negativity of the domain cost and positivity of this threshold.
proof idea
Pure definition: the real constant is introduced as the arithmetic expression $\varphi-3/2$. No tactic proof or lemma application is required. Equality with $J(\varphi)$ is the elementary identity $( \varphi + \varphi^{-1})/2-1=\varphi-3/2$ that follows from $\varphi^{-1}=\varphi-1$.
why it matters
This constant is the numerical content of the module claim that optimal RS encoding carries $J(\varphi)$ bits of overhead per symbol beyond Shannon entropy. It sits at the junction of T5 (J-uniqueness) and T6 ($\varphi$ forced), and supplies the concrete scale used by the data-compression certificate (DataCompr3Cert and related siblings) in the same file.
In the broader framework it is the information-theoretic reading of the same $J(\varphi)$ that appears as the Berry creation threshold scale and in the eight-tick / $\phi$-ladder bookkeeping. Naming it once keeps every later comparison to classical $+1$-bit Huffman slack dimensionally honest in RS units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.