The local three-cap policy from manuscript bundle v5

The two child counts are ordered only inside orderedBias. bias restores the fixed left/right spatial sign. Empty-child rates are auxiliary analytic rates; empty children still receive zero deletion mass.

def FD1D.V5.LocalPolicy.inventory (x y : ℕ) : ℝ

Parent inventory, coerced to ℝ.

Equations

• FD1D.V5.LocalPolicy.inventory x y = ↑x + ↑y

def FD1D.V5.LocalPolicy.parentMass (h : ℝ) (x y : ℕ) : ℝ

Parent deletion mass under the identity q = Nh.

Equations

• FD1D.V5.LocalPolicy.parentMass h x y = FD1D.V5.LocalPolicy.inventory x y * h

noncomputable def FD1D.V5.LocalPolicy.feedbackCandidate (a h : ℝ) (x y : ℕ) : ℝ

The feedback candidate, for ordered positive counts x ≥ y > 0.

Equations

• FD1D.V5.LocalPolicy.feedbackCandidate a h x y = 2 * a * FD1D.V5.LocalPolicy.parentMass h x y * (↑x - ↑y) / (↑x * ↑y)

noncomputable def FD1D.V5.LocalPolicy.uniformCandidate (h : ℝ) (x y : ℕ) : ℝ

The uniform-deletion cap, for ordered counts.

Equations

• FD1D.V5.LocalPolicy.uniformCandidate h x y = FD1D.V5.LocalPolicy.parentMass h x y * (↑x - ↑y) / FD1D.V5.LocalPolicy.inventory x y

noncomputable def FD1D.V5.LocalPolicy.floorCandidate (a p h : ℝ) (x y : ℕ) : ℝ

The rate-floor cap, for ordered counts and parent interval mass p.

Equations

• FD1D.V5.LocalPolicy.floorCandidate a p h x y = FD1D.V5.LocalPolicy.parentMass h x y - 2 * p * ↑y / (2 * ↑y + a)

noncomputable def FD1D.V5.LocalPolicy.orderedBias (a p h : ℝ) (x y : ℕ) : ℝ

Nonnegative bias magnitude after temporarily ordering x ≥ y.

Equations

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

noncomputable def FD1D.V5.LocalPolicy.bias (a p h : ℝ) (x y : ℕ) : ℝ

Signed left-minus-right deletion bias in fixed spatial labels.

Equations

• FD1D.V5.LocalPolicy.bias a p h x y = if y ≤ x then FD1D.V5.LocalPolicy.orderedBias a p h x y else -FD1D.V5.LocalPolicy.orderedBias a p h y x

noncomputable def FD1D.V5.LocalPolicy.massLeft (a p h : ℝ) (x y : ℕ) : ℝ

Left-child deletion mass.

Equations

• FD1D.V5.LocalPolicy.massLeft a p h x y = (FD1D.V5.LocalPolicy.parentMass h x y + FD1D.V5.LocalPolicy.bias a p h x y) / 2

noncomputable def FD1D.V5.LocalPolicy.massRight (a p h : ℝ) (x y : ℕ) : ℝ

Right-child deletion mass.

Equations

• FD1D.V5.LocalPolicy.massRight a p h x y = (FD1D.V5.LocalPolicy.parentMass h x y - FD1D.V5.LocalPolicy.bias a p h x y) / 2

noncomputable def FD1D.V5.LocalPolicy.rateLeft (a p h : ℝ) (x y : ℕ) : ℝ

Auxiliary child rate on the spatial left.

Equations

• FD1D.V5.LocalPolicy.rateLeft a p h x y = if x + y = 0 then h else if x = 0 then max h (p / a) else FD1D.V5.LocalPolicy.massLeft a p h x y / ↑x

noncomputable def FD1D.V5.LocalPolicy.rateRight (a p h : ℝ) (x y : ℕ) : ℝ

Auxiliary child rate on the spatial right.

Equations

• FD1D.V5.LocalPolicy.rateRight a p h x y = if x + y = 0 then h else if y = 0 then max h (p / a) else FD1D.V5.LocalPolicy.massRight a p h x y / ↑y

noncomputable def FD1D.V5.LocalPolicy.discrepancy (a p h : ℝ) (x y : ℕ) : ℝ

Discrepancy t = (p-q)/a.

Equations

