WitnessCover.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

A common hybrid containing a private-prime witness family

The product over all witness tests is expanded only to prove existence. No cardinality of that powerset is charged in an estimate. An omitted coordinate annihilates the full mixed difference; a surviving term must therefore cover every singleton coordinate in one common hybrid.

def OAI.TwoPointCorrelations.DependsOn line 22
Source documentation
A test depends only on the listed coordinates of the same configuration.
```
def DependsOn (support : Finset ι) (F : (ι → A) → Bool) : Prop :=
…
```
def OAI.TwoPointCorrelations.witnessIntersection line 25
def OAI.TwoPointCorrelations.witnessAvoidance line 28
def OAI.TwoPointCorrelations.witnessSupport line 31
lemma OAI.TwoPointCorrelations.mixedDifference_sum line 35
lemma OAI.TwoPointCorrelations.mixedDifference_const_mul line 41
lemma OAI.TwoPointCorrelations.mixedDifference_eq_zero_of_ignores line 51
Source documentation
If one coordinate is irrelevant, its forced-minus-original difference cancels exactly, regardless of the values of the other coordinates.
```
lemma mixedDifference_eq_zero_of_ignores (a : ι → A) (F : (ι → A) → ℝ) (x : ι → A)
    (i : ι) (hF : ∀ u v, (∀ j, j ≠ i → u j = v j) → F u = F v) :
    mixedDifference a F x = 0 := by
…
```
Mentions: OAI.TwoPointCorrelations.mixedDifference
lemma OAI.TwoPointCorrelations.witnessAvoidance_expansion line 74
lemma OAI.TwoPointCorrelations.witnessIntersection_ignores line 82
theorem OAI.TwoPointCorrelations.mixedDifference_common_cover line 99
Source documentation
A nonzero full mixed difference of the avoidance event forces a family covering all singleton coordinates, positive in one common hybrid.
```
theorem mixedDifference_common_cover (support : W → Finset ι) (I : W → (ι → A) → Bool)
    (hdepends : ∀ w, DependsOn (support w) (I w)) (a x : ι → A)
    (hnonzero : mixedDifference a (witnessAvoidance I) x ≠ 0) :
    ∃ S : Finset W, witnessSupport support S = Finset.univ ∧
      ∃ H : Finset ι, ∀ w ∈ S, I w (forceCoordinates H a x) = true := by
…
```
Mentions: OAI.TwoPointCorrelations.DependsOn, OAI.TwoPointCorrelations.mixedDifference, OAI.TwoPointCorrelations.witnessAvoidance, OAI.TwoPointCorrelations.witnessSupport, OAI.TwoPointCorrelations.forceCoordinates

theorem OAI.TwoPointCorrelations.exists_private_subcover line 137

Source documentation

An inclusion-minimal finite cover has a private coordinate in every member, and bounded support sizes bound its cardinality from below.

theorem exists_private_subcover (support : W → Finset ι) (S : Finset W)
    (hS : witnessSupport support S = Finset.univ) (B : ℕ)
    (hB : ∀ w ∈ S, (support w).card ≤ B) :
    ∃ R ⊆ S, witnessSupport support R = Finset.univ ∧
      Fintype.card ι ≤ R.card * B ∧
      ∀ w ∈ R, ∃ i ∈ support w, ∀ v ∈ R, v ≠ w → i ∉ support v := by
…

Mentions: OAI.TwoPointCorrelations.witnessSupport

theorem OAI.TwoPointCorrelations.mixedDifference_private_witnesses line 177

Source documentation

Finite-parameter witness cover: enough singleton coordinates compared with the maximum witness support yields T simultaneous witnesses with pairwise distinct private marked coordinates.

theorem mixedDifference_private_witnesses (support : W → Finset ι) (I : W → (ι → A) → Bool)
    (hdepends : ∀ w, DependsOn (support w) (I w)) (a x : ι → A)
    (hnonzero : mixedDifference a (witnessAvoidance I) x ≠ 0)
    (B T : ℕ) (hB : ∀ w, (support w).card ≤ B) (hT : T * B < Fintype.card ι) :
    ∃ R : Finset W, R.card = T ∧ ∃ H : Finset ι,
      (∀ w ∈ R, I w (forceCoordinates H a x) = true) ∧
      ∃ mark : R → ι, Function.Injective mark ∧
        ∀ w : R, mark w ∈ support w ∧ ∀ v ∈ R, v ≠ w → mark w ∉ support v := by
…

Mentions: OAI.TwoPointCorrelations.DependsOn, OAI.TwoPointCorrelations.mixedDifference, OAI.TwoPointCorrelations.witnessAvoidance, OAI.TwoPointCorrelations.forceCoordinates