dimensional_rigidity_full_forward
The theorem shows that any natural number D satisfying the sphere circle-linking invariant, the apsidal-angle condition of exactly 2π, and the synchronization-period minimizer property among all D ≥ 3 must equal 3. Researchers modeling dimensional selection in Recognition Science would cite it when deriving three spatial dimensions from the forcing chain. The proof is a one-line wrapper that applies the main dimensional rigidity lemma to the three supplied hypotheses.
claimLet $D$ be a natural number. If the $D$-sphere admits a circle-linking invariant, the apsidal angle equals $2π$, and $D$ is at least 3 while minimizing the synchronization period over all such dimensions, then $D=3$.
background
The Draft V1 module mirrors paper theorems using explicit hypothesis interfaces rather than new axioms, delegating the linking invariant to the cohomology-based predicate SphereAdmitsCircleLinking D. Constraint K is the closed-form apsidal-angle condition apsidalAngle D = 2π, while Constraint S requires both D ≥ 3 and that syncPeriod D is minimal among all admissible dimensions. The local setting imports quotient geometry, composition laws, and Alexander duality to keep the certified surface honest when external topology is needed.
proof idea
The proof is a one-line wrapper that applies the main dimensional rigidity lemma to the three hypotheses LinkingInvariantHypothesis D, ConstraintK D, and ConstraintS D.
why it matters in Recognition Science
This establishes the forward direction of dimensional rigidity and feeds directly into the corollary no_higher_dimensional_alternative showing that no D > 3 can satisfy all three constraints simultaneously. It aligns with the Recognition Science forcing chain (T8) that derives D = 3 from the eight-tick octave and self-similar fixed point phi. The paper notes that the converse direction remains dependent on further geometric infrastructure.
scope and limits
- Does not prove the converse from D=3 back to the three constraints.
- Does not apply if the linking invariant hypothesis is dropped.
- Does not address dimensions outside the natural numbers.
- Does not cover cases where the synchronization period fails to be minimal.
Lean usage
have h3 : D = 3 := dimensional_rigidity_full_forward D hT hK hSformal statement (Lean)
309theorem dimensional_rigidity_full_forward (D : ℕ)
310 (hT : LinkingInvariantHypothesis D) (hK : ConstraintK D) (hS : ConstraintS D) :
311 D = 3 :=
proof body
Term-mode proof.
312 dimensional_rigidity_main D hT hK hS
313
314/-- Paper corollary: there is no `D > 3` satisfying all three constraints simultaneously.
315
316We prove this using the (K)-based forcing `ConstraintK D → D=3`. -/