Constants Alpha Precision Curvature Correction Positive

A positive correction

The declaration curvature_correction_positive is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes a simple fact: the number called the curvature correction is greater than zero. That number is defined as phi raised to the power -5, where phi is the golden ratio, approximately 1.618. So the curvature correction is about 0.09017, a positive quantity. The proof is short: it relies on the fact that phi itself is positive, and any positive number raised to any integer power remains positive.

This theorem does not, by itself, say anything about the fine-structure constant alpha. It is one small piece in a larger construction. The framework's alpha-inverse formula uses a seed value of 44 pi, and a correction term that involves this curvature correction. The assembled expression for alpha-inverse is proved to lie in a band about 60 parts per million wide, from 137.030 to 137.039. The measured CODATA 2022 value is 137.035999177(21), which falls inside that band. But the theorem about the curvature correction being positive only guarantees that the correction term has the intended sign; it does not derive the value of alpha, and it does not by itself place the final number in the measured band.

What the theorem does establish is a consistency property. In the framework's account, the curvature correction is part of a chain of definitions and proofs that assemble the alpha-inverse expression. Having a formal proof that this piece is positive is a check on the construction's internal coherence. It is a small but real result: the framework can prove, from its definitions, that this particular factor has the sign it needs. The certificate structure in the library bundles this positivity proof with others, such as the positivity of the seed and of the gap correction, into a single object that asserts the construction is well-formed.

It is important to be clear about the scope. The theorem does not claim that the curvature correction is the reason alpha has its measured value. The seed 44 pi is an identification, not a derived coupling. The first-order value of the construction is excluded by CODATA at more than 30,000 sigma, according to the framework's own measurement verdict. The exact value of alpha-inverse at zero is a free boundary datum within the framework. The positivity theorem is a building block, not a derivation of the constant.

noncomputable def curvature_correction : ℝ := phi ^ (-(5 : ℤ))

theorem curvature_correction_positive : 0 < curvature_correction := by
  unfold curvature_correction; exact zpow_pos phi_pos _

theorem alpha_precision_cert_exists : Nonempty AlphaPrecisionCert :=
  ⟨{ seed_from_geometry := alpha_seed_eq
     seed_positive := alpha_seed_positive
     curvature_positive := curvature_correction_positive
     gap_positive := gap_correction_positive }⟩

noncomputable def alpha_seed : ℝ := 44 * Real.pi

What this page does not claim

This theorem does not derive the fine-structure constant alpha. This theorem does not, by itself, place the final alpha-inverse value in the measured band. This theorem does not claim that the curvature correction is the reason alpha has its measured value.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/AlphaPrecision.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: