syncPeriod_11
plain-language theorem explainer
The declaration computes the synchronization period for dimension 11 as exactly 15116288. Researchers comparing synchronization costs across odd dimensions in the Recognition framework would cite this value to confirm the growth of lcm(2^D, T(D²)) for D > 3. The proof is a direct native evaluation of the lcm definition.
Claim. The synchronization period for spatial dimension 11 equals 15116288, where the synchronization period is the least common multiple of $2^D$ and the triangular number $T(D^2)$.
background
The module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D ≥ 3, D = 3 uniquely minimizes the synchronization period lcm(2^D, T(D²)). The synchronization period for dimension D is defined as Nat.lcm (2^D) (phasePeriod D), with phasePeriod D the triangular number T(D²). Upstream results supply the general syncPeriod definition and the period function from astrophysics contexts.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the lcm expression for D = 11 directly.
why it matters
This numerical result supports the minimization argument by supplying the explicit period for D = 11, which exceeds the D = 3 value of 360. It fills a comparison entry in the paper's constraint (S) and the eight-tick octave generalization to 2^D. No downstream theorems depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.