The race of iid clocks: the exponential law is forced

Category: 1-Mathlib. No CSD content: this is the classical competing-risks characterisation, which Mathlib does not have.

Glossary: https://glossary.constraintsurfacedynamics.com/first-passage-race/ Plain-language, CSD-role and formal statements of the first-passage race, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

★★★ hasRaceProperty_iff_exists_expMeasure — for iid clocks at linear rates, the first to fire wins in proportion to its rate iff the waiting-time law is exponential. This is the statement of specs/record-layer-plan.md §3c, and the route to it is specs/q12c-exponential-characterisation-route.md. CompetingExponentials.lean supplies the ⇐ direction in its own framing; everything here is the ⇒ direction.

The change of framing

There, clock j had its own law Exp bⱼ and the race was ξ i < ξ j. Here all clocks are iid with one unknown law μ, and the rate enters as a scaling: clock j fires at ξ j / b j. For the exponential the two framings agree (hasRaceProperty_expMeasure); for a general μ only the second makes sense, because "the law of the clock" is exactly what is being solved for.

• scaledRaceCell — the readings on which clock i fires first. scaledRaceCell_one records that at unit rates it is raceCell.
• ★★ measure_scaledRaceCell — the kernel identity: the winning probability is ∫ ∏ⱼ G(bⱼ/bᵢ · t) dμ(t), with G t = μ (Ioi t) the survival function (survival). No hypothesis on μ beyond being a probability measure, and — unlike the exponential case — the slice is a box at every t, not merely almost every one.
• HasRaceProperty — the hypothesis of §3c, quantified over every number of clocks.

★ What the k-clock family buys

Instantiating the race at rates (1, c, c, …, c) turns an integral equation into a moment sequence — ★★ HasRaceProperty.lintegral_measure_Ioi_pow gives E[G(cξ)ᵏ] = 1/(1 + kc), and ★★ …_pow_mul_pow the mixed form E[G(cξ)ᵖ G(ξ)ᵏ] = 1/(1 + pc + k). G(cξ) takes values in [0,1], where moments determine the law — which is why the two-clock version of the same question looks like Choquet–Deny and this one does not. Three consequences, in order:

1. ★★ HasRaceProperty.map_survival — G(ξ) is uniform on [0,1], with no regularity hypothesis on μ: the c = 1 moments are the uniform moments, so Hausdorff determinacy (MeasureTheory.ext_of_forall_integral_pow_eq_of_null_compl) closes it. Atomlessness of μ is therefore derived from the race property, not assumed of it.
2. ★★ HasRaceProperty.survival_natMul_ae — G(mt) = G(t)ᵐ almost everywhere, for every natural m. ★ The proof needs no quantile, no determinacy in two variables and no injectivity of G: when the ratio is a natural number, G(t)ᵐ is itself a product of m survival factors at rate 1, so all three terms of ∫ (G(mt) − G(t)ᵐ)² dμ are instances of the same race family and cancel.
3. ★ raceRate_le — the rate is the same at every good reading. The functional equation ties G together only along the lattice {mt}; antitonicity connects two lattices, because mt ≤ nt' forces G(t)ᵐ ≥ G(t')ⁿ. Letting the integer ratio climb to t'/t gives the comparison, and the real ratios the argument never had are not missed.

Then HasRaceProperty.exists_eq_expMeasure reads the law off through map_survival.

⚠️ The second conjunct is not optional

HasRaceProperty quantifies over the number of clocks, and that is load-bearing: at a fixed number of outcomes n the family supplies only n−1 moments, and finitely many moments determine nothing. What is forced is the exponential law given that one clock law serves every n — the measurement-independence of the fibre law that specs/sigma-fibre-contextuality.md commits to. Never state the conclusion without it.

Nothing here is a new physical claim: it removes a posit from the record layer's fibre construction rather than adding one.

Reference: specs/q12c-exponential-characterisation-route.md; specs/q12-fibre-mechanism-scoping.md; specs/record-layer-plan.md §3b–§3c; specs/sigma-fibre-contextuality.md; specs/future-work.md. See ProbabilityTheory.measure_raceCell for the ⇐ direction in the other framing and MeasureTheory.ext_of_forall_integral_pow_eq_of_null_compl for the determinacy step.

The race at general rates

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

