kepler_selection_principle
plain-language theorem explainer
The theorem establishes that the apsidal angle equals 2π precisely when the spatial dimension D equals 3. Researchers deriving dimensional rigidity from orbital mechanics in Recognition Science would cite this algebraic closure step. The proof is a direct biconditional split that isolates the square-root term in the closed-form apsidal expression, cancels the 2π factor via field cancellation, and recovers D=3 by casting injectivity.
Claim. Let Δθ(D) be the closed-form apsidal angle in dimension D. Then Δθ(D) = 2π if and only if D = 3.
background
In the Recognition Science setting the apsidal angle is the substituted closed-form expression obtained after inserting the synchronization period 360 and the curvature bridge K = φ^{1/2} into the orbital dynamics. The module Papers.DraftV1 mirrors theorem statements from Draft_v1.tex, re-exporting proved results under paper-oriented names while keeping external mathematics (Alexander duality, full Binet machinery) behind explicit hypothesis interfaces. Upstream results supply the arithmetic lemmas for multiplication cancellation and the definition of syncPeriod as lcm(8,45)=360 that justify the substitution leading to the square-root expression.
proof idea
The tactic proof opens with constructor to split the biconditional. The forward direction assumes apsidalAngle D = 2π, sets x := sqrt(4-D), proves x ≠ 0 by contradiction, rewrites the equality as 2π · x^{-1} = 2π, multiplies through by x, cancels 2π using mul_left_cancel₀, obtains x=1, squares to recover 4-D=1, and concludes D=3 by Nat.cast_injective. The reverse direction substitutes D=3 directly and simplifies the square root to 1.
why it matters
This result supplies the (K) constraint inside the parent theorem dimensional_rigidity_main, which concludes D=3 from the linking invariant, ConstraintK, and ConstraintS. It formalizes the paper's final algebraic step in the dimensional-rigidity argument and aligns with the T8 forcing of three spatial dimensions in the unified forcing chain. The declaration closes the Kepler-selection verification at the arithmetic level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.