keplerian_falloff
plain-language theorem explainer
Keplerian falloff asserts that circular orbital velocity around a point mass or spherical distribution declines as the inverse square root of radius. Galaxy dynamicists cite it as the Newtonian baseline before introducing extended mass to explain flat curves. The proof is a one-line wrapper that applies the trivial tactic.
Claim. For a point mass or spherically symmetric distribution, the orbital velocity satisfies $v(r) = k / r^{1/2}$ for some constant $k$.
background
The module derives galaxy rotation from ledger distributions in Recognition Science, where dark matter corresponds to odd 8-tick phase shadows. Expected behavior splits into inner solid-body rise and outer decline, while observations show constant velocity at large radii requiring extra mass. Upstream results supply the primitive distinction axioms that reduce seven independent axioms to four structural conditions plus three definitional facts, and the universal forcing self-reference structure that records required meta-realization properties.
proof idea
The proof is a one-line wrapper that applies the trivial tactic to the stated relation.
why it matters
The declaration records the Newtonian baseline that any ledger-based halo model must overcome to produce flat curves. It sits inside the COS-011 development of J-cost equilibrium profiles and connects to the eight-tick octave and phi-ladder mass formulas. No downstream theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.