canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as φ − 3/2, with φ the golden ratio from the RS constants. Cosmology and cost-structure arguments in the D=3 count-law module cite it as the cut separating admissible domain costs from the rest. The body is a one-line real assignment, not a derived equality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio fixed by the Recognition self-similarity equation.
background
This module packages structural cosmology facts forced by D = 3: the RS count law states that there are $2^D - 1 = 7$ independent channels, exact once spatial dimension is three (T8 in the forcing chain). The file imports the global Constants (for $\varphi$) and Cost modules, so the J-cost and related nonnegativity lemmas are in scope.
Sibling definitions introduce a domain cost functional and prove it is nonnegative; the present constant is the numerical cut those cost comparisons use. $\varphi$ itself is the unique self-similar fixed point forced at T6, so the threshold is an RS-native scale rather than an external fit parameter.
proof idea
Pure definition: the real is set equal to phi - 3/2 from the Constants module. No tactics, no lemmas, no proof obligations.
why it matters
Gives the structural module a single named cut for domain-cost comparisons under the seven-channel count law. Downstream positivity (canonicalThreshold_pos) and the module certificate (RSCOSStructural003Cert) are expected to quote it when they assert that admissible costs sit above this floor. Numerically $\varphi - 3/2 \approx 0.118$, a small positive RS scale consistent with other φ-ladder gaps; it does not itself invoke the eight-tick octave or the fine-structure band, but it lives in the same D = 3 structural layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.