The scaled race cell: the readings on which clock i fires first, when clock j reads ξ j and fires at ξ j / b j.

The rate enters by scaling the reading rather than by changing the law, which is what lets the law stay an unknown. At unit rates this is raceCell (scaledRaceCell_one).

Equations

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

@[simp]

theorem ProbabilityTheory.mem_scaledRaceCell {n : ℕ} {b : Fin (n + 1) → ℝ} {i : Fin (n + 1)} {ξ : Fin (n + 1) → ℝ} : ξ ∈ scaledRaceCell b i ↔ ∀ (j : Fin (n + 1)), j ≠ i → ξ i / b i < ξ j / b j

theorem ProbabilityTheory.scaledRaceCell_one {n : ℕ} (i : Fin (n + 1)) : scaledRaceCell (fun (x : Fin (n + 1)) => 1) i = raceCell i

At unit rates the scaled race is the plain race of CompetingExponentials.lean.

theorem ProbabilityTheory.measurableSet_scaledRaceCell {n : ℕ} (b : Fin (n + 1) → ℝ) (i : Fin (n + 1)) : MeasurableSet (scaledRaceCell b i)

theorem ProbabilityTheory.scaledRaceCell_pairwiseDisjoint {n : ℕ} (b : Fin (n + 1) → ℝ) : Pairwise (Function.onFun Disjoint (scaledRaceCell b))

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

