vbarSq_with
plain-language theorem explainer
The definition assembles the squared baryonic velocity at radius r as the non-negative quadratic sum of gas, scaled stellar disk, and bulge contributions. Galactic dynamics researchers in the Recognition Science setting cite it when constructing the total rotation curve from baryonic components alone. The implementation is a direct algebraic expression that applies the max operator to the summed squares.
Claim. For configuration parameters including stellar mass-to-light ratio $Y_*$ and baryon curves supplying radius-dependent profiles $v_mathrm{gas}$, $v_mathrm{disk}$, $v_mathrm{bul}$, the squared baryonic velocity is defined by $v_mathrm{bar}^2(r) := max(0, v_mathrm{gas}(r)^2 + (sqrt(Y_*) v_mathrm{disk}(r))^2 + v_mathrm{bul}(r)^2)$.
background
The Gravity.ILG module models galactic rotation curves using two structures. Config supplies the stellar mass-to-light ratio upsilonStar together with four epsilon regularization parameters. BaryonCurves packages three independent functions that return gas, disk, and bulge velocities at any radius. These structures operate inside the Recognition Science treatment of gravity, where baryonic matter alone determines the visible velocity field before any dark-matter or modified-gravity corrections are considered.
proof idea
The declaration is a direct definition. It evaluates the three velocity terms, scales the disk term by the square root of the stellar mass-to-light ratio, squares each term, sums them, and applies the max operator with zero to guarantee a non-negative result.
why it matters
vbarSq_with supplies the squared input required by the downstream vbar_with definition, which then takes the square root after applying an epsilon floor. The construction therefore forms the baryonic core of the ILG velocity model and sits inside the Recognition Science derivation of gravity from the forcing chain (T0-T8) and the phi-ladder mass assignment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.