no_higher_dimensional_alternative
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of the linking invariant for any specific D.
- Does not derive the three constraints from the core Recognition functional equation.
- Does not address non-integer or non-Euclidean dimension candidates.
- Does not supply the geometric infrastructure needed for the converse direction.
formal statement (Lean)
317theorem no_higher_dimensional_alternative (D : ℕ) (hD : 3 < D)
318 (hT : LinkingInvariantHypothesis D) (hK : ConstraintK D) (hS : ConstraintS D) :
319 False := by
proof body
Tactic-mode proof.
320 have h3 : D = 3 := dimensional_rigidity_full_forward D hT hK hS
321 have : D ≤ 3 := by simp [h3]
322 exact (not_le_of_gt hD) this
323
324end DraftV1
325end Papers
326end IndisputableMonolith