syncPeriod_eq_mul
plain-language theorem explainer
The arithmetic identity establishes that the synchronization period S(D) defined as lcm(2^D, 45) equals 2^D times 45 for any natural number D. Authors formalizing the Draft_v1.tex paper on Recognition Science would invoke this to simplify the minimization argument for the synchronization selection principle. The proof is a short tactic sequence that unfolds the definition, establishes coprimeness of powers of 2 with 45, and invokes the lcm-multiplication identity for coprime arguments.
Claim. For every natural number $D$, $lcm(2^D, 45) = 2^D · 45$.
background
In the Draft_v1.tex formalization module, the synchronization period is introduced as S(D) := lcm(2^D, 45) to capture the least common multiple arising in the paper's synchronization arguments. This definition appears alongside the constant syncPeriod in RSNativeUnits, which evaluates to 360 when D=3. The module mirrors theorem statements from the LaTeX paper, providing explicit Lean counterparts where the underlying arithmetic is elementary. The upstream result from Constants.RSNativeUnits.syncPeriod defines the base case as 360, consistent with lcm(8,45)=360.
proof idea
The proof unfolds the definition of syncPeriod to expose the lcm expression. It then constructs the coprimeness fact Nat.Coprime 2 45 by decision, lifts it to Nat.Coprime (2^D) 45 via the pow_left lemma, and finally applies lcm_eq_mul to obtain the product form.
why it matters
This lemma supplies the closed-form expression required by the synchronization_selection_principle theorem, which asserts that among D ≥ 3 the function D ↦ lcm(2^D,45) is minimized uniquely at D=3. It directly supports the paper's minimization statement and aligns with the eight-tick octave structure (period 2^3) in the Recognition Science forcing chain. The result closes an arithmetic gap in the formalization of the Draft_v1.tex synchronization arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.