MarkedPivotFiniteOrder.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact finite interleavings for the source-level marked-pivot family

This bridge applies directly to the finite-old specification, including an empty label type. It does not extend an old list to an infinite sequence.

lemma OAI.MatroidProphet.MarkedPivots.firstSpans_orderPosition_iff line 17
lemma OAI.MatroidProphet.MarkedPivots.records_orderPosition_iff line 24
lemma OAI.MatroidProphet.MarkedPivots.oldOrdered_orderPosition_iff line 32

theorem OAI.MatroidProphet.MarkedPivots.mem_patterns_iff_finite_order line 39

Source documentation

The source family is exactly the family obtained by permuting the finite occurrence set into its finite set of positions, keeping the old order. No inhabitedness or distinctness assumption on labels is needed.

theorem mem_patterns_iff_finite_order (M : Matroid α)
    (old : Fin r → α) (movable : Fin q → α) (test : Fin n → α)
    (oldMark : Fin r → Bool) (pattern : Finset (Fin n)) :
    pattern ∈ patterns M old movable test oldMark ↔
      ∃ position : Occurrences r q ≃ Fin (Fintype.card (Occurrences r q)),
        OldOrdered (fun o => (position o).val) ∧
          ∃ movableMark : Fin q → Bool,
            Records M old movable test (fun o => (position o).val)
              oldMark movableMark pattern := by
…

Mentions: OAI.MatroidProphet.MarkedPivots.patterns, OAI.MatroidProphet.MarkedPivots.Occurrences, OAI.MatroidProphet.MarkedPivots.OldOrdered, OAI.MatroidProphet.MarkedPivots.Records