`NonCollapseCondition`

definition

show as: view math explainer →

module: IndisputableMonolith.RecogGeom.EffectiveManifold
domain: RecogGeom
line: 100 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.RecogGeom.EffectiveManifold on GitHub at line 100.

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

used by

formal source

  97/-- U4: The refinement does not collapse: at every stage, the quotient
  98has at least as many classes as the previous stage (monotone cardinality).
  99This prevents dimension from dropping. -/
 100structure NonCollapseCondition (sys : DirectedRefinement C) : Prop where
 101  nontrivial_at_all_stages : ∀ i : ℕ,
 102    ∃ c₁ c₂ : C, ¬Indistinguishable (sys.recognizer i) c₁ c₂
 103  monotone_separation : ∀ i : ℕ, ∀ c₁ c₂ : C,
 104    ¬Indistinguishable (sys.recognizer i) c₁ c₂ →
 105    ¬Indistinguishable (sys.recognizer (i + 1)) c₁ c₂
 106
 107/-- Monotone separation follows from refinement. -/
 108theorem monotone_separation_of_refinement (sys : DirectedRefinement C) :
 109    ∀ i : ℕ, ∀ c₁ c₂ : C,
 110      ¬Indistinguishable (sys.recognizer i) c₁ c₂ →
 111      ¬Indistinguishable (sys.recognizer (i + 1)) c₁ c₂ := by
 112  intro i c₁ c₂ hne habs
 113  exact hne (sys.refines i c₁ c₂ habs)
 114
 115/-! ## U1: The Effective Manifold Bundle -/
 116
 117/-- U1: The complete hypothesis bundle for the effective-manifold assumption.
 118This packages U2 + U4 (U3 is a consequence when the limit exists). -/
 119structure EffectiveManifoldHypotheses (C : Type*) where
 120  system : DirectedRefinement C
 121  converges : RefinementConverges system
 122  nonCollapse : NonCollapseCondition system
 123
 124/-- U2 + refinement implies U4's monotone separation automatically. -/
 125theorem nonCollapse_monotone_automatic (sys : DirectedRefinement C) :
 126    ∀ i c₁ c₂,
 127      ¬Indistinguishable (sys.recognizer i) c₁ c₂ →
 128      ¬Indistinguishable (sys.recognizer (i + 1)) c₁ c₂ :=
 129  monotone_separation_of_refinement sys
 130

papers checked against this theorem

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