ResidualFamilyContract.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Every witness residual belongs to one family fixed before the focal masks

This strengthens the existential residual used in the inherited payoff proof to cover every system of witnesses, as required by lem:pattern-family in the pinned manuscript. The family is defined from the reference incoming path and lower-group competition, not from the focal density, guard, or test bits.

theorem OAI.MatroidProphet.nominalResidualSet_mem_labeledFamily line 22

Source documentation

All witness choices with the stated total budget are captured. No canonical choice of basis, and no independence of the selected residual, is assumed.

theorem nominalResidualSet_mem_labeledFamily
    (M : Matroid α) (hE : M.E = Set.univ) (κ : ℕ) (hκ : 0 < κ)
    (D C T : ℕ → Set α) (h : ℕ) (U : Finset α)
    (hDU : D h ⊆ (U : Set α)) (hnonloop : ∀ e ∈ U, e ∉ M.closure ∅)
    (ε : Fin 2) (W : ParityWindow (activation h) ε → Set α)
    (hW : ∀ b, W b ⊆ nominalLayerSet M hE κ D C h (U : Set α) ε b)
    (hsum : (∑ b, (W b).ncard) ≤ U.card / κ) :
    (Set.toFinite (nominalResidualSet M hE κ D C T h (U : Set α) ε W)).toFinset ∈
      labeledResidualFamily M U κ (guardedPath M hE κ D C h) (activation h) ε
        (fun b => lowerCompetition M hE κ D C T b.val.val h) := by
…

Mentions: OAI.MatroidProphet.activation, OAI.MatroidProphet.nominalLayerSet, OAI.MatroidProphet.nominalResidualSet, OAI.MatroidProphet.labeledResidualFamily, OAI.MatroidProphet.guardedPath, OAI.MatroidProphet.lowerCompetition

theorem OAI.MatroidProphet.MainAlgorithm.focalResidualFamily_captures_all line 62

Source documentation

Holding the outside coordinates fixed, the same family captures every focal mask outcome and every small-budget witness system on that outcome.

theorem focalResidualFamily_captures_all
    (M : Matroid (Fin n)) (hE : M.E = Set.univ) (κ : ℕ) (hκ : 0 < κ)
    (d : MainMasks n) (s : Fin n → Option ℤ) (i : ℤ) (ε : Fin 2)
    (A B C : Finset (Fin n))
    (hA : A ⊆ trueGroup M d s i) (hB : B ⊆ trueGroup M d s i)
    (hC : C ⊆ trueGroup M d s i) (hne : A.Nonempty) :
    let U := trueGroup M d s i
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.trueGroup

theorem OAI.MatroidProphet.MainAlgorithm.uniform_residual_family line 99

Source documentation

The complete uniform-family conclusion of lem:pattern-family. The existential family precedes all three focal masks, including the test mask. The witness hypotheses are weaker than the manuscript's rank-witness conditions: only layer membership and the total cardinality budget are needed for capture.

theorem uniform_residual_family
    (M : Matroid (Fin n)) (hE : M.E = Set.univ) (κ : ℕ) (hκ : 2 ≤ κ)
    (d : MainMasks n) (s : Fin n → Option ℤ) (i : ℤ)
    (hsize : κ ≤ (trueGroup M d s i).card) (ε : Fin 2) :
    ∃ family : Finset (Finset (Fin n)),
      (∀ R ∈ family, R ⊆ trueGroup M d s i) ∧
      (family.card : ℝ) ≤ Real.exp
        (1000 * Real.log (κ : ℝ) / (κ : ℝ) * (trueGroup M d s i).card) ∧
      ∀ (A B C : Finset (Fin n)),
        A ⊆ trueGroup M d s i → B ⊆ trueGroup M d s i →
        C ⊆ trueGroup M d s i → A.Nonempty →
        let U := trueGroup M d s i
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.trueGroup

theorem OAI.MatroidProphet.MainAlgorithm.focalReference_focalMasks_invariant line 137
Source documentation
Replacing focal coordinates does not change the reference masks. This makes mask-independence explicit rather than relying only on an existential family.
```
theorem focalReference_focalMasks_invariant
    (M : Matroid (Fin n)) (d : MainMasks n) (s : Fin n → Option ℤ) (i : ℤ)
    (A B C : Finset (Fin n))
    (hA : A ⊆ trueGroup M d s i) (hB : B ⊆ trueGroup M d s i)
    (hC : C ⊆ trueGroup M d s i) :
    focalReference M (focalMasks d (trueGroup M d s i) A B C) s i =
      focalReference M d s i := by
…
```
Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.trueGroup, OAI.MatroidProphet.MainAlgorithm.focalReference, OAI.MatroidProphet.MainAlgorithm.focalMasks
theorem OAI.MatroidProphet.MainAlgorithm.focalIndex_focalMasks_invariant line 155

theorem OAI.MatroidProphet.MainAlgorithm.focalResidualFamily_focalMasks_invariant line 166

Source documentation

The actual family is unchanged by all focal density, guard, and test bits, including outcomes in which the focal group is not listed.

theorem focalResidualFamily_focalMasks_invariant
    (M : Matroid (Fin n)) (hE : M.E = Set.univ) (κ : ℕ)
    (d : MainMasks n) (s : Fin n → Option ℤ) (i : ℤ) (ε : Fin 2)
    (A B C : Finset (Fin n))
    (hA : A ⊆ trueGroup M d s i) (hB : B ⊆ trueGroup M d s i)
    (hC : C ⊆ trueGroup M d s i) :
    focalResidualFamily M hE κ (focalMasks d (trueGroup M d s i) A B C) s i ε =
      focalResidualFamily M hE κ d s i ε := by
…

Mentions: OAI.MatroidProphet.MainMasks, OAI.MatroidProphet.MainAlgorithm.trueGroup, OAI.MatroidProphet.MainAlgorithm.focalResidualFamily, OAI.MatroidProphet.MainAlgorithm.focalMasks