`sync_prime_factorization`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.DimensionForcing
domain: Foundation
line: 339 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.DimensionForcing on GitHub at line 339.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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
 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) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.