nonCollapse_monotone_automatic

formal source

 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
 131/-- The convergence condition implies: the intersection of all
 132equivalence relations is the identity (diagonal). -/
 133theorem convergence_implies_identity (sys : DirectedRefinement C)
 134    (hconv : RefinementConverges sys) :
 135    ∀ c₁ c₂ : C,
 136      (∀ i, Indistinguishable (sys.recognizer i) c₁ c₂) → c₁ = c₂ :=
 137  hconv.eventually_separates
 138
 139/-! ## Connecting U1–U4 to the Paper's Assumption 2.11
 140
 141The paper's Assumption 2.11 posits:
 142  (a) A directed refinement (R_i) exists
 143  (b) A smooth D-manifold M exists as the limit
 144  (c) Coarse-graining maps φ_i : C_{R_i} → M satisfy convergence
 145
 146Our EffectiveManifoldHypotheses bundle captures the RG-internal
 147conditions (a) + convergence + non-collapse. The existence of M
 148itself (b,c) is what would follow from these conditions under
 149additional topological hypotheses not formalized here.
 150-/
 151
 152/-- Summary: the three open problems and their formalization status. -/
 153def status_summary : String :=
 154  "U1: EffectiveManifoldHypotheses — bundles U2+U4 into single structure\n" ++
 155  "U2: RefinementConverges — eventually separates all distinct points\n" ++