Process

One-step spatial dynamics

This module lifts one transition of the hierarchical count chain to the actual labeled supply configuration. The selected label is retained, so replacing its coordinate and dyadic leaf gives a pathwise update rather than only a count-law coupling.

@[reducible, inline]

noncomputable abbrev FD1D.V5.Dynamics.stateDyadicMass {L m : ℕ} (a : ℝ) (x : InventoryState (DyadicNode L) m) : DyadicMass L

The v5 deletion-mass tree, re-exported at the spatial-dynamics boundary.

Equations

• FD1D.V5.Dynamics.stateDyadicMass a x = FD1D.V5.Transport.stateDyadicMass a x

theorem FD1D.V5.Dynamics.stateDyadicMass_isProbability {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) : (stateDyadicMass a x).IsProbability

theorem FD1D.V5.Dynamics.stateDyadicMass_leafMass_eq_deletionRule {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (x : InventoryState (DyadicNode L) m) (w : DyadicNode L) : (stateDyadicMass a x).leafMass w = (deletionRule a ha hm).prob x w

noncomputable def FD1D.V5.Dynamics.selectedSupplyLabel {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u : ℝ) : Fin m

The concrete supply label selected from the hierarchical dyadic mass.

Equations

• FD1D.V5.Dynamics.selectedSupplyLabel a C fallback u = C.selectedSupplyIndex (FD1D.V5.Dynamics.stateDyadicMass a C.countState) fallback u

noncomputable def FD1D.V5.Dynamics.selectedDeletedLeaf {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u : ℝ) : DyadicNode L

The leaf actually deleted by the concrete label selection.

Equations

• FD1D.V5.Dynamics.selectedDeletedLeaf a C fallback u = C.leaf (FD1D.V5.Dynamics.selectedSupplyLabel a C fallback u)

noncomputable def FD1D.V5.Dynamics.actualStep {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u v : ℝ) (hv : v ∈ Set.Icc 0 1) : SupplyConfiguration L m

One actual hierarchical-policy step: match demand u to the selected supply label and replace that same label by the replenishment coordinate v.

Equations

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

@[simp]

theorem FD1D.V5.Dynamics.actualStep_location_selected {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u v : ℝ) (hv : v ∈ Set.Icc 0 1) : (actualStep a C fallback u v hv).location (selectedSupplyLabel a C fallback u) = v

@[simp]

theorem FD1D.V5.Dynamics.actualStep_leaf_selected {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u v : ℝ) (hv : v ∈ Set.Icc 0 1) : (actualStep a C fallback u v hv).leaf (selectedSupplyLabel a C fallback u) = DyadicMass.uniformArrivalLeaf L v

theorem FD1D.V5.Dynamics.actualStep_location_of_ne {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u v : ℝ) (hv : v ∈ Set.Icc 0 1) (j : Fin m) (hj : j ≠ selectedSupplyLabel a C fallback u) : (actualStep a C fallback u v hv).location j = C.location j

theorem FD1D.V5.Dynamics.actualStep_leaf_of_ne {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u v : ℝ) (hv : v ∈ Set.Icc 0 1) (j : Fin m) (hj : j ≠ selectedSupplyLabel a C fallback u) : (actualStep a C fallback u v hv).leaf j = C.leaf j

noncomputable def FD1D.V5.Dynamics.actualLeafStep {L m : ℕ} (C : SupplyConfiguration L m) (fallback : Fin m) (deleted arrived : DyadicNode L) (v : ℝ) (hv : v ∈ dyadicCell arrived) : SupplyConfiguration L m

Replace the fixed representative of an occupied deletion leaf by an arbitrary point certified to lie in the arrival leaf. On an empty deletion leaf this is a no-op, matching InventoryState.move.

Equations

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

theorem FD1D.V5.Dynamics.actualLeafStep_of_occupied {L m : ℕ} (C : SupplyConfiguration L m) (fallback : Fin m) (deleted arrived : DyadicNode L) (v : ℝ) (hv : v ∈ dyadicCell arrived) (h : ∃ (j : Fin m), C.leaf j = deleted) : actualLeafStep C fallback deleted arrived v hv = { location := Function.update C.location (C.representative fallback deleted) v, leaf := Function.update C.leaf (C.representative fallback deleted) arrived, location_mem_unit := ⋯, location_mem_cell := ⋯ }

@[simp]

theorem FD1D.V5.Dynamics.actualLeafStep_countState {L m : ℕ} (C : SupplyConfiguration L m) (fallback : Fin m) (deleted arrived : DyadicNode L) (v : ℝ) (hv : v ∈ dyadicCell arrived) : (actualLeafStep C fallback deleted arrived v hv).countState = C.countState.move deleted arrived

The leaf-conditioned spatial update projects exactly to the finite count move, including the zero-probability empty-deletion case.

theorem FD1D.V5.Dynamics.selectedDeletedLeaf_count_pos {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u : ℝ) : 0 < ↑C.countState (selectedDeletedLeaf a C fallback u)

The selected concrete slot certifies that its old leaf is occupied.

@[simp]

theorem FD1D.V5.Dynamics.actualStep_countState {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u v : ℝ) (hv : v ∈ Set.Icc 0 1) : (actualStep a C fallback u v hv).countState = C.countState.move (selectedDeletedLeaf a C fallback u) (DyadicMass.uniformArrivalLeaf L v)

The spatial update projects exactly to deletion of the selected slot's old leaf followed by insertion of the uniform-arrival leaf.

theorem FD1D.V5.Dynamics.selectedDeletedLeaf_eq_selectedIndex {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (C : SupplyConfiguration L m) (fallback : Fin m) {u : ℝ} (hu : u ∈ Set.Icc 0 1) (hu0 : u ≠ 0) : selectedDeletedLeaf a C fallback u = (stateDyadicMass a C.countState).selectedIndex u

Away from the null boundary u = 0, the old leaf of the selected concrete slot is exactly the leaf selected by the hierarchical mass tree.

theorem FD1D.V5.Dynamics.actualStep_eq_actualLeafStep {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (C : SupplyConfiguration L m) (fallback : Fin m) {u v : ℝ} (hu : u ∈ Set.Icc 0 1) (hu0 : u ≠ 0) (hv : v ∈ Set.Icc 0 1) : actualStep a C fallback u v hv = actualLeafStep C fallback ((stateDyadicMass a C.countState).selectedIndex u) (DyadicMass.uniformArrivalLeaf L v) v ⋯

Off the null demand boundary, the continuous-coordinate update is exactly the corresponding leaf-conditioned update.

noncomputable def FD1D.V5.Dynamics.actualStepCost {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u : ℝ) : ℝ

Pathwise cost of the actual match made in one hierarchical step.

Equations

• FD1D.V5.Dynamics.actualStepCost a C fallback u = |C.location (FD1D.V5.Dynamics.selectedSupplyLabel a C fallback u) - u|

theorem FD1D.V5.Dynamics.actualStepCost_eq_selectedSupplyPoint {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u : ℝ) : actualStepCost a C fallback u = |C.selectedSupplyPoint (stateDyadicMass a C.countState) fallback u - u|

theorem FD1D.V5.Dynamics.integral_actualStepCost_eq_expectedActualDistance {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) : ∫ (u : ℝ) in Set.Icc 0 1, actualStepCost a C fallback u = C.expectedActualDistance (stateDyadicMass a C.countState) fallback

Integrating the pathwise one-step cost is exactly the existing configured matching-cost functional.

noncomputable def FD1D.V5.Dynamics.actualStepSquaredCost {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u : ℝ) : ℝ

Squared pathwise cost of the actual v5 match.

Equations

• FD1D.V5.Dynamics.actualStepSquaredCost a C fallback u = (C.location (FD1D.V5.Dynamics.selectedSupplyLabel a C fallback u) - u) ^ 2

theorem FD1D.V5.Dynamics.actualStepSquaredCost_eq_selectedSupplyPoint {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) (u : ℝ) : actualStepSquaredCost a C fallback u = (C.selectedSupplyPoint (stateDyadicMass a C.countState) fallback u - u) ^ 2

theorem FD1D.V5.Dynamics.integral_actualStepSquaredCost_eq_expected {L m : ℕ} (a : ℝ) (C : SupplyConfiguration L m) (fallback : Fin m) : ∫ (u : ℝ) in Set.Icc 0 1, actualStepSquaredCost a C fallback u = Transport.expectedActualSquaredDistance C (stateDyadicMass a C.countState) fallback

noncomputable def FD1D.V5.Dynamics.actualConfigurationCost {L m : ℕ} (a : ℝ) (hm : 0 < m) (C : SupplyConfiguration L m) : ℝ

The actual one-period expected distance of a concrete configuration.

Equations

• FD1D.V5.Dynamics.actualConfigurationCost a hm C = C.expectedActualDistance (FD1D.V5.Dynamics.stateDyadicMass a C.countState) (FD1D.SupplyConfiguration.canonicalFallback hm)

noncomputable def FD1D.V5.Dynamics.actualConfigurationSquaredCost {L m : ℕ} (a : ℝ) (hm : 0 < m) (C : SupplyConfiguration L m) : ℝ

The actual one-period expected squared distance.

Equations

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

theorem FD1D.V5.Dynamics.configured_transition_eq_kernel {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (C : SupplyConfiguration L m) (y : InventoryState (DyadicNode L) m) : (∑ deleted : DyadicNode L, ∑ arrived : DyadicNode L, if C.countState.move deleted arrived = y then ((stateDyadicMass a C.countState).selectedIndexLaw ⋯).mass deleted * (1 / ↑(Fintype.card (DyadicNode L))) else 0) = (kernel a ha hm).trans C.countState y

Selecting a leaf by the demand coordinate and adding an independent uniform arrival leaf produces exactly the v5 finite count transition.