RecognitionAtlas

formal source

 122/-! ## Recognition Atlas -/
 123
 124/-- A recognition atlas is a family of compatible charts that cover the space -/
 125structure RecognitionAtlas (L : LocalConfigSpace C) (r : Recognizer C E) (n : ℕ) where
 126  /-- The family of charts (indexed by some type) -/
 127  charts : Set (RecognitionChart L r n)
 128  /-- The charts are pairwise compatible -/
 129  compatible : ∀ φ₁ ∈ charts, ∀ φ₂ ∈ charts, ChartCompatible L r φ₁ φ₂
 130  /-- The charts cover the configuration space -/
 131  covers : ∀ c : C, ∃ φ ∈ charts, c ∈ φ.domain
 132
 133/-- An atlas covers the quotient space -/
 134theorem atlas_covers_quotient (A : RecognitionAtlas L r n) (q : RecognitionQuotient r) :
 135    ∃ φ ∈ A.charts, ∃ c ∈ φ.domain, recognitionQuotientMk r c = q := by
 136  obtain ⟨c, hc⟩ := Quotient.exists_rep q
 137  obtain ⟨φ, hφ, hcφ⟩ := A.covers c
 138  refine ⟨φ, hφ, c, hcφ, ?_⟩
 139  -- hc : ⟦c⟧ = q
 140  -- recognitionQuotientMk r c = Quotient.mk _ c = ⟦c⟧
 141  simp only [recognitionQuotientMk]
 142  exact hc
 143
 144/-! ## Recognition Dimension -/
 145
 146/-- The recognition dimension at a point is the dimension of any chart containing it -/
 147def hasRecognitionDimension (c : C) (n : ℕ) : Prop :=
 148  ∃ φ : RecognitionChart L r n, c ∈ φ.domain
 149
 150/-- **GEOMETRY AXIOM**: Dimension is well-defined.
 151
 152    **Status**: Axiom (invariance of domain)
 153    **Justification**: Brouwer's invariance of domain theorem
 154    **Reference**: Standard topology; Mathlib.Topology.Basic -/
 155def recognition_dimension_unique_hypothesis