Realization

Realizing fixed-total count states by spatial configurations

Every unit of a count vector is represented by one slot in the sigma type Σ i, Fin (x i). An equivalence with Fin m enumerates those slots, and placing each enumerated point at its cell's left endpoint gives an exact spatial realization.

@[reducible, inline]

abbrev FD1D.SupplyConfiguration.CountSlot {L m : ℕ} (x : InventoryState (DyadicNode L) m) : Type

One distinguishable slot for every unit of inventory in every leaf.

Equations

• FD1D.SupplyConfiguration.CountSlot x = ((i : FD1D.DyadicNode L) × Fin (↑x i))

noncomputable def FD1D.SupplyConfiguration.countSlotEquiv {L m : ℕ} (x : InventoryState (DyadicNode L) m) : Fin m ≃ CountSlot x

Enumerate all count slots by the m supply labels.

Equations

• FD1D.SupplyConfiguration.countSlotEquiv x = Fintype.equivOfCardEq ⋯

noncomputable def FD1D.SupplyConfiguration.countAssignment {L m : ℕ} (x : InventoryState (DyadicNode L) m) (j : Fin m) : DyadicNode L

The leaf label obtained by forgetting which copy of a count slot was used.

Equations

• FD1D.SupplyConfiguration.countAssignment x j = ((FD1D.SupplyConfiguration.countSlotEquiv x) j).fst

noncomputable def FD1D.SupplyConfiguration.ofCountState {L m : ℕ} (x : InventoryState (DyadicNode L) m) : SupplyConfiguration L m

The canonical spatial realization of a fixed-total leaf count state. Every point is placed at the left endpoint of its declared dyadic cell.

Equations

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

@[simp]

theorem FD1D.SupplyConfiguration.ofCountState_location {L m : ℕ} (x : InventoryState (DyadicNode L) m) (j : Fin m) : (ofCountState x).location j = dyadicCellLeft ((ofCountState x).leaf j)

@[simp]

theorem FD1D.SupplyConfiguration.ofCountState_leafCount {L m : ℕ} (x : InventoryState (DyadicNode L) m) (i : DyadicNode L) : (ofCountState x).leafCount i = ↑x i

@[simp]

theorem FD1D.SupplyConfiguration.ofCountState_countState {L m : ℕ} (x : InventoryState (DyadicNode L) m) : (ofCountState x).countState = x

The canonical spatial realization projects back to the original state.

theorem FD1D.SupplyConfiguration.exists_countState_eq {L m : ℕ} (x : InventoryState (DyadicNode L) m) : ∃ (C : SupplyConfiguration L m), C.countState = x

Every fixed-total leaf count state has an exact spatial realization.

def FD1D.SupplyConfiguration.canonicalFallback {m : ℕ} (hm : 0 < m) : Fin m

A canonical total representative fallback whenever the inventory is nonempty.

Equations

• FD1D.SupplyConfiguration.canonicalFallback hm = ⟨0, hm⟩

@[simp]

theorem FD1D.SupplyConfiguration.canonicalFallback_val {m : ℕ} (hm : 0 < m) : ↑(canonicalFallback hm) = 0