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

convergence_implies_identity

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)

 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₂ :=

proof body

Term-mode proof.

 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. -/

used by (1)

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

depends on (26)

Lean names referenced from this declaration's body.