canonicalThreshold_pos
plain-language theorem explainer
The canonical BIT dark-energy drift threshold is strictly positive. Cosmologists and RS auditors citing the admissible interval for δw₀ need this sign fact before treating the upper endpoint as a genuine bound. The proof is a one-line unfold of the threshold definition followed by linear arithmetic from φ > 1.5.
Claim. The canonical threshold equals $J(\varphi)=\varphi-3/2$ and satisfies $0 < \varphi - 3/2$.
background
Module BITKernelFamilies3 packages the v3 BIT kernel family built from the J-cost. The local claim is structural: BIT dark-energy drift δw₀ lives in the closed interval [0, J(φ)], with canonical kernel K(z)=1/(1+z). At the lower endpoint one recovers pure Λ; at the upper endpoint the maximum BIT drift is about 0.118 in the equation of state.
The golden ratio φ = (1+√5)/2 is the self-similar fixed point forced at T6. The cost functional is J(x)=(x+x⁻¹)/2−1, so on the golden ratio one has the elementary identity J(φ)=φ−3/2. The upstream lemma phi_gt_onePointFive supplies the tight real bound φ>1.5 (from √5>2), which is exactly the arithmetic content needed to make that difference positive.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (exposing the expression φ−3/2, equivalently J(φ)), then discharge 0<φ−3/2 by linarith against the imported lemma phi_gt_onePointFive.
why it matters
Positivity of the canonical threshold legitimizes the half-open geometry of the BIT drift window [0, J(φ)] stated in the module header. Without it the upper endpoint could collapse to a non-positive value and the “maximum BIT drift ≈ 0.118” calibration would be meaningless. The result sits inside the Foundation layer that feeds the BITKernel3Cert certificate family; it is a pure sign lemma, not a dynamical derivation, and closes no open forcing-chain step beyond making the J(φ) endpoint admissible. Downstream used-by edges are presently empty, so its immediate consumers are the sibling certificate constructors in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.