gbar_with
plain-language theorem explainer
The baryonic acceleration function computes the regularized gravitational acceleration from baryonic matter at a given radius using a configuration of parameters and velocity curves. Modelers of galactic dynamics in the recognition science approach would cite this when deriving effective potentials or accelerations. It is realized as a direct one-line algebraic combination of the companion velocity definition and a max-based denominator.
Claim. $g(r) = v(r)^2 / max(ε_r, r)$, where $v(r)$ is the regularized total baryonic speed obtained as the square root of the maximum between ε_v and the squared sum of the supplied gas, disk, and bulge velocity profiles, and ε_r, ε_v are taken from the configuration parameters.
background
The Config structure supplies numeric regularization parameters: upsilonStar for the stellar mass-to-light ratio, eps_r for the radial cutoff, eps_v for the velocity floor, plus eps_t and eps_a. BaryonCurves supplies the three radial velocity functions vgas, vdisk, and vbul. The upstream vbar_with definition first forms the squared sum via vbarSq_with and then takes the square root after applying the eps_v floor. This local setting in the Gravity.ILG module supplies the inputs needed to produce effective accelerations from baryonic data alone.
proof idea
One-line wrapper that applies vbar_with to obtain the regularized velocity, squares the result, and divides by max(cfg.eps_r, r).
why it matters
This definition supplies the baryonic g term required for rotation-curve modeling inside the ILG framework. It implements the regularization that lets the model match observed velocities without additional mass components, consistent with the Recognition Science derivation of gravity from the J-function and the phi-ladder. No downstream uses are recorded, leaving open its integration with the full forcing chain from T5 through T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.