theorem ProbabilityTheory.measure_scaledRaceCell {n : ℕ} (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (b : Fin (n + 1) → ℝ) (hb : ∀ (j : Fin (n + 1)), 0 < b j) (i : Fin (n + 1)) : (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => μ) (scaledRaceCell b i) = ∫⁻ (t : ℝ), ∏ j : Fin n, μ (Set.Ioi (b (i.succAbove j) / b i * t)) ∂μ

★★ The kernel identity. For iid clocks with law μ at rates b, clock i wins with probability ∫ ∏ⱼ G(bⱼ/bᵢ · t) dμ(t), where G t = μ (Ioi t) is the survival function and the product runs over the other clocks.

This is measure_raceCell with the exponential assumption removed and the integral left standing: there G was known and the integral could be evaluated, here G is the unknown. The proof splits coordinate i off the product (measurePreserving_piFinSuccAbove) and reads the remaining clocks' survival as a box (Measure.pi_pi) — and because the rates are carried by the scaling rather than by the law, the slice is a box at every t, so no almost-everywhere step is needed.

The race property, and the moment sequence it forces

def ProbabilityTheory.HasRaceProperty (μ : MeasureTheory.Measure ℝ) : Prop

The race property of specs/record-layer-plan.md §3c: for iid clocks with law μ, the first to fire is clock i with probability bᵢ / Σⱼ bⱼ, for every number of clocks and every positive rate vector.

The quantification over n is the load-bearing part and is not free — see the scope note in the module docstring. hasRaceProperty_expMeasure is the witness that the hypothesis is satisfiable.

Equations

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

theorem ProbabilityTheory.cons_one_pos {n : ℕ} {r : Fin n → ℝ} (hr : ∀ (j : Fin n), 0 < r j) (j : Fin (n + 1)) : 0 < Fin.cons 1 r j

Putting the winning clock at rate 1 in front of positive rates keeps every rate positive.

theorem ProbabilityTheory.measure_scaledRaceCell_cons_one {n : ℕ} (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (r : Fin n → ℝ) (hr : ∀ (j : Fin n), 0 < r j) : (MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => μ) (scaledRaceCell (Fin.cons 1 r) 0) = ∫⁻ (t : ℝ), ∏ j : Fin n, μ (Set.Ioi (r j * t)) ∂μ

The kernel identity at a unit-rate winner: clock 0 runs at rate 1 and the rest at rates r, so the ratios rⱼ/1 are the rates themselves.

theorem ProbabilityTheory.HasRaceProperty.lintegral_prod_measure_Ioi {n : ℕ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasRaceProperty μ) (r : Fin n → ℝ) (hr : ∀ (j : Fin n), 0 < r j) : ∫⁻ (t : ℝ), ∏ j : Fin n, μ (Set.Ioi (r j * t)) ∂μ = ENNReal.ofReal (1 / (1 + ∑ j : Fin n, r j))

★★ The race property turns into a family of moments. For any positive rates r on the losing clocks, ∫ ∏ⱼ G(rⱼ t) dμ(t) = 1/(1 + Σⱼ rⱼ).

This is step 1 of specs/q12c-exponential-characterisation-route.md in its general form; the two corollaries below are the instantiations the route uses.

theorem ProbabilityTheory.HasRaceProperty.lintegral_measure_Ioi_pow {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasRaceProperty μ) {c : ℝ} (hc : 0 < c) (k : ℕ) : ∫⁻ (t : ℝ), μ (Set.Ioi (c * t)) ^ k ∂μ = ENNReal.ofReal (1 / (1 + ↑k * c))

★★ (1) of the route memo. Racing one clock at rate 1 against k clocks at rate c gives the moment sequence E[G(cξ)ᵏ] = 1/(1 + kc).

The integral equation of the two-clock case has become a moment problem on [0,1], where the moments determine the law.

theorem ProbabilityTheory.HasRaceProperty.lintegral_measure_Ioi_pow_mul_pow {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasRaceProperty μ) {c : ℝ} (hc : 0 < c) (p k : ℕ) : ∫⁻ (t : ℝ), μ (Set.Ioi (c * t)) ^ p * μ (Set.Ioi t) ^ k ∂μ = ENNReal.ofReal (1 / (1 + ↑p * c + ↑k))

★★ The mixed moments, at rates (1, c^p, 1^k): E[G(cξ)ᵖ G(ξ)ᵏ] = 1/(1 + pc + k).

This is the form step 3′ consumes. At p = 1 the left-hand side is a fixed continuous weight integrated against every power of G(ξ), which is exactly the hypothesis of MeasureTheory.eq_of_forall_integral_mul_pow_eq — so no joint law, no rearrangement theory and no two-dimensional determinacy is needed.

Non-vacuity: the exponential laws have the race property

theorem ProbabilityTheory.hasRaceProperty_expMeasure {r : ℝ} (hr : 0 < r) : HasRaceProperty (expMeasure r)

The hypothesis is satisfiable. Every exponential law has the race property — which is the ⇐ direction of §3c in the iid framing, and the check that HasRaceProperty is not vacuous.

Compare measure_raceCell, which is the same fact in the other framing: there the rate lived in the law (Exp bⱼ) and the race was unscaled; here one law serves every clock and the rate scales the reading. The two agree because ξ / b is Exp (rb) when ξ is Exp r — visible in the proof as the rate r cancelling out of r / (r + r·S/bᵢ).

Step 2: the race property forces the survival function to be uniform

noncomputable def ProbabilityTheory.survival (μ : MeasureTheory.Measure ℝ) (t : ℝ) : ℝ

The survival function G t = P(ξ > t) of a law on the line, as a real-valued function.

Real-valued, whereas the kernel identity above states the same thing in ℝ≥0∞ because that is where lintegral lives: the analytic half of the route consumes a continuous real function (MeasureTheory.eq_of_forall_integral_mul_pow_eq lives on C(Icc a b, ℝ)), and this is the form it wants.

Equations

• ProbabilityTheory.survival μ t = (μ (Set.Ioi t)).toReal

theorem ProbabilityTheory.survival_nonneg (μ : MeasureTheory.Measure ℝ) (t : ℝ) : 0 ≤ survival μ t

theorem ProbabilityTheory.survival_le_one (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (t : ℝ) : survival μ t ≤ 1

theorem ProbabilityTheory.survival_mem_Icc (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (t : ℝ) : survival μ t ∈ Set.Icc 0 1

theorem ProbabilityTheory.antitone_survival (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] : Antitone (survival μ)

theorem ProbabilityTheory.measurable_survival (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] : Measurable (survival μ)

theorem ProbabilityTheory.integral_survival_pow (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) : ∫ (t : ℝ), survival μ t ^ k ∂μ = (∫⁻ (t : ℝ), μ (Set.Ioi t) ^ k ∂μ).toReal

The ℝ≥0∞ form of the moment identity, read back as a real integral of survival.

theorem ProbabilityTheory.HasRaceProperty.map_survival {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasRaceProperty μ) : MeasureTheory.Measure.map (survival μ) μ = MeasureTheory.volume.restrict (Set.Icc 0 1)

★★ Step 2 — the probability integral transform, and the regularity comes free.

G(ξ) is uniform on [0,1].

The route memo assumes G continuous and strictly decreasing, and reaches this by the standard probability integral transform. It does not have to: the c = 1 case of the moment family already says E[G(ξ)ᵏ] = 1/(1+k) for every k, and those are exactly the moments of the uniform law, so Hausdorff determinacy (MeasureTheory.ext_of_forall_integral_pow_eq_of_null_compl) delivers the conclusion with no hypothesis on μ at all.

So atomlessness of μ is a consequence of the race property rather than an assumption on it — as it must be, since the k+1-clock race at equal rates says the smallest of k+1 iid readings is strictly smallest with probability 1/(k+1), and ties would cost.

Step 3: the multiplicative functional equation, almost everywhere

theorem ProbabilityTheory.ofReal_survival (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (t : ℝ) : ENNReal.ofReal (survival μ t) = μ (Set.Ioi t)

theorem ProbabilityTheory.measurable_survival_pow_mul_pow (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsFiniteMeasure μ] (c : ℝ) (p k : ℕ) : Measurable fun (t : ℝ) => survival μ (c * t) ^ p * survival μ t ^ k

theorem ProbabilityTheory.survival_pow_mul_pow_nonneg (μ : MeasureTheory.Measure ℝ) (c : ℝ) (p k : ℕ) (t : ℝ) : 0 ≤ survival μ (c * t) ^ p * survival μ t ^ k

theorem ProbabilityTheory.integrable_survival_pow_mul_pow (μ : MeasureTheory.Measure ℝ) [MeasureTheory.IsProbabilityMeasure μ] (c : ℝ) (p k : ℕ) : MeasureTheory.Integrable (fun (t : ℝ) => survival μ (c * t) ^ p * survival μ t ^ k) μ

theorem ProbabilityTheory.HasRaceProperty.integral_survival_pow_mul_pow {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasRaceProperty μ) {c : ℝ} (hc : 0 < c) (p k : ℕ) : ∫ (t : ℝ), survival μ (c * t) ^ p * survival μ t ^ k ∂μ = 1 / (1 + ↑p * c + ↑k)

The mixed moment identity as a real integral of survival.

theorem ProbabilityTheory.HasRaceProperty.survival_natMul_ae {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasRaceProperty μ) {m : ℕ} (hm : 0 < m) : ∀ᵐ (t : ℝ) ∂μ, survival μ (↑m * t) = survival μ t ^ m

★★ The multiplicative functional equation. For every m ≥ 1, G(mt) = G(t)ᵐ for μ-almost every t.

★ This is the route's real surprise, and it replaces all three of the assemblies the memo had mapped — no quantile G⁻¹, no two-dimensional determinacy, no injectivity of G. The reason is that when the ratio is a natural number m, the function G(t)ᵐ is itself a product of m survival factors at rate 1, so all three terms of ∫ (G(mt) − G(t)ᵐ)² dμ are instances of the same race family:

• ∫ G(mt)² dμ = 1/(1+2m) at rates (1, m, m);
• ∫ G(mt)·G(t)ᵐ dμ = 1/(1+2m) at rates (1, m, 1ᵐ);
• ∫ G(t)²ᵐ dμ = 1/(1+2m) at rates (1, 1²ᵐ).

They cancel, so the square has integral zero and vanishes almost everywhere. Restricting the ratio to the integers is exactly what makes the cross term computable — and HasRaceProperty.eq_expMeasure shows the integers are enough, because monotonicity supplies what the missing real ratios would have.

Step 4: from the functional equation to the exponential law

theorem ProbabilityTheory.HasRaceProperty.survival_mem_Ioo_ae {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasRaceProperty μ) : ∀ᵐ (t : ℝ) ∂μ, survival μ t ∈ Set.Ioo 0 1

The survival function avoids both endpoints almost everywhere — immediate from step 2, since {0, 1} is Lebesgue-null.

theorem ProbabilityTheory.HasRaceProperty.pos_ae {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasRaceProperty μ) : ∀ᵐ (t : ℝ) ∂μ, 0 < t

The clock readings are almost surely positive — derived, not assumed.

The route memo sets the problem up with ξ supported on (0,∞); it does not have to. Antitonicity plus the m = 2 case of the functional equation is enough: for t ≤ 0 one has 2t ≤ t, so G(t) ≤ G(2t) = G(t)², which is false for G(t) ∈ (0,1).

def ProbabilityTheory.RaceRegular (μ : MeasureTheory.Measure ℝ) (t : ℝ) : Prop

A good reading: positive, with the survival function strictly inside (0,1), and satisfying the whole multiplicative family. HasRaceProperty.ae_regular says almost every reading is good; everything after this point is an argument about good readings and their ratios to one another.

Equations

• ProbabilityTheory.RaceRegular μ t = (0 < t ∧ ProbabilityTheory.survival μ t ∈ Set.Ioo 0 1 ∧ ∀ (m : ℕ), 0 < m → ProbabilityTheory.survival μ (↑m * t) = ProbabilityTheory.survival μ t ^ m)

theorem ProbabilityTheory.HasRaceProperty.ae_regular {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasRaceProperty μ) : ∀ᵐ (t : ℝ) ∂μ, RaceRegular μ t

The three almost-everywhere facts, bundled: positivity, both endpoints avoided, and the whole multiplicative family at once (a countable intersection, via ae_all_iff).

noncomputable def ProbabilityTheory.raceRate (μ : MeasureTheory.Measure ℝ) (t : ℝ) : ℝ

The rate read off at a good reading: the λ for which G t = e^{-λt} at that one point.

Equations

• ProbabilityTheory.raceRate μ t = -Real.log (ProbabilityTheory.survival μ t) / t

theorem ProbabilityTheory.raceRate_pos {μ : MeasureTheory.Measure ℝ} {t : ℝ} (ht : RaceRegular μ t) : 0 < raceRate μ t

theorem ProbabilityTheory.survival_eq_exp_raceRate {μ : MeasureTheory.Measure ℝ} {t : ℝ} (ht : RaceRegular μ t) : survival μ t = Real.exp (-(raceRate μ t * t))

theorem ProbabilityTheory.raceRate_le {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] {t t' : ℝ} (ht : RaceRegular μ t) (ht' : RaceRegular μ t') : raceRate μ t ≤ raceRate μ t'

★ The rate is the same at every good reading, which is what makes the integer ratios of survival_natMul_ae enough to pin the law down.

The functional equation ties G together only along the lattice {mt}, and a priori nothing connects the lattices of two different readings. Antitonicity connects them: whenever mt ≤ nt' one has G(t)ᵐ = G(mt) ≥ G(nt') = G(t')ⁿ, so m·λ(t)·t ≤ n·λ(t')·t'. Letting the integer ratio m/n climb to t'/t gives λ(t) ≤ λ(t'), and symmetry gives equality. Neither density of the support nor a real ratio is needed anywhere.

theorem ProbabilityTheory.HasRaceProperty.exists_eq_expMeasure {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] (h : HasRaceProperty μ) : ∃ (lam : ℝ), 0 < lam ∧ μ = expMeasure lam

★★★ The race property forces the exponential law.

This is the ⇒ direction of specs/record-layer-plan.md §3c: if for every number of clocks and every positive rate vector the first of n iid clocks to fire is clock i with probability bᵢ/Σⱼbⱼ, then the clock law is exponential. With hasRaceProperty_expMeasure for the converse it is the characterisation.

⚠️ The second conjunct travels with the first. HasRaceProperty quantifies over the number of clocks, and that is not a formality: at a fixed number of outcomes n the family supplies only n−1 moments, and finitely many moments determine nothing. So what is forced is the exponential law given that one clock law serves every n — the measurement-independence of the fibre law that specs/sigma-fibre-contextuality.md commits to. Never state the conclusion without it.

theorem ProbabilityTheory.hasRaceProperty_iff_exists_expMeasure {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsProbabilityMeasure μ] : HasRaceProperty μ ↔ ∃ (lam : ℝ), 0 < lam ∧ μ = expMeasure lam

★★★ The characterisation of specs/record-layer-plan.md §3c: for iid linear clocks, first-to-fire is proportional to the rate iff the waiting times are exponential.

The ⇐ direction is hasRaceProperty_expMeasure; the ⇒ direction is HasRaceProperty.exists_eq_expMeasure, and it carries the second conjunct documented there — HasRaceProperty quantifies over the number of clocks, so what is characterised is the law that serves every n.