curvature_correction_positive
plain-language theorem explainer
The positivity of the curvature correction term is established for use in alpha inverse refinement. Researchers working on RS constant precision would cite it to confirm the exponential resummation improves the seed interval without sign issues. The proof is a one-line wrapper that unfolds the definition and applies positivity of phi to a negative integer power.
Claim. $0 < phi^{-5}$ where $phi$ is the self-similar fixed point of the forcing chain.
background
The Alpha-Inverse Precision Refinement module (Q8) defines two formulas for alpha inverse: the additive seed alpha^{-1}_add = 4 pi times 11 and the exponential resummation alpha^{-1} = alpha_seed times exp(-w_8 ln phi / alpha_seed) with alpha_seed = 44 pi. The curvature correction enters as phi to the negative fifth to tighten the proved interval (137.030, 137.039) toward 1 ppm around the CODATA value. Upstream the definition states curvature_correction equals phi raised to negative five. This positivity result is required for the AlphaPrecisionCert that bundles seed equality, seed positivity, curvature positivity and gap positivity.
proof idea
The proof is a one-line wrapper. It unfolds the definition of curvature_correction to reveal phi to the negative fifth power, then invokes the lemma that a positive base raised to any integer power remains positive.
why it matters
This result supplies the curvature_positive field required by the existence theorem for AlphaPrecisionCert. It advances the Q8 refinement step that targets alpha^{-1} inside (137.030, 137.039) and is consistent with the RS-native constants hbar = phi^{-5} and G = phi^5 / pi. It closes the positivity check that follows phi forcing in T6 and precedes full constant certification in the chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.