Refresh

Explicit initialization by labeled refresh

During the first m requests, label k is matched and replaced at step k < m. Labels below k have already been refreshed, while labels at or above k still denote the original supply. This makes it impossible for the initialization schedule to delete a previously refreshed label.

Spatial.lean is deliberately not imported here: its current dependency on the transport development is transient. Exact coordinates are instead parameterized by a unit-interval location rule. The count projection and its law are independent of that rule.

def FD1D.refreshAssignment {ι : Type u_1} {m : ℕ} (initial replenishment : Assignment ι m) (k : ℕ) : Assignment ι m

Replace exactly the labels whose indices are strictly below k.

Equations

• FD1D.refreshAssignment initial replenishment k j = if ↑j < k then replenishment j else initial j

@[simp]

theorem FD1D.refreshAssignment_zero {ι : Type u_1} {m : ℕ} (initial replenishment : Assignment ι m) : refreshAssignment initial replenishment 0 = initial

@[simp]

theorem FD1D.refreshAssignment_at_card {ι : Type u_1} {m : ℕ} (initial replenishment : Assignment ι m) : refreshAssignment initial replenishment m = replenishment

theorem FD1D.refreshAssignment_apply_of_lt {ι : Type u_1} {m k : ℕ} (initial replenishment : Assignment ι m) (j : Fin m) (hj : ↑j < k) : refreshAssignment initial replenishment k j = replenishment j

theorem FD1D.refreshAssignment_apply_of_le {ι : Type u_1} {m k : ℕ} (initial replenishment : Assignment ι m) (j : Fin m) (hj : k ≤ ↑j) : refreshAssignment initial replenishment k j = initial j

theorem FD1D.refreshAssignment_current_is_original {ι : Type u_1} {m k : ℕ} (initial replenishment : Assignment ι m) (hk : k < m) : refreshAssignment initial replenishment k ⟨k, hk⟩ = initial ⟨k, hk⟩

Immediately before step k, label k still denotes original supply.

theorem FD1D.refreshAssignment_current_is_replenished {ι : Type u_1} {m k : ℕ} (initial replenishment : Assignment ι m) (hk : k < m) : refreshAssignment initial replenishment (k + 1) ⟨k, hk⟩ = replenishment ⟨k, hk⟩

Immediately after step k, label k denotes its replenishment.

theorem FD1D.refreshAssignment_preserves_refreshed {ι : Type u_1} {m k : ℕ} (initial replenishment : Assignment ι m) (j : Fin m) (hj : ↑j < k) : refreshAssignment initial replenishment (k + 1) j = refreshAssignment initial replenishment k j

Advancing the schedule cannot alter a previously refreshed label. Both sides equal that label's prescribed replenishment.

theorem FD1D.refreshAssignment_preserves_later {ι : Type u_1} {m k : ℕ} (initial replenishment : Assignment ι m) (j : Fin m) (hj : k < ↑j) : refreshAssignment initial replenishment (k + 1) j = refreshAssignment initial replenishment k j

Advancing step k also leaves every label strictly above k alone.

def FD1D.refreshState {L m : ℕ} (initial replenishment : DyadicAssignment L m) (k : ℕ) : InventoryState (DyadicNode L) m

The leaf-count state after the first k labeled replacements.

Equations

• FD1D.refreshState initial replenishment k = FD1D.assignmentState (FD1D.refreshAssignment initial replenishment k)

@[simp]

theorem FD1D.refreshState_zero {L m : ℕ} (initial replenishment : DyadicAssignment L m) : refreshState initial replenishment 0 = assignmentState initial

@[simp]

theorem FD1D.refreshState_at_card {L m : ℕ} (initial replenishment : DyadicAssignment L m) : refreshState initial replenishment m = assignmentState replenishment

After all m replacements, the count state forgets the initial supply.

structure FD1D.RefreshSupply (L m : ℕ) : Type

An arbitrary labeled supply configuration at the resolution used by the count chain. No distributional assumption is imposed on the initial supply.

• location : Fin m → ℝ

  Spatial coordinate of each labeled supply item.

• leaf : DyadicAssignment L m

  Dyadic leaf assigned to each labeled supply item.

