is_ilg_vrot
plain-language theorem explainer
The ILG rotation velocity predicate holds exactly when squared orbital speed equals the ILG time-weight function at the orbital period times G times enclosed mass over radius. Galaxy dynamics researchers modeling flat rotation curves without dark matter would cite this predicate when stating the self-consistent velocity condition for a given radius. It is supplied as a direct equational definition with no lemmas or tactics required.
Claim. Let $S$ be a rotation system, $P$ a set of ILG parameters, and $t_0$ the fundamental tick time. For radius $r$ and velocity $v$, the predicate holds if and only if $v^2 = w_t(P, 2π r / v, t_0) · (G · M_enc(r) / r)$, where $w_t$ is the ILG weight function, $G$ is the gravitational constant, and $M_enc$ is the enclosed-mass function of $S$.
background
The Gravity.RotationILG module augments Newtonian rotation-curve balance with the ILG weight function $w_t$ that arises from the Recognition Composition Law. A rotation system $S$ carries the constant $G$ (defined in Constants as $λ_rec^2 c^3 / (π ħ)$) and the enclosed-mass function $M_enc(r)$. The parameter $t_0$ is the fundamental tick duration supplied by Constants.tau0, while $w_t$ and the parameter record $P$ are imported from the ILG module.
proof idea
The declaration is a direct definition that simply equates the left-hand side $v^2$ to the product of the ILG weight function evaluated at the orbital period $2π r / v$ and the Newtonian term $G M_enc(r) / r$. No lemmas are applied and no tactics are used; the body is the fixed-point equation itself.
why it matters
The predicate is the sole hypothesis of the downstream theorem solution_exists, which proves existence of a positive velocity by applying the intermediate-value theorem to $f(v) = v^2 - w_t · K$. It supplies the ILG-adjusted rotation condition inside the gravity section, consistent with the phi-ladder and the derived value $G = φ^5 / π$ in RS-native units. The definition therefore closes the interface needed for further analysis of galaxy rotation curves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.