ConstraintS
plain-language theorem explainer
ConstraintS encodes the paper (S) constraint: dimension D must be at least 3 and must minimize the synchronization period among all such dimensions. It is invoked in every proof that combines the (T,K,S) triple to recover D=3. The declaration is a direct definition that simply conjoins the lower bound with the universal minimality statement over the lcm-based period function.
Claim. Let $S(D) = {lcm}(2^D,45)$. The predicate ConstraintS$(D)$ holds if and only if $D≥3$ and $S(D)≤S(D')$ for every integer $D'≥3$.
background
In the Recognition Science setting the synchronization period is the arithmetic quantity $S(D) := {lcm}(2^D,45)$ that appears in the (S) leg of the dimensional-rigidity argument. The module Papers.DraftV1 supplies paper-oriented names for statements already available in the core library or recorded as hypothesis interfaces. Upstream, syncPeriod is defined in Gap45.SyncMinimization as Nat.lcm (2^D) (phasePeriod D) and specialized in Papers.DraftV1 to the constant 45 phase factor.
proof idea
The declaration is a pure definition. It directly forms the conjunction of the lower bound 3 ≤ D with the quantified statement ∀ D' ≥ 3, syncPeriod D ≤ syncPeriod D'. No lemmas or tactics are applied inside the definition.
why it matters
ConstraintS supplies the (S) component of the (T,K,S) triple used by dimensional_rigidity_main and its corollaries constraintS_forces_D3, constraintS_iff_D3, and no_higher_dimensional_alternative. Those results conclude that only D=3 satisfies the full set of constraints, recovering the spatial dimension forced by the eight-tick octave (T7) and the self-similar fixed point phi (T6). The definition closes the arithmetic half of the argument while the geometric linking-invariant hypothesis remains under an explicit interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.