syncPeriod_3_eq_360
The equality establishes that the synchronization period evaluates to 360 at three dimensions in Recognition Science units. Researchers modeling the eight-tick octave or fixing spatial dimension D=3 would cite this when anchoring the phi-ladder constants. The proof reduces to a single native_decide tactic that computes the closed-form expression directly.
claimThe synchronization period at three spatial dimensions satisfies $syncPeriod(3) = 360$.
background
In Recognition Science the synchronization period is the function $D mapsto 2^D times 45$, which equals lcm(8,45) at D=3. This definition appears in RSNativeUnits and is used throughout the forcing chain to realize the eight-tick octave (T7) and the emergence of D=3 (T8). The Papers.DraftV1 module re-exports such equalities from Draft_v1.tex so that paper statements can be audited against the certified library without introducing new axioms.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the equality from the definition of syncPeriod.
why it matters in Recognition Science
This pins the minimal value of the synchronization period at the dimension forced by the unified forcing chain, directly supporting the synchronization_selection_principle that proves uniqueness of the minimum among D greater than or equal to 3. It aligns with the resource-functional minimization packaged in the same paper section and with the T7 eight-tick octave landmark.
scope and limits
- Does not derive the closed form of syncPeriod from the Recognition Composition Law.
- Does not treat non-integer or continuous values of D.
- Does not incorporate the fine-structure constant alpha or the mass-ladder formula.
- Does not prove the full resource-functional minimization statement.
formal statement (Lean)
119theorem syncPeriod_3_eq_360 : syncPeriod 3 = 360 := by
proof body
Term-mode proof.
120 native_decide
121
122/-! The paper also packages the minimization in terms of a resource functional
123\(\mathcal{F}(D,45)=\alpha\,\mathrm{lcm}(2^D,45)+\beta D\) with \(\alpha>0,\beta\ge0\).
124We record that consequence here. -/
125
126/-- If `α>0` and `β≥0`, then the resource functional
127`F(D)=α * lcm(2^D,45) + β * D` is minimized at `D=3` among `D≥3`. -/