sync_3_lt_5
The declaration establishes that the synchronization period for three spatial dimensions is strictly smaller than for five dimensions. Researchers modeling dimensional selection via synchronization cost in Recognition Science would cite this when arguing that D=3 uniquely minimizes the period among odd integers D >= 3. The proof is a direct numerical comparison executed by the native_decide tactic on the concrete lcm values.
claimLet $S(D) = {lcm}(2^D, T(D^2))$ where $T(n) = n(n+1)/2$ is the triangular number. Then $S(3) < S(5)$.
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^2)). Here syncPeriod D is defined as Nat.lcm (2^D) (phasePeriod D), with phasePeriod D returning the triangular number T(D^2). For D=3 this yields lcm(8,45)=360; for D=5 it yields lcm(32,325)=10400. Upstream results include the fixed syncPeriod constant 360 in RSNativeUnits and the period function phi^k in PulsarEmissionRegimesFromRS.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the concrete numerical inequality between the lcm expressions for D=3 and D=5.
why it matters in Recognition Science
This result supports the claim that D=3 minimizes synchronization cost, directly explaining the selection of 45 as T(9) in the Recognition framework. It connects to the eight-tick octave generalized from 2^3 to 2^D and the coprimality argument for odd D. The declaration fills the concrete comparison step in the Dimensional Rigidity paper's uniqueness argument for constraint (S).
scope and limits
- Does not prove that D=3 is minimal over all integers D, only the stated pair.
- Does not address even dimensions where gcd(2^D, T(D^2)) > 1.
- Does not incorporate J-cost, defectDist, or the phi-ladder mass formula.
- Does not derive the full uniqueness claim without further comparisons to D=7 and beyond.
formal statement (Lean)
97theorem sync_3_lt_5 : syncPeriod 3 < syncPeriod 5 := by native_decide
proof body
Term-mode proof.
98
99/-- D = 3 has strictly smaller sync period than D = 7. -/