Competing exponential clocks: the first to fire wins in proportion to its rate

Category: 1-Mathlib. No CSD content: this is the classical competing-risks computation for independent exponential waiting times.

It is the engine for the record layer's order-free Born partition (specs/q12-fibre-mechanism-scoping.md, brick Q12-b). The partition already in the corpus (RecordLayer/BornFibrePartition.cdfCell) stacks intervals in index order, which reproduces Born but imposes an arbitrary outcome order; record-layer-plan.md §3b asks instead for the symmetric noisy-argmax / race form, in which no index is privileged.

The two one-dimensional facts

• expMeasure_Ioi — the survival function: P(T > t) = e^{-rt} for t ≥ 0.
• lintegral_exp_neg_expMeasure — the rescaling identity ∫ e^{-St} d(Exp r) = r/(r+S). Proved without evaluating an improper integral: the integrand times the Exp r density is a constant multiple of the Exp (r+S) density, whose total mass is one (lintegral_exponentialPDF_eq_one).

The race

• raceCell i — the readings on which clock i fires strictly first. No index order, no cumulative sums, no privileged outcome.
• raceCell_pairwiseDisjoint — the partition content; needs no hypothesis on the rates.
• ★★ measure_raceCell — clock i wins with probability bᵢ / Σⱼ bⱼ, and ★★ measure_raceCell_of_sum_eq_one — hence exactly bᵢ for a probability vector of rates.

⚠️ Scope, and two findings worth carrying

Nothing here is a new physical claim. The Born numbers this feeds are already proved for the ordered partition (RecordLayer.volume_bornCell); what the race buys is that the construction privileges no outcome.

Two things the build turned up, both recorded in specs/q12-fibre-mechanism-scoping.md:

• The race does not fit the corpus's record-layer interface. RecordLayer.DeIsolationInteraction takes pointer : ℝ → Fin n — a one-dimensional fibre — whereas the race needs Fin (n+1) → ℝ. That is not an accident of this construction: record-layer-plan.md §3b states the minimal fibre dimension is n − 1. So the existing interface is committed to the ordered CDF construction, and admitting the symmetric race would require generalising it. Q12-a's witness (cdfDeIsolationInteraction) remains the only instance.
• Strictly positive rates only. An exponential clock needs r > 0, so measure_raceCell applies to states with every amplitude nonzero. A zero amplitude means a clock that never fires, which is the right physics but is outside expMeasure's domain.

Reference: specs/q12-fibre-mechanism-scoping.md; specs/record-layer-plan.md §3b–§3c; specs/future-work.md.

theorem ProbabilityTheory.expMeasure_Ioi {r : ℝ} (hr : 0 < r) {t : ℝ} (ht : 0 ≤ t) : (expMeasure r) (Set.Ioi t) = ENNReal.ofReal (Real.exp (-(r * t)))

The survival function of an exponential clock: P(T > t) = e^{-rt} for t ≥ 0.

theorem ProbabilityTheory.lintegral_exp_neg_expMeasure {r S : ℝ} (hr : 0 < r) (hS : 0 ≤ S) : ∫⁻ (t : ℝ), ENNReal.ofReal (Real.exp (-(S * t))) ∂expMeasure r = ENNReal.ofReal (r / (r + S))

The rescaling identity ∫ e^{-St} d(Exp r) = r/(r+S).

No improper integral is evaluated: e^{-St} times the Exp r density is exactly r/(r+S) times the Exp (r+S) density, and that density integrates to one.

theorem ProbabilityTheory.expMeasure_ae_nonneg {r : ℝ} (hr : 0 < r) : ∀ᵐ (t : ℝ) ∂expMeasure r, 0 ≤ t

The exponential measure lives on [0, ∞).

The race

def ProbabilityTheory.raceCell {n : ℕ} (i : Fin (n + 1)) : Set (Fin (n + 1) → ℝ)

The race cell: the clock readings on which clock i fires first.

Note what is absent: no index order, no cumulative sums, no privileged outcome. Relabelling the clocks permutes the cells, which is exactly the symmetry record-layer-plan.md §3b asks for and which cdfCell does not have.

Equations

• ProbabilityTheory.raceCell i = {ξ : Fin (n + 1) → ℝ | ∀ (j : Fin (n + 1)), j ≠ i → ξ i < ξ j}

theorem ProbabilityTheory.measurableSet_raceCell {n : ℕ} (i : Fin (n + 1)) : MeasurableSet (raceCell i)

theorem ProbabilityTheory.measure_raceCell {n : ℕ} (b : Fin (n + 1) → ℝ) (hb : ∀ (j : Fin (n + 1)), 0 < b j) (i : Fin (n + 1)) : (MeasureTheory.Measure.pi fun (j : Fin (n + 1)) => expMeasure (b j)) (raceCell i) = ENNReal.ofReal (b i / ∑ j : Fin (n + 1), b j)

★★ The first clock to fire wins in proportion to its rate.

For independent exponential clocks with rates b, clock i fires first with probability bᵢ / Σⱼ bⱼ. Feeding a probability vector of rates (Σ b = 1) this is bᵢ on the nose — the order-free Born partition.

The proof splits coordinate i off the product (measurePreserving_piFinSuccAbove), reads the remaining clocks' survival as a box (Measure.pi_pi on Set.pi univ (fun _ => Ioi t)), and integrates the resulting e^{-St} against clock i by lintegral_exp_neg_expMeasure.

theorem ProbabilityTheory.raceCell_pairwiseDisjoint {n : ℕ} : Pairwise (Function.onFun Disjoint raceCell)

The race cells are pairwise disjoint: two clocks cannot both be strictly first. This is the partition content, and it needs no hypothesis on the rates at all.

theorem ProbabilityTheory.measure_raceCell_of_sum_eq_one {n : ℕ} (b : Fin (n + 1) → ℝ) (hb : ∀ (j : Fin (n + 1)), 0 < b j) (hsum : ∑ j : Fin (n + 1), b j = 1) (i : Fin (n + 1)) : (MeasureTheory.Measure.pi fun (j : Fin (n + 1)) => expMeasure (b j)) (raceCell i) = ENNReal.ofReal (b i)

★★ The order-free Born partition. For a rate vector that is already a probability vector, clock i wins with probability exactly bᵢ.

Compare RecordLayer.volume_bornCell, which gets the same numbers from cdfCell — but by stacking intervals in index order. Here no index is privileged: raceCell is defined by "fires strictly first", and relabelling the clocks just permutes the cells.