Pith. sign in
module module moderate

IndisputableMonolith.Verification.DimensionKepler

show as:
view Lean formalization →

Module packaging the closed-form apsidal angle and the Kepler selection principle used when specializing Recognition Science to inverse-square orbits. A reader checking the D=3 forcing chain or classical-limit consistency would cite it. Content is definitional plus a selection identity: the apsidal angle is written in closed form and fed into the Kepler criterion that singles out the Newtonian force law in three dimensions.

claimThe module introduces the closed-form apsidal angle $\Theta$ for central-force orbits and the Kepler selection principle: among power-law forces, only the inverse-square law yields a closed apsidal angle compatible with stable bound orbits in $D=3$ spatial dimensions.

background

In classical central-force mechanics the apsidal angle is the polar angle between successive periapsis and apoapsis. For a force $F\propto r^{-\beta}$ it admits a closed expression in terms of $\beta$ and the effective potential; the inverse-square case $\beta=2$ gives $\Theta=\pi$, hence closed ellipses (Bertrand's theorem in the classical setting).

Recognition Science forces $D=3$ at step T8 of the unified forcing chain. This module sits in the verification layer: it records the elementary orbital quantity needed to match that dimensional conclusion against the Kepler problem, without re-deriving the full celestial-mechanics apparatus.

Sibling declarations supply the explicit formula for the apsidal angle and the selection principle that isolates the Newtonian exponent once $D=3$ is fixed.

proof idea

Definition-plus-selection module rather than a deep proof development. The apsidal angle is introduced as a closed-form expression (standard reduction of the orbit integral for power-law forces). The Kepler selection principle is then the elementary identity that this angle equals $\pi$ precisely for the inverse-square law in three spatial dimensions, matching the RS-forced $D=3$. No multi-step tactic scripts; the argument is algebraic specialization of the classical formula.

why it matters in Recognition Science

Links the abstract dimensional forcing (T8: $D=3$) to a concrete classical observable: closed Keplerian ellipses. Downstream verification results that claim consistency of the RS classical limit with Newtonian gravity can point here for the apsidal-angle identity and the selection principle. It does not itself prove T8; it supplies the Kepler-side dictionary entry once $D=3$ is already on the table. Framework landmark: T8 spatial dimensions, read against the inverse-square specialization.

scope and limits

declarations in this module (2)