kepler_selection_principle
plain-language theorem explainer
The closed-form apsidal angle equals a full turn exactly when the spatial dimension is three: Δθ(D)=2π iff D=3. Anyone citing the algebraic (K) specialization in the dimensional-rigidity argument uses this selector. The proof is a short bidirectional real-arithmetic argument: cancel 2π, force √(4−D)=1, then recover D=3 by injectivity of Nat→ℝ.
Claim. For every natural number $D$, the apsidal angle $\Delta\theta(D) := 2\pi / \sqrt{4-D}$ satisfies $\Delta\theta(D) = 2\pi$ if and only if $D = 3$.
background
The module isolates the algebraic core of the Kepler (K) specialization used in dimensional rigidity. After the classical mechanics derivation is stripped away, one is left with the closed form $\Delta\theta(D) = 2\pi / \sqrt{4-D}$ and the pure equivalence $\Delta\theta(D)=2\pi \Leftrightarrow D=3$.
In Recognition Science the same integer $D=3$ is forced independently by the forcing chain (T8 spatial dimensions; T9 linking). Constants modules expose D := 3 as that forced value. Here $D$ is an arbitrary natural parameter; the theorem shows the Kepler selector singles out exactly that value.
The only analytic ingredients are the real square root, cancellation of the nonzero factor $2\pi$, and injectivity of the cast $\mathbb{N}\to\mathbb{R}$. Upstream arithmetic lemmas supply associativity, units, and nonzero products used in the cancellation steps.
proof idea
Bidirectional constructor.
Forward: assume $\Delta\theta(D)=2\pi$. Set $x=\sqrt{4-D}$. Nonzeroness of $2\pi$ rules out $x=0$ (else the angle would vanish). Rewrite the hypothesis as $(2\pi),x^{-1}=2\pi$, multiply through by $x$, cancel via inv_mul_cancel and mul_left_cancel₀ to obtain $x=1$. Nonnegativity of $4-D$ follows (else the square root is zero, contradicting $x=1$). Then $x^2=4-D$ and $x=1$ give $D=3$ in $\mathbb{R}$, hence in $\mathbb{N}$ by cast injectivity.
Reverse: substitute $D=3$, note $4-3=1$, and simplify the definition of the apsidal angle to $2\pi$.
why it matters
This is the reduced-form endpoint theorem of the Kepler specialization: once mechanics has produced $\Delta\theta(D)=2\pi/\sqrt{4-D}$, dimension selection collapses to a one-line algebraic fact. It sits in the verification layer so the dimensional-rigidity paper can cite a machine-checked selector rather than a hand calculation.
Framework landmark: T8 already forces spatial dimension three; the present result shows that the classical Kepler apsidal condition independently recovers the same integer. Together they tighten the claim that $D=3$ is not an input but an output of the recognition axioms. No downstream Lean consumers are wired yet; the declaration is the stable citation target for that paper step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.