no_higher_dimensional_alternative
plain-language theorem explainer
The theorem shows that no natural number D greater than 3 can simultaneously satisfy the sphere linking invariant, the apsidal-angle condition, and the synchronization-period minimality condition. Researchers formalizing dimensional selection in Recognition Science cite this corollary to close the case against higher-dimensional alternatives. The proof invokes the forward rigidity theorem to force D equal to 3 and immediately derives a contradiction with the strict inequality D greater than 3.
Claim. Let $D$ be a natural number with $D>3$. Suppose $D$ admits an integer-valued loop-linking invariant on the sphere, the apsidal angle equals $2π$, and $D$ minimizes the synchronization period among all admissible dimensions at least 3. Then a contradiction follows.
background
The module mirrors theorem statements from Draft_v1.tex, employing hypothesis interfaces for geometric premises that rely on external infrastructure such as Alexander duality. LinkingInvariantHypothesis D stands for SphereAdmitsCircleLinking D, the paper's premise that an integer-valued loop-linking invariant exists. ConstraintK D encodes the closed-form apsidal-angle condition apsidalAngle D = 2π. ConstraintS D requires both D ≥ 3 and that D minimizes syncPeriod among all such dimensions. The upstream theorem dimensional_rigidity_full_forward states that these three conditions together force D = 3; its doc-comment notes that only the forward direction is proved here while the converse remains dependent on substantial geometric infrastructure.
proof idea
The tactic proof is a one-line wrapper around the forward rigidity theorem. It applies dimensional_rigidity_full_forward D hT hK hS to obtain D = 3, then uses simp to derive D ≤ 3, and finishes with the negation of the assumption 3 < D to reach falsehood.
why it matters
This corollary directly supports the Recognition Science claim that spatial dimension equals 3 (T8 in the forcing chain). It closes the higher-dimensional case under the three paper constraints and feeds the parent result dimensional_rigidity_full_forward. The declaration therefore strengthens the argument that only D = 3 survives the linking, apsidal, and synchronization requirements simultaneously.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.