theorem
proved
gap_45_has_factor_9
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.DimensionForcing on GitHub at line 329.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
formal source
326theorem gap_45_factorization : gap_45 = 9 * 5 := rfl
327
328/-- Gap-45 has factor 9 = 3². -/
329theorem gap_45_has_factor_9 : 9 ∣ gap_45 := ⟨5, rfl⟩
330
331/-- The sync period 360 = 8 × 45 / gcd(8,45) = 360. -/
332theorem sync_factorization : sync_period = 8 * 45 := by
333 unfold sync_period eight_tick gap_45
334 -- lcm(8, 45) = 8 * 45 / gcd(8, 45) = 360 / 1 = 360
335 -- But actually gcd(8, 45) = 1, so lcm = 8 * 45 = 360
336 rfl
337
338/-- 360 = 2³ × 3² × 5. -/
339theorem sync_prime_factorization : sync_period = 2^3 * 3^2 * 5 := by
340 unfold sync_period eight_tick gap_45; rfl
341
342/-- 360 degrees in a circle relates to SO(3). -/
343theorem rotation_period : sync_period = 360 := sync_period_eq_360
344
345/-- The 2³ factor in 360 corresponds to D = 3. -/
346theorem sync_implies_D3 : 2^3 ∣ sync_period := by
347 rw [sync_period_eq_360]
348 use 45; rfl
349
350/-! ## Combined Forcing -/
351
352/-- A dimension is RS-compatible if it satisfies all forcing conditions:
353 1. Supports non-trivial linking (ledger conservation)
354 2. 2^D = 8 (eight-tick synchronization)
355 3. Compatible with gap-45 sync -/
356structure RSCompatibleDimension (D : Dimension) : Prop where
357 linking : SupportsNontrivialLinking D
358 eight_tick : EightTickFromDimension D = eight_tick
359 gap_sync : 2^D ∣ sync_period