pith. machine review for the scientific record. sign in
theorem proved tactic proof high

misalignment_exists

show as:
view Lean formalization →

The misalignment_exists theorem asserts that any natural-number tick count not divisible by 360 fails to align with at least one of the 8-tick or 45-tick cadences. Cosmologists working on perpetual complexity cite it to show that recognition mismatches persist at every epoch. The proof proceeds by contradiction: assuming both divisors hold, coprimality of 8 and 45 forces 360 to divide the count, violating the hypothesis.

claimLet $t$ be a natural number. If $360$ does not divide $t$, then $8$ does not divide $t$ or $45$ does not divide $t$.

background

The PerpetualComplexity module combines positive vacuum energy with the coprimality of the 8-tick octave and the 45-tick gap period. The 8-tick cadence originates in the self-similar forcing chain (T7), while the 45-tick period enters through Gap45 synchronization minimization. Upstream structures include J-cost convexity from PhysicsComplexityStructure, which shows that misaligned voxels carry positive structured excitations, and SpectralEmergence, which fixes the underlying gauge and generation content.

proof idea

Proof by contradiction. Assume both $t$ mod 8 equals zero and $t$ mod 45 equals zero. Apply Nat.Coprime.mul_dvd_of_dvd_of_dvd to the coprimality fact (native_decide) together with the two divisibility hypotheses to obtain that 360 divides $t$. This immediately contradicts the input hypothesis that $t$ mod 360 is nonzero.

why it matters in Recognition Science

The result supplies the coprimality implication required by the perpetual_complexity theorem, which states that positive vacuum energy together with gcd(8,45)=1 guarantees perpetual local complexity generation. It fills the gap in Dark_Energy_Mode_Counting.tex §10, Theorem 10.1, and rests on the eight-tick octave (T7) and gap-45 frustration. The lemma closes the logical step that prevents global synchronization and therefore heat death.

scope and limits

Lean usage

theorem perpetual_complexity_example (omega_lambda_pos : (0 : ℝ) < 11/16) (gap45_coprime : Nat.Coprime 8 45) : ∀ t : ℕ, t % 360 ≠ 0 → (t % 8 ≠ 0 ∨ t % 45 ≠ 0) := by intro t ht; exact misalignment_exists t ht

formal statement (Lean)

  69theorem misalignment_exists (t : ℕ) (h : t % 360 ≠ 0) :
  70    t % 8 ≠ 0 ∨ t % 45 ≠ 0 := by

proof body

Tactic-mode proof.

  71  by_contra h_neg
  72  push_neg at h_neg
  73  obtain ⟨h8, h45⟩ := h_neg
  74  have : 360 ∣ t := by
  75    have := Nat.Coprime.mul_dvd_of_dvd_of_dvd (by native_decide : Nat.Coprime 8 45)
  76      (Nat.dvd_of_mod_eq_zero h8) (Nat.dvd_of_mod_eq_zero h45)
  77    simpa using this
  78  exact h (Nat.mod_eq_zero_of_dvd this)
  79
  80/-- Between any two multiples of 360, there are 359 misaligned ticks. -/

used by (2)

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

depends on (6)

Lean names referenced from this declaration's body.