MainFeasibilityContract.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Source-facing feasibility and information contract

Pinned source: sections/algorithm.tex, Lemma lem:feasibility, lines 179–204. The rule here is the actual main rule, not an abstract feasible substitute. The first component gives prefix feasibility. The remaining components make measurability, the permitted observations, irrevocability, and sacrifice explicit. None of these components assumes a source theorem or any algorithm-validity axiom.

theorem OAI.MatroidProphet.MainAlgorithm.source_feasibility_contract line 20

Source documentation

Full feasibility/information content of the manuscript's main-rule lemma.

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

Mentions: OAI.MatroidProphet.Feasible, OAI.MatroidProphet.MainAlgorithm.core, OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.Weights, OAI.MatroidProphet.History, OAI.MatroidProphet.MainAlgorithm.hidden, OAI.MatroidProphet.observed, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough

theorem OAI.MatroidProphet.MainAlgorithm.source_accepted_isNonloop line 49
Source documentation
Loops are never selected, including when their weights have no moment bound.
```
theorem source_accepted_isNonloop {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (w : Weights n) (hw : ∀ e, 0 ≤ w e)
    (r : Seed (mainSeedBits n)) (π : ArrivalOrder n) (t : ℕ) (e : Fin n)
    (he : e ∈ hiddenAcceptedThrough (hidden M hE) r w π t) :
    M.IsNonloop e :=
…
```
Mentions: OAI.MatroidProphet.Weights, OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.ArrivalOrder, OAI.MatroidProphet.hiddenAcceptedThrough, OAI.MatroidProphet.MainAlgorithm.hidden
theorem OAI.MatroidProphet.MainAlgorithm.source_observation_mask line 57
Source documentation
The disclosed mask is determined by the initial seed, with no weight input.
```
theorem source_observation_mask {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (r : Seed (mainSeedBits n)) :
    (hidden M hE).mask r = (mainMasks r).H ∪ (mainMasks r).D ∪ (mainMasks r).C := rfl
```
Mentions: OAI.MatroidProphet.Seed, OAI.MatroidProphet.mainSeedBits, OAI.MatroidProphet.MainAlgorithm.hidden, OAI.MatroidProphet.mainMasks
theorem OAI.MatroidProphet.MainAlgorithm.source_loop_not_candidate line 62
Source documentation
Loops fail the candidate test before the layer selection is attempted.
```
theorem source_loop_not_candidate {n : ℕ} (M : Matroid (Fin n))
    (d : MainMasks n) (seen : Fin n → Option ℤ) (e : Fin n) (level : Option ℤ)
    (he : e ∈ M.closure ∅) : ¬ candidate M d seen e level := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.candidate
theorem OAI.MatroidProphet.MainAlgorithm.source_nonpositive_unassigned line 69
Source documentation
Zero (and negative off-domain) values never receive an eligible layer.
```
theorem source_nonpositive_unassigned {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (d : MainMasks n) (seen : Fin n → Option ℤ)
    (e : Fin n) (x : ℝ) (hx : x ≤ 0) :
    assign M hE d seen e (roundedLevel weightBase x) = none := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.assign, OAI.MatroidProphet.roundedLevel, OAI.MatroidProphet.weightBase
theorem OAI.MatroidProphet.MainAlgorithm.source_empty_groups_unassigned line 76
Source documentation
An empty listed-group collection assigns no arriving value to a layer.
```
theorem source_empty_groups_unassigned {n : ℕ} (M : Matroid (Fin n))
    (hE : M.E = Set.univ) (d : MainMasks n) (seen : Fin n → Option ℤ)
    (hg : groups M d seen = []) (e : Fin n) (level : Option ℤ) :
    assign M hE d seen e level = none := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.groups, OAI.MatroidProphet.MainAlgorithm.assign