pith. machine review for the scientific record. sign in
theorem proved term proof

constant_recognizer_regular

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 115theorem constant_recognizer_regular (L : LocalConfigSpace C) (r : Recognizer C E)
 116    (hconst : ∀ c₁ c₂, r.R c₁ = r.R c₂) :
 117    IsRegular L r := by

proof body

Term-mode proof.

 118  intro c
 119  obtain ⟨U, hU⟩ := L.N_nonempty c
 120  use U, hU
 121  intro c₁ c₂ _ _
 122  exact hconst c₁ c₂
 123
 124/-! ## The Role of RG5 in Geometry -/
 125
 126/-- **Intuition**: RG5 ensures that "resolution cells don't fragment".
 127
 128    Without RG5, a resolution cell could look like a Cantor set:
 129    infinitely fragmented within any neighborhood. With RG5, resolution
 130    cells are locally "blob-like"—they stay together coherently.
 131
 132    This is what allows smooth geometric structure to emerge:
 133    resolution cells become the "atoms" of recognition geometry,
 134    and RG5 ensures these atoms are well-behaved. -/
 135
 136/-! ## Module Status -/
 137

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (21)

Lean names referenced from this declaration's body.