• FD1D.V5.LocalPolicy.discrepancy a p h x y = (p - FD1D.V5.LocalPolicy.parentMass h x y) / a

noncomputable def FD1D.V5.LocalPolicy.regularizedMass (a p : ℝ) (x y : ℕ) : ℝ

Regularized inverse inventory Z = p/(N+a/2).

Equations

• FD1D.V5.LocalPolicy.regularizedMass a p x y = p / (FD1D.V5.LocalPolicy.inventory x y + a / 2)

noncomputable def FD1D.V5.LocalPolicy.discrepancyLeft (a p h : ℝ) (x y : ℕ) : ℝ

Left-child discrepancy.

Equations

• FD1D.V5.LocalPolicy.discrepancyLeft a p h x y = (p / 2 - FD1D.V5.LocalPolicy.massLeft a p h x y) / a

noncomputable def FD1D.V5.LocalPolicy.discrepancyRight (a p h : ℝ) (x y : ℕ) : ℝ

Right-child discrepancy.

Equations

• FD1D.V5.LocalPolicy.discrepancyRight a p h x y = (p / 2 - FD1D.V5.LocalPolicy.massRight a p h x y) / a

noncomputable def FD1D.V5.LocalPolicy.regularizedMassLeft (a p : ℝ) (x : ℕ) : ℝ

Left-child regularized inverse inventory.

Equations

• FD1D.V5.LocalPolicy.regularizedMassLeft a p x = p / 2 / (↑x + a / 2)

noncomputable def FD1D.V5.LocalPolicy.regularizedMassRight (a p : ℝ) (y : ℕ) : ℝ

Right-child regularized inverse inventory.

Equations

• FD1D.V5.LocalPolicy.regularizedMassRight a p y = p / 2 / (↑y + a / 2)

noncomputable def FD1D.V5.LocalPolicy.bellman (h t Z : ℝ) : ℝ

The quadratic Bellman correction in equation (15).

Equations

• FD1D.V5.LocalPolicy.bellman h t Z = (t - h / 2) * Z - t ^ 2 / 6

theorem FD1D.V5.LocalPolicy.inventory_nonneg (x y : ℕ) : 0 ≤ inventory x y

theorem FD1D.V5.LocalPolicy.inventory_pos {x y : ℕ} (hne : x + y ≠ 0) : 0 < inventory x y

theorem FD1D.V5.LocalPolicy.parentMass_swap (h : ℝ) (x y : ℕ) : parentMass h y x = parentMass h x y

theorem FD1D.V5.LocalPolicy.bias_swap (a p h : ℝ) (x y : ℕ) : bias a p h y x = -bias a p h x y

theorem FD1D.V5.LocalPolicy.massLeft_swap (a p h : ℝ) (x y : ℕ) : massLeft a p h y x = massRight a p h x y

theorem FD1D.V5.LocalPolicy.massRight_swap (a p h : ℝ) (x y : ℕ) : massRight a p h y x = massLeft a p h x y

theorem FD1D.V5.LocalPolicy.rateLeft_swap (a p h : ℝ) (x y : ℕ) : rateLeft a p h y x = rateRight a p h x y

theorem FD1D.V5.LocalPolicy.rateRight_swap (a p h : ℝ) (x y : ℕ) : rateRight a p h y x = rateLeft a p h x y

theorem FD1D.V5.LocalPolicy.massLeft_add_massRight (a p h : ℝ) (x y : ℕ) : massLeft a p h x y + massRight a p h x y = parentMass h x y

theorem FD1D.V5.LocalPolicy.bias_eq_massLeft_sub_massRight (a p h : ℝ) (x y : ℕ) : bias a p h x y = massLeft a p h x y - massRight a p h x y

theorem FD1D.V5.LocalPolicy.discrepancyLeft_eq (a p h : ℝ) (x y : ℕ) : discrepancyLeft a p h x y = (discrepancy a p h x y - bias a p h x y / a) / 2

theorem FD1D.V5.LocalPolicy.discrepancyRight_eq (a p h : ℝ) (x y : ℕ) : discrepancyRight a p h x y = (discrepancy a p h x y + bias a p h x y / a) / 2

theorem FD1D.V5.LocalPolicy.bellman_nonpos {h t Z : ℝ} (hZ : 0 ≤ Z) (ht : t ≤ h / 2) : bellman h t Z ≤ 0