diff --git a/Physlib.lean b/Physlib.lean
index 963a36361..a3e0494e0 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -253,6 +253,21 @@ public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.Yukawa
 public import Physlib.Particles.SuperSymmetry.SU5.ChargeSpectrum.ZMod
 public import Physlib.Particles.SuperSymmetry.SU5.FieldLabels
 public import Physlib.Particles.SuperSymmetry.SU5.Potential
+public import Physlib.ProbabilisticTheory.Channel.Basic
+public import Physlib.ProbabilisticTheory.Effect.Basic
+public import Physlib.ProbabilisticTheory.Effect.Complement
+public import Physlib.ProbabilisticTheory.Effect.Convex
+public import Physlib.ProbabilisticTheory.Effect.Metric
+public import Physlib.ProbabilisticTheory.Effect.Sharp
+public import Physlib.ProbabilisticTheory.OrderUnit.Archimedean
+public import Physlib.ProbabilisticTheory.OrderUnit.Basic
+public import Physlib.ProbabilisticTheory.OrderUnit.Cone
+public import Physlib.ProbabilisticTheory.State.Basic
+public import Physlib.ProbabilisticTheory.State.Convex
+public import Physlib.ProbabilisticTheory.State.Discrimination
+public import Physlib.ProbabilisticTheory.State.Metric
+public import Physlib.ProbabilisticTheory.Weight.Basic
+public import Physlib.ProbabilisticTheory.Weight.Extension
 public import Physlib.QFT.AnomalyCancellation.Basic
 public import Physlib.QFT.AnomalyCancellation.GroupActions
 public import Physlib.QFT.PerturbationTheory.CreateAnnihilate
