pith. sign in
module module high

IndisputableMonolith.Gap45.Beat

show as:
view Lean formalization →

The Gap45.Beat module establishes the beat synchronization between the eight-tick cycle and a 45-unit interval through gcd, lcm, and derived cycle counts. Researchers working on discrete synchronization in the Recognition Science measurement layer would cite these results when aligning periodic streams. The module proceeds as a chain of elementary arithmetic lemmas that compute the common period 360 and verify minimal divisors.

claimLet $b = 8$ and $c = 45$. Then $gcd(b,c)=1$, $lcm(b,c)=360$, beats equals the common period 360, cycles_of_8 equals 45, cycles_of_45 equals 8, and the minimal synchronization condition holds that 360 is the least common multiple.

background

This module sits inside the Gap45 domain and imports the eight-tick stream invariants re-exported by IndisputableMonolith.Measurement. Those invariants supply the discrete periodic structure (period 2^3) used throughout the measurement scaffold. The module introduces the beat as the least common multiple of the 8-tick period and the 45-unit interval, together with the associated cycle counts and the minimal divisor condition that guarantees alignment.

proof idea

The module is organized as a linear sequence of number-theoretic lemmas. It first establishes gcd_8_45_eq_one, derives lcm_8_45_eq_360 from the identity lcm(a,b)=a*b/gcd(a,b), then defines beats and the two cycle counters, and finally proves the minimal_sync_divides and no_smaller_multiple statements by direct comparison of divisors.

why it matters in Recognition Science

Gap45.Beat supplies the synchronization primitives required by the downstream Ethics.CostModel. It completes the discrete-cycle layer of the eight-tick octave framework, providing the concrete period and repetition counts needed for cost calculations that rest on the Measurement re-exports.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (16)