curvature_numerator_forced_at_pi5
plain-language theorem explainer
Matching the legacy curvature correction δ_κ by a pure numerator trial −n/(102 π⁵) forces the integer numerator n = 103. Verification and α-resolution authors cite this when locking the curvature triple (exponent, denominator, numerator). The proof is a one-line unfold of δ_κ into the upstream numerator-uniqueness biconditional.
Claim. For every natural number $n$, the equality $-n/(102\pi^5)=\delta_\kappa$ holds if and only if $n=103$, where $\delta_\kappa:=-103/(102\pi^5)$ is the legacy curvature correction.
background
Alpha Resolution Pass 2 turns the residual between the symbolic RS inverse-fine-structure formula and the CODATA anchor into an explicit additive closure target. It does not yet derive a new geometric term; it packages the exact correction needed for CODATA alignment and proves uniqueness statements about candidate curvature forms.
The legacy curvature correction is the real constant $\delta_\kappa=-103/(102\pi^5)$, retained for compatibility with older reports. The family under study here freezes the canonical denominator $102$ and the power $\pi^5$, and varies only the natural numerator $n$.
Upstream, curvature_numerator_at_pi5_eq_canonical_iff already proves that $-n/(102\pi^5)$ equals the fully expanded canonical value $-103/(102\pi^5)$ if and only if $n=103$. The present declaration simply names that uniqueness against the definition $\delta_\kappa$.
proof idea
One-line term proof. Unfold the definition $\delta_\kappa=-103/(102\pi^5)$ via simpa [delta_kappa], then apply the upstream biconditional curvature_numerator_at_pi5_eq_canonical_iff n, which already equates membership in the frozen-denominator/exponent family to the canonical numerator $n=103$.
why it matters
This is the numerator leg of the verification-layer curvature-tuple uniqueness package. Downstream, curvature_tuple_uniqueness_bundle_for_delta_kappa conjoins it with the parallel forcing statements for the exponent ($d=5$) and the denominator factor ($k=102$), and closure_status records the full bundle among the α-resolution closure claims.
In the broader RS picture the curvature correction sits inside the α⁻¹ assembly that targets the narrow band $(137.030,137.039)$. Pass 2 still treats geometric derivation of the correction as open; this lemma only certifies that, once the form $-n/(102\pi^5)$ is fixed, the numerator cannot float. It therefore supplies a sharp target for any future first-principles derivation of $\delta_\kappa$ from RS geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.