ConstraintS_Cert
plain-language theorem explainer
The constraint (S) certificate packages the six numerical and minimality properties that select dimension D=3 and its phase 45 as the unique minimizer of the synchronization period among odd dimensions up to 11. A physicist working on dimensional rigidity in Recognition Science cites this record when invoking the verified content of constraint (S) from the 2026 paper. The structure is assembled by direct arithmetic checks via native_decide together with two auxiliary lemmas that handle even-D failures and the strict increase on odd dimensions.
Claim. Let $T(n)$ be the $n$th triangular number. The certificate asserts $T(9)=45$, $lcm(8,45)=360$, $gcd(8,45)=1$, that even $D$ in {2,4,6,8,10} fail coprimality between $2^D$ and $T(D^2)$, that for every odd $D$ with $3<D≤11$ the period at $D=3$ is strictly smaller than at $D$, and that the periods strictly increase along the odd sequence 3<5<7<9<11.
background
The SyncMinimization module formalizes constraint (S) from the Dimensional Rigidity paper. For a spatial dimension $D$, phasePeriod $D$ is defined as the triangular number $T(D^2)$, which accumulates the phase contributions from the $D^2$ entries of the parity matrix on the $D$-cube. syncPeriod $D$ is then $lcm(2^D, T(D^2))$, the least common multiple that sets the synchronization barrier for that dimension.
proof idea
ConstraintS_Cert is a structure definition whose six fields collect the required assertions. The first three fields (phase_at_D3, sync_at_D3, coprime_at_D3) are discharged by native_decide on the concrete values 45, 360 and gcd(8,45)=1. The remaining three fields are supplied by the lemmas even_D_not_coprime and D3_unique_minimizer, which are referenced in the downstream construction of constraintS.
why it matters
This certificate supplies the verified content for constraint (S) and is used directly by the definition constraintS. It closes the numerical part of the argument that D=3 is selected because it minimizes synchronization cost, thereby realizing the eight-tick octave (T7) and the emergence of three spatial dimensions (T8) inside the Recognition Science forcing chain. The module doc states that D=3 yields the minimal lcm among odd dimensions ≥3, with explicit values 360, 10400 and 156800 for D=3,5,7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.