diff --git a/Physlib.lean b/Physlib.lean
index 963a36361..28a38b2c9 100644
--- a/Physlib.lean
+++ b/Physlib.lean
@@ -253,6 +253,14 @@ 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.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.QFT.AnomalyCancellation.Basic
 public import Physlib.QFT.AnomalyCancellation.GroupActions
 public import Physlib.QFT.PerturbationTheory.CreateAnnihilate
diff --git a/Physlib/ProbabilisticTheory/Effect/Basic.lean b/Physlib/ProbabilisticTheory/Effect/Basic.lean
new file mode 100644
index 000000000..0947097d2
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Effect/Basic.lean
@@ -0,0 +1,92 @@
+/-
+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.Tactic.Positivity
+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
+
+open OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace E]
+
+instance instZero : Zero (Effect E) := ⟨0, le_refl 0, one_nonneg⟩
+
+instance instOne : One (Effect E) := ⟨1, one_nonneg, le_refl 1⟩
+
+@[simp] lemma coe_zero : ((0 : Effect E) : E) = 0 := rfl
+
+@[simp] lemma coe_one : ((1 : Effect E) : E) = 1 := rfl
+
+/-- 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⟩ := exists_nsmul_one_le B
+  rw [← Nat.cast_smul_eq_nsmul ℝ n (1 : E)] at hn
+  refine ⟨((n : ℝ) + 1)⁻¹, by positivity, smul_nonneg (by positivity) hB, ?_⟩
+  have hle : (n : ℝ) * ((n : ℝ) + 1)⁻¹ ≤ 1 := by
+    rw [← div_eq_mul_inv, div_le_one (by positivity)]
+    exact le_add_of_nonneg_right zero_le_one
+  calc ((n : ℝ) + 1)⁻¹ • B ≤ ((n : ℝ) + 1)⁻¹ • ((n : ℝ) • (1 : E)) :=
+        smul_le_smul_of_nonneg_left hn (by positivity)
+    _ = ((n : ℝ) * ((n : ℝ) + 1)⁻¹) • (1 : E) := by rw [smul_smul, mul_comm]
+    _ ≤ (1 : ℝ) • (1 : E) := smul_le_smul_of_nonneg_right hle one_nonneg
+    _ = 1 := one_smul ℝ 1
+
+end Effect
diff --git a/Physlib/ProbabilisticTheory/Effect/Complement.lean b/Physlib/ProbabilisticTheory/Effect/Complement.lean
new file mode 100644
index 000000000..01369646f
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Effect/Complement.lean
@@ -0,0 +1,82 @@
+/-
+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.Convex
+
+/-!
+# 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
+
+variable {E : Type*} [OrderUnitSpace 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 :=
+  Subtype.ext (by 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
+
+@[simp]
+lemma complement_zero : complement (0 : Effect E) = 1 := Subtype.ext (by simp [complement])
+
+@[simp]
+lemma complement_one : complement (1 : Effect E) = 0 := Subtype.ext (by 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 Effect
diff --git a/Physlib/ProbabilisticTheory/Effect/Convex.lean b/Physlib/ProbabilisticTheory/Effect/Convex.lean
new file mode 100644
index 000000000..980abc2ef
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Effect/Convex.lean
@@ -0,0 +1,57 @@
+/-
+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.Convex.Basic
+public import Mathlib.Topology.UnitInterval
+public import Physlib.ProbabilisticTheory.Effect.Basic
+
+/-!
+# 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*} [OrderUnitSpace 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. -/
+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..10765d9cf
--- /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 Mathlib.Tactic.Module
+public import Physlib.ProbabilisticTheory.Effect.Basic
+public import Physlib.ProbabilisticTheory.OrderUnit.Archimedean
+
+/-!
+# 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 instMetricSpace : 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..bbea22355
--- /dev/null
+++ b/Physlib/ProbabilisticTheory/Effect/Sharp.lean
@@ -0,0 +1,83 @@
+/-
+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.Convex.Strict.Extreme
+public import Physlib.ProbabilisticTheory.Effect.Complement
+
+/-!
+# 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
+
+open OrderUnitSpace
+
+variable {E : Type*} [OrderUnitSpace 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 ℝ (Effect E : Set E)
+
+/-- The impossible outcome 0 is sharp. -/
+lemma isSharp_zero : IsSharp (0 : Effect E) := by
+  refine ⟨⟨le_refl 0, one_nonneg⟩,
+    fun x₁ hx₁ x₂ hx₂ ⟨a, b, ha, hb, _, hz⟩ => ?_⟩
+  have hax := (add_eq_zero_iff_of_nonneg (smul_nonneg ha.le hx₁.1)
+    (smul_nonneg hb.le hx₂.1)).mp (by simpa using hz) |>.1
+  exact (smul_eq_zero.mp hax).resolve_left ha.ne'
+
+/-- 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 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