apsidalAngle
plain-language theorem explainer
Closed-form apsidal angle Δθ(D) = 2π/√(4−D) for natural-number spatial dimension D. Anyone citing the algebraic Kepler selector for dimensional rigidity uses this expression. It is a plain noncomputable definition: the classical reduced formula, not a derived identity.
Claim. For each natural number $D$, the apsidal angle is the real number $\Delta\theta(D) = \dfrac{2\pi}{\sqrt{4-D}}$ (undefined as a real when $D \ge 4$).
background
The module isolates the algebraic core of the (K) specialization in the dimensional rigidity argument: after the classical mechanics derivation is stripped away, only the closed-form apsidal angle and the equality $\Delta\theta(D)=2\pi$ remain.
In orbital mechanics the apsidal angle is the polar angle between successive periapsis passages. For the isotropic harmonic-like effective problem that appears in the reduced Kepler specialization, that angle collapses to $\Delta\theta(D)=2\pi/\sqrt{4-D}$. The formula is stated for a natural-number dimension parameter $D$, matching the RS convention that spatial dimension is a discrete forced integer.
Upstream, several modules already fix $D:=3$ (T8 spatial-dimension forcing, T9 linking). This definition keeps $D$ free so the selector theorem can recover $D=3$ from the angle condition alone.
proof idea
No proof: a one-line noncomputable definition. The body is the real expression $(2\pi)/\sqrt{4-(D:\mathbb{R})}$, using Mathlib square root and $\pi$. Domain issues for $D\ge 4$ are left to consumers.
why it matters
This is the reduced-form endpoint expression referenced from the verification layer. The sole downstream consumer is kepler_selection_principle, which proves $\Delta\theta(D)=2\pi$ if and only if $D=3$. That biconditional is the algebraic Kepler selector: closed apsides (full $2\pi$ precession-free return) pick out three spatial dimensions exactly.
In the Recognition Science forcing chain this sits beside T8 ($D=3$ spatial dimensions). The module presents the same conclusion from the classical Kepler side, so the verification graph can cite a short algebraic fact rather than the full mechanics derivation. No open scaffold remains on this declaration itself; it is pure notation for the selector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.