canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in the white-dwarf radius module is strictly positive. Anyone citing the structural match φ^19 · 0.75 km ≈ 7000 km needs this positivity to keep the threshold well-defined as a scale cut. The proof is a one-line unfold-plus-linarith wrapper off the bound φ > 1.5.
Claim. The canonical threshold (the real scale cut built from the golden ratio $\varphi$) satisfies $0 < \mathrm{canonical\ threshold}$.
background
Module RS_Astro_Module_005 records a structural white-dwarf radius match: $\varphi^{19}\cdot 0.75,\mathrm{km}\approx 7012,\mathrm{km}\sim 7000,\mathrm{km}$, with status STRUCTURAL THEOREM (no sorry, no axiom). The module imports the global constants and the J-cost layer; the only numeric constant needed here is the golden ratio $\varphi=(1+\sqrt{5})/2$.
The sibling definition canonicalThreshold is the real threshold against which domain costs are compared in this astrophysics certificate. Its positivity is the elementary well-definedness fact required before any comparison or certificate packing.
Upstream, phi_gt_onePointFive supplies the tight lower bound $\varphi>1.5$, obtained from $\sqrt{5}>2$. That single inequality is enough to force the unfolded threshold expression above zero by linear arithmetic.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then apply linarith to the hypothesis $\varphi>1.5$ from phi_gt_onePointFive. No further case splits or Recognition-Composition identities are required.
why it matters
Inside the white-dwarf radius certificate chain, every comparison against the canonical threshold presupposes that the threshold itself is positive. This lemma discharges that obligation with zero axioms, keeping the module's STRUCTURAL THEOREM status intact.
It sits at the constants layer of the forcing chain: positivity is inherited from T6 (φ forced as the self-similar fixed point) via the elementary bound φ > 1.5. No downstream theorems currently list it as a direct dependency, so it functions as a local hygiene fact for the astrophysics certificate rather than a global bridge lemma.
The result does not itself produce the 7000 km match; it only guarantees that the scale cut used in that match is a positive real.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.