Green's open problem 39

namespace Green39Submission

abbrev PrimeIndex := {p : ℕ // p.Prime}

end Green39Submission

section PrimeNonzero

variable [primeNonzero : ∀ p : Green39Submission.PrimeIndex, NeZero (p : ℕ)]

/- Deterministic development assembly. No submission-readiness claim. -/

/- Source: Green39Submission.Definitions; SHA256 a1749b0be3c7a3e555ec52daedd29e35c843a382292a058a1582536218ebde1f -/
section Green39AssemblyScope_a6f04a854f1bd118
                                                   
                                                      
                                   
                              

/-!
Shared finite definitions for the Green39 formalization.

Input probabilities are exact finite counts, including on the exact-cardinality
slice. The auxiliary Bernoulli definitions below concern source thinning only.
No assertion about the principal covering theorem is made in this module.
-/

namespace Green39Submission

open scoped BigOperators Pointwise

universe u v

/-- Uniform probability on a finite sample space. The empty-space value is zero. -/
noncomputable def uniformProb {α : Type u} (sample : Finset α)
    (event : α → Prop) : ℝ := by
  classical
  exact ((sample.filter event).card : ℝ) / (sample.card : ℝ)

/-- Exact finite mean. The empty-space value is zero. -/
noncomputable def uniformMean {α : Type u} (sample : Finset α)
    (f : α → ℝ) : ℝ :=
  (∑ a ∈ sample, f a) / (sample.card : ℝ)

/-- The finite sample space of all `k`-element subsets of `universe`. -/
def exactSlice {α : Type u} (U : Finset α) (k : ℕ) : Finset (Finset α) :=
  U.powersetCard k

/-- Number of representations of `x` as an element of `A` plus an element of `T`. -/
def representationCount {G : Type v} [AddCommGroup G] [DecidableEq G]
    (A T : Finset G) (x : G) : ℕ :=
  (T.filter (fun t => x - t ∈ A)).card

/-- Targets left uncovered by the translating set `T`. -/
def holeSet {G : Type v} [AddCommGroup G] [DecidableEq G] [Fintype G]
    (A T : Finset G) : Finset G :=
  Finset.univ \ (A + T)

/-- Coverability with at most the literal number `c` of distinct translates. -/
def coverable {G : Type v} [AddCommGroup G] [DecidableEq G] [Fintype G]
    (A : Finset G) (c : ℕ) : Prop :=
  ∃ T : Finset G, T.card ≤ c ∧ A + T = Finset.univ

/-- Source-thinning weight; used for `selected ⊆ universe`. -/
noncomputable def bernoulliWeight {α : Type u} [DecidableEq α]
    (U selected : Finset α) (θ : ℝ) : ℝ :=
  θ ^ selected.card * (1 - θ) ^ (U \ selected).card

/-- Finite source-thinning mean, summed over every subset of the fixed universe. -/
noncomputable def bernoulliMean {α : Type u} [DecidableEq α]
    (U : Finset α) (θ : ℝ) (f : Finset α → ℝ) : ℝ :=
  ∑ selected ∈ U.powerset, bernoulliWeight U selected θ * f selected

/-- Inputs protected by an exceptional set or by a selected ordinary alias. -/
def protectedInputs {G : Type v} [AddCommGroup G] [DecidableEq G]
    (A E0 S D : Finset G) : Finset G :=
  E0 ∪ (A ∩ (S - D))

/-- A finite nonnegative-containment polynomial when its supplied weights are nonnegative.
The definition itself permits arbitrary real weights and retains repeated support labels. -/
noncomputable def containmentSum {α : Type u} {ι : Type v} (I : Finset ι)
    (support : ι → Finset α) (weight : ι → ℝ) (B : Finset α) : ℝ := by
  classical
  exact ∑ i ∈ I, if support i ⊆ B then weight i else 0

theorem mem_exactSlice {α : Type u} {U A : Finset α} {k : ℕ} :
    A ∈ exactSlice U k ↔ A ⊆ U ∧ A.card = k := by
  exact Finset.mem_powersetCard

theorem card_exactSlice {α : Type u} (U : Finset α) (k : ℕ) :
    (exactSlice U k).card = U.card.choose k := by
  exact Finset.card_powersetCard k U

theorem exactSlice_nonempty {α : Type u} {U : Finset α} {k : ℕ} :
    (exactSlice U k).Nonempty ↔ k ≤ U.card := by
  exact Finset.powersetCard_nonempty

theorem exactSlice_eq_empty_iff {α : Type u} {U : Finset α} {k : ℕ} :
    exactSlice U k = ∅ ↔ U.card < k := by
  exact Finset.powersetCard_eq_empty

/-- Exact cardinality of the containing slice, with no independence approximation. -/
theorem card_exactSlice_filter_subset {α : Type u} [DecidableEq α]
    (U S : Finset α) (k : ℕ) (hSU : S ⊆ U) (hSk : S.card ≤ k) :
    ((exactSlice U k).filter (fun B => S ⊆ B)).card =
      (U.card - S.card).choose (k - S.card) := by
  exact Finset.card_filter_powersetCard_subset S U k hSU hSk

theorem mem_holeSet {G : Type v} [AddCommGroup G] [DecidableEq G]
    [Fintype G] (A T : Finset G) (x : G) :
    x ∈ holeSet A T ↔ x ∉ A + T := by
  simp [holeSet]

end Green39Submission
end Green39AssemblyScope_a6f04a854f1bd118

/- Source: Green39Submission.Coverage; SHA256 2a772767667b5df7ba18196a4426499b07edd0fd21b8a1c61b1c59cac12add8e -/
section Green39AssemblyScope_e55302cfa6458e3c
                                    
                     

/-!
Deterministic coverage identities used to connect the two probabilistic
obstructions to the exact native cover event. No probabilistic conclusion is
assumed or proved in this module.
-/

namespace Green39Submission

open scoped BigOperators Pointwise

universe u

variable {G : Type u} [AddCommGroup G] [DecidableEq G]

theorem representationCount_pos_iff {A T : Finset G} {x : G} :
    0 < representationCount A T x ↔ x ∈ A + T := by
  classical
  rw [representationCount, Finset.card_pos]
  constructor
  · rintro ⟨t, ht⟩
    rcases Finset.mem_filter.mp ht with ⟨ht, hxt⟩
    exact Finset.mem_add.mpr ⟨x - t, hxt, t, ht, sub_add_cancel x t⟩
  · intro hx
    rcases Finset.mem_add.mp hx with ⟨a, ha, t, ht, rfl⟩
    exact ⟨t, Finset.mem_filter.mpr ⟨ht, by simpa using ha⟩⟩

theorem representationCount_eq_zero_iff {A T : Finset G} {x : G} :
    representationCount A T x = 0 ↔ x ∉ A + T := by
  rw [← representationCount_pos_iff]
  omega

theorem representationCount_le_card_right (A T : Finset G) (x : G) :
    representationCount A T x ≤ T.card :=
  Finset.card_filter_le _ _

theorem representationCount_le_card_left (A T : Finset G) (x : G) :
    representationCount A T x ≤ A.card := by
  classical
  unfold representationCount
  apply Finset.card_le_card_of_injOn (fun t : G => x - t)
  · intro t ht
    exact (Finset.mem_filter.mp ht).2
  · intro a ha b hb hab
    exact sub_right_inj.mp hab

theorem representationCount_mono {A A' T T' : Finset G}
    (hA : A ⊆ A') (hT : T ⊆ T') (x : G) :
    representationCount A T x ≤ representationCount A' T' x := by
  apply Finset.card_le_card
  intro t ht
  rcases Finset.mem_filter.mp ht with ⟨ht, hxt⟩
  exact Finset.mem_filter.mpr ⟨hT ht, hA hxt⟩

section Finite

variable [Fintype G]

theorem holeSet_eq_filter_zero (A T : Finset G) :
    holeSet A T = Finset.univ.filter (fun x => representationCount A T x = 0) := by
  ext x
  simp [mem_holeSet, representationCount_eq_zero_iff]

theorem holeSet_eq_empty_iff (A T : Finset G) :
    holeSet A T = ∅ ↔ A + T = Finset.univ := by
  rw [holeSet, Finset.sdiff_eq_empty_iff_subset]
  exact ⟨fun h => Finset.Subset.antisymm (Finset.subset_univ _) h,
    fun h => h ▸ Finset.Subset.refl _⟩

theorem holeSet_card_eq_zero_iff (A T : Finset G) :
    (holeSet A T).card = 0 ↔ A + T = Finset.univ := by
  rw [Finset.card_eq_zero, holeSet_eq_empty_iff]

theorem holeSet_card_add_covered_card (A T : Finset G) :
    (holeSet A T).card + (A + T).card = Fintype.card G := by
  simpa [holeSet] using
    Finset.card_sdiff_add_card_eq_card (Finset.subset_univ (A + T))

theorem holeSet_antitone {A A' T T' : Finset G}
    (hA : A ⊆ A') (hT : T ⊆ T') : holeSet A' T' ⊆ holeSet A T := by
  intro x hx
  apply (mem_holeSet A T x).2
  intro hxt
  exact (mem_holeSet A' T' x).1 hx (Finset.add_subset_add hA hT hxt)

theorem coverable_mono_budget {A : Finset G} {c c' : ℕ}
    (hcc' : c ≤ c') (h : coverable A c) : coverable A c' := by
  rcases h with ⟨T, hT, hcover⟩
  exact ⟨T, hT.trans hcc', hcover⟩

theorem coverable_mono_input {A A' : Finset G} {c : ℕ}
    (hA : A ⊆ A') (h : coverable A c) : coverable A' c := by
  rcases h with ⟨T, hT, hcover⟩
  refine ⟨T, hT, Finset.Subset.antisymm (Finset.subset_univ _) ?_⟩
  rw [← hcover]
  exact Finset.add_subset_add hA (Finset.Subset.refl _)

/-- Padding here preserves coverage and the rich-target lower profile. It does
not assert the finer off-exception profile cap needed by the sparse theorem. -/
theorem exists_cover_exact_budget {A : Finset G} {c : ℕ}
    (hc : c ≤ Fintype.card G) (h : coverable A c) :
    ∃ T : Finset G, T.card = c ∧ A + T = Finset.univ := by
  rcases h with ⟨T, hT, hcover⟩
  obtain ⟨T', hTT', _, hT'⟩ := Finset.exists_subsuperset_card_eq
    (Finset.subset_univ T) hT (by simpa using hc)
  refine ⟨T', hT', Finset.Subset.antisymm (Finset.subset_univ _) ?_⟩
  rw [← hcover]
  exact Finset.add_subset_add (Finset.Subset.refl _) hTT'

theorem not_coverable_of_positive_holes {A : Finset G} {c : ℕ}
    (h : ∀ T : Finset G, T.card ≤ c → 0 < (holeSet A T).card) :
    ¬ coverable A c := by
  rintro ⟨T, hT, hcover⟩
  have hz := (holeSet_card_eq_zero_iff A T).2 hcover
  have hp := h T hT
  omega

theorem not_coverable_of_linear_holes {A : Finset G} {c : ℕ} {γ : ℝ}
    (hγ : 0 < γ)
    (h : ∀ T : Finset G, T.card ≤ c →
      γ * (Fintype.card G : ℝ) ≤ ((holeSet A T).card : ℝ)) :
    ¬ coverable A c := by
  apply not_coverable_of_positive_holes
  intro T hT
  have hcard : (0 : ℝ) < Fintype.card G := by
    exact_mod_cast (Fintype.card_pos : 0 < Fintype.card G)
  have hpos : (0 : ℝ) < (holeSet A T).card :=
    (mul_pos hγ hcard).trans_le (h T hT)
  exact_mod_cast hpos

theorem card_targets_for_source (A : Finset G) (t : G) :
    (Finset.univ.filter (fun x : G => x - t ∈ A)).card = A.card := by
  have hset : Finset.univ.filter (fun x : G => x - t ∈ A) =
      A.image (fun a => a + t) := by
    ext x
    simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_image]
    constructor
    · intro hx
      exact ⟨x - t, hx, sub_add_cancel x t⟩
    · rintro ⟨a, ha, rfl⟩
      simpa using ha
  rw [hset]
  exact Finset.card_image_of_injective _ (fun a b h => add_right_cancel h)

/-- The total representation mass is exact, without independence assumptions. -/
theorem sum_representationCount (A T : Finset G) :
    (∑ x : G, representationCount A T x) = A.card * T.card := by
  classical
  calc
    (∑ x : G, representationCount A T x) =
        ∑ x : G, ∑ t ∈ T, if x - t ∈ A then (1 : ℕ) else 0 := by
      simp only [representationCount, Finset.card_eq_sum_ones, Finset.sum_filter]
    _ = ∑ t ∈ T, ∑ x : G, if x - t ∈ A then (1 : ℕ) else 0 :=
      Finset.sum_comm
    _ = ∑ _t ∈ T, A.card := by
      apply Finset.sum_congr rfl
      intro t ht
      rw [← Finset.sum_filter]
      simpa using card_targets_for_source A t
    _ = A.card * T.card := by simp [Nat.mul_comm]

end Finite

end Green39Submission
end Green39AssemblyScope_e55302cfa6458e3c

/- Source: Green39Submission.FiniteProbability; SHA256 a0b1fb70f16e5ba336854516633dcb7728e2957fcf2ee07e357f71d75fc10115 -/
section Green39AssemblyScope_610abb236bf2a449
                                    
                     

/-!
Exact finite probability and expectation.

All results here are finite count identities or elementary inequalities. The
principal zero-limit theorem is neither assumed nor proved in this module.
This module is independent of the native conjecture and target bridge.
-/

namespace Green39Submission

open scoped BigOperators Pointwise

universe u v

variable {α : Type u} {ι : Type v}

/-- Count form with any supplied decidability instance. -/
theorem uniformProb_eq_card_filter (sample : Finset α) (event : α → Prop)
    [DecidablePred event] :
    uniformProb sample event = ((sample.filter event).card : ℝ) / (sample.card : ℝ) := by
  unfold uniformProb
  congr

theorem uniformProb_empty (event : α → Prop) :
    uniformProb (∅ : Finset α) event = 0 := by
  classical
  simp [uniformProb]

theorem uniformProb_false (sample : Finset α) :
    uniformProb sample (fun _ => False) = 0 := by
  classical
  simp [uniformProb]

theorem uniformProb_true (sample : Finset α) (hs : sample.Nonempty) :
    uniformProb sample (fun _ => True) = 1 := by
  classical
  have hc : (sample.card : ℝ) ≠ 0 := by
    exact_mod_cast hs.card_pos.ne'
  simp [uniformProb, hc]

theorem uniformProb_nonneg (sample : Finset α) (event : α → Prop) :
    0 ≤ uniformProb sample event := by
  classical
  unfold uniformProb
  positivity

theorem uniformProb_le_one (sample : Finset α) (event : α → Prop) :
    uniformProb sample event ≤ 1 := by
  classical
  by_cases hs : sample = ∅
  · simp [hs, uniformProb_empty]
  have hc : 0 < (sample.card : ℝ) := by
    exact_mod_cast (Finset.nonempty_iff_ne_empty.mpr hs).card_pos
  unfold uniformProb
  apply (div_le_one hc).2
  exact_mod_cast Finset.card_filter_le sample event

theorem uniformProb_congr (sample : Finset α) (P Q : α → Prop)
    (h : ∀ a ∈ sample, P a ↔ Q a) :
    uniformProb sample P = uniformProb sample Q := by
  classical
  have hf : sample.filter P = sample.filter Q := Finset.filter_congr h
  simp only [uniformProb, hf]

theorem uniformProb_mono (sample : Finset α) (P Q : α → Prop)
    (h : ∀ a ∈ sample, P a → Q a) :
    uniformProb sample P ≤ uniformProb sample Q := by
  classical
  have hf : sample.filter P ⊆ sample.filter Q := by
    intro a ha
    rcases Finset.mem_filter.mp ha with ⟨has, hPa⟩
    exact Finset.mem_filter.mpr ⟨has, h a has hPa⟩
  unfold uniformProb
  apply div_le_div_of_nonneg_right _ (Nat.cast_nonneg sample.card)
  exact_mod_cast Finset.card_le_card hf

theorem uniformProb_or_le (sample : Finset α) (P Q : α → Prop) :
    uniformProb sample (fun a => P a ∨ Q a) ≤
      uniformProb sample P + uniformProb sample Q := by
  classical
  have hf : sample.filter (fun a => P a ∨ Q a) ⊆
      sample.filter P ∪ sample.filter Q := by
    intro a ha
    rcases Finset.mem_filter.mp ha with ⟨has, hPa | hQa⟩
    · exact Finset.mem_union_left _ (Finset.mem_filter.mpr ⟨has, hPa⟩)
    · exact Finset.mem_union_right _ (Finset.mem_filter.mpr ⟨has, hQa⟩)
  have hc : (sample.filter (fun a => P a ∨ Q a)).card ≤
      (sample.filter P).card + (sample.filter Q).card :=
    (Finset.card_le_card hf).trans (Finset.card_union_le _ _)
  have hcr : ((sample.filter (fun a => P a ∨ Q a)).card : ℝ) ≤
      ((sample.filter P).card : ℝ) + ((sample.filter Q).card : ℝ) := by
    exact_mod_cast hc
  simp only [uniformProb_eq_card_filter, ← add_div]
  apply div_le_div_of_nonneg_right _ (Nat.cast_nonneg sample.card)
  convert hcr using 1 <;> congr

theorem uniformProb_union_le (sample : Finset α) (P Q : α → Prop) :
    uniformProb sample (fun a => P a ∨ Q a) ≤
      uniformProb sample P + uniformProb sample Q :=
  uniformProb_or_le sample P Q

theorem uniformProb_exists_mem_le_sum (sample : Finset α) (I : Finset ι)
    (event : ι → α → Prop) :
    uniformProb sample (fun a => ∃ i ∈ I, event i a) ≤
      ∑ i ∈ I, uniformProb sample (event i) := by
  classical
  induction I using Finset.induction_on with
  | empty => simp [uniformProb]
  | @insert i I hi ih =>
      calc
        uniformProb sample (fun a => ∃ j ∈ insert i I, event j a) =
            uniformProb sample (fun a => event i a ∨ ∃ j ∈ I, event j a) := by
              apply uniformProb_congr
              intro a ha
              simp
        _ ≤ uniformProb sample (event i) +
            uniformProb sample (fun a => ∃ j ∈ I, event j a) :=
              uniformProb_or_le _ _ _
        _ ≤ uniformProb sample (event i) +
            ∑ j ∈ I, uniformProb sample (event j) := add_le_add le_rfl ih
        _ = ∑ j ∈ insert i I, uniformProb sample (event j) := by simp [hi]

theorem uniformProb_add_not (sample : Finset α) (P : α → Prop)
    (hs : sample.Nonempty) :
    uniformProb sample P + uniformProb sample (fun a => ¬ P a) = 1 := by
  classical
  have hc : (sample.card : ℝ) ≠ 0 := by
    exact_mod_cast hs.card_pos.ne'
  unfold uniformProb
  rw [← add_div, ← Nat.cast_add, Finset.card_filter_add_card_filter_not, div_self hc]

theorem uniformProb_not (sample : Finset α) (P : α → Prop)
    (hs : sample.Nonempty) :
    uniformProb sample (fun a => ¬ P a) = 1 - uniformProb sample P := by
  have h := uniformProb_add_not sample P hs
  linarith

theorem uniformMean_empty (f : α → ℝ) :
    uniformMean (∅ : Finset α) f = 0 := by
  simp [uniformMean]

theorem uniformMean_zero (sample : Finset α) :
    uniformMean sample (fun _ => 0) = 0 := by
  simp [uniformMean]

theorem uniformMean_nonneg (sample : Finset α) (f : α → ℝ)
    (hf : ∀ a ∈ sample, 0 ≤ f a) :
    0 ≤ uniformMean sample f := by
  unfold uniformMean
  exact div_nonneg (Finset.sum_nonneg hf) (Nat.cast_nonneg sample.card)

theorem uniformMean_mono (sample : Finset α) (f g : α → ℝ)
    (hfg : ∀ a ∈ sample, f a ≤ g a) :
    uniformMean sample f ≤ uniformMean sample g := by
  unfold uniformMean
  exact div_le_div_of_nonneg_right (Finset.sum_le_sum hfg) (Nat.cast_nonneg sample.card)

theorem uniformMean_add (sample : Finset α) (f g : α → ℝ) :
    uniformMean sample (fun a => f a + g a) =
      uniformMean sample f + uniformMean sample g := by
  simp only [uniformMean, Finset.sum_add_distrib, add_div]

theorem uniformMean_const_mul (sample : Finset α) (c : ℝ) (f : α → ℝ) :
    uniformMean sample (fun a => c * f a) = c * uniformMean sample f := by
  unfold uniformMean
  rw [← Finset.mul_sum, mul_div_assoc]

theorem uniformMean_const (sample : Finset α) (hs : sample.Nonempty) (c : ℝ) :
    uniformMean sample (fun _ => c) = c := by
  have hc : (sample.card : ℝ) ≠ 0 := by
    exact_mod_cast hs.card_pos.ne'
  simp [uniformMean, nsmul_eq_mul, hc]

theorem uniformProb_eq_uniformMean_indicator (sample : Finset α) (event : α → Prop)
    [DecidablePred event] :
    uniformProb sample event = uniformMean sample (fun a => if event a then 1 else 0) := by
  classical
  simp [uniformProb, uniformMean]
  congr

theorem uniformMean_sum (sample : Finset α) (I : Finset ι) (f : ι → α → ℝ) :
    uniformMean sample (fun a => ∑ i ∈ I, f i a) =
      ∑ i ∈ I, uniformMean sample (f i) := by
  simp only [uniformMean, ← Finset.sum_div]
  rw [Finset.sum_comm]

/-- Finite Markov inequality before division by the threshold. -/
theorem uniformProb_mul_le_uniformMean_of_nonneg (sample : Finset α)
    (f : α → ℝ) (t : ℝ) (hf : ∀ a ∈ sample, 0 ≤ f a) (_ht : 0 ≤ t) :
    t * uniformProb sample (fun a => t ≤ f a) ≤ uniformMean sample f := by
  classical
  have hsum : (∑ a ∈ sample, if t ≤ f a then t else 0) ≤ ∑ a ∈ sample, f a := by
    apply Finset.sum_le_sum
    intro a ha
    split_ifs with hta
    · exact hta
    · exact hf a ha
  have hi : (∑ a ∈ sample, if t ≤ f a then t else 0) =
      t * ((sample.filter (fun a => t ≤ f a)).card : ℝ) := by
    rw [← Finset.sum_filter]
    simp [mul_comm]
  rw [hi] at hsum
  unfold uniformProb uniformMean
  rw [← mul_div_assoc]
  exact div_le_div_of_nonneg_right hsum (Nat.cast_nonneg sample.card)

theorem uniformProb_le_uniformMean_div (sample : Finset α)
    (f : α → ℝ) (t : ℝ) (hf : ∀ a ∈ sample, 0 ≤ f a) (ht : 0 < t) :
    uniformProb sample (fun a => t ≤ f a) ≤ uniformMean sample f / t := by