FeasibilityContract.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Complete source contract for algorithm.tex, lem:feasibility (lines 179--183; source SHA256 b702fa1da832d3cbebcf5a70f0b0e9505b3423e2ed9884c22fe4194ba4974fbe). The actual main rule is used, not an abstract feasible-rule hypothesis.

theorem OAI.MatroidProphet.FeasibilityContract.observed_eq_of_eq_on_mask line 17
Source documentation
Hidden observations depend only on the initially sacrificed coordinates.
```
theorem observed_eq_of_eq_on_mask {n bits : ℕ} (A : HiddenRule n bits)
    (r : Seed bits) (w w' : Weights n)
    (h : ∀ e ∈ A.mask r, w e = w' e) :
    observed A r w = observed A r w' := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.observed
theorem OAI.MatroidProphet.FeasibilityContract.hidden_decision_congr line 29
Source documentation
Hidden execution is nonanticipating: equal initial observations and equal revealed histories force equal current decisions, irrespective of future data.
```
theorem hidden_decision_congr {n bits : ℕ} (A : HiddenRule n bits)
    (r : Seed bits) (w w' : Weights n) (π π' : ArrivalOrder n) (k : Fin n)
    (hmask : ∀ e ∈ A.mask r, w e = w' e)
    (hhist : history w π k = history w' π' k) :
    decisionAt A.core r (observed A r w) w π k =
      decisionAt A.core r (observed A r w') w' π' k := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.history, OAI.MatroidProphet.decisionAt, OAI.MatroidProphet.observed
theorem OAI.MatroidProphet.FeasibilityContract.hiddenAcceptedThrough_mono line 39
Source documentation
Sacrificing the fixed mask preserves irrevocability.
```
theorem hiddenAcceptedThrough_mono {n bits : ℕ} (A : HiddenRule n bits)
    (r : Seed bits) (w : Weights n) (π : ArrivalOrder n)
    {t t' : ℕ} (h : t ≤ t') :
    hiddenAcceptedThrough A r w π 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.FeasibilityContract.hiddenAcceptedThrough_disjoint_mask line 49
Source documentation
No sacrificed observation label is ever accepted.
```
theorem hiddenAcceptedThrough_disjoint_mask {n bits : ℕ} (A : HiddenRule n bits)
    (r : Seed bits) (w : Weights n) (π : ArrivalOrder n) (t : ℕ) :
    Disjoint (hiddenAcceptedThrough A r w π t) (A.mask r) := by
…
```
Mentions: OAI.MatroidProphet.HiddenRule, OAI.MatroidProphet.Seed, OAI.MatroidProphet.Weights, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough

theorem OAI.MatroidProphet.FeasibilityContract.main_rule line 59

Source documentation

All parts of the manuscript's feasibility and information contract for the actual layered main algorithm. Empty ground sets, loops, zero weights, ties, and empty group lists remain within the quantified input domain.

theorem main_rule {n : ℕ} (M : Matroid (Fin n)) (hE : M.E = Set.univ) :
    (∀ (w : Weights n), (∀ e, 0 ≤ w e) →
      ∀ (r : Seed (mainSeedBits n)) (π : ArrivalOrder n) (t : ℕ),
        M.Indep (hiddenAcceptedThrough (MainAlgorithm.hidden M hE) r w π t : Set (Fin n))) ∧
    (∀ k, Measurable
      (fun x : Seed (mainSeedBits n) × (Weights n × History n k) =>
        (MainAlgorithm.core M hE).decide k x.1 x.2.1 x.2.2)) ∧
    (∀ (r : Seed (mainSeedBits n)) (w w' : Weights n)
      (π π' : ArrivalOrder n) (k : Fin n),
      (∀ e ∈ (MainAlgorithm.hidden M hE).mask r, w e = w' e) →
      history w π k = history w' π' k →
      decisionAt (MainAlgorithm.core M hE) r
…

Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough, OAI.MatroidProphet.MainAlgorithm.hidden, OAI.MatroidProphet.History, OAI.MatroidProphet.MainAlgorithm.core, OAI.MatroidProphet.history, OAI.MatroidProphet.decisionAt

theorem OAI.MatroidProphet.FeasibilityContract.assign_none_of_groups_nil line 89
Source documentation
The empty listed-group case cannot assign any arriving label to a layer.
```
theorem assign_none_of_groups_nil {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (d : MainMasks n) (seen : Fin n → Option ℤ)
    (hg : MainAlgorithm.groups M d seen = []) (e : Fin n) (w : Option ℤ) :
    MainAlgorithm.assign M hE d seen e w = none := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.groups, OAI.MatroidProphet.MainAlgorithm.assign
theorem OAI.MatroidProphet.FeasibilityContract.assign_zero line 103
Source documentation
Zero weights do not enter a logarithm and are assigned no layer.
```
theorem assign_zero {n : ℕ} (M : Matroid (Fin n)) (hE : M.E = Set.univ)
    (d : MainMasks n) (seen : Fin n → Option ℤ) (e : Fin n) :
    MainAlgorithm.assign M hE d seen e (roundedLevel weightBase 0) = none := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.assign, OAI.MatroidProphet.roundedLevel, OAI.MatroidProphet.weightBase
theorem OAI.MatroidProphet.FeasibilityContract.not_candidate_of_loop line 109
Source documentation
A loop can never pass the actual candidate test, regardless of priorities.
```
theorem not_candidate_of_loop {n : ℕ} (M : Matroid (Fin n)) (d : MainMasks n)
    (seen : Fin n → Option ℤ) (e : Fin n) (w : Option ℤ)
    (he : e ∈ M.closure ∅) : ¬ MainAlgorithm.candidate M d seen e w := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.candidate
theorem OAI.MatroidProphet.FeasibilityContract.source_main_feasibility line 116
Source documentation
The complete required lem:feasibility contract, for the concrete source rule.
```
theorem source_main_feasibility {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) : MainRuleFeasibility M (MainAlgorithm.hidden M hE) :=
…
```
Mentions: OAI.MatroidProphet.MainRuleFeasibility, OAI.MatroidProphet.MainAlgorithm.hidden