• location_mem_unit (j : Fin m) : self.location j ∈ Set.Icc 0 1

structure FD1D.ReplenishmentCoordinates (L m : ℕ) : Type

Coordinates for every possible replenishment-leaf assignment. This is the coordinate-level parameter used while Spatial.lean is unavailable.

• location : DyadicAssignment L m → Fin m → ℝ

  Replenishment coordinates associated with each dyadic assignment.

• location_mem_unit (ω : DyadicAssignment L m) (j : Fin m) : self.location ω j ∈ Set.Icc 0 1

def FD1D.ReplenishmentCoordinates.supply {L m : ℕ} (R : ReplenishmentCoordinates L m) (ω : DyadicAssignment L m) : RefreshSupply L m

The realized labeled replenishment configuration for outcome ω.

Equations

• R.supply ω = { location := R.location ω, leaf := ω, location_mem_unit := ⋯ }

@[simp]

theorem FD1D.ReplenishmentCoordinates.supply_location {L m : ℕ} (R : ReplenishmentCoordinates L m) (ω : DyadicAssignment L m) (j : Fin m) : (R.supply ω).location j = R.location ω j

@[simp]

theorem FD1D.ReplenishmentCoordinates.supply_leaf {L m : ℕ} (R : ReplenishmentCoordinates L m) (ω : DyadicAssignment L m) : (R.supply ω).leaf = ω

def FD1D.RefreshSupply.countState {L m : ℕ} (C : RefreshSupply L m) : InventoryState (DyadicNode L) m

Count projection of a labeled supply configuration.

Equations

• C.countState = FD1D.assignmentState C.leaf

def FD1D.RefreshSupply.refresh {L m : ℕ} (initial replenishment : RefreshSupply L m) (k : ℕ) : RefreshSupply L m

The labeled configuration after the first k replacements.

Equations

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

@[simp]

theorem FD1D.RefreshSupply.refresh_location {L m : ℕ} (initial replenishment : RefreshSupply L m) (k : ℕ) (j : Fin m) : (initial.refresh replenishment k).location j = refreshAssignment initial.location replenishment.location k j

@[simp]

theorem FD1D.RefreshSupply.refresh_leaf {L m : ℕ} (initial replenishment : RefreshSupply L m) (k : ℕ) : (initial.refresh replenishment k).leaf = refreshAssignment initial.leaf replenishment.leaf k

@[simp]

theorem FD1D.RefreshSupply.refresh_countState {L m : ℕ} (initial replenishment : RefreshSupply L m) (k : ℕ) : (initial.refresh replenishment k).countState = refreshState initial.leaf replenishment.leaf k

theorem FD1D.RefreshSupply.refresh_countState_at_card {L m : ℕ} (initial : RefreshSupply L m) (R : ReplenishmentCoordinates L m) (ω : DyadicAssignment L m) : (initial.refresh (R.supply ω) m).countState = assignmentState ω

For every replenishment outcome, the terminal count state is exactly the fiber-count state of that outcome.

theorem FD1D.RefreshSupply.refresh_current_location_is_original {L m k : ℕ} (initial replenishment : RefreshSupply L m) (hk : k < m) : (initial.refresh replenishment k).location ⟨k, hk⟩ = initial.location ⟨k, hk⟩

At step k, the scheduled match removes original label k, not any label that was replenished at an earlier step.

noncomputable def FD1D.refreshCountLaw {L m : ℕ} (initial : RefreshSupply L m) (R : ReplenishmentCoordinates L m) (k : ℕ) : FiniteLaw (InventoryState (DyadicNode L) m)

The count-state law after k scheduled replacements, with all replenishment leaf labels sampled jointly from the uniform law on assignments.

Equations

• FD1D.refreshCountLaw initial R k = FD1D.FiniteLaw.map (fun (ω : FD1D.DyadicAssignment L m) => (initial.refresh (R.supply ω) k).countState) FD1D.FiniteLaw.uniform

@[simp]

theorem FD1D.refreshCountLaw_at_card {L m : ℕ} (initial : RefreshSupply L m) (R : ReplenishmentCoordinates L m) : refreshCountLaw initial R m = refreshedLaw L m

The explicit m-step schedule has exactly the iid refreshed count law, independently of the arbitrary initial supply and coordinate rule.

