alphaInvValueStr
plain-language theorem explainer
The definition evaluates the Recognition Science curvature pipeline to emit a 12-decimal string for α^{-1} via the explicit combination 4π·11 − (w8·ln φ + δ_κ). Researchers auditing the predicted alpha band (137.030, 137.039) cite it for reproducible, library-free numerics. The body assembles the value through rational arithmetic on an 80-term alternating series for ln(1 + 1/φ) followed by the gap-weight multiplication and correction.
Claim. $α^{-1} ≈ 4π·11 − (w_8 ln φ + δ_κ)$ emitted as a 12-decimal string, where π ≈ 104348/33215, φ ≈ 161803399/100000000, w_8 ≈ 2488254397846/10^{12}, and δ_κ = −103/(102·π^5).
background
The module provides minimal rational formatting helpers. Upstream f_gap is the gap weight w8 · ln φ drawn from the DFT-8 projection and the eight-tick octave; the master gap value acts as generator at z=1. The local setting is pure computable arithmetic that avoids Real.log by using an alternating series on the rational 1/φ.
proof idea
The definition builds the result by defining rational add/mul/neg helpers, computing y^k via a recursive power function, summing the alternating ln(1+y) series to 80 terms, scaling by the rational w8, adding the rational δ_κ, subtracting from 44π, and calling the sibling ratToDecimal to produce the final string.
why it matters
This definition supplies the concrete string consumed by alphaInvValue in URCAdapters.Audit, closing the computable path from the Recognition Composition Law and phi-ladder to the alpha band. It implements the first-order curvature correction inside the forcing chain (T5–T7) without floating-point operations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.