RunningCoupling
plain-language theorem explainer
RunningCoupling encodes the hypothesis that the lag coupling runs with length scale, equaling the RS value at galactic lengths while falling below 10^{-10} at laboratory lengths. Modelers of ILG weight kernels in rotating devices cite it to enforce consistency with null results at meter scales. The structure is introduced directly by a function field plus two pinning constraints at the extremes.
Claim. Structure consisting of a map $C_ {lag} : ℝ → ℝ$ such that $C_{lag}(10^{20}) = φ^{-5}$ and $C_{lag}(1) < 10^{-10}$.
background
The module connects the ILG weight kernel $w_t(T_{dyn}, τ_0) = 1 + C_{lag} ((T_{dyn}/τ_0)^α - 1)$ to flight models, with $τ_0 ≈ 7.3$ fs and $α ≈ 0.191$. C_lag_RS supplies the constant value $φ^{-5} ≈ 0.0902$ derived from the golden-ratio fixed point. Upstream structures from LedgerFactorization and PhiForcingDerived calibrate the underlying J-cost, while the eight-tick resonance supplies the lag constant at galactic scales.
proof idea
This declaration is a bare structure definition. It introduces the function field and the two constraints without applying lemmas or tactics.
why it matters
The structure supplies the scale-dependent interface consumed by the RunningCoupling declaration in Physics.RGTransport. It implements Option C of the module documentation, ensuring the weight deviation vanishes at laboratory scales while retaining the RS value at galactic scales. The construction links the phi-derived coupling from Gravity.EightTickResonance to the flight schedule and addresses whether the eight-tick octave produces observable effects at lab periods.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.