PivotOrderInvariance.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Timestamp representations of finite insertion orders

The marked-pivot proof uses injective natural-number timestamps, whereas the manuscript speaks about positions in a finite interleaving. We prove that timestamps can be normalized to a permutation of the finite position set without changing any prefix, first-spanning pivot, or recorded mark vector. No bound on gaps between timestamps is imposed.

def OAI.MatroidProphet.Pivots.orderPosition line 23
Source documentation
The position of an occurrence is the number of its strict predecessors.
```
noncomputable def orderPosition (time : β → ℕ) (o : β) : ℕ := by
…
```
lemma OAI.MatroidProphet.Pivots.orderPosition_mono line 27
lemma OAI.MatroidProphet.Pivots.orderPosition_strict line 35
lemma OAI.MatroidProphet.Pivots.orderPosition_lt_iff line 49
lemma OAI.MatroidProphet.Pivots.orderPosition_le_iff line 56
lemma OAI.MatroidProphet.Pivots.orderPosition_lt_card line 60
def OAI.MatroidProphet.Pivots.finiteOrderPosition line 74
Source documentation
The normalized timestamp lies in the actual finite position set.
```
noncomputable def finiteOrderPosition (time : β → ℕ) (o : β) : Fin (Fintype.card β) :=
…
```
lemma OAI.MatroidProphet.Pivots.finiteOrderPosition_injective line 77
lemma OAI.MatroidProphet.Pivots.finiteOrderPosition_bijective line 87

lemma OAI.MatroidProphet.Pivots.isPivot_iff_of_same_order line 94

Source documentation

Only the relative occurrence order, not the timestamp magnitudes, matters.

lemma isPivot_iff_of_same_order (M : Matroid α) (label : β → α)
    (time time' : β → ℕ) (horder : ∀ o p, time o < time p ↔ time' o < time' p)
    (e : α) (o : β) : IsPivot M label time e o ↔ IsPivot M label time' e o := by
…

Mentions: OAI.MatroidProphet.Pivots.IsPivot

lemma OAI.MatroidProphet.Pivots.isPivot_orderPosition_iff line 105
lemma OAI.MatroidProphet.Pivots.recordsPivots_orderPosition_iff line 111
lemma OAI.MatroidProphet.Pivots.oldOrdered_orderPosition_iff line 118

lemma OAI.MatroidProphet.Pivots.mem_markedPivotPatterns_iff_finite_order line 124

Source documentation

The counted family is exactly the family obtained from genuine finite interleavings. Arbitrary natural-number gaps neither add nor remove patterns.

lemma mem_markedPivotPatterns_iff_finite_order [Fintype α] {r q n : ℕ}
    (M : Matroid α) (b : ℕ → α) (a : Fin q → α) (test : Fin n → α)
    (oldMark : Fin r → Bool) (t : Finset (Fin n)) :
    t ∈ markedPivotPatterns M b a test oldMark ↔
      ∃ position : Occurrence r q ≃ Fin (Fintype.card (Occurrence r q)),
        OldOrdered (fun o => (position o).val) ∧
          ∃ movableMark : Fin q → Bool,
            RecordsPivots M (occurrenceLabel b a) test (fun o => (position o).val)
              oldMark movableMark t := by
…

Mentions: OAI.MatroidProphet.Pivots.markedPivotPatterns, OAI.MatroidProphet.Pivots.Occurrence, OAI.MatroidProphet.Pivots.OldOrdered, OAI.MatroidProphet.Pivots.RecordsPivots, OAI.MatroidProphet.Pivots.occurrenceLabel