sync_3_lt_9
The declaration proves that the synchronization period for spatial dimension 3 is strictly smaller than for dimension 9. Researchers modeling dimensional rigidity in Recognition Science cite this when showing D equals 3 uniquely minimizes the lcm of the octave period and the triangular number of D squared among odd dimensions. The proof evaluates the concrete natural-number expressions for both sides using native decision procedures.
claimLet $S(D) :=$ lcm$(2^D, T(D^2))$ where $T(n) = n(n+1)/2$ is the triangular number. Then $S(3) < S(9)$.
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 function syncPeriod D is defined as Nat.lcm (2^D) (phasePeriod D), where phasePeriod D computes the triangular number T(D²). Upstream results include the constant syncPeriod fixing the D=3 value at 360 and the DraftV1 version using lcm(2^D, 45) to reflect T(9)=45.
proof idea
The proof is a direct term-mode application of native_decide, which computes the numerical values of syncPeriod 3 and syncPeriod 9 and verifies the strict inequality.
why it matters in Recognition Science
This result supports the selection of D=3 in the eight-tick octave framework (T7) and the forcing of three spatial dimensions (T8). It contributes to the argument in the Dimensional Rigidity paper that D=3 uniquely minimizes synchronization cost, explaining the emergence of the 45 in the phi-ladder mass formula. No open questions are directly addressed here, but it closes a computational check in the sync minimization chain.
scope and limits
- Does not establish minimality for all odd D greater than 9.
- Does not compare against even dimensions where partial alignment occurs.
- Does not derive the phasePeriod definition from first principles.
- Does not address physical observability of the sync period.
formal statement (Lean)
103theorem sync_3_lt_9 : syncPeriod 3 < syncPeriod 9 := by native_decide
proof body
Term-mode proof.
104
105/-- D = 3 has strictly smaller sync period than D = 11. -/