DegenerateCases.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Degenerate inputs and loop coordinates

These lemmas concern the actual optimum and online execution, not a surrogate benchmark. They make explicit the empty-ground, all-loop, zero-optimum and fully-sacrificed cases admitted by setup.tex and secretary.tex. In particular, no moment or boundedness hypothesis on a loop coordinate is needed for OPT.

theorem OAI.MatroidProphet.DegenerateCases.optimum_congr_on_nonloops line 20
Source documentation
Offline optimization is unaffected by any change in loop coordinates.
```
theorem optimum_congr_on_nonloops {n : ℕ} (M : Matroid (Fin n))
    (v w : Weights n) (h : ∀ e, M.IsNonloop e → v e = w e) :
    optimum M v = optimum M w := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.DegenerateCases.optimum_zero line 34
Source documentation
Zero weights have zero optimum, without a full-ground assumption.
```
theorem optimum_zero {n : ℕ} (M : Matroid (Fin n)) :
    optimum M (fun _ => 0) = 0 := by
…
```
Mentions: OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.DegenerateCases.optimum_eq_zero_of_nonloops_zero line 41
Source documentation
If every nonloop has zero weight, arbitrary loop weights do not affect OPT.
```
theorem optimum_eq_zero_of_nonloops_zero {n : ℕ} (M : Matroid (Fin n))
    (w : Weights n) (hw : ∀ e, M.IsNonloop e → w e = 0) :
    optimum M w = 0 := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.DegenerateCases.optimum_eq_zero_of_all_loops line 47
Source documentation
The all-loop case includes arbitrarily large and arbitrary-sign loop weights.
```
theorem optimum_eq_zero_of_all_loops {n : ℕ} (M : Matroid (Fin n))
    (hM : ∀ e, M.IsLoop e) (w : Weights n) : optimum M w = 0 := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.DegenerateCases.optimum_empty line 54
Source documentation
No labels is a valid input, and its actual offline optimum is zero.
```
theorem optimum_empty (M : Matroid (Fin 0)) (w : Weights 0) :
    optimum M w = 0 := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.DegenerateCases.nonloop_weight_le_optimum line 61
Source documentation
A nonloop singleton is one of the sets in the optimization benchmark.
```
theorem nonloop_weight_le_optimum {n : ℕ} (M : Matroid (Fin n))
    (w : Weights n) (e : Fin n) (he : M.IsNonloop e) :
    w e ≤ optimum M w := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.DegenerateCases.optimum_eq_zero_iff line 67
Source documentation
On nonnegative vectors, OPT vanishes exactly when every nonloop weight does.
```
theorem optimum_eq_zero_iff {n : ℕ} (M : Matroid (Fin n))
    (w : Weights n) (hw : ∀ e, 0 ≤ w e) :
    optimum M w = 0 ↔ ∀ e, M.IsNonloop e → w e = 0 := by
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.optimum
theorem OAI.MatroidProphet.DegenerateCases.reward_eq_zero_of_optimum_eq_zero line 76
Source documentation
Every feasible rule has exactly zero reward on a zero-OPT input.
```
theorem reward_eq_zero_of_optimum_eq_zero {n bits : ℕ}
    (M : Matroid (Fin n)) (A : OnlineRule n bits) (hA : Feasible M A)
    (r : Seed bits) (s v : Weights n) (π : ArrivalOrder n)
    (hs : ∀ e, 0 ≤ s e) (hv : ∀ e, 0 ≤ v e) (hopt : optimum M v = 0) :
    reward A r s v π = 0 := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Feasible, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.optimum, OAI.MatroidProphet.reward
theorem OAI.MatroidProphet.DegenerateCases.acceptedThrough_stabilizes line 86
Source documentation
Running past the finite final arrival does not create any further decisions.
```
theorem acceptedThrough_stabilizes {n bits : ℕ} (A : OnlineRule n bits)
    (r : Seed bits) (s v : Weights n) (π : ArrivalOrder n)
    (t : ℕ) (ht : n ≤ t) :
    acceptedThrough A r s v π t = accepted A r s v π := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.acceptedThrough, OAI.MatroidProphet.accepted
theorem OAI.MatroidProphet.DegenerateCases.acceptedThrough_zero line 96
Source documentation
The empty prefix never accepts anything, regardless of the rule.
```
theorem acceptedThrough_zero {n bits : ℕ} (A : OnlineRule n bits)
    (r : Seed bits) (s v : Weights n) (π : ArrivalOrder n) :
    acceptedThrough A r s v π 0 = ∅ := by
…
```
Mentions: OAI.MatroidProphet.OnlineRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.acceptedThrough
theorem OAI.MatroidProphet.DegenerateCases.hiddenAcceptedThrough_eq_empty_of_full_mask line 103
Source documentation
Fully revealed hidden-vector inputs are fully sacrificed, at every prefix.
```
theorem hiddenAcceptedThrough_eq_empty_of_full_mask {n bits : ℕ}
    (A : HiddenRule n bits) (r : Seed bits) (hmask : A.mask r = Finset.univ)
    (w : Weights n) (π : ArrivalOrder n) (t : ℕ) :
    hiddenAcceptedThrough A r w π t = ∅ := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough
theorem OAI.MatroidProphet.DegenerateCases.hiddenReward_eq_zero_of_full_mask line 110
Source documentation
Full sacrifice gives zero reward for every order, including the empty order.
```
theorem hiddenReward_eq_zero_of_full_mask {n bits : ℕ}
    (A : HiddenRule n bits) (r : Seed bits) (hmask : A.mask r = Finset.univ)
    (w : Weights n) (π : ArrivalOrder n) : hiddenReward A r w π = 0 := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenReward
theorem OAI.MatroidProphet.DegenerateCases.hiddenWorstReward_eq_zero_of_full_mask line 116
Source documentation
The seed-wise adversarial minimum also vanishes under full sacrifice.
```
theorem hiddenWorstReward_eq_zero_of_full_mask {n bits : ℕ}
    (A : HiddenRule n bits) (r : Seed bits) (hmask : A.mask r = Finset.univ)
    (w : Weights n) : hiddenWorstReward A w r = 0 := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.hiddenWorstReward