phasePeriod_7
The theorem supplies the explicit value of the phase period at dimension 7 as 1225. Researchers comparing synchronization costs across odd dimensions in the dimensional rigidity argument cite it to complete the numerical table for D greater than 3. The proof is a direct native decision that evaluates the definition of phasePeriod at input 7.
claim$T(49) = 1225$, where $T(n) = n(n+1)/2$ denotes the $n$th triangular number and phasePeriod$(D) := T(D^2)$.
background
The Gap45 module formalizes constraint (S) from the Dimensional Rigidity paper: among odd spatial dimensions D at least 3, only D=3 minimizes the synchronization period lcm(2^D, T(D^2)). The function phasePeriod is defined upstream as phasePeriod(D) := T(D * D), where T is the standard triangular-number function. This supplies the concrete T(49) entry required for the D=7 comparison line in the module argument.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic on the definition of phasePeriod at 7, which reduces directly to the arithmetic evaluation of the 49th triangular number.
why it matters in Recognition Science
The result completes the explicit numerical check for D=7 in the module's minimality argument, showing the synchronization period reaches 156800 versus 360 at D=3. It therefore supports the paper claim that D=3 uniquely selects the minimal sync cost among odd dimensions and closes the D=7 case in the broader forcing-chain analysis of eight-tick periodicity.
scope and limits
- Does not derive a closed-form expression for phasePeriod at arbitrary D.
- Does not prove that D=3 minimizes the lcm expression.
- Does not address even dimensions or the coprimality argument.
- Does not connect the value to J-cost, phi-ladder, or Recognition constants.
formal statement (Lean)
57@[simp] theorem phasePeriod_7 : phasePeriod 7 = 1225 := by native_decide