TransferContract.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Source-facing sample-to-rank transfer

Source: sections/transfer.tex, lem:transfer / eq:rank-transfer. The comparison set is the actual priority-greedy survivor group; its independence and containment are proved, not supplied as extra assumptions. mainMean fixes only H and averages the density, guard, test, and parity coins. trueZ uses zero on unlisted outcomes, so the expectation is not conditioned on listing.

lemma OAI.MatroidProphet.SourceProof.mainMean_filter_congr line 22
Source documentation
Conditional averaging depends on the fixed filter mask only. All other fields of the initial record are overwritten by independent product samples.
```
lemma mainMean_filter_congr {n : ℕ} (d d' : MainMasks n)
    (hH : d.H = d'.H) (f : MainMasks n → ℝ) : mainMean d f = mainMean d' f := by
…
```
Mentions: OAI.MatroidProphet.MainMasks

lemma OAI.MatroidProphet.SourceProof.trueZ_unlisted line 31

Source documentation

The unlisted branch is included in the product average with zero statistic.

lemma trueZ_unlisted {n : ℕ} (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (d : MainMasks n) (s : Fin n → Option ℤ) (i : ℤ)
    (hi : i ∉ groups M d s) : trueZ M hE d s i = 0 := by
…

Mentions: OAI.MatroidProphet.MainMasks

lemma OAI.MatroidProphet.SourceProof.trueZ_zero_of_no_discovery line 39
Source documentation
In particular, a true group missed by the discovery sample contributes zero; no positivity or listing assumption is imposed on the individual outcomes.
```
lemma trueZ_zero_of_no_discovery {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (d : MainMasks n) (s : Fin n → Option ℤ) (i : ℤ)
    (hmiss : d.D ∩ trueGroup M d s i = ∅) : trueZ M hE d s i = 0 := by
…
```
Mentions: OAI.MatroidProphet.MainMasks
theorem OAI.MatroidProphet.SourceProof.transfer_keys line 51
Source documentation
The source transfer at arbitrary rounded-level keys. This stronger helper also covers the none keys representing zero/nonpositive weights.
```
theorem transfer_keys {n : ℕ} (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (s : Fin n → Option ℤ) (H : Finset (Fin n)) (i : ℤ) :
    let d : MainMasks n := ⟨H, ∅, ∅, ∅, false⟩
…
```
Mentions: OAI.MatroidProphet.MainMasks
theorem OAI.MatroidProphet.SourceProof.transfer line 77
Source documentation
lem:transfer for the manuscript's actual rounded nonnegative weights, with literal constants gamma = 2^-16 and kappa = 2^100.
```
theorem transfer {n : ℕ} (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (w : Weights n) (_hw : ∀ e, 0 ≤ w e) (H : Finset (Fin n)) (i : ℤ) :
    let s : Fin n → Option ℤ := fun e => roundedLevel weightBase (w e)
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.roundedLevel, OAI.MatroidProphet.weightBase
theorem OAI.MatroidProphet.SourceProof.transfer_claim line 89
Source documentation
Thin proof alias for the independent root-target specification.
```
theorem transfer_claim : TransferClaim := by
…
```
Mentions: OAI.MatroidProphet.TransferClaim