phasePeriod_5
plain-language theorem explainer
phasePeriod_5 evaluates the triangular number T(25) to 325 for dimension 5 in the synchronization analysis. Researchers comparing sync periods across odd dimensions cite this value when verifying that D=3 produces the shortest lcm. The proof applies native decision to evaluate the closed-form triangular number directly.
Claim. $T(25) = 325$, where $T(n) = n(n+1)/2$ is the nth triangular number.
background
In the Gap45 module, phasePeriod(D) is defined as T(D²) with T the triangular number. This enters the synchronization period lcm(2^D, T(D²)) used to select D=3 among odd dimensions. The upstream definition states that phasePeriod computes T(D * D). Module documentation notes that for odd D the periods are coprime, with D=3 minimizing the lcm to 360 while D=5 yields 10400.
proof idea
Native_decide evaluates the arithmetic expression for the triangular number at 25 in one step.
why it matters
This supplies the concrete T(25) value used to demonstrate that D=3 minimizes the synchronization period in the Dimensional Rigidity argument. The module lists D=5 as producing the larger period 10400, reinforcing uniqueness of the 45 selection. It ties into the generalization of the eight-tick period to 2^D for odd spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.