theorem
proved
sync_implies_D3
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 346.
browse module
All declarations in this module, on Recognition.
explainer page
Derivations using this theorem
depends on
formal source
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
374/-- **THE DIMENSION FORCING THEOREM**
375
376 D = 3 is forced by Alexander duality: