From c7d51c1966647e7baa1d2b07fa31d8699d215c48 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 2 Oct 2026 05:16:01 +0100
Subject: [PATCH 1/3] refactor: Fix build

---
 Physlib/ProbabilisticTheory/Effect/Basic.lean      | 4 ++++
 Physlib/ProbabilisticTheory/Effect/Complement.lean | 4 ++++
 Physlib/ProbabilisticTheory/Effect/Convex.lean     | 4 ++++
 Physlib/ProbabilisticTheory/Effect/Metric.lean     | 4 ++++
 Physlib/ProbabilisticTheory/Effect/Sharp.lean      | 4 ++++
 5 files changed, 20 insertions(+)

diff --git a/Physlib/ProbabilisticTheory/Effect/Basic.lean b/Physlib/ProbabilisticTheory/Effect/Basic.lean
index 35ff12794..c8cccf08c 100644
--- a/Physlib/ProbabilisticTheory/Effect/Basic.lean
+++ b/Physlib/ProbabilisticTheory/Effect/Basic.lean
@@ -39,6 +39,8 @@ elements of a POVM.
 
 @[expose] public section
 
+namespace ProbabilisticTheory
+
 /-!
 
 ## A. Effects
@@ -86,3 +88,5 @@ lemma exists_pos_smul_mem {B : E} (hB : 0 ≤ B) :
   exact hn.trans (smul_le_smul_of_nonneg_right (by linarith) one_nonneg)
 
 end Effect
+
+end ProbabilisticTheory
diff --git a/Physlib/ProbabilisticTheory/Effect/Complement.lean b/Physlib/ProbabilisticTheory/Effect/Complement.lean
index af066f2fd..cb1faa91d 100644
--- a/Physlib/ProbabilisticTheory/Effect/Complement.lean
+++ b/Physlib/ProbabilisticTheory/Effect/Complement.lean
@@ -31,6 +31,8 @@ Physically, a state's probability of "no" is always `1` minus its probability of
 
 @[expose] public section
 
+namespace ProbabilisticTheory
+
 namespace Effect
 
 variable {E : Type*} [OrderUnitSpace E]
@@ -80,3 +82,5 @@ lemma complement_mix (e f : Effect E) (t : unitInterval) :
   ext; simp; module
 
 end Effect
+
+end ProbabilisticTheory
diff --git a/Physlib/ProbabilisticTheory/Effect/Convex.lean b/Physlib/ProbabilisticTheory/Effect/Convex.lean
index 6933492c2..f061616dd 100644
--- a/Physlib/ProbabilisticTheory/Effect/Convex.lean
+++ b/Physlib/ProbabilisticTheory/Effect/Convex.lean
@@ -30,6 +30,8 @@ actually run is itself a legitimate measurement.
 
 @[expose] public section
 
+namespace ProbabilisticTheory
+
 variable {E : Type*} [OrderUnitSpace E]
 
 namespace Effect
@@ -54,3 +56,5 @@ 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
+
+end ProbabilisticTheory
diff --git a/Physlib/ProbabilisticTheory/Effect/Metric.lean b/Physlib/ProbabilisticTheory/Effect/Metric.lean
index a206c08c1..4632a2ac3 100644
--- a/Physlib/ProbabilisticTheory/Effect/Metric.lean
+++ b/Physlib/ProbabilisticTheory/Effect/Metric.lean
@@ -32,6 +32,8 @@ Effects also correspond to points of the order-unit-norm ball, by the affine res
 
 @[expose] public section
 
+namespace ProbabilisticTheory
+
 open ArchimedeanOrderUnitSpace
 
 variable {E : Type*} [ArchimedeanOrderUnitSpace E]
