constraintS_forces_D3
plain-language theorem explainer
The theorem shows that the arithmetic constraint requiring a dimension D to be at least 3 and to minimize the synchronization period function holds exclusively for D equal to 3. Researchers deriving spatial dimensionality from Recognition Science minimization principles would cite this when closing the arithmetic selection step. The short term proof extracts the lower bound from ConstraintS, applies minimality at 3 to obtain one inequality, invokes the selection principle for the reverse, uses antisymmetry to equate periods, and applies the Unq
Claim. If $D$ is a natural number satisfying $D ≥ 3$ and $∀ D' ≥ 3, S(D) ≤ S(D')$ where $S(D) := lcm(2^D, 45)$, then $D = 3$.
background
ConstraintS D is the paper-style (S) constraint: D is admissible (D ≥ 3) and minimizes the synchronization period among all admissible dimensions. The module mirrors theorem statements from Draft_v1.tex, supplying certified arithmetic versions where the underlying mathematics is already formalized in the repository. syncPeriod is defined locally as Nat.lcm (2 ^ D) 45, matching the paper's S(D) := lcm(2^D, 45). Upstream, the synchronization_selection_principle states that among all D ≥ 3 the map D ↦ lcm(2^D, 45) is minimized uniquely at D = 3; its doc-comment describes it as a direct formalization of the paper's minimization statement.
proof idea
The proof is a term-mode derivation. From the hypothesis hS it extracts the lower bound 3 ≤ D. The minimality clause of ConstraintS applied at D' = 3 yields syncPeriod D ≤ syncPeriod 3. The selection principle supplies the reverse inequality syncPeriod 3 ≤ syncPeriod D. Antisymmetry of ≤ then forces equality of the periods. The uniqueness clause of the selection principle applied to this equality concludes D = 3.
why it matters
This result closes the arithmetic part of the (S) constraint by showing it selects D = 3 uniquely. It is used directly by the equivalence constraintS_iff_D3, which establishes the if-and-only-if between the constraint and D = 3. In the Recognition framework it supplies the step from the synchronization minimization (T7 eight-tick octave) to the spatial dimension D = 3 (T8). The parent theorem in the paper is the derivation of three-dimensionality from the constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.