curvature_tuple_uniqueness_bundle
plain-language theorem explainer
The theorem packages three uniqueness statements for the curvature correction parameters in the fine structure constant derivation. It forces the exponent on pi to equal five, the denominator coefficient to equal 102, and the numerator to equal 103 to recover the canonical form -103 over 102 pi to the fifth. Workers deriving alpha or integrating over ledger phase space cite the bundle for a single handle on the tuple. The proof is a one-line term wrapper that applies the three separate uniqueness lemmas for power family, denominator, and numer.
Claim. For natural numbers $d,k,n$, the equivalences hold: $-103/(102 pi^d) = -103/(102 pi^5)$ if and only if $d=5$; $-103/(k pi^5) = -103/(102 pi^5)$ if and only if $k=102$; and $-n/(102 pi^5) = -103/(102 pi^5)$ if and only if $n=103$.
background
The module derives the curvature correction term delta_kappa = -103/(102 pi^5) that appears in the fine structure constant formula alpha inverse = 4 pi times 11 minus f_gap minus the correction. The denominator exponent five arises because the relevant integration runs over a five-dimensional configuration space: three spatial dimensions forced by the self-similar fixed point, one temporal dimension from the eight-tick cycle, and one dual-balance dimension from ledger conservation. Each angular integration contributes a factor of pi, so the phase-space volume is pi^5. The upstream definition curvature_correction_derived states that the correction equals the negative seam ratio divided by this volume, yielding exactly -103/(102 pi^5).
proof idea
The proof is a term-mode exact constructor that directly applies three component lemmas. It invokes curvature_power_family_eq_canonical_iff on the exponent variable d, curvature_denominator_at_pi5_eq_canonical_iff on the denominator coefficient k, and curvature_numerator_at_pi5_eq_canonical_iff on the numerator variable n. Each lemma was already proved by case analysis on zero and algebraic rearrangement to isolate the integer equality.
why it matters
The bundle supplies a single theorem handle for downstream consumers of the curvature correction inside the alpha derivation. It closes the uniqueness argument for the five-dimensional phase space that follows from three spatial dimensions (T8), the eight-tick octave (T7), and the balance constraint. The result sits inside the constants module that feeds the overall Recognition Science derivation of alpha inverse inside the interval (137.030, 137.039). No open scaffolding remains for this tuple.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.