@@ -105,3 +107,5 @@ noncomputable def effectEquiv : Effect E ≃ {A : E // orderUnitNorm A ≤ 1} wh
   right_inv A := Subtype.ext (two_smul_two_inv_smul_one_add_sub_one (A : E))
 
 end Effect
+
+end ProbabilisticTheory
diff --git a/Physlib/ProbabilisticTheory/Effect/Sharp.lean b/Physlib/ProbabilisticTheory/Effect/Sharp.lean
index 04c741001..44d36ebb9 100644
--- a/Physlib/ProbabilisticTheory/Effect/Sharp.lean
+++ b/Physlib/ProbabilisticTheory/Effect/Sharp.lean
@@ -30,6 +30,8 @@ be written as a nontrivial mixture of two distinct effects. Sharp effects genera
 
 @[expose] public section
 
+namespace ProbabilisticTheory
+
 namespace Effect
 
 variable {E : Type*} [OrderUnitSpace E]
@@ -70,3 +72,5 @@ lemma isSharp_one : IsSharp (1 : Effect E) :=
   complement_zero (E := E) ▸ isSharp_complement isSharp_zero
 
 end Effect
+
+end ProbabilisticTheory

From c16082949bcccc55f546bb68db0039479c7fe4f7 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 2 Oct 2026 05:29:11 +0100
Subject: [PATCH 2/3] feat: fix PhyslibAlpha build

---
 PhyslibAlpha.lean                             |   4 -
 .../CStarAlgebra/SharpEffect.lean             |   2 +-
 .../Channel/Operation.lean                    |   2 +-
 .../Classical/FiniteSystem.lean               |   2 +-
 .../ProbabilisticTheory/Effect/Basic.lean     |  58 ++--------
 .../Effect/Complement.lean                    |  84 --------------
 .../ProbabilisticTheory/Effect/Convex.lean    |  61 ----------
 .../ProbabilisticTheory/Effect/Metric.lean    | 109 ------------------
 .../ProbabilisticTheory/Effect/Sharp.lean     |  80 -------------
 .../JB/GeneratedByOne/Effect.lean             |   2 +-
 .../JordanOrderUnit/Observable.lean           |   3 +-
 .../Measurement/EffectValuedMeasure.lean      |   2 +-
 .../State/Discrimination.lean                 |  18 +--
 .../ProbabilisticTheory/State/Metric.lean     |  12 +-
 .../ProbabilisticTheory/State/Pairing.lean    |   2 +-
 15 files changed, 31 insertions(+), 410 deletions(-)
 delete mode 100644 PhyslibAlpha/ProbabilisticTheory/Effect/Complement.lean
 delete mode 100644 PhyslibAlpha/ProbabilisticTheory/Effect/Convex.lean
 delete mode 100644 PhyslibAlpha/ProbabilisticTheory/Effect/Metric.lean
 delete mode 100644 PhyslibAlpha/ProbabilisticTheory/Effect/Sharp.lean

diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean
index 4be967869..2ab231a9a 100644
--- a/PhyslibAlpha.lean
+++ b/PhyslibAlpha.lean
@@ -123,10 +123,6 @@ public import PhyslibAlpha.ProbabilisticTheory.Dynamics.Generator
 public import PhyslibAlpha.ProbabilisticTheory.Dynamics.GeneratorIsDerivation
 public import PhyslibAlpha.ProbabilisticTheory.Dynamics.OneParameterGroup
 public import PhyslibAlpha.ProbabilisticTheory.Effect.Basic
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Complement
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Convex
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Metric
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Sharp
 public import PhyslibAlpha.ProbabilisticTheory.Examples.GBit
 public import PhyslibAlpha.ProbabilisticTheory.Examples.NormCone
 public import PhyslibAlpha.ProbabilisticTheory.Examples.Qubit
diff --git a/PhyslibAlpha/ProbabilisticTheory/CStarAlgebra/SharpEffect.lean b/PhyslibAlpha/ProbabilisticTheory/CStarAlgebra/SharpEffect.lean
index 3f006b5e8..c836c4079 100644
--- a/PhyslibAlpha/ProbabilisticTheory/CStarAlgebra/SharpEffect.lean
+++ b/PhyslibAlpha/ProbabilisticTheory/CStarAlgebra/SharpEffect.lean
@@ -6,7 +6,7 @@ Authors: Tom Ole Diem
 module
 
 public import PhyslibAlpha.ProbabilisticTheory.CStarAlgebra.OrderUnit
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Sharp
+public import Physlib.ProbabilisticTheory.Effect.Sharp
 public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
 public import Mathlib.Analysis.CStarAlgebra.Basic
 public import Mathlib.Algebra.Module.Torsion.Free
diff --git a/PhyslibAlpha/ProbabilisticTheory/Channel/Operation.lean b/PhyslibAlpha/ProbabilisticTheory/Channel/Operation.lean
index af994d421..7a0b001fd 100644
--- a/PhyslibAlpha/ProbabilisticTheory/Channel/Operation.lean
+++ b/PhyslibAlpha/ProbabilisticTheory/Channel/Operation.lean
@@ -5,7 +5,7 @@ Authors: Tom Ole Diem
 -/
 module
 
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Sharp
+public import Physlib.ProbabilisticTheory.Effect.Sharp
 public import PhyslibAlpha.ProbabilisticTheory.Channel.Normal
 public import PhyslibAlpha.ProbabilisticTheory.State.Basic
 public import Mathlib.Algebra.Order.Module.PositiveLinearMap
diff --git a/PhyslibAlpha/ProbabilisticTheory/Classical/FiniteSystem.lean b/PhyslibAlpha/ProbabilisticTheory/Classical/FiniteSystem.lean
index a8187029e..400121bc3 100644
--- a/PhyslibAlpha/ProbabilisticTheory/Classical/FiniteSystem.lean
+++ b/PhyslibAlpha/ProbabilisticTheory/Classical/FiniteSystem.lean
@@ -5,7 +5,7 @@ Authors: Tom Ole Diem
 -/
 module
 
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Sharp
+public import Physlib.ProbabilisticTheory.Effect.Sharp
 public import Physlib.ProbabilisticTheory.OrderUnit.Archimedean
 public import PhyslibAlpha.ProbabilisticTheory.State.Convex
 public import PhyslibAlpha.Mathematics.Geometry.Simplex
diff --git a/PhyslibAlpha/ProbabilisticTheory/Effect/Basic.lean b/PhyslibAlpha/ProbabilisticTheory/Effect/Basic.lean
index 76f015dec..61aeb39a2 100644
--- a/PhyslibAlpha/ProbabilisticTheory/Effect/Basic.lean
+++ b/PhyslibAlpha/ProbabilisticTheory/Effect/Basic.lean
@@ -5,30 +5,24 @@ Authors: Tom Ole Diem
 -/
 module
 
-public import Mathlib.Tactic.Positivity
-public import Physlib.ProbabilisticTheory.OrderUnit.Cone
+public import Physlib.ProbabilisticTheory.Effect.Basic
 
 /-!
-# Effects
+# Orthogonal 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.
+Two effects are orthogonal when their sum is still an effect, that is, still bounded by the order
+unit. Their partial sum is then again an effect.
 
 ## 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.
+- `Effect.Orthogonal` : two effects whose sum is bounded by the order unit.
+- `Effect.addOfOrthogonal` : the partial sum of two orthogonal effects.
 
 ## iii. Table of contents
 
-- A. Effects
+- A. Orthogonal effects
 
 ## iv. References
 
@@ -43,40 +37,14 @@ namespace ProbabilisticTheory
 
 /-!
 
-## A. Effects
+## A. Orthogonal 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⟩
-
-instance instNonempty : Nonempty (Effect E) := ⟨0⟩
-
-@[simp] lemma coe_zero : ((0 : Effect E) : E) = 0 := rfl
-
-@[simp] lemma coe_one : ((1 : Effect E) : E) = 1 := rfl
-
 /-- Two effects are orthogonal when their sum is still bounded by the order unit. -/
 def Orthogonal (e f : Effect E) : Prop := (e : E) + (f : E) ≤ 1
 
@@ -89,16 +57,6 @@ def addOfOrthogonal (e f : Effect E) (h : Orthogonal e f) : Effect E :=
 lemma coe_addOfOrthogonal (e f : Effect E) (h : Orthogonal e f) :
     (addOfOrthogonal e f h : E) = (e : E) + (f : E) := 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 ℝ] at hn
