misaligned_ticks_per_cycle
plain-language theorem explainer
The theorem states that for any natural number k and any j with 1 ≤ j ≤ 359, the quantity 360k + j is never divisible by 360. Cosmologists working on perpetual complexity in Recognition Science would cite it to establish that phase mismatches occur in every cycle. The proof is a direct modular-arithmetic reduction discharged by the omega tactic after variable introduction.
Claim. For all natural numbers $k$ and $j$ with $1 ≤ j ≤ 359$, $(360k + j) mod 360 ≠ 0$.
background
In Recognition Science, time is discretized into fundamental ticks (τ₀ = 1), with an eight-tick octave as the basic evolution period. The integer 360 arises as the product of the recognition cadence 8 and the phase cadence 45; their coprimality (gcd(8,45)=1) prevents global synchronization. The module PerpetualComplexity combines this arithmetic fact with Ω_Λ > 0 to guarantee ongoing local complexity generation and the impossibility of heat death, as stated in the module doc: 'The combination guarantees that the universe generates local complexity at every epoch.' Upstream, the H function from CostAlgebra reparametrizes J-cost via H(x) = J(x) + 1, satisfying the d'Alembert equation H(xy) + H(x/y) = 2·H(x)·H(y), which assigns positive cost to misaligned states.
proof idea
The proof is a one-line wrapper. After the intro tactic binds k, j and the inequalities 1 ≤ j and j ≤ 359, the omega tactic resolves the modular goal by reducing (360k + j) % 360 to j, which lies strictly between 1 and 359.
why it matters
This arithmetic lemma supplies the counting step inside the Perpetual Complexity Theorem (Dark_Energy_Mode_Counting.tex §10, Theorem 10.1), which concludes that thermal equilibrium is unreachable because periods 8 and 45 never align simultaneously. It operationalizes the eight-tick octave (T7) and the Recognition Composition Law by ensuring that every 360-tick cycle contains 359 misaligned ticks, each carrying positive J-cost. The result directly supports the no_heat_death claim in the same module and closes the scaffolding path from coprimality to perpetual complexity generation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.