diff --git a/Physlib/ProbabilisticTheory/Channel/Basic.lean b/Physlib/ProbabilisticTheory/Channel/Basic.lean
new file mode 100644
index 000000000..e0350a64c
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Channel/Basic.lean
@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Mathlib.Algebra.Order.Module.PositiveLinearMap
+
+/-!
+# Positive unital maps
+
+## i. Overview
+
+A channel is the most general physical transformation the theory allows: time evolution, noise,
+or a measurement whose outcome is never recorded. Whatever it does, it must send observables to
+observables without turning a possible outcome negative, and it must leave the certain outcome
+certain. In the Heisenberg picture, where a channel acts on observables rather than states,
+that's exactly a positive linear map preserving the distinguished unit.
+
+## ii. Key results
+
+- `UnitalPositiveLinearMap` : a positive linear map preserving `1`, notated `E →ₚ₁[R] F`.
+- `UnitalPositiveLinearMap.ofLinearMap` : bundle a linear map after checking positivity and
+  unitality.
+
+## iii. Table of contents
+
+- A. Unital positive linear maps
+- B. Constructing unital positive linear maps
+
+-/
+
+@[expose] public section
+
+/-!
+
+## A. Unital positive linear maps
+
+-/
+
+/-- A positive linear map preserving `1`. -/
+structure UnitalPositiveLinearMap (R E F : Type*) [Semiring R]
+    [AddCommMonoid E] [PartialOrder E] [AddCommMonoid F] [PartialOrder F]
+    [Module R E] [Module R F] [One E] [One F] extends E →ₚ[R] F, OneHom E F
+
+attribute [nolint docBlame] UnitalPositiveLinearMap.toOneHom
+
+/-- Notation for positive unital linear maps. -/
+notation:25 E " →ₚ₁[" R:25 "] " F:0 => UnitalPositiveLinearMap R E F
+
+namespace UnitalPositiveLinearMap
+
+variable {R E F : Type*} [Semiring R]
+  [AddCommMonoid E] [PartialOrder E] [AddCommMonoid F] [PartialOrder F]
+  [Module R E] [Module R F] [One E] [One F]
+
+instance : FunLike (E →ₚ₁[R] F) E F where
+  coe f := f.toFun
+  coe_injective f g h := by
+    cases f
+    cases g
+    congr
+    exact DFunLike.coe_injective h
+
+instance : LinearMapClass (E →ₚ₁[R] F) R E F where
+  map_add f := map_add f.toLinearMap
+  map_smulₛₗ f := f.toLinearMap.map_smul'
+
+instance : OrderHomClass (E →ₚ₁[R] F) E F where
+  map_rel f {_ _} h := f.monotone' h
+
+instance : OneHomClass (E →ₚ₁[R] F) E F where
+  map_one f := f.map_one'
+
+@[ext]
+lemma ext {f g : E →ₚ₁[R] F} (h : ∀ x, f x = g x) : f = g :=
+  DFunLike.ext f g h
+
+/-- Unital positive linear maps are determined by their underlying linear map. -/
+lemma toLinearMap_injective : Function.Injective (fun f : E →ₚ₁[R] F => f.toLinearMap) :=
+  fun _ _ h => ext fun x => congrArg (fun k : E →ₗ[R] F => k x) h
+
+end UnitalPositiveLinearMap
+
+namespace UnitalPositiveLinearMap
+
+variable {R E F : Type*} [Semiring R]
+  [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E]
+  [AddCommGroup F] [PartialOrder F] [IsOrderedAddMonoid F]
+  [Module R E] [Module R F] [One E] [One F]
+
+/-!
+
+## B. Constructing unital positive linear maps
+
+-/
+
+/-- Bundle a linear map after proving only positivity and preservation of `1`. -/
+def ofLinearMap (f : E →ₗ[R] F) (hpos : ∀ x, 0 ≤ x → 0 ≤ f x) (hone : f 1 = 1) : E →ₚ₁[R] F where
+  toPositiveLinearMap := PositiveLinearMap.mk₀ f hpos
+  map_one' := hone
+
+end UnitalPositiveLinearMap
diff --git a/Physlib/ProbabilisticTheory/Effect/Basic.lean b/Physlib/ProbabilisticTheory/Effect/Basic.lean
new file mode 100644
index 000000000..1ca3d35bb
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Effect/Basic.lean
@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Mathlib.Order.Interval.Set.Defs
+public import Physlib.ProbabilisticTheory.OrderUnit.Basic
+public import Physlib.ProbabilisticTheory.OrderUnit.Cone
+
+/-!
+# Effects
+
+## i. Overview
+
+An effect models a yes/no measurement outcome, ranging continuously between the impossible
+outcome `0` and the certain outcome `1`. Formally, it is a point of the order interval `[0, 1]`
+inside `E`. For self-adjoint matrices, effects are exactly the operators `0 ≤ M ≤ 1` — the
+elements of a POVM.
+
+## ii. Key results
+
+- `Effect` : a bounded measurement outcome, the order interval `[0, 1]`.
+- `Effect.mem_iff_mem_posCone_and_one_sub_mem_posCone` : an effect is exactly a positive element
+  whose complement from the order unit is also positive.
+- `Effect.exists_pos_smul_mem` : every positive observable becomes an effect after scaling it down
+  enough.
+
+## iii. Table of contents
+
+- A. Effects
+
+## iv. References
+
+- G. Ludwig, *Foundations of Quantum Mechanics I*, Springer, 1983.
+  <https://link.springer.com/book/10.1007/978-3-642-86751-4>
+
+-/
+
+@[expose] public section
+
+/-!
+
+## A. Effects
+
+-/
+
+/-- A bounded measurement outcome. -/
+abbrev Effect (E : Type*) [PartialOrder E] [One E] [Zero E] := Set.Icc (0 : E) 1
+
+namespace Effect
+
+section OrderedVectorSpace
+
+variable {E : Type*} [OrderedVectorSpace E] [One E]
+
+/-- An effect is a positive element whose complement from the order unit is positive. -/
+lemma mem_iff_mem_posCone_and_one_sub_mem_posCone {A : E} :
+    A ∈ (Effect E : Set E) ↔ A ∈ PosCone E ∧ 1 - A ∈ PosCone E := by
+  simp only [Set.mem_Icc, PointedCone.mem_positive, sub_nonneg]
+
+end OrderedVectorSpace
+
+section OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+/-- Every nonnegative observable becomes an effect after scaling it down by a large enough
+positive real: the effect interval reaches in every direction the positive cone does. -/
+lemma exists_pos_smul_mem {B : E} (hB : 0 ≤ B) :
+    ∃ r : ℝ, 0 < r ∧ r • B ∈ (Effect E : Set E) := by
+  obtain ⟨n, hn⟩ := OrderUnitSpace.exists_nsmul_one_le B
+  have hn1 : (0 : ℝ) < (n : ℝ) + 1 := by positivity
+  refine ⟨((n : ℝ) + 1)⁻¹, by positivity, smul_nonneg (by positivity) hB, ?_⟩
+  have hBr : B ≤ ((n : ℝ) + 1) • (1 : E) :=
+    calc
+      B ≤ n • (1 : E) := hn
+      _ = (n : ℝ) • (1 : E) := (Nat.cast_smul_eq_nsmul ℝ n (1 : E)).symm
+      _ ≤ ((n : ℝ) + 1) • (1 : E) :=
+        smul_le_smul_of_nonneg_right (by linarith) OrderUnitSpace.one_nonneg
+  have hs := smul_le_smul_of_nonneg_left hBr (by positivity : (0 : ℝ) ≤ ((n : ℝ) + 1)⁻¹)
+  simpa [smul_smul, hn1.ne'] using hs
+
+end OrderUnitSpace
+
+end Effect
diff --git a/Physlib/ProbabilisticTheory/Effect/Complement.lean b/Physlib/ProbabilisticTheory/Effect/Complement.lean
new file mode 100644
index 000000000..10d8491b3
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Effect/Complement.lean
@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.OrderUnit.Basic
+public import Physlib.ProbabilisticTheory.Effect.Basic
+public import Physlib.ProbabilisticTheory.Effect.Convex
+public import Mathlib.Tactic.Module
+
+/-!
+# Complementary effects
+
+## i. Overview
+
+The complement of an effect `e` is the yes/no test that fires exactly when `e` doesn't: `1 - e`.
+Physically, a state's probability of "no" is always `1` minus its probability of "yes".
+
+## ii. Key results
+
+- `Effect.complement` : the complementary effect `1 - e`.
+- `Effect.complement_antitone` : the complement reverses order.
+- `Effect.complement_mix` : the complement of a mixture is the mixture of the complements.
+
+## iii. Table of contents
+
+- A. The complement
+- B. Monotonicity of the complement
+- C. The complement and mixtures
+
+-/
+
+@[expose] public section
+
+namespace Effect
+
+section OrderedVectorSpace
+
+variable {E : Type*} [OrderedVectorSpace E] [One E]
+
+/-!
+
+## A. The complement
+
+-/
+
+/-- The complementary effect. -/
+def complement (e : Effect E) : Effect E :=
+  ⟨1 - e.1, sub_nonneg.mpr e.2.2, sub_le_self 1 e.2.1⟩
+
+@[simp]
+lemma complement_complement (e : Effect E) : complement (complement e) = e := by
+  apply Subtype.ext
+  simp [complement]
+
+/-!
+
+## B. Monotonicity of the complement
+
+-/
+
+/-- The complement reverses order: a more certain test's complement is a less certain one. -/
+lemma complement_antitone : Antitone (complement (E := E)) :=
+  fun _ _ h => sub_le_sub_left (show (_ : E) ≤ _ from h) 1
+
+end OrderedVectorSpace
+
+section OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+instance : Zero (Effect E) := ⟨0, le_refl 0, OrderUnitSpace.one_nonneg⟩
+instance : One (Effect E) := ⟨1, OrderUnitSpace.one_nonneg, le_refl 1⟩
+instance : Nonempty (Effect E) := ⟨0⟩
+
+@[simp] lemma coe_zero : ((0 : Effect E) : E) = 0 := rfl
+
+@[simp] lemma coe_one : ((1 : Effect E) : E) = 1 := rfl
+
+@[simp]
+lemma complement_zero : complement (0 : Effect E) = 1 := by
+  apply Subtype.ext
+  simp [complement]
+
+@[simp]
+lemma complement_one : complement (1 : Effect E) = 0 := by
+  apply Subtype.ext
+  simp [complement]
+
+/-!
+
+## C. The complement and mixtures
+
+-/
+
+/-- Mixing commutes with taking the complement. -/
+lemma complement_mix (e f : Effect E) (t : unitInterval) :
+    complement (mix e f t) = mix (complement e) (complement f) t := by
+  apply Subtype.ext
+  show (1 : E) - ((t : ℝ) • (e : E) + (1 - (t : ℝ)) • (f : E))
+      = (t : ℝ) • ((1 : E) - (e : E)) + (1 - (t : ℝ)) • ((1 : E) - (f : E))
+  module
+
+end OrderUnitSpace
+
+end Effect
diff --git a/Physlib/ProbabilisticTheory/Effect/Convex.lean b/Physlib/ProbabilisticTheory/Effect/Convex.lean
new file mode 100644
index 000000000..55a106ff6
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Effect/Convex.lean
@@ -0,0 +1,56 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.Effect.Basic
+public import Mathlib.Topology.UnitInterval
+
+/-!
+# Convexity and mixtures of effects
+
+## i. Overview
+
+The effect interval `[0, 1]` is convex: randomizing between two effects with some probability
+gives back an effect. Physically, flipping a biased coin to decide which of two measurements to
+actually run is itself a legitimate measurement.
+
+## ii. Key results
+
+- `Effect.convex` : the effect interval is convex.
+- `Effect.mix` : randomize between two effects with a given probability.
+
+## iii. Table of contents
+
+- A. Convexity and mixtures of effects
+
+-/
+
+@[expose] public section
+
+variable {E : Type*} [OrderedVectorSpace E] [One E]
+
+namespace Effect
+
+/-!
+
+## A. Convexity and mixtures of effects
+
+-/
+
+/-- The effect interval is convex. -/
+lemma convex : Convex ℝ (Effect E : Set E) := convex_Icc 0 1
+
+/-- Randomize between two effects with probability `t` of testing the first. -/
+noncomputable def mix (e f : Effect E) (t : unitInterval) : Effect E :=
+  ⟨(t : ℝ) • (e : E) + (1 - (t : ℝ)) • (f : E),
+    convex e.2 f.2 t.2.1 (sub_nonneg.mpr t.2.2) (by ring)⟩
+
+/-- Evaluation of a mixture is the pointwise convex combination. -/
+@[simp]
+lemma coe_mix (e f : Effect E) (t : unitInterval) :
+    ((mix e f t : Effect E) : E) = (t : ℝ) • (e : E) + (1 - (t : ℝ)) • (f : E) := rfl
+
+end Effect
diff --git a/Physlib/ProbabilisticTheory/Effect/Metric.lean b/Physlib/ProbabilisticTheory/Effect/Metric.lean
new file mode 100644
index 000000000..c743fbee4
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Effect/Metric.lean
@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.Effect.Basic
+public import Physlib.ProbabilisticTheory.OrderUnit.Archimedean
+public import Mathlib.Topology.MetricSpace.Defs
+
+/-!
+# The metric space of effects
+
+## i. Overview
+
+Effects sit inside `E`, so pulling back the order-unit norm along the inclusion `Effect E ↪ E`
+gives them a metric space structure for free.
+
+Effects also correspond to points of the order-unit-norm ball, by the affine rescaling
+`e ↦ 2 • e - 1` that turns `[0, 1]` into the symmetric `[-1, 1]` the norm itself ranges over.
+
+## ii. Key results
+
+- `Effect.dist_eq_orderUnitNorm` : the effect metric is the order-unit norm of the difference.
+- `Effect.equivBall` : effects correspond to points of the order-unit-norm ball.
+
+## iii. Table of contents
+
+- A. The effect metric
+- B. Effects as points of the order-unit-norm ball
+
+-/
+
+@[expose] public section
+
+open ArchimedeanOrderUnitSpace
+
+variable {E : Type*} [ArchimedeanOrderUnitSpace E]
+
+namespace Effect
+
+/-!
+
+## A. The effect metric
+
+-/
+
+/-- Effects, metrized by restricting the order-unit norm: pulling back the normed group structure
+on `E` along the inclusion `Effect E ↪ E` -/
+noncomputable instance : MetricSpace (Effect E) :=
+  MetricSpace.induced Subtype.val Subtype.val_injective inferInstance
+
+lemma dist_eq_orderUnitNorm (e f : Effect E) : dist e f = orderUnitNorm ((e : E) - (f : E)) :=
+  dist_eq_norm (e : E) (f : E)
+
+/-!
+
+## B. Effects as points of the order-unit-norm ball
+
+-/
+
+/-- Doubling and re-centering an effect at the order unit lands in the order-unit-norm ball. -/
+lemma orderUnitNorm_two_smul_sub_one_le_one (e : Effect E) :
+    orderUnitNorm ((2 : ℝ) • (e : E) - 1) ≤ 1 := by
+  rw [orderUnitNorm_le_iff]
+  refine ⟨by norm_num, ?_, ?_⟩
+  · rw [one_smul, ← sub_nonneg,
+      show (2 : ℝ) • (e : E) - 1 - -(1 : E) = (2 : ℝ) • (e : E) from by module]
+    exact smul_nonneg (by norm_num) e.2.1
+  · rw [one_smul, ← sub_nonneg,
+      show (1 : E) - ((2 : ℝ) • (e : E) - 1) = (2 : ℝ) • (1 - (e : E)) from by module]
+    exact smul_nonneg (by norm_num) (sub_nonneg.mpr e.2.2)
+
+/-- Undoing the re-centering on a point of the order-unit-norm ball gives back an effect. -/
+lemma mem_effect_two_inv_smul_one_add (A : {A : E // orderUnitNorm A ≤ 1}) :
+    (2 : ℝ)⁻¹ • (1 + (A : E)) ∈ (Effect E : Set E) := by
+  obtain ⟨-, hAl, hAu⟩ := orderUnitNorm_le_iff.mp A.2
+  rw [one_smul] at hAl hAu
+  refine ⟨smul_nonneg (by norm_num) (by simpa using add_le_add (le_refl (1 : E)) hAl), ?_⟩
+  have h := add_le_add (le_refl (1 : E)) hAu
+  rw [show (1 : E) + 1 = (2 : ℝ) • (1 : E) from by module] at h
+  have h2 := smul_le_smul_of_nonneg_left h (show (0 : ℝ) ≤ (2 : ℝ)⁻¹ by norm_num)
+  rwa [smul_smul, inv_mul_cancel₀ (two_ne_zero), one_smul] at h2
+
+/-- Re-centering, then undoing it, returns the original effect. -/
+lemma two_inv_smul_one_add_two_smul_sub_one (e : Effect E) :
+    (2 : ℝ)⁻¹ • (1 + ((2 : ℝ) • (e : E) - 1)) = (e : E) := by module
+
+/-- Undoing the re-centering, then redoing it, returns the original ball point. -/
+lemma two_smul_two_inv_smul_one_add_sub_one (A : {A : E // orderUnitNorm A ≤ 1}) :
+    (2 : ℝ) • ((2 : ℝ)⁻¹ • (1 + (A : E))) - 1 = (A : E) := by
+  rw [smul_smul, mul_inv_cancel₀ (two_ne_zero), one_smul]
+  module
+
+/-- Effects correspond to points of the order-unit-norm ball by doubling and re-centering at the
+order unit: `e ↦ 2 • e - 1`, with inverse `A ↦ (1 + A) / 2`. -/
+noncomputable def equivBall : Effect E ≃ {A : E // orderUnitNorm A ≤ 1} where
+  toFun e := ⟨(2 : ℝ) • (e : E) - 1, orderUnitNorm_two_smul_sub_one_le_one e⟩
+  invFun A := ⟨(2 : ℝ)⁻¹ • (1 + (A : E)), mem_effect_two_inv_smul_one_add A⟩
+  left_inv e := Subtype.ext (two_inv_smul_one_add_two_smul_sub_one e)
+  right_inv A := Subtype.ext (two_smul_two_inv_smul_one_add_sub_one A)
+
+end Effect
diff --git a/Physlib/ProbabilisticTheory/Effect/Sharp.lean b/Physlib/ProbabilisticTheory/Effect/Sharp.lean
new file mode 100644
index 000000000..a8c46b94f
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Effect/Sharp.lean
@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.Effect.Complement
+public import Physlib.ProbabilisticTheory.Effect.Convex
+public import Mathlib.Analysis.Convex.Strict.Extreme
+
+/-!
+# Sharp effects
+
+## i. Overview
+
+The effect interval `[0, 1]` is convex. A sharp effect is an extreme point of it: one that cannot
+be written as a nontrivial mixture of two distinct effects. Sharp effects generalize projections.
+
+## ii. Key results
+
+- `Effect.IsSharp` : an effect that cannot be written as a nontrivial mixture of two distinct
+  effects.
+- `Effect.isSharp_complement_iff` : sharpness is preserved by taking the complement.
+
+## iii. Table of contents
+
+- A. Sharp effects
+
+-/
+
+@[expose] public section
+
+namespace Effect
+
+section OrderedVectorSpace
+
+variable {E : Type*} [OrderedVectorSpace E] [One E]
+
+/-!
+
+## A. Sharp effects
+
+-/
+
+/-- An effect is sharp when it is an extreme point of the effect interval: it cannot be written as
+a nontrivial mixture of two distinct effects. -/
+def IsSharp (e : Effect E) : Prop := (e : E) ∈ Set.extremePoints ℝ (Set.Icc (0 : E) 1)
+
+end OrderedVectorSpace
+
+section OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+/-- The impossible outcome 0 is sharp. -/
+lemma isSharp_zero : IsSharp (0 : Effect E) := by
+  refine ⟨⟨le_refl 0, OrderUnitSpace.one_nonneg⟩,
+    fun x₁ hx₁ _ hx₂ ⟨a, b, ha, hb, _, hz⟩ => ?_⟩
+  have hax : a • x₁ = 0 :=
+    PosCone.nonneg_add_eq_zero
+      (smul_nonneg ha.le hx₁.1) (smul_nonneg hb.le hx₂.1) (by simpa using hz)
+  have := congrArg (a⁻¹ • ·) hax
+  rwa [inv_smul_smul₀ ha.ne', smul_zero] at this
+
+/-- Sharpness is preserved by taking the complement:
+`e ↦ 1 - e` is an affine involution of the effect interval. -/
+lemma isSharp_complement {e : Effect E} (h : IsSharp e) : IsSharp (complement e) := by
+  refine ⟨(complement e).2, fun x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, hab, hz⟩ => ?_⟩
+  have hone : a • (1 : E) + b • (1 : E) = 1 := by rw [← add_smul, hab, one_smul]
+  have key : a • (1 - x₁) + b • (1 - x₂) = (e : E) := by
+    have hsplit : a • (1 - x₁) + b • (1 - x₂) =
+        (a • (1 : E) + b • (1 : E)) - (a • x₁ + b • x₂) := by
+      simp only [smul_sub]; abel
+    rw [hsplit, hone, hz]
+    show (1 : E) - (1 - (e : E)) = (e : E)
+    abel
+  have x1eq := (mem_extremePoints_iff_left.mp h).2 (1 - x₁)
+    ⟨sub_nonneg.mpr hx₁.2, sub_le_self 1 hx₁.1⟩ (1 - x₂)
+    ⟨sub_nonneg.mpr hx₂.2, sub_le_self 1 hx₂.1⟩ ⟨a, b, ha, hb, hab, key⟩
+  have hsum : x₁ + (e : E) = 1 := by rw [← x1eq]; abel
+  exact eq_sub_of_add_eq hsum
+
+/-- Sharpness is preserved by taking the complement, in either direction. -/
+lemma isSharp_complement_iff {e : Effect E} : IsSharp (complement e) ↔ IsSharp e :=
+  ⟨fun h => complement_complement e ▸ isSharp_complement h, isSharp_complement⟩
+
+/-- The certain outcome 1 is sharp. -/
+lemma isSharp_one : IsSharp (1 : Effect E) :=
+  complement_zero (E := E) ▸ isSharp_complement isSharp_zero
+
+end OrderUnitSpace
+
+end Effect
diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean b/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean
new file mode 100644
index 000000000..986c2bea2
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/OrderUnit/Archimedean.lean
@@ -0,0 +1,353 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Mathlib.Analysis.Normed.Module.Basic
+public import Mathlib.Topology.Sequences
+public import Mathlib.Topology.Order.OrderClosed
+public import Physlib.ProbabilisticTheory.OrderUnit.Basic
+
+/-!
+
+# Archimedean order-unit spaces
+
+## i. Overview
+
+The Archimedean condition is a regularity assumption on an order-unit space that rules out
+infinitesimal elements. With it, the order and the distinguished unit `1` determine a natural
+norm,
+
+`‖A‖₁ = inf {r ≥ 0 | -r • 1 ≤ A ≤ r • 1}`.
+
+Thus the unit interval sets the scale of the theory: `[-1, 1]` is exactly the closed unit ball. For
+self-adjoint matrices, this recovers the usual operator norm. Concretely, this is the Minkowski
+functional of the order interval `[-1, 1]`: convexity of that interval gives the triangle
+inequality, and its symmetry gives homogeneity, for free. The Archimedean condition is only needed
+afterwards, to upgrade this from a seminorm to a genuine norm.
+
+This file develops the norm as an explicit function. When a Mathlib result requires typeclass
+norms, the corresponding structures are available for local installation.
+
+## ii. Key results
+
+- `ArchimedeanOrderUnitSpace.orderUnitNorm_eq_zero_iff` : the order-unit norm separates points.
+- `ArchimedeanOrderUnitSpace.closedIciTopology` : the positive cone is closed in the order-unit-norm
+  topology.
+
+## iii. Table of contents
+
+- A. Archimedean order units
+- B. The order-unit bounds and norm
+- C. Norm axioms
+- D. The induced normed space
+- E. Order-closedness of the topology
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+/-!
+
+## A. Archimedean order units
+
+-/
+
+/-- An order-unit space whose distinguished order unit is Archimedean. -/
+class ArchimedeanOrderUnitSpace (E : Type*) extends OrderUnitSpace E where
+  /-- If `A` is smaller than every positive multiple of `1`, `A` is already `≤ 0`. -/
+  le_zero_of_forall_pos_smul_one_le : ∀ A : E, (∀ ε : ℝ, 0 < ε → A ≤ ε • (1 : E)) → A ≤ 0
+
+/-- The real numbers form an Archimedean order-unit space. -/
+instance instArchimedeanOrderUnitSpaceReal : ArchimedeanOrderUnitSpace ℝ where
+  one_nonneg := zero_le_one
+  exists_nsmul_one_le A := by
+    obtain ⟨n, hn⟩ := exists_nat_ge A
+    exact ⟨n, by simpa using hn⟩
+  le_zero_of_forall_pos_smul_one_le A hA := by
+    by_contra h
+    have := hA (A / 2) (by positivity [lt_of_not_ge h])
+    rw [smul_eq_mul, mul_one] at this
+    linarith
+
+namespace ArchimedeanOrderUnitSpace
+
+open OrderUnitSpace
+
+section OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+/-!
+
+## B. The order-unit bounds and norm
+
+-/
+
+/-- The nonnegative scalars that bound an element on both sides by the order unit. -/
+def orderUnitBounds (A : E) : Set ℝ :=
+  {r | 0 ≤ r ∧ -(r • (1 : E)) ≤ A ∧ A ≤ r • (1 : E)}
+
+/-- The order-unit norm is the infimum of the order-unit bounds. -/
+noncomputable def orderUnitNorm (A : E) : ℝ :=
+  sInf (orderUnitBounds A)
+
+/-- The order-unit bounds are bounded below by `0`, so their infimum (the norm) is well-behaved. -/
+lemma orderUnitBounds_bddBelow (A : E) : BddBelow (orderUnitBounds A) :=
+  ⟨0, fun _ hr ↦ hr.1⟩
+
+/-- Any order-unit bound on `A` is an upper bound for `A`'s order-unit norm. -/
+lemma orderUnitNorm_le {A : E} {r : ℝ} (hr : r ∈ orderUnitBounds A) :
+    orderUnitNorm A ≤ r :=
+  csInf_le (orderUnitBounds_bddBelow A) hr
+
+/-- Every element has some order-unit bound: this is just `OrderUnitSpace`'s two-sided bound,
+repackaged as a natural number in `orderUnitBounds`. -/
+lemma orderUnitBounds_nonempty (A : E) : (orderUnitBounds A).Nonempty := by
+  obtain ⟨n, hl, hu⟩ := exists_two_sided_bound A
+  refine ⟨n, Nat.cast_nonneg n, ?_, ?_⟩
+  · simpa only [Nat.cast_smul_eq_nsmul] using hl
+  · simpa only [Nat.cast_smul_eq_nsmul] using hu
+
+/-- The order-unit norm is an infimum of nonnegative reals, hence itself nonnegative. -/
+lemma orderUnitNorm_nonneg (A : E) : 0 ≤ orderUnitNorm A :=
+  le_csInf (orderUnitBounds_nonempty A) fun _ hr ↦ hr.1
+
+@[simp]
+lemma orderUnitNorm_zero : orderUnitNorm (0 : E) = 0 := by
+  apply le_antisymm
+  · exact orderUnitNorm_le ⟨le_rfl, by simp, by simp⟩
+  · exact orderUnitNorm_nonneg 0
+
+/-- Negation preserves the set of order-unit bounds: a symmetric interval bounding `A` bounds
+`-A` too. -/
+lemma orderUnitBounds_neg (A : E) : orderUnitBounds (-A) = orderUnitBounds A := by
+  ext r
+  constructor <;> rintro ⟨hr, hl, hu⟩ <;>
+    exact ⟨hr, by simpa only [neg_neg] using neg_le_neg hu,
+      by simpa only [neg_smul, neg_neg] using neg_le_neg hl⟩
+
+@[simp]
+lemma orderUnitNorm_neg (A : E) : orderUnitNorm (-A) = orderUnitNorm A := by
+  unfold orderUnitNorm
+  rw [orderUnitBounds_neg]
+
+/-- Order-unit bounds add: a bound for `A` and a bound for `B` combine to a bound for `A + B`,
+which is what drives the triangle inequality for `orderUnitNorm`. -/
+lemma add_mem_orderUnitBounds {A B : E} {r s : ℝ} (hr : r ∈ orderUnitBounds A)
+    (hs : s ∈ orderUnitBounds B) : r + s ∈ orderUnitBounds (A + B) := by
+  refine ⟨add_nonneg hr.1 hs.1, ?_, ?_⟩
+  · rw [add_smul, neg_add]
+    exact add_le_add hr.2.1 hs.2.1
+  · rw [add_smul]
+    exact add_le_add hr.2.2 hs.2.2
+
+end OrderUnitSpace
+
+variable {E : Type*} [ArchimedeanOrderUnitSpace E]
+
+/-- An infimum can always be approximated from above: there is an order-unit bound on `A` within
+`ε` of the norm itself. -/
+lemma exists_orderUnitBound_lt (A : E) {ε : ℝ} (hε : 0 < ε) :
+    ∃ r ∈ orderUnitBounds A, r < orderUnitNorm A + ε :=
+  exists_lt_of_csInf_lt (orderUnitBounds_nonempty A) (lt_add_of_pos_right _ hε)
+
+lemma orderUnitNorm_add_le (A B : E) :
+    orderUnitNorm (A + B) ≤ orderUnitNorm A + orderUnitNorm B := by
+  apply le_of_forall_pos_le_add
+  intro ε hε
+  obtain ⟨r, hr, hrlt⟩ := exists_orderUnitBound_lt A (half_pos hε)
+  obtain ⟨s, hs, hslt⟩ := exists_orderUnitBound_lt B (half_pos hε)
+  calc
+    orderUnitNorm (A + B) ≤ r + s := orderUnitNorm_le (add_mem_orderUnitBounds hr hs)
+    _ ≤ (orderUnitNorm A + ε / 2) + (orderUnitNorm B + ε / 2) :=
+      add_le_add hrlt.le hslt.le
+    _ = orderUnitNorm A + orderUnitNorm B + ε := by ring
+
+/-!
+
+## C. Norm axioms
+
+-/
+
+/-- Scaling the unit by a larger nonnegative real gives a larger multiple: `r ↦ r • 1` is
+monotone. -/
+lemma smul_one_mono {r s : ℝ} (hrs : r ≤ s) :
+    r • (1 : E) ≤ s • (1 : E) := by
+  have h : 0 ≤ (s - r) • (1 : E) :=
+    smul_nonneg (sub_nonneg.mpr hrs) one_nonneg
+  calc
+    r • (1 : E) = s • (1 : E) - (s - r) • (1 : E) := by
+      rw [← sub_smul, sub_sub_cancel]
+    _ ≤ s • (1 : E) := sub_le_self _ h
+
+/-- The infimum defining the order-unit norm is attained. This is where the Archimedean axiom
+is used, to pass from "bounded by `r + ε` for every `ε`" to "bounded by `r`". -/
+lemma le_orderUnitNorm_smul_one (A : E) : A ≤ orderUnitNorm A • (1 : E) := by
+  apply sub_nonpos.mp
+  apply le_zero_of_forall_pos_smul_one_le
+  intro ε hε
+  obtain ⟨r, hr, hrlt⟩ := exists_orderUnitBound_lt A hε
+  calc
+    A - orderUnitNorm A • (1 : E) ≤ r • (1 : E) - orderUnitNorm A • (1 : E) :=
+      sub_le_sub_right hr.2.2 _
+    _ = (r - orderUnitNorm A) • (1 : E) := by rw [sub_smul]
+    _ ≤ ε • (1 : E) := smul_one_mono (by linarith)
+
+/-- `A` is also bounded below by `-(orderUnitNorm A • 1)`. -/
+lemma neg_orderUnitNorm_smul_one_le (A : E) : -(orderUnitNorm A • (1 : E)) ≤ A := by
+  have h := le_orderUnitNorm_smul_one (-A)
+  rw [orderUnitNorm_neg] at h
+  simpa only [neg_smul, neg_neg] using neg_le_neg h
+
+/-- The norm itself is an order-unit bound, i.e. the infimum defining `orderUnitNorm` is a
+minimum. -/
+lemma orderUnitNorm_mem_orderUnitBounds (A : E) : orderUnitNorm A ∈ orderUnitBounds A :=
+  ⟨orderUnitNorm_nonneg A, neg_orderUnitNorm_smul_one_le A, le_orderUnitNorm_smul_one A⟩
+
+/-- An element with order-unit norm strictly below `ε` is itself bounded above by `ε • 1`. -/
+lemma le_smul_one_of_orderUnitNorm_lt {A : E} {ε : ℝ} (h : orderUnitNorm A < ε) :
+    A ≤ ε • (1 : E) :=
+  (le_orderUnitNorm_smul_one A).trans (smul_one_mono h.le)
+
+/-- The mirror image of `le_smul_one_of_orderUnitNorm_lt`. -/
+lemma neg_smul_one_le_of_orderUnitNorm_lt {A : E} {ε : ℝ} (h : orderUnitNorm A < ε) :
+    -(ε • (1 : E)) ≤ A := by
+  have h' : -A ≤ ε • (1 : E) := le_smul_one_of_orderUnitNorm_lt (by rwa [orderUnitNorm_neg])
+  simpa using neg_le_neg h'
+
+/-- The order-unit norm is characterized exactly by its symmetric order interval. -/
+lemma orderUnitNorm_le_iff {A : E} {r : ℝ} :
+    orderUnitNorm A ≤ r ↔ 0 ≤ r ∧ -(r • (1 : E)) ≤ A ∧ A ≤ r • (1 : E) := by
+  constructor
+  · intro h
+    refine ⟨(orderUnitNorm_nonneg A).trans h, ?_, ?_⟩
+    · exact (neg_le_neg (smul_one_mono h)).trans (neg_orderUnitNorm_smul_one_le A)
+    · exact (le_orderUnitNorm_smul_one A).trans (smul_one_mono h)
+  · exact orderUnitNorm_le
+
+/-- The order-unit norm is definite: `‖A‖₁ = 0` forces `A = 0`. -/
+lemma orderUnitNorm_eq_zero_iff {A : E} : orderUnitNorm A = 0 ↔ A = 0 := by
+  constructor
+  · intro hA
+    have h := orderUnitNorm_mem_orderUnitBounds A
+    have hu : A ≤ 0 := by simpa [hA] using h.2.2
+    have hl : 0 ≤ A := by simpa [hA] using h.2.1
+    exact le_antisymm hu hl
+  · rintro rfl
+    exact orderUnitNorm_zero
+
+/-- Nonnegative scalar multiplication scales the order-unit norm from above. -/
+lemma orderUnitNorm_smul_le {r : ℝ} (hr : 0 ≤ r) (A : E) :
+    orderUnitNorm (r • A) ≤ r * orderUnitNorm A := by
+  apply orderUnitNorm_le_iff.mpr
+  refine ⟨mul_nonneg hr (orderUnitNorm_nonneg A), ?_, ?_⟩
+  · calc
+    -((r * orderUnitNorm A) • (1 : E)) = r • -(orderUnitNorm A • (1 : E)) := by
+      rw [smul_neg, smul_smul]
+    _ ≤ r • A :=
+      smul_le_smul_of_nonneg_left (neg_orderUnitNorm_smul_one_le A) hr
+  · calc
+    r • A ≤ r • (orderUnitNorm A • (1 : E)) :=
+      smul_le_smul_of_nonneg_left (le_orderUnitNorm_smul_one A) hr
+    _ = (r * orderUnitNorm A) • (1 : E) := by rw [smul_smul]
+
+/-- Positive scalar multiplication scales the order-unit norm. -/
+lemma orderUnitNorm_smul_of_pos {r : ℝ} (hr : 0 < r) (A : E) :
+    orderUnitNorm (r • A) = r * orderUnitNorm A := by
+  apply le_antisymm
+  · exact orderUnitNorm_smul_le hr.le A
+  · have h := orderUnitNorm_smul_le (inv_nonneg.mpr hr.le) (r • A)
+    have hA : orderUnitNorm A ≤ r⁻¹ * orderUnitNorm (r • A) := by
+      calc
+        orderUnitNorm A = orderUnitNorm (r⁻¹ • (r • A)) := by
+          rw [smul_smul, inv_mul_cancel₀ hr.ne', one_smul]
+      _ ≤ r⁻¹ * orderUnitNorm (r • A) := h
+    calc
+      r * orderUnitNorm A ≤ r * (r⁻¹ * orderUnitNorm (r • A)) :=
+        mul_le_mul_of_nonneg_left hA hr.le
+      _ = orderUnitNorm (r • A) := by
+        rw [← mul_assoc, mul_inv_cancel₀ hr.ne', one_mul]
+
+/-- The order-unit norm is absolutely homogeneous. -/
+lemma orderUnitNorm_smul (r : ℝ) (A : E) :
+    orderUnitNorm (r • A) = |r| * orderUnitNorm A := by
+  rcases lt_trichotomy r 0 with hr | rfl | hr
+  · calc
+      orderUnitNorm (r • A) = orderUnitNorm ((-r) • (-A)) := by
+        rw [smul_neg, neg_smul, neg_neg]
+      _ = (-r) * orderUnitNorm (-A) := orderUnitNorm_smul_of_pos (neg_pos.mpr hr) (-A)
+      _ = (-r) * orderUnitNorm A := by rw [orderUnitNorm_neg]
+      _ = |r| * orderUnitNorm A := by rw [abs_of_neg hr]
+  · simp
+  · rw [orderUnitNorm_smul_of_pos hr, abs_of_pos hr]
+
+/-- Rescaling any nonzero element down to the unit ball: `(orderUnitNorm A)⁻¹ • A` has norm at
+most `1`, and scaling it back up by `orderUnitNorm A` recovers `A`. -/
+lemma exists_orderUnitNorm_le_one_smul_eq {A : E} (hA : orderUnitNorm A ≠ 0) :
+    ∃ B : E, orderUnitNorm B ≤ 1 ∧ orderUnitNorm A • B = A := by
+  refine ⟨(orderUnitNorm A)⁻¹ • A, ?_, ?_⟩
+  · rw [orderUnitNorm_smul, abs_of_nonneg (inv_nonneg.mpr (orderUnitNorm_nonneg A)),
+      inv_mul_cancel₀ hA]
+  · rw [smul_smul, mul_inv_cancel₀ hA, one_smul]
+
+/-!
+
+## D. The induced normed space
+
+-/
+
+/-- The order-unit norm packaged as an additive-group norm. -/
+noncomputable def orderUnitAddGroupNorm : AddGroupNorm E where
+  toFun := orderUnitNorm
+  map_zero' := orderUnitNorm_zero
+  add_le' := orderUnitNorm_add_le
+  neg' := orderUnitNorm_neg
+  eq_zero_of_map_eq_zero' _ hA := orderUnitNorm_eq_zero_iff.mp hA
+
+/-- The normed additive group induced by the Archimedean order unit.
+
+This is a `scoped instance`, not a plain one: registering it globally would put a second,
+non-defeq `NormedAddCommGroup` instance on every `ArchimedeanOrderUnitSpace` that already has a
+norm of its own (starting with `ℝ` itself), which is a textbook instance diamond. Opting in with
+`open scoped ArchimedeanOrderUnitSpace` keeps the convenience of instance search without poisoning
+unrelated files. -/
+noncomputable scoped instance orderUnitNormedAddCommGroup : NormedAddCommGroup E :=
+  orderUnitAddGroupNorm.toNormedAddCommGroup
+
+/-- The real normed-space structure induced by the Archimedean order unit. See
+`orderUnitNormedAddCommGroup` for why this is a `scoped instance`. -/
+noncomputable scoped instance orderUnitNormedSpace : NormedSpace ℝ E where
+  norm_smul_le r A := le_of_eq (orderUnitNorm_smul r A)
+
+/-!
+
+## E. Order-closedness of the topology
+
+-/
+
+/-- No sequence of elements that are all `≥ 0` can converge to something negative. -/
+lemma isClosed_Ici_zero : IsClosed (Set.Ici (0 : E)) := by
+  apply IsSeqClosed.isClosed
+  intro x p hx hp
+  apply neg_nonpos.mp
+  apply le_zero_of_forall_pos_smul_one_le
+  intro ε hε
+  obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp hp ε hε
+  specialize hN N (le_refl N)
+  rw [dist_eq_norm] at hN
+  apply le_trans _ (le_smul_one_of_orderUnitNorm_lt hN)
+  simpa using hx N
+
+/-- The same holds relative to any reference `a`, not just `0`. See `orderUnitNormedAddCommGroup`
+for why this is a `scoped instance`: its statement already pins down the scoped topology. -/
+scoped instance closedIciTopology : ClosedIciTopology E where
+  isClosed_Ici a := by
+    rw [← zero_add a, ← Set.preimage_sub_const_Ici]
+    exact isClosed_Ici_zero.preimage (continuous_sub_right a)
+
+end ArchimedeanOrderUnitSpace
diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Basic.lean b/Physlib/ProbabilisticTheory/OrderUnit/Basic.lean
new file mode 100644
index 000000000..7a8831980
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/OrderUnit/Basic.lean
@@ -0,0 +1,108 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Mathlib.Algebra.Order.Module.Defs
+public import Mathlib.Data.Real.Basic
+
+/-!
+
+# Ordered vector spaces and order units
+
+## i. Overview
+
+Order-unit spaces capture the basic structure needed for a probabilistic theory: observables,
+positivity, effects, states and probabilities. They do this without assuming that the theory is
+classical or quantum, or that observables have any particular algebraic structure.
+
+In quantum mechanics, the standard example is the real vector space of self-adjoint matrices,
+ordered by positive semidefiniteness, with the identity matrix as 1. Keeping only the vector
+space, its order, and this distinguished unit gives the abstract order-unit setting.
+
+## ii. Key results
+
+- `OrderUnitSpace.exists_two_sided_bound` : every observable sits between `-(n • 1)` and `n • 1`,
+  for some `n`.
+- `OrderUnitSpace.exists_eq_sub_nonneg` : every observable is a difference of two positive
+  observables.
+- `OrderUnitSpace.exists_real_shift_nonneg` : enough copies of the order unit shift any element
+  into the positive cone.
+- `OrderedVectorSpace.nonneg_add_eq_zero` : the positive cone meets its negation only at `0`.
+
+## iii. Table of contents
+
+- A. Ordered vector spaces and order units
+- B. Consequences of being an order unit
+
+## iv. References
+
+-/
+
+@[expose] public section
+
+/-!
+
+## A. Ordered vector spaces and order-unit elements
+
+-/
+
+/-- An ordered real vector space. -/
+class OrderedVectorSpace (E : Type*) extends AddCommGroup E, PartialOrder E, Module ℝ E,
+    IsOrderedAddMonoid E, PosSMulMono ℝ E
+
+/-- An ordered real vector space whose distinguished element `1` is an order unit: it is
+nonnegative, and every element is bounded above by a natural multiple of it. No multiplication is
+assumed. -/
+class OrderUnitSpace (E : Type*) extends OrderedVectorSpace E, One E where
+  /-- The distinguished unit is nonnegative. -/
+  one_nonneg : 0 ≤ (1 : E)
+  /-- Every element is bounded above by a natural multiple of the order unit. -/
+  exists_nsmul_one_le : ∀ B : E, ∃ n : ℕ, B ≤ n • (1 : E)
+
+namespace OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+/-!
+
+## B. Consequences of being an order unit
+
+-/
+
+/-- Every element is bounded on both sides by a natural multiple of the order unit. -/
+lemma exists_two_sided_bound (A : E) : ∃ n : ℕ, -(n • (1 : E)) ≤ A ∧ A ≤ n • (1 : E) := by
+  obtain ⟨n, hn⟩ := exists_nsmul_one_le A
+  obtain ⟨m, hm⟩ := exists_nsmul_one_le (-A)
+  refine ⟨max n m, ?_, hn.trans (nsmul_le_nsmul_left one_nonneg (le_max_left n m))⟩
+  exact neg_le_of_neg_le <| hm.trans (nsmul_le_nsmul_left one_nonneg (le_max_right n m))
+
+/-- Every element is a difference of two positive elements. -/
+lemma exists_eq_sub_nonneg (A : E) : ∃ Ap An : E, 0 ≤ Ap ∧ 0 ≤ An ∧ A = Ap - An := by
+  obtain ⟨n, hn⟩ := exists_nsmul_one_le (-A)
+  refine ⟨A + n • (1 : E), n • (1 : E), ?_, nsmul_nonneg one_nonneg n, ?_⟩
+  · exact neg_le_iff_add_nonneg'.mp hn
+  · exact (add_sub_cancel_right A (n • (1 : E))).symm
+
+/-- Every element becomes nonnegative after adding enough copies of the order unit: the positive
+cone reaches everywhere, once you're allowed to shift by the unit. -/
+lemma exists_real_shift_nonneg (A : E) : ∃ r : ℝ, 0 ≤ r • (1 : E) + A := by
+  obtain ⟨n, hn⟩ := exists_nsmul_one_le (-A)
+  use n
+  rw [← sub_neg_eq_add, sub_nonneg]
+  exact_mod_cast hn
+
+end OrderUnitSpace
+
+namespace OrderedVectorSpace
+
+variable {E : Type*} [OrderedVectorSpace E]
+
+/-- A nonnegative vector that adds with another nonnegative vector to `0` is itself `0`: the
+positive cone meets its negation only at `0`. -/
+lemma nonneg_add_eq_zero {A B : E} (hA : 0 ≤ A) (hB : 0 ≤ B) (hAB : A + B = 0) : A = 0 :=
+  le_antisymm (hAB ▸ le_add_of_nonneg_right hB) hA
+
+end OrderedVectorSpace
diff --git a/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean b/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean
new file mode 100644
index 000000000..2a2ad7d7f
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/OrderUnit/Cone.lean
@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Mathlib.Geometry.Convex.Cone.Pointed
+public import Mathlib.Data.Real.Basic
+public import Mathlib.Data.NNReal.Defs
+public import Physlib.ProbabilisticTheory.OrderUnit.Archimedean
+
+/-!
+# Ordered positive cones
+
+## i. Overview
+
+`PosCone E` collects the positive elements of `E`. In quantum mechanics, `E` is the real vector
+space of self-adjoint matrices, whose spectra are real. Its positive cone consists exactly of
+those matrices whose spectra are nonnegative.
+These elements form a cone: they are closed under addition and scaling by nonnegative reals.
+
+## ii. Key results
+
+- `PosCone` : the cone of positive observables, `PointedCone.positive ℝ E`. Its carrier is exactly
+  `{A | 0 ≤ A}` (`PointedCone.mem_positive`) and it is convex (`PointedCone.convex`).
+- `PosCone.isClosed` : the positive cone is closed in the order-unit-norm topology of an
+  Archimedean order-unit space.
+
+## iii. Table of contents
+
+- A. The positive cone
+- B. Topological closedness
+- C. The order unit
+
+-/
+
+@[expose] public section
+
+open scoped NNReal
+
+/-!
+
+## A. The positive cone
+
+-/
+
+/-- The positive pointed cone of an ordered real module. -/
+abbrev PosCone (E : Type*) [OrderedVectorSpace E] : PointedCone ℝ E :=
+  PointedCone.positive ℝ E
+
+namespace PosCone
+
+section OrderedVectorSpace
+
+variable {E : Type*} [OrderedVectorSpace E]
+
+/-- The positive cone carries a nonnegative-real scalar action. -/
+instance instModule : Module ℝ≥0 (PosCone E) :=
+  inferInstanceAs (Module {c : ℝ // 0 ≤ c} (PointedCone.positive ℝ E))
+
+end OrderedVectorSpace
+
+/-!
+
+## B. Topological closedness
+
+-/
+
+section ArchimedeanOrderUnitSpace
+
+open ArchimedeanOrderUnitSpace
+open scoped ArchimedeanOrderUnitSpace
+
+variable {E : Type*} [ArchimedeanOrderUnitSpace E]
+
+/-- The positive cone is closed in the topology induced by the order-unit norm. -/
+lemma isClosed : IsClosed (PosCone E : Set E) := isClosed_Ici_zero
+
+end ArchimedeanOrderUnitSpace
+
+/-!
+
+## C. The order unit
+
+-/
+
+section OrderUnitSpace
+
+open OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+/-- The order unit, regarded as a point of the positive cone. -/
+instance instOne : One (PosCone E) := ⟨⟨1, one_nonneg⟩⟩
+
+@[simp]
+lemma coe_one : ((1 : PosCone E) : E) = (1 : E) := rfl
+
+end OrderUnitSpace
+
+end PosCone
diff --git a/Physlib/ProbabilisticTheory/State/Basic.lean b/Physlib/ProbabilisticTheory/State/Basic.lean
new file mode 100644
index 000000000..8c3207c97
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/State/Basic.lean
@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.Channel.Basic
+public import Mathlib.Data.Complex.Basic
+
+/-!
+# States
+
+## i. Overview
+
+A state assigns each observable its expectation value: a positive linear functional
+(`0 ≤ A ⟹ 0 ≤ ω A`), normalized so the certain outcome reads `ω 1 = 1`. In quantum mechanics,
+`ω A = tr(ρA)` for a density matrix `ρ`.
+
+## ii. Key results
+
+- `𝓢[𝕜, A]` : states on an ordered `𝕜`-vector space with a distinguished unit.
+
+## iii. Table of contents
+
+- A. Notation for positive functionals and states
+
+-/
+
+@[expose] public section
+
+/-!
+
+## A. Notation for positive functionals and states
+
+-/
+
+/-- Positive linear functionals on an ordered `𝕜`-vector space. -/
+notation " 𝓟[" 𝕜 ", " A "] " => A →ₚ[𝕜] 𝕜
+
+/-- States on an ordered `𝕜`-vector space with a distinguished unit. -/
+notation " 𝓢[" 𝕜 ", " A "] " => A →ₚ₁[𝕜] 𝕜
+
+/-- States on an ordered complex vector space with a distinguished unit. -/
+notation " 𝓢[" A "] " => A →ₚ₁[ℂ] ℂ
diff --git a/Physlib/ProbabilisticTheory/State/Convex.lean b/Physlib/ProbabilisticTheory/State/Convex.lean
new file mode 100644
index 000000000..13ac316a0
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/State/Convex.lean
@@ -0,0 +1,148 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.State.Basic
+public import Mathlib.Analysis.Convex.Extreme
+public import Mathlib.Topology.UnitInterval
+
+/-!
+# Convex state spaces
+
+## i. Overview
+
+States mix: a probabilistic combination of two states is again a state, and the state space
+embeds convexly into the algebraic dual. A pure state is one that's never a genuine mixture of
+two others, an extreme point of that convex set. A mixed state is one that is a mixture.
+
+## ii. Key results
+
+- `UnitalPositiveLinearMap.mix` : randomize between two states with a given probability.
+- `UnitalPositiveLinearMap.stateSpace_convex` : the state space is convex in the algebraic dual.
+- `UnitalPositiveLinearMap.isPure_iff_forall_mix_eq` : a state is pure iff every genuine mixture
+  producing it is trivial.
+
+## iii. Table of contents
+
+- A. Mixing states
+- B. The state space
+- C. Pure and mixed states
+
+-/
+
+@[expose] public section
+
+namespace UnitalPositiveLinearMap
+
+variable {E : Type*} [AddCommGroup E] [PartialOrder E] [IsOrderedAddMonoid E]
+  [Module ℝ E] [One E]
+
+/-!
+
+## A. Mixing states
+
+-/
+
+/-- Randomize between two states with probability `t` of choosing the first. -/
+def mix (ω φ : 𝓢[ℝ, E]) (t : unitInterval) : 𝓢[ℝ, E] :=
+  ofLinearMap ((t : ℝ) • ω.toLinearMap + (1 - (t : ℝ)) • φ.toLinearMap)
+    (fun A hA => by
+      simp only [LinearMap.add_apply, LinearMap.smul_apply, smul_eq_mul]
+      exact add_nonneg (mul_nonneg t.2.1 (map_nonneg ω hA))
+        (mul_nonneg (sub_nonneg.mpr t.2.2) (map_nonneg φ hA)))
+    (by
+      show (t : ℝ) * ω 1 + (1 - (t : ℝ)) * φ 1 = 1
+      rw [map_one, map_one]
+      ring)
+
+/-- Evaluation of a mixture is the pointwise convex combination. -/
+@[simp]
+lemma mix_apply (ω φ : 𝓢[ℝ, E]) (t : unitInterval) (A : E) :
+    mix ω φ t A = (t : ℝ) * ω A + (1 - (t : ℝ)) * φ A := rfl
+
+/-!
+
+## B. The state space
+
+-/
+
+/-- States embedded into the algebraic dual. -/
+def stateSpace : Set (E →ₗ[ℝ] ℝ) :=
+  Set.range fun ω : 𝓢[ℝ, E] => ω.toLinearMap
+
+/-- The state space is convex in the algebraic dual. -/
+lemma stateSpace_convex : Convex ℝ (stateSpace (E := E)) := by
+  rintro x ⟨ω, rfl⟩ y ⟨φ, rfl⟩ t s ht hs hts
+  have hst : s = 1 - t := by linarith
+  subst hst
+  exact ⟨mix ω φ ⟨t, ht, by linarith⟩, rfl⟩
+
+/-!
+
+## C. Pure and mixed states
+
+-/
+
+/-- A state is pure when it is an extreme point of the state space. -/
+def IsPure (ω : 𝓢[ℝ, E]) : Prop := ω.toLinearMap ∈ stateSpace.extremePoints ℝ
+
+/-- A state is mixed when it isn't pure. -/
+def IsMixed (ω : 𝓢[ℝ, E]) : Prop := ¬ ω.IsPure
+
+/-- A state lies in the open segment between two states exactly when it is a genuine (`t ≠ 0, 1`)
+mixture of them. -/
+private lemma mem_openSegment_iff_exists_mix (ω φ ψ : 𝓢[ℝ, E]) :
+    ω.toLinearMap ∈ openSegment ℝ φ.toLinearMap ψ.toLinearMap ↔
+      ∃ t : unitInterval, t ≠ 0 ∧ t ≠ 1 ∧ mix φ ψ t = ω := by
+  constructor
+  · rintro ⟨t, s, ht, hs, hts, heq⟩
+    have ht1 : t < 1 := by linarith
+    let u : unitInterval := ⟨t, by exact ⟨ht.le, ht1.le⟩⟩
+    refine ⟨u, ?_, ?_, ?_⟩
+    · exact ne_of_gt (by exact_mod_cast ht)
+    · exact ne_of_lt (by exact_mod_cast ht1)
+    · apply toLinearMap_injective
+      change t • φ.toLinearMap + (1 - t) • ψ.toLinearMap = ω.toLinearMap
+      rwa [show 1 - t = s from by linarith]
+  · rintro ⟨t, ht0, ht1, rfl⟩
+    refine ⟨(t : ℝ), 1 - (t : ℝ), ?_, ?_, by ring, ?_⟩
+    · exact_mod_cast unitInterval.pos_iff_ne_zero.mpr ht0
+    · exact sub_pos.mpr (by exact_mod_cast unitInterval.lt_one_iff_ne_one.mpr ht1)
+    · rfl
+
+/-- A state is pure exactly when every genuine (`t ≠ 0, 1`) binary decomposition is trivial: both
+components already equal it. -/
+lemma isPure_iff_forall_mix_eq {ω : 𝓢[ℝ, E]} :
+    ω.IsPure ↔ ∀ (φ ψ : 𝓢[ℝ, E]) (t : unitInterval), t ≠ 0 → t ≠ 1 →
+      mix φ ψ t = ω → φ = ω ∧ ψ = ω := by
+  simp only [IsPure, Set.extremePoints, Set.mem_ofPred_eq]
+  constructor
+  · rintro ⟨-, hext⟩ φ ψ t ht0 ht1 hmix
+    have hseg := (mem_openSegment_iff_exists_mix ω φ ψ).2 ⟨t, ht0, ht1, hmix⟩
+    have hseg' : ω.toLinearMap ∈ openSegment ℝ ψ.toLinearMap φ.toLinearMap := by
+      rwa [openSegment_symm]
+    exact ⟨toLinearMap_injective (hext ⟨φ, rfl⟩ ⟨ψ, rfl⟩ hseg),
+      toLinearMap_injective (hext ⟨ψ, rfl⟩ ⟨φ, rfl⟩ hseg')⟩
+  · intro h
+    refine ⟨⟨ω, rfl⟩, ?_⟩
+    rintro x₁ ⟨φ, rfl⟩ x₂ ⟨ψ, rfl⟩ hseg
+    obtain ⟨t, ht0, ht1, hmix⟩ := (mem_openSegment_iff_exists_mix ω φ ψ).1 hseg
+    exact congrArg (·.toLinearMap) (h φ ψ t ht0 ht1 hmix).1
+
+/-- A genuine mixture equal to a pure state can only repeat that state at both endpoints. -/
+lemma IsPure.eq_of_mix {ω φ ψ : 𝓢[ℝ, E]} (hω : ω.IsPure) (t : unitInterval)
+    (ht0 : t ≠ 0) (ht1 : t ≠ 1) (hmix : mix φ ψ t = ω) : φ = ω ∧ ψ = ω :=
+  isPure_iff_forall_mix_eq.mp hω φ ψ t ht0 ht1 hmix
+
+/-- A state is mixed exactly when it has a genuine nontrivial binary decomposition. -/
+lemma isMixed_iff_exists_mix_ne {ω : 𝓢[ℝ, E]} :
+    ω.IsMixed ↔ ∃ (φ ψ : 𝓢[ℝ, E]) (t : unitInterval), t ≠ 0 ∧ t ≠ 1 ∧
+      mix φ ψ t = ω ∧ (φ ≠ ω ∨ ψ ≠ ω) := by
+  rw [IsMixed, isPure_iff_forall_mix_eq]
+  push Not
+  simp only [imp_iff_not_or]
+
+end UnitalPositiveLinearMap
diff --git a/Physlib/ProbabilisticTheory/State/Discrimination.lean b/Physlib/ProbabilisticTheory/State/Discrimination.lean
new file mode 100644
index 000000000..c866461aa
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/State/Discrimination.lean
@@ -0,0 +1,215 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.State.Metric
+public import Physlib.ProbabilisticTheory.Effect.Complement
+
+/-!
+# State discrimination
+
+## i. Overview
+
+A system is prepared in state `ω₀` (with probability `p`) or `ω₁` (with probability `1 - p`). We
+get to run a single yes/no test on it — an effect `e` — and have to guess which state it was,
+based only on whether `e` "clicked". We guess `ω₀` on a click and `ω₁` otherwise; `successProb`
+is the probability that guess is right.
+
+Always guessing `ω₁`, without even looking at the system, is already right with probability
+`1 - p` — that's our baseline. Running a test can only add to it: its `advantage` is how much
+extra success probability it buys over that baseline. The best possible test maximizes this
+advantage, giving the classic Helstrom bound (`optimalSuccessProb_eq`).
+
+For equal priors (`p = 1/2`) the bound simplifies to `1/2 + dist ω₀ ω₁ / 4`.
+Two equally likely states are easier to tell apart exactly when they sit farther apart.
+
+## ii. Key results
+
+- `UnitalPositiveLinearMap.optimalSuccessProb_eq` : the Helstrom bound.
+- `UnitalPositiveLinearMap.optimalSuccessProb_half_half_eq` : for equal priors, the bound is the
+  state distance.
+
+## iii. Table of contents
+
+- A. Success probability and the advantage of a test
+- B. The Helstrom bound
+- C. Equal priors: the bound is the state distance
+
+## iv. References
+
+- C.W. Helstrom, *Quantum Detection and Estimation Theory*, Academic Press, 1976.
+
+-/
+
+@[expose] public section
+
+namespace UnitalPositiveLinearMap
+
+section OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+/-! ## A. Success probability and the advantage of a test -/
+
+/-- Probability of guessing right between `ω₀` (prior `p`) and `ω₁` (prior `1 - p`) using test
+`e`: guess `ω₀` on a click, `ω₁` otherwise. -/
+def successProb (ω₀ ω₁ : 𝓢[ℝ, E]) (p : unitInterval) (e : Effect E) : ℝ :=
+  (p : ℝ) * ω₀ (e : E) + (1 - (p : ℝ)) * ω₁ ((Effect.complement e : E))
+
+/-- How much test `e` improves on the baseline of always guessing `ω₁`. -/
+def advantage (ω₀ ω₁ : 𝓢[ℝ, E]) (p : unitInterval) (e : Effect E) : ℝ :=
+  (p : ℝ) * ω₀ (e : E) - (1 - (p : ℝ)) * ω₁ (e : E)
+
+/-- Success probability equals the baseline `1 - p` plus the advantage of test `e`. -/
+lemma successProb_eq_add_advantage (ω₀ ω₁ : 𝓢[ℝ, E]) (p : unitInterval) (e : Effect E) :
+    successProb ω₀ ω₁ p e = (1 - (p : ℝ)) + advantage ω₀ ω₁ p e := by
+  show (p : ℝ) * ω₀ (e : E) + (1 - (p : ℝ)) * ω₁ (1 - (e : E))
+      = (1 - (p : ℝ)) + ((p : ℝ) * ω₀ (e : E) - (1 - (p : ℝ)) * ω₁ (e : E))
+  rw [map_sub, map_one]
+  ring
+
+/-! ## B. The Helstrom bound -/
+
+/-- No test's advantage beats the prior weight `p` of the state it favors. -/
+lemma advantage_le (ω₀ ω₁ : 𝓢[ℝ, E]) (p : unitInterval) (e : Effect E) :
+    advantage ω₀ ω₁ p e ≤ (p : ℝ) := by
+  show (p : ℝ) * ω₀ (e : E) - (1 - (p : ℝ)) * ω₁ (e : E) ≤ (p : ℝ)
+  have h1 : ω₀ (e : E) ≤ 1 := (ω₀.monotone' e.2.2).trans_eq (map_one ω₀)
+  have h2 : 0 ≤ ω₁ (e : E) := map_nonneg ω₁ e.2.1
+  have h3 : (p : ℝ) * ω₀ (e : E) ≤ (p : ℝ) * 1 := mul_le_mul_of_nonneg_left h1 p.2.1
+  have h4 : 0 ≤ (1 - (p : ℝ)) * ω₁ (e : E) := mul_nonneg (by linarith [p.2.2]) h2
+  linarith
+
+private lemma bddAbove_advantage (ω₀ ω₁ : 𝓢[ℝ, E]) (p : unitInterval) :
+    BddAbove (Set.range (advantage ω₀ ω₁ p)) :=
+  ⟨(p : ℝ), by rintro _ ⟨e, rfl⟩; exact advantage_le ω₀ ω₁ p e⟩
+
+private lemma bddAbove_successProb (ω₀ ω₁ : 𝓢[ℝ, E]) (p : unitInterval) :
+    BddAbove (Set.range (successProb ω₀ ω₁ p)) := by
+  obtain ⟨b, hb⟩ := bddAbove_advantage ω₀ ω₁ p
+  exact ⟨(1 - (p : ℝ)) + b, by
+    rintro _ ⟨e, rfl⟩
+    rw [successProb_eq_add_advantage]
+    linarith [hb (Set.mem_range_self e)]⟩
+
+/-- The best a single test can do. -/
+noncomputable def optimalSuccessProb (ω₀ ω₁ : 𝓢[ℝ, E]) (p : unitInterval) : ℝ :=
+  ⨆ e : Effect E, successProb ω₀ ω₁ p e
+
+/-- The Helstrom bound: optimal success probability is the baseline `1 - p` plus the best
+advantage any test can give. -/
+lemma optimalSuccessProb_eq (ω₀ ω₁ : 𝓢[ℝ, E]) (p : unitInterval) :
+    optimalSuccessProb ω₀ ω₁ p = (1 - (p : ℝ)) + ⨆ e : Effect E, advantage ω₀ ω₁ p e := by
+  have hbdd := bddAbove_advantage ω₀ ω₁ p
+  have hbdd' := bddAbove_successProb ω₀ ω₁ p
+  unfold optimalSuccessProb
+  apply le_antisymm
+  · exact ciSup_le fun e => by rw [successProb_eq_add_advantage]; linarith [le_ciSup hbdd e]
+  · have hle : (⨆ e : Effect E, advantage ω₀ ω₁ p e) ≤
+        (⨆ e : Effect E, successProb ω₀ ω₁ p e) - (1 - (p : ℝ)) := by
+      apply ciSup_le
+      intro e
+      have h1 := le_ciSup hbdd' e
+      rw [successProb_eq_add_advantage] at h1
+      linarith
+    linarith
+
+end OrderUnitSpace
+
+/-! ## C. Equal priors: the bound is the state distance -/
+
+section Archimedean
+
+variable {E : Type*} [ArchimedeanOrderUnitSpace E]
+
+open ArchimedeanOrderUnitSpace
+
+/-- Complementing an effect negates `ω₀ e - ω₁ e`. -/
+private lemma sub_complement_eq_neg_sub (ω₀ ω₁ : 𝓢[ℝ, E]) (e : Effect E) :
+    ω₀ ((Effect.complement e : E)) - ω₁ ((Effect.complement e : E))
+      = -(ω₀ (e : E) - ω₁ (e : E)) := by
+  show ω₀ (1 - (e : E)) - ω₁ (1 - (e : E)) = _
+  simp only [map_sub, map_one]; ring
+
+private lemma bddAbove_sub (ω₀ ω₁ : 𝓢[ℝ, E]) :
+    BddAbove (Set.range fun e : Effect E => ω₀ (e : E) - ω₁ (e : E)) :=
+  ⟨1, by
+    rintro _ ⟨e, rfl⟩
+    have h1 : ω₀ (e : E) ≤ 1 := (ω₀.monotone' e.2.2).trans_eq (map_one ω₀)
+    have h2 : (0 : ℝ) ≤ ω₁ (e : E) := map_nonneg ω₁ e.2.1
+    linarith⟩
+
+private lemma bddAbove_abs_advantage (ω₀ ω₁ : 𝓢[ℝ, E]) :
+    BddAbove (Set.range fun e : Effect E => |ω₀ (e : E) - ω₁ (e : E)|) :=
+  ⟨1, by
+    rintro _ ⟨e, rfl⟩
+    have h1 : ω₀ (e : E) ≤ 1 := (ω₀.monotone' e.2.2).trans_eq (map_one ω₀)
+    have h2 : (0 : ℝ) ≤ ω₁ (e : E) := map_nonneg ω₁ e.2.1
+    have h3 : ω₁ (e : E) ≤ 1 := (ω₁.monotone' e.2.2).trans_eq (map_one ω₁)
+    have h4 : (0 : ℝ) ≤ ω₀ (e : E) := map_nonneg ω₀ e.2.1
+    rw [abs_le]; constructor <;> linarith⟩
+
+/-- The best advantage equals its own absolute value: complementing an effect flips its sign. -/
+lemma ciSup_advantage_eq_ciSup_abs (ω₀ ω₁ : 𝓢[ℝ, E]) :
+    (⨆ e : Effect E, (ω₀ (e : E) - ω₁ (e : E))) = ⨆ e : Effect E, |ω₀ (e : E) - ω₁ (e : E)| := by
+  have hbdd := bddAbove_sub ω₀ ω₁
+  have hbdd' := bddAbove_abs_advantage ω₀ ω₁
+  apply le_antisymm
+  · exact ciSup_le fun e => (le_abs_self _).trans (le_ciSup hbdd' e)
+  · apply ciSup_le
+    intro e
+    have h1 := le_ciSup hbdd e
+    have h2 := le_ciSup hbdd (Effect.complement e)
+    rw [sub_complement_eq_neg_sub] at h2
+    exact abs_le.mpr ⟨by linarith, h1⟩
+
+/-- The state distance is the largest `|ω₀ e - ω₁ e|` over unit-ball effects
+(`Effect.equivBall`). -/
+private lemma dist_eq_ciSup_abs_advantage (ω₀ ω₁ : 𝓢[ℝ, E]) :
+    dist ω₀ ω₁ =
+      ⨆ e : Effect E, |ω₀ ((Effect.equivBall e : E)) - ω₁ ((Effect.equivBall e : E))| := by
+  have : Nonempty {A : E // orderUnitNorm A ≤ 1} := ⟨0, by simp⟩
+  have hbdd' : BddAbove (Set.range
+      fun e : Effect E => |ω₀ ((Effect.equivBall e : E)) - ω₁ ((Effect.equivBall e : E))|) := by
+    obtain ⟨b, hb⟩ := dist_bddAbove ω₀ ω₁
+    exact ⟨b, by rintro _ ⟨e, rfl⟩; exact hb (Set.mem_range_self (Effect.equivBall e))⟩
+  apply le_antisymm
+  · apply ciSup_le
+    intro A
+    rw [← Effect.equivBall.apply_symm_apply A]
+    exact le_ciSup hbdd' (Effect.equivBall.symm A)
+  · exact ciSup_le fun e => le_ciSup (dist_bddAbove ω₀ ω₁) (Effect.equivBall e)
+
+/-- The state distance is exactly twice the largest advantage a single effect can give. -/
+lemma dist_eq_two_mul_ciSup_advantage (ω₀ ω₁ : 𝓢[ℝ, E]) :
+    dist ω₀ ω₁ = 2 * ⨆ e : Effect E, (ω₀ (e : E) - ω₁ (e : E)) := by
+  rw [ciSup_advantage_eq_ciSup_abs, dist_eq_ciSup_abs_advantage]
+  simp_rw [apply_equivBall]
+  have hpt : ∀ e : Effect E, |2 * ω₀ (e : E) - 1 - (2 * ω₁ (e : E) - 1)|
+      = 2 * |ω₀ (e : E) - ω₁ (e : E)| := fun e => by
+    rw [show 2 * ω₀ (e : E) - 1 - (2 * ω₁ (e : E) - 1) = 2 * (ω₀ (e : E) - ω₁ (e : E)) from by ring,
+      abs_mul, show |(2 : ℝ)| = 2 from by norm_num]
+  simp_rw [hpt]
+  rw [show (⨆ e : Effect E, (2 : ℝ) * |ω₀ (e : E) - ω₁ (e : E)|)
+      = 2 * ⨆ e : Effect E, |ω₀ (e : E) - ω₁ (e : E)| from by
+    rw [← smul_eq_mul, Real.smul_iSup_of_nonneg (by norm_num : (0 : ℝ) ≤ 2)]; simp [smul_eq_mul]]
+
+/-- For equal priors, the Helstrom bound is `1/2` plus a quarter of the state distance. -/
+lemma optimalSuccessProb_half_half_eq (ω₀ ω₁ : 𝓢[ℝ, E]) :
+    optimalSuccessProb ω₀ ω₁ ⟨1 / 2, by norm_num, by norm_num⟩ = 1 / 2 + dist ω₀ ω₁ / 4 := by
+  rw [optimalSuccessProb_eq, dist_eq_two_mul_ciSup_advantage]
+  have hfun : (fun e : Effect E => advantage ω₀ ω₁ ⟨1 / 2, by norm_num, by norm_num⟩ e)
+      = fun e : Effect E => (1 / 2 : ℝ) • (ω₀ (e : E) - ω₁ (e : E)) := by
+    ext e
+    show (1 / 2 : ℝ) * ω₀ (e : E) - (1 - 1 / 2 : ℝ) * ω₁ (e : E) = _
+    simp only [smul_eq_mul]; ring
+  simp_rw [hfun]
+  rw [← Real.smul_iSup_of_nonneg (by norm_num : (0 : ℝ) ≤ 1 / 2), smul_eq_mul]
+  ring
+
+end Archimedean
+
+end UnitalPositiveLinearMap
diff --git a/Physlib/ProbabilisticTheory/State/Metric.lean b/Physlib/ProbabilisticTheory/State/Metric.lean
new file mode 100644
index 000000000..38daec080
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/State/Metric.lean
@@ -0,0 +1,175 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.State.Convex
+public import Physlib.ProbabilisticTheory.Effect.Metric
+public import Mathlib.Topology.MetricSpace.HausdorffDistance
+
+/-!
+# The metric space of states
+
+## i. Overview
+
+A state is just a positive linear functional — no continuity is assumed. It turns out to be
+automatically bounded: `|ω A| ≤ ‖A‖`. Physically, a state can never predict
+an expectation value bigger than what the observable itself can read.
+
+That bound induces a genuine operator-norm distance between states, `dist`, making `𝓢[ℝ, E]` a
+`MetricSpace`. That in turn gives a notion of how mixed a state is: `distToPure`, its distance to
+the nearest pure state.
+
+## ii. Key results
+
+- `UnitalPositiveLinearMap.abs_apply_le_orderUnitNorm` : a state's values are bounded by the
+  order-unit norm.
+- `UnitalPositiveLinearMap.dist` : the operator-norm distance between states.
+- `UnitalPositiveLinearMap.distToPure` : a state's distance to the nearest pure state.
+
+## iii. Table of contents
+
+- A. States are bounded by the order-unit norm
+- B. The state metric
+- C. Distance to the nearest pure state
+
+-/
+
+@[expose] public section
+
+open ArchimedeanOrderUnitSpace
+
+variable {E : Type*} [ArchimedeanOrderUnitSpace E]
+
+namespace UnitalPositiveLinearMap
+
+/-!
+
+## A. States are bounded by the order-unit norm
+
+-/
+
+/-- A state never overshoots the order-unit norm. -/
+lemma apply_le_orderUnitNorm (ω : 𝓢[ℝ, E]) (A : E) : ω A ≤ orderUnitNorm A := by
+  apply le_of_forall_pos_le_add
+  intro ε hε
+  obtain ⟨r, hr, hrε⟩ := exists_orderUnitBound_lt A hε
+  have hpos : 0 ≤ ω (r • (1 : E) - A) := map_nonneg ω (sub_nonneg.mpr hr.2.2)
+  simp only [map_sub, map_smul, smul_eq_mul, map_one, mul_one] at hpos
+  linarith
+
+/-- A state's values are bounded by the order-unit norm in both directions. -/
+lemma abs_apply_le_orderUnitNorm (ω : 𝓢[ℝ, E]) (A : E) : |ω A| ≤ orderUnitNorm A := by
+  have h1 : ω A ≤ orderUnitNorm A := apply_le_orderUnitNorm ω A
+  have h2 : ω (-A) ≤ orderUnitNorm (-A) := apply_le_orderUnitNorm ω (-A)
+  rw [_root_.map_neg, orderUnitNorm_neg] at h2
+  exact abs_le.mpr ⟨by linarith, h1⟩
+
+/-- Two states' predictions on any observable of order-unit norm at most `1` never differ by more
+than `2`. -/
+lemma abs_apply_sub_apply_le_two (ω φ : 𝓢[ℝ, E]) {A : E} (hA : orderUnitNorm A ≤ 1) :
+    |ω A - φ A| ≤ 2 := by
+  have h1 := abs_apply_le_orderUnitNorm ω A
+  have h2 := abs_apply_le_orderUnitNorm φ A
+  calc |ω A - φ A| ≤ |ω A| + |φ A| := abs_sub _ _
+    _ ≤ orderUnitNorm A + orderUnitNorm A := add_le_add h1 h2
+    _ ≤ 1 + 1 := add_le_add hA hA
+    _ = 2 := by norm_num
+
+/-!
+
+## B. The state metric
+
+-/
+
+/-- The values `|ω A - φ A|` of two states, restricted to the order-unit-norm unit ball, are
+bounded by `2`. -/
+lemma dist_bddAbove (ω φ : 𝓢[ℝ, E]) :
+    BddAbove (Set.range fun A : {A : E // orderUnitNorm A ≤ 1} => |ω A - φ A|) :=
+  ⟨2, by rintro _ ⟨A, rfl⟩; exact abs_apply_sub_apply_le_two ω φ A.2⟩
+
+/-- The operator-norm distance between two states: how far apart their predictions can get on an
+observable of order-unit norm at most `1`. -/
+noncomputable def dist (ω φ : 𝓢[ℝ, E]) : ℝ :=
+  ⨆ A : {A : E // orderUnitNorm A ≤ 1}, |ω A - φ A|
+
+lemma dist_nonneg (ω φ : 𝓢[ℝ, E]) : 0 ≤ dist ω φ :=
+  le_trans (abs_nonneg _) (le_ciSup (dist_bddAbove ω φ) ⟨0, by simp⟩)
+
+/-- The whole state space has diameter at most `2`: it's a bounded metric space. -/
+lemma dist_le_two (ω φ : 𝓢[ℝ, E]) : dist ω φ ≤ 2 := by
+  have : Nonempty {A : E // orderUnitNorm A ≤ 1} := ⟨0, by simp⟩
+  exact ciSup_le fun A => abs_apply_sub_apply_le_two ω φ A.2
+
+@[simp]
+lemma dist_self (ω : 𝓢[ℝ, E]) : dist ω ω = 0 := by
+  have : Nonempty {A : E // orderUnitNorm A ≤ 1} := ⟨0, by simp⟩
+  have : (fun A : {A : E // orderUnitNorm A ≤ 1} => |ω A - ω A|) = fun _ => (0 : ℝ) := by
+    ext A; simp
+  unfold dist
+  rw [this, ciSup_const]
+
+lemma dist_comm (ω φ : 𝓢[ℝ, E]) : dist ω φ = dist φ ω := by
+  unfold dist
+  simp_rw [abs_sub_comm]
+
+lemma dist_triangle (ω φ ψ : 𝓢[ℝ, E]) : dist ω ψ ≤ dist ω φ + dist φ ψ := by
+  have : Nonempty {A : E // orderUnitNorm A ≤ 1} := ⟨0, by simp⟩
+  apply ciSup_le
+  intro A
+  calc |ω A - ψ A| ≤ |ω A - φ A| + |φ A - ψ A| := abs_sub_le _ _ _
+    _ ≤ dist ω φ + dist φ ψ :=
+      add_le_add (le_ciSup (dist_bddAbove ω φ) A) (le_ciSup (dist_bddAbove φ ψ) A)
+
+/-- `dist` separates states: two states at distance `0` are equal. -/
+lemma eq_of_dist_eq_zero {ω φ : 𝓢[ℝ, E]} (h : dist ω φ = 0) : ω = φ := by
+  apply ext
+  intro A
+  rcases eq_or_ne (orderUnitNorm A) 0 with hr | hr
+  · simp [orderUnitNorm_eq_zero_iff.mp hr]
+  · obtain ⟨B, hB1, hAB⟩ := exists_orderUnitNorm_le_one_smul_eq hr
+    have hle : |ω B - φ B| ≤ dist ω φ := le_ciSup (dist_bddAbove ω φ) ⟨B, hB1⟩
+    rw [h] at hle
+    have heq : ω B = φ B := sub_eq_zero.mp (abs_eq_zero.mp (le_antisymm hle (abs_nonneg _)))
+    have hstep : orderUnitNorm A • ω B = orderUnitNorm A • φ B := congrArg (orderUnitNorm A • ·) heq
+    rwa [← map_smul, ← map_smul, hAB] at hstep
+
+/-- A state's value at a doubled, re-centered effect (`Effect.equivBall`) is twice its value at
+the effect, minus one. -/
+lemma apply_equivBall (ψ : 𝓢[ℝ, E]) (e : Effect E) :
+    ψ ((Effect.equivBall e : E)) = 2 * ψ (e : E) - 1 := by
+  show ψ ((2 : ℝ) • (e : E) - 1) = _
+  rw [map_sub, map_smul, map_one, smul_eq_mul]
+
+/-- States, metrized by the operator norm induced by the order-unit norm on `E`. -/
+noncomputable instance : MetricSpace (𝓢[ℝ, E]) where
+  dist := dist
+  dist_self := dist_self
+  dist_comm := dist_comm
+  dist_triangle := dist_triangle
+  eq_of_dist_eq_zero := eq_of_dist_eq_zero
+
+/-!
+
+## C. Distance to the nearest pure state
+
+-/
+
+/-- How mixed a state is: its distance to the nearest pure state. -/
+noncomputable def distToPure (ω : 𝓢[ℝ, E]) : ℝ :=
+  Metric.infDist ω {φ : 𝓢[ℝ, E] | IsPure φ}
+
+lemma distToPure_nonneg (ω : 𝓢[ℝ, E]) : 0 ≤ distToPure ω :=
+  Metric.infDist_nonneg
+
+/-- A pure state is at distance `0` from the set of pure states. -/
+lemma distToPure_eq_zero_of_isPure {ω : 𝓢[ℝ, E]} (h : IsPure ω) : distToPure ω = 0 :=
+  Metric.infDist_zero_of_mem h
+
+/-- `distToPure` is `1`-Lipschitz: states close in `dist` are similarly mixed. -/
+lemma lipschitzWith_distToPure : LipschitzWith 1 (distToPure (E := E)) :=
+  Metric.lipschitz_infDist_pt {φ : 𝓢[ℝ, E] | IsPure φ}
+
+end UnitalPositiveLinearMap
diff --git a/Physlib/ProbabilisticTheory/Weight/Basic.lean b/Physlib/ProbabilisticTheory/Weight/Basic.lean
new file mode 100644
index 000000000..3f7961cc6
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Weight/Basic.lean
@@ -0,0 +1,169 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Mathlib.Data.ENNReal.Basic
+public import Mathlib.Data.ENNReal.Inv
+public import Mathlib.Data.ENNReal.Action
+public import Physlib.ProbabilisticTheory.OrderUnit.Basic
+public import Physlib.ProbabilisticTheory.OrderUnit.Cone
+
+/-!
+# Weights
+
+## i. Overview
+
+A state assigns each positive observable a nonnegative expectation value, normalized so the
+certain outcome reads exactly `1`. A *weight* generalizes this by dropping the normalization and
+letting the values be extended nonnegative reals, possibly `+∞`. This matters especially in
+infinite dimensions: the trace on `B(H)` is only finite on the trace-class operators and genuinely
+diverges to `+∞` elsewhere. A state is then the special case that happens to be finite everywhere
+and normalized.
+
+## ii. Key results
+
+- `Weight.mono` : weights are monotone on the positive cone.
+- `Weight.IsFinite.isSemifinite` : a finite weight is automatically semifinite.
+- `Weight.IsFinite.normalize_isState` : rescaling a finite weight that's nonzero at the order unit
+  turns it into a state.
+
+## iii. Table of contents
+
+- A. Weights
+- B. States as weights
+
+## iv. References
+
+- G. Ludwig, *Foundations of Quantum Mechanics I*, Springer, 1983.
+  <https://link.springer.com/book/10.1007/978-3-642-86751-4>
+
+-/
+
+@[expose] public section
+
+open scoped ENNReal NNReal
+
+/-!
+
+## A. Weights
+
+-/
+
+section OrderedVectorSpace
+
+variable {E : Type*} [OrderedVectorSpace E]
+
+/-- An extended nonnegative linear functional on the positive cone. -/
+abbrev Weight (E : Type*) [OrderedVectorSpace E] := PosCone E →ₗ[ℝ≥0] ℝ≥0∞
+
+end OrderedVectorSpace
+
+namespace Weight
+
+section OrderedVectorSpace
+
+variable {E : Type*} [OrderedVectorSpace E]
+
+@[ext]
+lemma ext {w₁ w₂ : Weight E} (h : ∀ A, w₁ A = w₂ A) : w₁ = w₂ :=
+  LinearMap.ext h
+
+/-- Only the zero positive element has weight zero. -/
+def IsFaithful (w : Weight E) : Prop := ∀ A : PosCone E, w A = 0 → A = 0
+
+/-- A weight has no infinite values. -/
+def IsFinite (w : Weight E) : Prop := ∀ A : PosCone E, w A ≠ ⊤
+
+/-- A weight is the supremum of its finite values below each positive element. -/
+def IsSemifinite (w : Weight E) : Prop := ∀ A : PosCone E,
+  w A = ⨆ B : {B : PosCone E // B ≤ A ∧ w B ≠ ⊤}, w B
+
+/-- Weights are monotone on the positive cone. -/
+lemma mono (w : Weight E) : Monotone (w : PosCone E → ℝ≥0∞) := by
+  intro A B hAB
+  have hC : (0 : E) ≤ (B : E) - (A : E) := sub_nonneg.mpr hAB
+  let C : PosCone E := ⟨(B : E) - (A : E), hC⟩
+  have hAC : A + C = B := by
+    ext
+    change (A : E) + ((B : E) - (A : E)) = B
+    abel
+  calc
+    w A ≤ w A + w C := le_self_add
+    _ = w (A + C) := (map_add w A C).symm
+    _ = w B := by rw [hAC]
+
+/-- A finite weight is semifinite. -/
+lemma IsFinite.isSemifinite {w : Weight E} (hw : w.IsFinite) : w.IsSemifinite := by
+  intro A
+  apply le_antisymm
+  · exact le_iSup (fun B : {B : PosCone E // B ≤ A ∧ w B ≠ ⊤} => w B)
+      ⟨A, le_rfl, hw A⟩
+  · apply iSup_le
+    intro B
+    exact w.mono B.2.1
+
+/-- A finite weight's real value is additive. -/
+lemma IsFinite.toReal_map_add {w : Weight E} (hw : w.IsFinite) (A B : PosCone E) :
+    (w (A + B)).toReal = (w A).toReal + (w B).toReal := by
+  rw [w.map_add, ENNReal.toReal_add (hw A) (hw B)]
+
+/-- A weight's real value scales linearly under nonnegative real scaling, whether or not it's
+finite: on the infinite side, both sides read `0`. -/
+lemma toReal_map_nnreal_smul (w : Weight E) (k : ℝ≥0) (A : PosCone E) :
+    (w (k • A)).toReal = k * (w A).toReal := by
+  rw [w.map_smul, ENNReal.smul_def, smul_eq_mul, ENNReal.toReal_mul, ENNReal.coe_toReal]
+
+/-- A weight preserves existing directed suprema in the positive cone. -/
+def IsNormal (w : Weight E) : Prop := ∀ (D : Set (PosCone E)) (A : PosCone E),
+  D.Nonempty → DirectedOn (· ≤ ·) D → IsLUB D A → IsLUB (w '' D) (w A)
+
+end OrderedVectorSpace
+
+/-!
+
+## B. States as weights
+
+-/
+
+section OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+/-- A weight that's finite everywhere and gives the certain outcome weight exactly `1`. -/
+structure IsState (w : Weight E) : Prop where
+  /-- A state is finite everywhere. -/
+  finite : w.IsFinite
+  /-- A state gives the certain outcome weight exactly `1`. -/
+  normalized : w 1 = 1
+
+/-- Rescaling a finite weight that's nonzero at the order unit. -/
+noncomputable def IsFinite.normalize {w : Weight E} (_hw : w.IsFinite) (_h : w 1 ≠ 0) :
+    Weight E where
+  toFun A := (w 1)⁻¹ * w A
+  map_add' A B := by rw [map_add, mul_add]
+  map_smul' c A := by
+    simp only [map_smul, ENNReal.smul_def, smul_eq_mul, RingHom.id_apply]
+    ring
+
+lemma IsFinite.normalize_apply {w : Weight E} (hw : w.IsFinite) (h : w 1 ≠ 0)
+    (A : PosCone E) : hw.normalize h A = (w 1)⁻¹ * w A := rfl
+
+/-- Normalizing a finite weight keeps it finite. -/
+lemma IsFinite.normalize_isFinite {w : Weight E} (hw : w.IsFinite) (h : w 1 ≠ 0) :
+    (hw.normalize h).IsFinite := fun A => by
+  rw [normalize_apply]
+  exact ENNReal.mul_ne_top (ENNReal.inv_ne_top.mpr h) (hw A)
+
+/-- Normalizing a finite weight makes it a state: the order unit is scaled to weight exactly
+`1`. -/
+lemma IsFinite.normalize_isState {w : Weight E} (hw : w.IsFinite) (h : w 1 ≠ 0) :
+    (hw.normalize h).IsState where
+  finite := hw.normalize_isFinite h
+  normalized := by rw [normalize_apply]; exact ENNReal.inv_mul_cancel h (hw 1)
+
+end OrderUnitSpace
+
+end Weight
diff --git a/Physlib/ProbabilisticTheory/Weight/Extension.lean b/Physlib/ProbabilisticTheory/Weight/Extension.lean
new file mode 100644
index 000000000..9b9ebfb8c
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Weight/Extension.lean
@@ -0,0 +1,170 @@
+/-
+Copyright (c) 2026 Tom Ole Diem. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tom Ole Diem
+-/
+module
+
+public import Physlib.ProbabilisticTheory.Weight.Basic
+public import Mathlib.Tactic.Module
+
+/-!
+# Extending finite weights
+
+## i. Overview
+
+A finite weight on the positive cone of an order-unit space extends uniquely to a positive linear
+functional on the whole space. Since `1` is an order unit, any `A : E` becomes nonnegative after
+adding enough copies of `1`, so we set `toFun A := w (r • 1 + A) - r * w 1` for such an `r`, and
+check the result does not depend on the `r` chosen.
+
+## ii. Key results
+
+- `Weight.IsFinite.toLinearMap` : the `ℝ`-linear map extending a finite weight to all of `E`.
+
+## iii. Table of contents
+
+- A. The raw shifted value
+- B. The linear extension
+
+-/
+
+@[expose] public section
+
+open scoped ENNReal NNReal
+
+variable {E : Type*} [OrderUnitSpace E]
+
+namespace Weight
+
+variable {w : Weight E}
+
+namespace IsFinite
+
+/-!
+
+## A. The raw shifted value
+
+-/
+
+/-- `A` shifted into the cone by `r` copies of the order unit, minus the corresponding multiple
+of the weight of the order unit. -/
+noncomputable def rawValue (_hw : w.IsFinite) (A : E) (r : ℝ) (h : 0 ≤ r • (1 : E) + A) : ℝ :=
+  (w ⟨r • (1 : E) + A, h⟩).toReal - r * (w 1).toReal
+
+/-- Shifting by a larger `s` and a smaller `r` agree: the extra `s - r` copies of the unit added
+to the cone element are exactly cancelled by the extra `(s - r) * w 1` subtracted off. -/
+lemma rawValue_of_le (hw : w.IsFinite) (A : E) {r s : ℝ} (hr : 0 ≤ r • (1 : E) + A)
+    (hs : 0 ≤ s • (1 : E) + A) (hrs : r ≤ s) : rawValue hw A s hs = rawValue hw A r hr := by
+  set t : ℝ≥0 := (s - r).toNNReal with ht_def
+  have ht : (t : ℝ) = s - r := Real.coe_toNNReal _ (by linarith)
+  have hcone : (⟨s • (1 : E) + A, hs⟩ : PosCone E) =
+      ⟨r • (1 : E) + A, hr⟩ + t • (1 : PosCone E) := by
+    apply Subtype.ext
+    show s • (1 : E) + A = (r • (1 : E) + A) + (t : ℝ) • (1 : E)
+    rw [ht]
+    module
+  unfold rawValue
+  rw [hcone, hw.toReal_map_add, w.toReal_map_nnreal_smul, ht]
+  ring
+
+/-- The shifted value of a finite weight does not depend on the chosen shift. -/
+lemma rawValue_indep (hw : w.IsFinite) (A : E) {r s : ℝ} (hr : 0 ≤ r • (1 : E) + A)
+    (hs : 0 ≤ s • (1 : E) + A) : rawValue hw A r hr = rawValue hw A s hs := by
+  rcases le_total r s with hrs | hrs
+  · exact (rawValue_of_le hw A hr hs hrs).symm
+  · exact rawValue_of_le hw A hs hr hrs
+
+/-!
+
+## B. The linear extension
+
+-/
+
+open Classical in
+/-- The linear extension of a finite weight from the positive cone to all of `E`. -/
+noncomputable def toFun (hw : w.IsFinite) (A : E) : ℝ :=
+  rawValue hw A (PosCone.exists_real_shift_nonneg A).choose
+    (PosCone.exists_real_shift_nonneg A).choose_spec
+
+/-- The extension can be computed via any valid shift `r`, not just the one `toFun` happens to
+pick. -/
+lemma toFun_eq (hw : w.IsFinite) (A : E) {r : ℝ} (h : 0 ≤ r • (1 : E) + A) :
+    toFun hw A = rawValue hw A r h :=
+  rawValue_indep hw A _ h
+
+@[simp]
+lemma toFun_of_nonneg (hw : w.IsFinite) (A : PosCone E) : toFun hw (A : E) = (w A).toReal := by
+  have h0 : (0 : E) ≤ (0 : ℝ) • (1 : E) + (A : E) := by
+    rw [zero_smul, zero_add]
+    exact (PointedCone.mem_positive (R := ℝ) (E := E)).mp A.2
+  rw [toFun_eq hw (A : E) h0, rawValue]
+  simp
+
+/-- The extension of a finite weight sends `0` to `0`. -/
+lemma toFun_zero (hw : w.IsFinite) : toFun hw (0 : E) = 0 := by
+  have h := toFun_of_nonneg hw (0 : PosCone E)
+  simpa using h
+
+/-- The extension of a finite weight is additive. -/
+lemma toFun_add (hw : w.IsFinite) (A B : E) : toFun hw (A + B) = toFun hw A + toFun hw B := by
+  obtain ⟨r, hr⟩ := PosCone.exists_real_shift_nonneg A
+  obtain ⟨s, hs⟩ := PosCone.exists_real_shift_nonneg B
+  have hrs : (0 : E) ≤ (r + s) • (1 : E) + (A + B) := by
+    have heq : (r + s) • (1 : E) + (A + B) = (r • (1 : E) + A) + (s • (1 : E) + B) := by module
+    rw [heq]; exact add_nonneg hr hs
+  rw [toFun_eq hw A hr, toFun_eq hw B hs, toFun_eq hw (A + B) hrs]
+  have hcone : (⟨(r + s) • (1 : E) + (A + B), hrs⟩ : PosCone E) =
+      ⟨r • (1 : E) + A, hr⟩ + ⟨s • (1 : E) + B, hs⟩ := by
+    apply Subtype.ext
+    show (r + s) • (1 : E) + (A + B) = (r • (1 : E) + A) + (s • (1 : E) + B)
+    module
+  unfold rawValue
+  rw [hcone, hw.toReal_map_add]
+  ring
+
+/-- The extension of a finite weight negates: a corollary of additivity and `toFun_zero`. -/
+lemma toFun_neg (hw : w.IsFinite) (A : E) : toFun hw (-A) = -toFun hw A := by
+  have h := toFun_add hw A (-A)
+  rw [add_neg_cancel, toFun_zero] at h
+  linarith
+
+/-- Nonnegative real homogeneity of the finite-weight extension. -/
+lemma toFun_real_nonneg_smul (hw : w.IsFinite) {t : ℝ} (ht : 0 ≤ t) (A : E) :
+    toFun hw (t • A) = t * toFun hw A := by
+  obtain ⟨r, hr⟩ := PosCone.exists_real_shift_nonneg A
+  have hcr : (0 : E) ≤ (t * r) • (1 : E) + t • A := by
+    have heq : (t * r) • (1 : E) + t • A = t • (r • (1 : E) + A) := by module
+    rw [heq]; exact smul_nonneg ht hr
+  rw [toFun_eq hw A hr, toFun_eq hw (t • A) hcr]
+  have hcone : (⟨(t * r) • (1 : E) + t • A, hcr⟩ : PosCone E) =
+      t.toNNReal • (⟨r • (1 : E) + A, hr⟩ : PosCone E) := by
+    apply Subtype.ext
+    show (t * r) • (1 : E) + t • A = (t.toNNReal : ℝ) • (r • (1 : E) + A)
+    rw [Real.coe_toNNReal t ht]
+    module
+  unfold rawValue
+  rw [hcone, w.toReal_map_nnreal_smul, Real.coe_toNNReal t ht]
+  ring
+
+/-- Full real homogeneity of the finite-weight extension. -/
+lemma toFun_smul (hw : w.IsFinite) (t : ℝ) (A : E) : toFun hw (t • A) = t * toFun hw A := by
+  rcases le_total (0 : ℝ) t with ht | ht
+  · exact toFun_real_nonneg_smul hw ht A
+  · have h1 : t • A = -((-t) • A) := by rw [neg_smul, neg_neg]
+    rw [h1, toFun_neg, toFun_real_nonneg_smul hw (neg_nonneg.mpr ht) A]
+    ring
+
+/-- The `ℝ`-linear map extending a finite weight. -/
+noncomputable def toLinearMap (hw : w.IsFinite) : E →ₗ[ℝ] ℝ where
+  toFun := toFun hw
+  map_add' := toFun_add hw
+  map_smul' := toFun_smul hw
+
+/-- The linear extension agrees with `toFun` by construction. -/
+@[simp]
+lemma toLinearMap_apply (hw : w.IsFinite) (A : E) : toLinearMap hw A = toFun hw A := rfl
+
+end IsFinite
+
+end Weight