vbar_with
This definition supplies the regularized baryonic velocity at radius r for use in galaxy rotation curve calculations inside the ILG gravity module. Modelers assembling baryonic contributions to observed velocities cite it when building the effective gravitational field from gas, disk, and bulge components. The definition is a one-line wrapper that applies the square root after taking the maximum of the velocity regularization floor eps_v and the squared velocity sum produced by vbarSq_with.
claimLet $v(r) = sqrt(max(eps_v, v^2(r)))$, where $v^2(r)$ equals the sum of the squared gas velocity, the disk velocity scaled by the square root of the stellar mass-to-light ratio, and the bulge velocity, all evaluated at radius $r$, and $eps_v$ is the velocity regularization threshold supplied by the configuration parameters.
background
Config is the structure holding the model parameters upsilonStar (stellar mass-to-light ratio), eps_r (radial regularization), eps_v (velocity floor), eps_t, and eps_a. BaryonCurves is the structure supplying the three component velocity profiles vgas, vdisk, and vbul, each a function from radius to velocity. The local setting is the Gravity.ILG module, which assembles baryonic velocity contributions for the recognition-based gravity model. It depends on the upstream definition vbarSq_with, which computes the unregularized squared velocity as max(0, vgas(r)^2 + (sqrt(upsilonStar) * vdisk(r))^2 + vbul(r)^2).
proof idea
The definition is a one-line wrapper that applies Real.sqrt to the maximum of cfg.eps_v and the result of vbarSq_with cfg C r.
why it matters in Recognition Science
This definition feeds directly into gbar_with, which computes the baryonic gravitational acceleration as the square of vbar_with divided by max(eps_r, r). In the Recognition Science framework it supplies the regularized velocity input needed for the gravity sector before the force law is applied, consistent with the eight-tick octave and D = 3 spatial dimensions. It closes the regularization step for baryonic curves.
scope and limits
- Does not include non-baryonic velocity contributions.
- Does not enforce positivity beyond the max with eps_v.
- Does not depend on the modal possibility Config structure.
- Does not compute time derivatives or evolutionary terms.
Lean usage
let v := vbar_with cfg C r; v^2 / max cfg.eps_r rformal statement (Lean)
45def vbar_with (cfg : Config) (C : BaryonCurves) (r : ℝ) : ℝ :=
proof body
Definition body.
46 Real.sqrt (max cfg.eps_v (vbarSq_with cfg C r))
47