convergence_implies_identity

formal source

 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" ++
 156  "U3: DimensionInvariant — stated as hypothesis interface\n" ++
 157  "U4: NonCollapseCondition — monotone separation (auto from refinement)\n" ++
 158  "    monotone_separation_of_refinement: PROVED (no sorry)\n" ++
 159  "    convergence_implies_identity: PROVED (no sorry)\n" ++
 160  "STATUS: Hypothesis interfaces complete; manifold existence is the\n" ++
 161  "        genuinely open mathematics (requires topology of inverse limits)."
 162
 163end EffectiveManifold