rotational_flatness_implies_positive_vflat
plain-language theorem explainer
Rotational flatness forced by the ILG time-kernel implies the existence of a positive asymptotic flat velocity v_flat. Researchers deriving modified gravity from recognition principles cite this when confirming that flat rotation curves cannot collapse to zero velocity scale. The proof is a one-line term extraction that discards the placeholder from the upstream forced-flatness witness.
Claim. For ILG parameters $P$ with fine-structure constant satisfying $P.alpha > 0$, there exists a real number $v_{flat} > 0$.
background
The Params structure records the fine-structure constant alpha, recognition lag Clag set to phi^{-5}, and auxiliary scales A, r0, p. The upstream theorem rotational_flatness_forced states that when alpha is positive, in the large-r limit where dynamical time T_dyn greatly exceeds tau_0, the ILG correction w_t diverges as (T_dyn)^alpha, exactly canceling the Newtonian 1/r decay and forcing constant v_rot. This declaration belongs to the Gravity.ILGDerivation module whose module doc derives the time-kernel w_t uniquely from C_lag = phi^{-5} and alpha, connecting RRF gradient cost to effective modified gravity at large scales.
proof idea
The term proof applies rotational_flatness_forced to P, r and the positivity hypothesis on alpha, performs rcases to bind the witness v_flat together with its positivity hypothesis hv while discarding the placeholder, then returns the pair consisting of v_flat and hv.
why it matters
This supplies the strict positivity of v_flat required by the downstream theorem rotational_flatness_implies_nonzero_vflat. It advances the ILG derivation of flat galactic rotation curves inside the Recognition Science framework, where the forcing chain yields the eight-tick octave, D = 3, and the alpha band inside (137.030, 137.039). The module formalizes how the time-kernel produces large-scale gravity modifications consistent with the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.