`refinement`

proved

show as: view math explainer →

module: IndisputableMonolith.Papers.DraftV1
domain: Papers
line: 43 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Papers.DraftV1 on GitHub at line 43.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  40/-! ## Paper Theorem: Refinement (Composition of Recognizers) -/
  41
  42/-- Paper theorem: the composite quotient maps surjectively to each component quotient. -/
  43theorem refinement {C E₁ E₂ : Type*} (r₁ : Recognizer C E₁) (r₂ : Recognizer C E₂) :
  44    Function.Surjective (quotientMapLeft r₁ r₂) ∧
  45    Function.Surjective (quotientMapRight r₁ r₂) :=
  46  refinement_theorem (r₁ := r₁) (r₂ := r₂)
  47
  48end RecognitionGeometry
  49
  50/-! ## Constraint (S): Dyadic synchronization (N = 45) -/
  51
  52open Nat
  53
  54/-- The synchronization period used in `Draft_v1.tex`: `S(D) := lcm(2^D, 45)`. -/
  55def syncPeriod (D : ℕ) : ℕ := Nat.lcm (2 ^ D) 45
  56
  57lemma syncPeriod_def (D : ℕ) : syncPeriod D = Nat.lcm (2 ^ D) 45 := rfl
  58
  59/-! The key arithmetic lemma used in the paper's proof: since `45` is odd,
  60`gcd(2^D,45)=1`, hence `lcm(2^D,45)=2^D*45`. -/
  61theorem syncPeriod_eq_mul (D : ℕ) : syncPeriod D = (2 ^ D) * 45 := by
  62  unfold syncPeriod
  63  have h2 : Nat.Coprime 2 45 := by decide
  64  have h : Nat.Coprime (2 ^ D) 45 := h2.pow_left D
  65  simpa using h.lcm_eq_mul
  66
  67/-! ### Synchronization Selection Principle (proved) -/
  68
  69/-- A direct formalization of the paper's minimization statement:
  70among all `D ≥ 3`, the function `D ↦ lcm(2^D,45)` is minimized uniquely at `D = 3`. -/
  71theorem synchronization_selection_principle {D : ℕ} (hD : 3 ≤ D) :
  72    syncPeriod 3 ≤ syncPeriod D ∧ (syncPeriod D = syncPeriod 3 → D = 3) := by
  73  constructor

papers checked against this theorem

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