CandidateContracts.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Source-facing contracts for the candidate filter (setup.tex, Lemma lem:filter). The sets below are the actual rounded-priority greedy survivors and candidate labels, not arbitrary sets satisfying a desired inequality. The fair-mask law is the concrete product law bitsExpectation on the entire labeled ground set.

theorem OAI.MatroidProphet.CandidateContracts.candidate_mass line 19
Source documentation
The full candidate-mass contract, including pointwise independence and containment for every mask. No positivity premise is needed here because the rounding map itself discards nonpositive coordinates.
```
theorem candidate_mass {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (w : Weights n) :
    let a := fun e => roundedLevel weightBase (w e)
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.roundedLevel, OAI.MatroidProphet.weightBase
theorem OAI.MatroidProphet.CandidateContracts.rounding_and_greedy line 42
Source documentation
Both inequalities of the source's rounding bound, together with an actual independent positive-priority greedy maximizer. This includes zero weights, loops, ties, the empty ground set, and rank zero.
```
theorem rounding_and_greedy {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (w : Weights n) (hw : ∀ e, 0 ≤ w e) :
    let u := fun e => roundedWeight weightBase (w e)
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.roundedWeight, OAI.MatroidProphet.weightBase
theorem OAI.MatroidProphet.CandidateContracts.candidate_positive_nonloop line 63
Source documentation
The actual candidate predicate never includes a loop or a nonpositive label. This is a pointwise statement for every mask, not only almost surely.
```
theorem candidate_positive_nonloop {n : ℕ} (M : Matroid (Fin n))
    (w : Weights n) (H : Finset (Fin n)) (e : Fin n)
    (he : e ∈ candidateLabels M (fun f => roundedLevel weightBase (w f)) H) :
    0 < w e ∧ e ∉ H ∧ e ∉ M.closure ∅ := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.roundedLevel, OAI.MatroidProphet.weightBase