Constants Rsnative Units Sync Period Eq Lcm

The sync period

A ledger, a discrete record of events, often marks time by counting repeated patterns. The Recognition Science framework defines its atomic time quantum, the tick, as one such posting interval. Around this tick, the framework builds two larger cycles: an eight-tick octave and a 45-tick gap. The declaration syncPeriod_eq_lcm proves that the period after which these two cycles realign is their least common multiple, 360 ticks.

The theorem itself is a small piece of arithmetic. It states that the number 360 equals the least common multiple of 8 and 45. The proof is a direct computation, checked by the machine. Its significance is structural: it guarantees that the two cycles, one tied to the octave and one to the gap, return to the same phase together exactly every 360 ticks. This synchronization is a definitional choice within the framework, not a derived physical law.

In Recognition Science, the framework models time as a count of ticks, and the sync period is the natural interval over which the octave and gap cycles complete together. The declaration does not claim that 360 ticks has any external physical meaning, nor that this synchronization drives any particular phenomenon. It is a formal fact about the framework's own units, useful for maintaining consistent cycle bookkeeping.

The practical consequence is a clean calendar for the framework's internal rhythms. Any process that depends on both the octave and the gap can be studied over a single 360-tick window without missing an alignment. This makes the sync period a convenient unit for describing longer-term behavior in the framework's native time.

lemma syncPeriod_eq_lcm : syncPeriod = Nat.lcm 8 45 := by native_decide

/-- The synchronization period: lcm(8, 45) = 360. -/
@[simp] def syncPeriod : ℕ := 360

What this page does not claim

The sync period is not claimed to correspond to any measured physical time interval. The theorem does not claim that the octave and gap cycles are physically coupled; it only states their alignment period. The declaration does not establish that 360 ticks has any significance outside the framework's own unit system.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/RSNativeUnits.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: