deltaKappa
The curvature-closure constant δ_κ is defined exactly as -103/(102 π^5) for use in the Recognition Science α pipeline. Researchers assembling the predicted inverse fine-structure constant would cite this term when forming the expression 4π·11 − (ln φ + δ_κ). The definition is a direct assignment of the closed rational expression with no lemmas or reductions.
claim$δ_κ := -103/(102 π^5)$
background
The Pipelines module treats the golden ratio φ as a concrete real number. The curvature-closure constant δ_κ supplies the adjustment term in the α pipeline, obtained from the voxel seam count. Module imports bring in structures for collision-free programs and simplicial edge lengths, yet this definition remains an isolated exact expression.
proof idea
Direct definition that assigns the value -103/(102 π^5) to deltaKappa. No tactics, lemmas, or reductions are invoked; the body is a single closed-form expression.
why it matters in Recognition Science
This supplies the δ_κ term required by alphaInvPrediction, which assembles the predicted α^{-1} = 4π·11 − (ln φ + δ_κ). It supports the Recognition Science claim that α^{-1} lies inside the interval (137.030, 137.039) and originates from the eight-tick octave and voxel counting in the forcing chain.
scope and limits
- Does not derive the coefficient 103/102 from first principles.
- Does not compute or approximate the numerical value of δ_κ.
- Does not link to specific upstream theorems beyond module-level imports.
- Does not state falsification criteria for the α prediction.
Lean usage
noncomputable def alphaInvPrediction : ℝ := 4 * Real.pi * 11 - (Real.log phi + deltaKappa)formal statement (Lean)
39noncomputable def deltaKappa : ℝ := - (103 : ℝ) / (102 * Real.pi ^ 5)
proof body
Definition body.
40
41/-- The predicted dimensionless inverse fine-structure constant
42α^{-1} = 4π·11 − (ln φ + δ_κ).
43This is a pure expression-level definition (no numerics here). -/