dimensional_rigidity_main
plain-language theorem explainer
Under the linking invariant hypothesis, the apsidal-angle constraint, and the synchronization-period minimizer constraint, the only admissible spatial dimension is three. Researchers formalizing dimensional selection from the DraftV1 paper would cite this result. The proof is a one-line term that applies the first component of the Kepler selection principle to the apsidal constraint.
Claim. If the linking invariant hypothesis holds for dimension $D$, the apsidal angle equals $2π$, and $D$ minimizes the synchronization period among all integers $D' ≥ 3$, then $D = 3$.
background
The module mirrors theorem statements from Draft_v1.tex and maps them to available Lean content. It uses explicit hypothesis interfaces for premises whose full geometric content, such as Alexander duality for complements of embeddings, is not yet formalized. This keeps the certified surface honest: theorems depending on those hypotheses are only as strong as the supplied interfaces.
proof idea
The proof is the term (kepler_selection_principle D).1 hK. It is a one-line wrapper that applies the first projection of the Kepler selection principle to the ConstraintK hypothesis.
why it matters
This theorem supplies the forward direction of the paper's main result on dimensional rigidity and is re-exported by dimensional_rigidity_full_forward. It realizes the T8 step of the forcing chain by showing that the three constraints force D = 3. The converse direction remains open pending additional geometric infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.