-  refine ⟨((n : ℝ) + 1)⁻¹, by positivity, smul_nonneg (by positivity) hB, ?_⟩
-  rw [inv_smul_le_iff_of_pos (by positivity)]
-  exact hn.trans (smul_le_smul_of_nonneg_right (by linarith) one_nonneg)
-
 end Effect
 
 end ProbabilisticTheory
diff --git a/PhyslibAlpha/ProbabilisticTheory/Effect/Complement.lean b/PhyslibAlpha/ProbabilisticTheory/Effect/Complement.lean
deleted file mode 100644
index 5080a91ce..000000000
--- a/PhyslibAlpha/ProbabilisticTheory/Effect/Complement.lean
+++ /dev/null
@@ -1,84 +0,0 @@
-/-
-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 PhyslibAlpha.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 ProbabilisticTheory
-
-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 :=
-  Subtype.ext (show (1 : E) - ((t : ℝ) • (e : E) + (1 - (t : ℝ)) • (f : E))
-      = (t : ℝ) • ((1 : E) - (e : E)) + (1 - (t : ℝ)) • ((1 : E) - (f : E)) from by module)
-
-end Effect
-
-end ProbabilisticTheory
diff --git a/PhyslibAlpha/ProbabilisticTheory/Effect/Convex.lean b/PhyslibAlpha/ProbabilisticTheory/Effect/Convex.lean
deleted file mode 100644
index cf755bb7b..000000000
--- a/PhyslibAlpha/ProbabilisticTheory/Effect/Convex.lean
+++ /dev/null
@@ -1,61 +0,0 @@
-/-
-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 PhyslibAlpha.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
-
-namespace ProbabilisticTheory
-
-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
-
-end ProbabilisticTheory
diff --git a/PhyslibAlpha/ProbabilisticTheory/Effect/Metric.lean b/PhyslibAlpha/ProbabilisticTheory/Effect/Metric.lean
deleted file mode 100644
index dcd05b68f..000000000
--- a/PhyslibAlpha/ProbabilisticTheory/Effect/Metric.lean
+++ /dev/null
@@ -1,109 +0,0 @@
-/-
-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 PhyslibAlpha.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`
-makes them a metric space.
-
-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
-
-namespace ProbabilisticTheory
-
-open ArchimedeanOrderUnitSpace
-
-variable {E : Type*} [ArchimedeanOrderUnitSpace E]
-
-namespace Effect
-
-/-!
-
-## A. The effect metric
-
--/
-
-/-- Effects, metrized by the order-unit norm on `E`. -/
-noncomputable scoped instance instMetricSpace : MetricSpace (Effect E) :=
-  MetricSpace.induced Subtype.val Subtype.val_injective inferInstance
-
-open scoped Effect
-
-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 h2 := smul_le_smul_of_nonneg_left (add_le_add (le_refl (1 : E)) hAu)
-    (show (0 : ℝ) ≤ (2 : ℝ)⁻¹ by norm_num)
-  rw [show (1 : E) + 1 = (2 : ℝ) • (1 : E) from by module] at h2
-  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
-
-end ProbabilisticTheory
diff --git a/PhyslibAlpha/ProbabilisticTheory/Effect/Sharp.lean b/PhyslibAlpha/ProbabilisticTheory/Effect/Sharp.lean
deleted file mode 100644
index 6187f2644..000000000
--- a/PhyslibAlpha/ProbabilisticTheory/Effect/Sharp.lean
+++ /dev/null
@@ -1,80 +0,0 @@
-/-
-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 PhyslibAlpha.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 ProbabilisticTheory
-
-namespace Effect
-
-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 ⟨(0 : Effect E).2, 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 key : a • (1 - x₁) + b • (1 - x₂) = (e : E) := by
-    rw [show a • (1 - x₁) + b • (1 - x₂) = (a • (1 : E) + b • (1 : E)) - (a • x₁ + b • x₂) from
-      by module, ← add_smul, hab, one_smul, 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⟩
-  exact eq_sub_of_add_eq (by rw [← x1eq]; abel)
-
-/-- 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
-
-end ProbabilisticTheory
diff --git a/PhyslibAlpha/ProbabilisticTheory/JordanOrderUnit/JB/GeneratedByOne/Effect.lean b/PhyslibAlpha/ProbabilisticTheory/JordanOrderUnit/JB/GeneratedByOne/Effect.lean
index 658a5116d..c71230afe 100644
--- a/PhyslibAlpha/ProbabilisticTheory/JordanOrderUnit/JB/GeneratedByOne/Effect.lean
+++ b/PhyslibAlpha/ProbabilisticTheory/JordanOrderUnit/JB/GeneratedByOne/Effect.lean
@@ -6,7 +6,7 @@ Authors: Tom Ole Diem
 module
 
 public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.GeneratedByOne.CFC
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Sharp
+public import Physlib.ProbabilisticTheory.Effect.Sharp
 
 /-!
 
diff --git a/PhyslibAlpha/ProbabilisticTheory/JordanOrderUnit/Observable.lean b/PhyslibAlpha/ProbabilisticTheory/JordanOrderUnit/Observable.lean
index 55afee1bc..e28a07781 100644
--- a/PhyslibAlpha/ProbabilisticTheory/JordanOrderUnit/Observable.lean
+++ b/PhyslibAlpha/ProbabilisticTheory/JordanOrderUnit/Observable.lean
@@ -7,7 +7,8 @@ module
 
 public import PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Operator
 public import PhyslibAlpha.ProbabilisticTheory.State.Basic
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Sharp
+public import Physlib.ProbabilisticTheory.Effect.Sharp
+public import PhyslibAlpha.ProbabilisticTheory.Effect.Basic
 public import PhyslibAlpha.ProbabilisticTheory.Algebra.Statistics
 
 /-!
diff --git a/PhyslibAlpha/ProbabilisticTheory/Measurement/EffectValuedMeasure.lean b/PhyslibAlpha/ProbabilisticTheory/Measurement/EffectValuedMeasure.lean
index 3eb118632..959d5580e 100644
--- a/PhyslibAlpha/ProbabilisticTheory/Measurement/EffectValuedMeasure.lean
+++ b/PhyslibAlpha/ProbabilisticTheory/Measurement/EffectValuedMeasure.lean
@@ -6,7 +6,7 @@ Authors: Tom Ole Diem
 module
 
 public import Mathlib.MeasureTheory.MeasurableSpace.Defs
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Complement
+public import Physlib.ProbabilisticTheory.Effect.Complement
 public import Mathlib.Algebra.Order.BigOperators.Group.Finset
 
 /-!
diff --git a/PhyslibAlpha/ProbabilisticTheory/State/Discrimination.lean b/PhyslibAlpha/ProbabilisticTheory/State/Discrimination.lean
index 46c04bff9..4a26ce745 100644
--- a/PhyslibAlpha/ProbabilisticTheory/State/Discrimination.lean
+++ b/PhyslibAlpha/ProbabilisticTheory/State/Discrimination.lean
@@ -6,7 +6,7 @@ Authors: Tom Ole Diem
 module
 
 public import PhyslibAlpha.ProbabilisticTheory.State.Metric
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Complement
+public import Physlib.ProbabilisticTheory.Effect.Complement
 public import Mathlib.Algebra.Order.Group.CompleteLattice
 
 /-!
@@ -149,27 +149,27 @@ lemma ciSup_sub_eq_ciSup_abs_sub (ω₀ ω₁ : 𝓢[ℝ, E]) :
     exact abs_le.mpr ⟨by linarith, h1⟩
 
 /-- The state distance is the largest `|ω₀ e - ω₁ e|` over unit-ball effects
-(`Effect.equivBall`). -/
+(`Effect.effectEquiv`). -/
 lemma dist_eq_ciSup_abs_sub (ω₀ ω₁ : 𝓢[ℝ, E]) :
     dist ω₀ ω₁ =
-      ⨆ e : Effect E, |ω₀ ((Effect.equivBall e : E)) - ω₁ ((Effect.equivBall e : E))| := by
+      ⨆ e : Effect E, |ω₀ ((Effect.effectEquiv e : E)) - ω₁ ((Effect.effectEquiv e : E))| := by
   have hbdd' : BddAbove (Set.range
-      fun e : Effect E => |ω₀ ((Effect.equivBall e : E)) - ω₁ ((Effect.equivBall e : E))|) := by
+      fun e : Effect E => |ω₀ ((Effect.effectEquiv e : E)) - ω₁ ((Effect.effectEquiv e : E))|) := by
     obtain ⟨b, hb⟩ := dist_bddAbove ω₀ ω₁
-    exact ⟨b, by rintro _ ⟨e, rfl⟩; exact hb (Set.mem_range_self (Effect.equivBall e))⟩
+    exact ⟨b, by rintro _ ⟨e, rfl⟩; exact hb (Set.mem_range_self (Effect.effectEquiv 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)
+    rw [← Effect.effectEquiv.apply_symm_apply A]
+    exact le_ciSup hbdd' (Effect.effectEquiv.symm A)
+  · exact ciSup_le fun e => le_ciSup (dist_bddAbove ω₀ ω₁) (Effect.effectEquiv e)
 
 /-- The state distance is twice the largest state-value difference over all effects. -/
 lemma dist_eq_two_mul_ciSup_sub (ω₀ ω₁ : 𝓢[ℝ, E]) :
     dist ω₀ ω₁ = 2 * ⨆ e : Effect E, (ω₀ (e : E) - ω₁ (e : E)) := by
   rw [ciSup_sub_eq_ciSup_abs_sub, dist_eq_ciSup_abs_sub, Real.mul_iSup_of_nonneg zero_le_two]
   congr 1 with e
-  rw [apply_equivBall, apply_equivBall, ← abs_two, ← abs_mul]
+  rw [apply_effectEquiv, apply_effectEquiv, ← abs_two, ← abs_mul]
   ring_nf
 
 /-- For equal priors, the Helstrom bound is `1/2` plus a quarter of the state distance. -/
diff --git a/PhyslibAlpha/ProbabilisticTheory/State/Metric.lean b/PhyslibAlpha/ProbabilisticTheory/State/Metric.lean
index 1eb531021..4a5d60298 100644
--- a/PhyslibAlpha/ProbabilisticTheory/State/Metric.lean
+++ b/PhyslibAlpha/ProbabilisticTheory/State/Metric.lean
@@ -6,7 +6,7 @@ Authors: Tom Ole Diem
 module
 
 public import PhyslibAlpha.ProbabilisticTheory.State.Convex
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Metric
+public import Physlib.ProbabilisticTheory.Effect.Metric
 public import Mathlib.Topology.MetricSpace.HausdorffDistance
 
 /-!
@@ -126,12 +126,12 @@ lemma eq_of_dist_eq_zero {ω φ : 𝓢[ℝ, E]} (h : dist ω φ = 0) : ω = φ :
     have hB : |ω B - φ B| ≤ 0 := (le_ciSup (dist_bddAbove ω φ) ⟨B, hB1⟩).trans h.le
     rw [← hAB, map_smul, map_smul, sub_eq_zero.mp (abs_nonpos_iff.mp hB)]
 
-/-- A state's value at a doubled, re-centered effect (`Effect.equivBall`) is twice its value at
+/-- A state's value at a doubled, re-centered effect (`Effect.effectEquiv`) 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]
+lemma apply_effectEquiv (ψ : 𝓢[ℝ, E]) (e : Effect E) :
+    ψ ((Effect.effectEquiv e : E)) = 2 * ψ (e : E) - 1 := by
+  show ψ (2 • (e : E) - 1) = _
+  rw [map_sub, map_nsmul, map_one, nsmul_eq_mul, Nat.cast_ofNat]
 
 /-- States, metrized by the operator norm induced by the order-unit norm on `E`. -/
 noncomputable instance : MetricSpace (𝓢[ℝ, E]) where
diff --git a/PhyslibAlpha/ProbabilisticTheory/State/Pairing.lean b/PhyslibAlpha/ProbabilisticTheory/State/Pairing.lean
index df06e0ac9..70603c643 100644
--- a/PhyslibAlpha/ProbabilisticTheory/State/Pairing.lean
+++ b/PhyslibAlpha/ProbabilisticTheory/State/Pairing.lean
@@ -6,7 +6,7 @@ Authors: Tom Ole Diem
 module
 
 public import PhyslibAlpha.ProbabilisticTheory.State.Separation
-public import PhyslibAlpha.ProbabilisticTheory.Effect.Convex
+public import Physlib.ProbabilisticTheory.Effect.Convex
 
 /-!
 # The state–effect pairing

From d0ff94ebe58d16270bac58cbbd51a87d2236b7f2 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 2 Oct 2026 06:17:19 +0100
Subject: [PATCH 3/3] Update build.yml

---
 .github/workflows/build.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 7a6ec517a..1638f9a84 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -6,6 +6,7 @@ on:
   pull_request:
     branches:
       - master
+  merge_group:
 
 name: Style linters