canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in the rung-56 structural physics certificate is strictly positive. Anyone citing domain-cost comparisons or the M56 structural certificate needs this positivity fact. The proof is a one-line unfold-and-linarith wrapper off the bound φ > 1.5.
Claim. The canonical threshold is strictly positive: $0 < \tau_{\mathrm{can}}$, where $\tau_{\mathrm{can}}$ is the real constant obtained by unfolding the canonical-threshold definition (an affine expression in the golden ratio $\varphi$).
background
Module Structural_Physics_mod56 packages a structural Recognition Science certificate for the Physics domain at recognition rung 56. Status is a pure structural theorem (no sorry, no extra axioms). Sibling definitions introduce a domain cost and the canonical threshold against which that cost is compared.
The only external arithmetic input is the golden ratio $\varphi = (1+\sqrt{5})/2$. Upstream, Constants records the tighter lower bound $\varphi > 1.5$, justified by $\sqrt{5} > 2$. After unfolding, the canonical threshold is an expression whose positivity is linear in that bound.
In the broader RS ledger, $\varphi$ is the self-similar fixed point forced at T6 of the unified forcing chain; positivity facts of this kind keep cost and threshold comparisons well-defined on the $\varphi$-ladder.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge $0 < \tau_{\mathrm{can}}$ by linarith using the single lemma $\varphi > 1.5$. No case splits, no induction, no cost-functional identities.
why it matters
Keeps the rung-56 structural physics certificate on a positive threshold, so domain-cost nonnegativity and threshold comparisons are meaningful rather than vacuous. Siblings include the domain cost, its nonnegativity, the threshold itself, and the inhabited M56 certificate bundle; this lemma is the positivity half of that bundle.
No downstream edges are recorded yet, so the immediate consumer is the local certificate construction rather than a named parent theorem. Framework-wise it sits under the T6 forcing of $\varphi$ and the structural (not dynamical) layer of RS physics predictions. It does not touch the RCL, eight-tick octave, or $\alpha$ band directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.