canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant appearing in the rung-61 astrophysics structural certificate is strictly positive. Certificate and domain-cost lemmas that need a positive floor cite this fact. Proof is a one-line unfold plus linear arithmetic from the bound φ > 1.5.
Claim. The canonical threshold (the real constant built from $\varphi$ for the astrophysics structural certificate) satisfies $0 < \text{canonical threshold}$.
background
Module Structural_Astrophysics_mod61 is a Recognition Science structural certificate for the astrophysics domain at recognition rung 61 (Plan v7, 120th pass). Status is structural theorem: zero sorry, zero axiom.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced by the RS chain (T6). The upstream lemma phi_gt_onePointFive records the elementary bound $\varphi > 1.5$, obtained from $\sqrt{5} > 2$. The canonical threshold is a real constant defined from $\varphi$ (unfolded in the proof) and used as a positivity floor beside the domain-cost functionals in this certificate.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the resulting linear inequality, feeding the single fact $\varphi > 1.5$ from phi_gt_onePointFive. No further case splits or RS identities are required.
why it matters
Supplies the positivity half of the constant infrastructure for the rung-61 astrophysics structural certificate. Sibling lemmas (domainCost_nonneg, the certificate inhabitation cert_inhabited, and StructAstrophysicsM61Cert) sit next to it in the same module; the certificate is marked structural with zero sorry. In the broader RS picture this is routine hygiene on $\varphi$-scales (T5–T6, J-cost uniqueness and the self-similar fixed point), not a new forcing step. No downstream dependents are recorded yet; the lemma exists so later domain-cost and certificate arguments can quote a named positivity fact rather than re-deriving $\varphi > 1.5$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.