canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold used in the RS BAO-scale exactness module is strictly positive. Anyone citing the BAO scale match (phi^14 yardstick versus Planck r_drag) needs this sign fact as a local arithmetic guard. The proof is a one-line unfold-plus-linarith wrapper off the bound phi > 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 module's canonical-threshold definition (an expression in the golden ratio $\varphi$).
background
The module treats the baryon acoustic oscillation (BAO) scale in Recognition Science units. Planck reports $r_{\mathrm{drag}} \approx 147.09,\mathrm{Mpc}$; the RS claim is $\varphi^{14}\cdot 0.174,\mathrm{Mpc} = 146.7,\mathrm{Mpc}$, within $0.3%$. Status is structural: zero sorry, zero axiom.
The golden ratio $\varphi = (1+\sqrt{5})/2$ is the self-similar fixed point forced at T6 of the unified forcing chain. The imported lemma phi_gt_onePointFive strengthens the elementary bound to $\varphi > 1.5$, via $\sqrt{5} > 2$. The Cost and Constants imports supply the J-cost infrastructure and $\varphi$ itself; the threshold is a local real constant built from those.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting strict inequality by linarith using the single upstream fact $\varphi > 1.5$. No case splits, no induction, no cost identities.
why it matters
Local positivity guard inside the BAO Scale RS Exact5 certificate path (siblings include the exactness cert and its inhabited instance). It does not itself state the $146.7$ versus $147.09$ match; it only ensures the threshold constant that appears in the domain-cost side conditions is positive, so downstream nonnegativity and comparison lemmas stay well-typed over $\mathbb{R}$.
In the broader framework this sits under Foundation, feeding the structural claim that the BAO scale is a pure $\varphi$-ladder multiple of a fixed yardstick. No T0–T8 forcing step is proved here; the link is only through $\varphi$ as the T6 fixed point and the numerical ladder power $\varphi^{14}$. Used-by is empty in the graph snapshot, so the lemma is presently a leaf helper for the module cert rather than a widely reused primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.