theorem FD1D.abs_sub_le_one_of_mem_unit {x y : ℝ} (hx : x ∈ Set.Icc 0 1) (hy : y ∈ Set.Icc 0 1) : |x - y| ≤ 1

Unit-interval points are at distance at most one.

def FD1D.scheduledInitializationStepCost {L m : ℕ} (initial : RefreshSupply L m) (R : ReplenishmentCoordinates L m) (ω : DyadicAssignment L m) (demand : Fin m → ℝ) (j : Fin m) : ℝ

Cost at initialization step j: match the request to label j in the configuration just before that label is refreshed.

Equations

• FD1D.scheduledInitializationStepCost initial R ω demand j = |demand j - (initial.refresh (R.supply ω) ↑j).location j|

@[simp]

theorem FD1D.scheduledInitializationStepCost_eq {L m : ℕ} (initial : RefreshSupply L m) (R : ReplenishmentCoordinates L m) (ω : DyadicAssignment L m) (demand : Fin m → ℝ) (j : Fin m) : scheduledInitializationStepCost initial R ω demand j = |demand j - initial.location j|

The scheduled step always matches the still-unrefreshed original label.

def FD1D.initializationMatchingCost {L m : ℕ} (initial : RefreshSupply L m) (demand : Fin m → ℝ) : ℝ

The total cost of matching each initialization request to its old label.

Equations

• FD1D.initializationMatchingCost initial demand = ∑ j : Fin m, |demand j - initial.location j|

theorem FD1D.sum_scheduledInitializationStepCost_eq {L m : ℕ} (initial : RefreshSupply L m) (R : ReplenishmentCoordinates L m) (ω : DyadicAssignment L m) (demand : Fin m → ℝ) : ∑ j : Fin m, scheduledInitializationStepCost initial R ω demand j = initializationMatchingCost initial demand

The pathwise schedule cost is independent of replenishment outcomes.

theorem FD1D.scheduledInitializationStepCost_le_one {L m : ℕ} (initial : RefreshSupply L m) (R : ReplenishmentCoordinates L m) (ω : DyadicAssignment L m) (demand : Fin m → ℝ) (hdemand : ∀ (j : Fin m), demand j ∈ Set.Icc 0 1) (j : Fin m) : scheduledInitializationStepCost initial R ω demand j ≤ 1

Every initialization match has cost at most one.

theorem FD1D.initializationMatchingCost_le_card {L m : ℕ} (initial : RefreshSupply L m) (demand : Fin m → ℝ) (hdemand : ∀ (j : Fin m), demand j ∈ Set.Icc 0 1) : initializationMatchingCost initial demand ≤ ↑m

The complete m-step initialization period costs at most m.

theorem FD1D.finite_horizon_expected_cost_le_seven_after_refresh {m N : ℕ} (hm : 1 ≤ m) (hN : 2 * m ^ 2 ≤ N) (initial : RefreshSupply (treeDepth m) m) (R : ReplenishmentCoordinates (treeDepth m) m) (demand : Fin m → ℝ) (hdemand : ∀ (j : Fin m), demand j ∈ Set.Icc 0 1) (cost : ℕ → InventoryState (DyadicNode (treeDepth m)) m → ℝ) (htransport : (∑ t ∈ Finset.range (N - m), (refreshedIterate m hm t).expect (cost t)) / ↑(N - m) ≤ 1 / ↑(leafCount m) + ↑(parameterA m) / √6 * √((∑ t ∈ Finset.range (N - m), (refreshedIterate m hm t).expect (parameterizedHazardEnergy m)) / ↑(N - m) - 1 / ↑m ^ 2)) : refreshCountLaw initial R m = refreshedLaw (treeDepth m) m ∧ (initializationMatchingCost initial demand + ∑ t ∈ Finset.range (N - m), (refreshedIterate m hm t).expect (cost t)) / ↑N ≤ 7 * ↑(parameterA m) / ↑m

The final finite-horizon wrapper. Its first conclusion identifies the explicit schedule's terminal count law with refreshedLaw; its second conclusion invokes the main arithmetic theorem with the initialization bound proved above, so neither fact remains a hypothesis.