canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold is strictly positive. Anyone wiring domain-cost or creation-threshold inequalities in the RS physics stack cites this fact. The proof unfolds the threshold definition and finishes by linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \mathrm{canonicalThreshold}$. After unfolding, this is the elementary consequence of $\varphi > 1.5$.
background
Physics RS Module 8 packages the structural claim that QCD θ vanishes from eight-tick uniqueness, presented as a zero-sorry structural theorem for the strong-CP problem.
The golden ratio φ is the self-similar fixed point forced earlier in the T0–T8 chain. The sibling definition canonicalThreshold is the numeric cutoff used by the module’s domain-cost comparisons; the only arithmetic fact needed for its sign is the tighter lower bound φ > 1.5.
That bound is supplied by phi_gt_onePointFive, whose doc-comment records the elementary estimate √5 > 2 ⇒ (1+√5)/2 > 1.5.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then invoke linarith on the single lemma phi_gt_onePointFive : (1.5 : ℝ) < phi. No further case splits or field identities are required.
why it matters
Gives a certified positive cutoff for whatever domain-cost or creation-threshold comparisons the module builds next (siblings include domainCost, domainCost_nonneg, and the package certificate RSPhysics008Cert). In the broader RS picture the same scale sits next to the Berry creation threshold φ^{-1} and the eight-tick octave (T7) that the module invokes for θ = 0. With no downstream edges yet, the lemma is local scaffolding for the module certificate rather than a global forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.