rotational_flatness_implies_nonzero_vflat
plain-language theorem explainer
Rotational flatness in the ILG parameter structure forces a nonzero asymptotic velocity scale v_flat for any radius r when the fine-structure constant alpha is positive. Modified-gravity and galaxy-dynamics researchers would cite this result to exclude the trivial zero-velocity solution in derivations of flat rotation curves. The proof is a one-line wrapper that invokes the positive-velocity predecessor and applies the fact that every positive real is nonzero.
Claim. Let $P$ be an ILG parameter record whose fine-structure constant component satisfies $P.α>0$. For any real radius $r$, there exists a real asymptotic velocity $v_∞$ such that $v_∞≠0$.
background
The module derives the ILG time-kernel $w_t$ from the recognition lag $C_{lag}=ϕ^{-5}$ and the fine-structure exponent $α$. The parameter record Params packages the inputs $α$, $C_{lag}$, $A$, $r_0$ and $p$ required by the ILG and SpiralField submodules. The upstream theorem rotational_flatness_implies_positive_vflat states that rotational-flatness structure yields an explicitly positive asymptotic velocity scale; its own proof rests on rotational_flatness_forced. The constant alpha is defined as the reciprocal of the inverse fine-structure constant and is treated as a positive real throughout the derivation.
proof idea
The term proof performs a rcases on the positive-velocity theorem to obtain a witness $v_flat$ together with the strict inequality $v_flat>0$, then applies ne_of_gt to replace the positivity hypothesis by the required non-equality.
why it matters
The declaration closes the logical gap between the forced positive velocity and the weaker nonzero claim required by downstream ILG rotation-curve arguments. It sits inside the ILG Time-Kernel Derivation that links the RRF gradient cost to effective modified gravity at large scales. The result uses the positivity of alpha and the rotational-flatness structure already established by rotational_flatness_forced; no further open scaffolding is attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.