dimensional_rigidity_full_forward
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.