From point conflicts to disjoint recovery sets

Finite point slots represent each request's recovery set; invalid slots are discarded. If the valid slots of one request enumerate distinct points, absence of all point conflicts is exactly the scheduler's Clean property.

def Algebraic.MassProduction.Nonuniform.EnumeratedClean.pointSet {Point : Type u_1} [DecidableEq Point] {slots : ℕ} (valid : Fin slots → Bool) (points : Fin slots → Point) : Finset Point

The valid point slots of one recovery set.

Equations

• Algebraic.MassProduction.Nonuniform.EnumeratedClean.pointSet valid points = Finset.image points {slot : Fin slots | valid slot = true}

theorem Algebraic.MassProduction.Nonuniform.EnumeratedClean.mem_pointSet_iff {Point : Type u_1} [DecidableEq Point] {slots : ℕ} (valid : Fin slots → Bool) (points : Fin slots → Point) (point : Point) : point ∈ pointSet valid points ↔ ∃ (slot : Fin slots), valid slot = true ∧ points slot = point

Membership is witnessed by a valid point slot.

def Algebraic.MassProduction.Nonuniform.EnumeratedClean.Conflict {Point : Type u_1} {requests slots : ℕ} (valid : Fin requests → Fin slots → Bool) (points : Fin requests → Fin slots → Point) (occupied : Finset Point) (request : Fin requests) (slot : Fin slots) : Prop

A valid slot conflicts with another valid record or an occupied point.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.MassProduction.Nonuniform.EnumeratedClean.noConflict_iff_clean {Point : Type u_1} [DecidableEq Point] {requests slots : ℕ} (valid : Fin requests → Fin slots → Bool) (points : Fin requests → Fin slots → Point) (occupied : Finset Point) (withinRequest : ∀ (request : Fin requests) (left right : Fin slots), valid request left = true → valid request right = true → points request left = points request right → left = right) (request : Fin requests) : (∀ (slot : Fin slots), ¬Conflict valid points occupied request slot) ↔ Clean (fun (request : Fin requests) (x : Unit) => pointSet (valid request) (points request)) occupied (fun (x : Fin requests) => ()) request

Under valid-slot injectivity, pointwise conflict absence is exactly disjointness from occupancy and from every other request's recovery set.