rotational_flatness_implies_nonzero_vflat
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute an explicit numerical value for v_flat.
- Does not derive or assume the rotational-flatness condition itself.
- Does not address dynamical stability of the resulting velocity field.
- Does not extend to the case alpha ≤ 0.
formal statement (Lean)
45theorem rotational_flatness_implies_nonzero_vflat (P : Params) (r : ℝ)
46 (hα : P.alpha > 0) :
47 ∃ v_flat : ℝ, v_flat ≠ 0 := by
proof body
Term-mode proof.
48 rcases rotational_flatness_implies_positive_vflat P r hα with ⟨v_flat, hv⟩
49 exact ⟨v_flat, ne_of_gt hv⟩
50
51end ILG
52end IndisputableMonolith.Gravity