`injectivity_of_observable_map`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Papers.DraftV1 on GitHub at line 36.

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

  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

papers checked against this theorem

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