syncPeriod_3_eq_360
plain-language theorem explainer
At spatial dimension three the synchronization period equals 360. Anyone citing the eight-tick/45 Chinese-remainder hinge or the D=3 forcing arithmetic needs this numeric anchor. The proof is a one-shot native decision procedure on the concrete natural-number equality.
Claim. The synchronization period evaluated at spatial dimension $3$ equals $360$: $\mathrm{syncPeriod}(3)=360$. (In context this is the value of $\mathrm{lcm}(2^3,45)$.)
background
Recognition Science forces spatial dimension $D=3$ (T8) and an eight-tick octave of length $2^3=8$ (T7). A second arithmetic period of length 45 appears from the fine-structure / gap side of the ledger. Their least common multiple is the global synchronization period that must close both clocks.
In this verification module the period is treated as a function of candidate dimension: $\mathrm{syncPeriod}(d)=\mathrm{lcm}(2^d,45)$. The constant form recorded in RS-native units is simply the evaluated value at the forced dimension, $\mathrm{lcm}(8,45)=360$. Upstream definitions fix $D:=3$ both in the alpha-derivation constants and in the gap-derivation layer.
The surrounding lemmas package a Chinese-remainder style forcing statement: only $D=3$ makes $\mathrm{lcm}(2^D,45)$ equal the observed sync length 360.
proof idea
Term-mode proof consisting of a single native_decide tactic. Lean reduces the concrete natural-number expression for the period at argument 3 (equivalently $\mathrm{lcm}(8,45)$) and checks equality with 360 by kernel computation. No intermediate lemmas are invoked.
why it matters
Supplies the numeric witness that the synchronization minimum sits at 360 when the dimension is three. Downstream siblings in the same module (lcm_pow2_45_forces_D3, lcm_pow2_45_eq_360_iff, syncPeriod_minimized_at_three) turn this equality into the arithmetic half of dimension forcing: only $D=3$ satisfies $\mathrm{lcm}(2^D,45)=360$.
That packages the 8↔45 hinge as a pure number-theoretic fact, linking the eight-tick octave (T7) to the forced spatial dimension (T8) inside the verification layer. Even with no external used_by edges yet, the lemma is the concrete base case the CRT-style forcing chain rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.