theorem
proved
rotation_period
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 343.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
formal source
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
360
361/-- D = 3 is RS-compatible. -/
362theorem D3_compatible : RSCompatibleDimension 3 := {
363 linking := D3_has_linking
364 eight_tick := rfl
365 gap_sync := by rw [sync_period_eq_360]; use 45; rfl
366}
367
368/-- D = 3 is the unique RS-compatible dimension. -/
369theorem dimension_unique (D : Dimension) :
370 RSCompatibleDimension D → D = 3 := by
371 intro ⟨hlink, height, _⟩
372 exact linking_requires_D3 D hlink
373