injectivity_of_observable_map

formal source

  33open RecogGeom
  34
  35/-- Paper theorem: the induced map `R̄ : C_R → E` is injective. -/
  36theorem injectivity_of_observable_map {C E : Type*} (r : Recognizer C E) :
  37    Function.Injective (quotientEventMap r) :=
  38  quotientEventMap_injective (r := r)
  39
  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