constraintS_iff_D3
plain-language theorem explainer
The biconditional shows that the (S) constraint, requiring a dimension to be at least three and to minimize the synchronization period among admissible dimensions, holds precisely for three dimensions. Researchers formalizing the Recognition Science derivation of spatial dimensionality would cite this to anchor the T8 step. The proof splits the equivalence and invokes the forcing lemma in one direction together with the selection principle in the other.
Claim. Let $D$ be a natural number. The (S) constraint on $D$ holds if and only if $D=3$, where the (S) constraint asserts that $D$ is at least 3 and that $D$ minimizes the synchronization period among all integers $D' $ at least 3.
background
This module mirrors theorem statements from Draft_v1.tex, re-exporting proved results under paper-oriented names and supplying hypothesis interfaces for external mathematics such as Alexander duality. The (S) constraint is defined as admissibility ($D$ at least 3) together with minimality of the synchronization period syncPeriod. Upstream results include SphereAdmitsCircleLinking, which states that the D-sphere admits nontrivial circle linking precisely when reduced cohomology of the complement is nontrivial, and synchronization_selection_principle, which encodes the minimality property.
proof idea
The term-mode proof applies constructor to split the biconditional. The forward direction invokes constraintS_forces_D3 directly on the hypothesis. The reverse substitutes the equality $D=3$ and refines the remaining goal by applying the first component of synchronization_selection_principle to an arbitrary admissible $D'$.
why it matters
This equivalence closes the dimension-selection step that supports T8 in the forcing chain, confirming that three spatial dimensions are the unique minimizer under the (S) constraint. It directly mirrors a statement required in Draft_v1.tex and rests on the Alexander duality interface for the topological characterization. With zero current downstream uses, the declaration remains available for later derivations involving the phi-ladder or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.