BaryonCurves
plain-language theorem explainer
BaryonCurves is a record type holding three independent real functions of radius that supply the gas, disk, and bulge velocity contributions to galactic rotation curves. Galaxy-dynamics modelers cite it when assembling total baryonic velocity fields for comparison with observed rotation data. The declaration is a direct structure definition that introduces the three fields with no computational steps or lemmas.
Claim. A structure consisting of three functions $v_ {gas}, v_{disk}, v_{bul} : ℝ → ℝ$ that return the respective velocity components at radial distance $r$.
background
The Gravity.ILG module constructs effective gravitational accelerations from baryonic matter alone, consistent with Recognition Science's derivation of dynamics from the J-function and phi fixed point. BaryonCurves serves as the input container for the three separate baryonic velocity profiles. Downstream definitions combine them explicitly: vbarSq_with forms the squared total as max 0 of (vgas r)^2 plus (sqrt(upsilonStar) * vdisk r)^2 plus (vbul r)^2, after which vbar_with takes the regularized square root and gbar_with converts to an acceleration via division by max(eps_r, r).
proof idea
The declaration is a bare structure definition that specifies the three fields vgas, vdisk, and vbul. No tactics, lemmas, or reductions are applied.
why it matters
BaryonCurves supplies the baryonic velocity inputs required by vbar_with, vbarSq_with, and gbar_with, which in turn compute the effective fields used to test the Recognition Science mass ladder and eight-tick octave against galaxy data. It therefore occupies the interface between observed baryonic distributions and the framework's phi-based predictions for rotation curves. The structure leaves open how the component functions are obtained from mass densities or from the J-cost functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.