@[implicit_reducible]

instance instMonoidForallOption_gaudisCrypt {m : Type u_1} : Monoid (m → Option m)

Kleisli composition for Option: apply g first, then f on the result.

Equations

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

structure OptionLensRange (m : Type u_1) : Type u_1

Analogue of DetermFootprint where updates are partial functions m → Option m composed via Kleisli composition for Option.

• updates : Set (m → Option m)
• one_mem : 1 ∈ self.updates
• mul_mem {f g : m → Option m} : f ∈ self.updates → g ∈ self.updates → f * g ∈ self.updates
• double_commutant : (Submonoid.centralizer (Submonoid.centralizer self.updates).carrier).carrier = self.updates

def OptionLensRange.from {m : Type u_1} (generators : Set (m → Option m)) : OptionLensRange m

Equations

• OptionLensRange.from generators = { updates := ↑(Submonoid.centralizer (Submonoid.centralizer generators).carrier), one_mem := ⋯, mul_mem := ⋯, double_commutant := ⋯ }

@[implicit_reducible]

instance instMonoidForallForallProp_gaudisCrypt {m : Type u_1} : Monoid (m → m → Prop)

Relational composition: (R * S) x z = ∃ y, S x y ∧ R y z (apply S first, then R — mirrors f * g = f ∘ g for functions).

Equations

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

structure RelLensRange (m : Type u_1) : Type u_1

Analogue of DetermFootprint where updates are relations on m composed via relational composition.

• updates : Set (m → m → Prop)
• one_mem : 1 ∈ self.updates
• mul_mem {R S : m → m → Prop} : R ∈ self.updates → S ∈ self.updates → R * S ∈ self.updates
• double_commutant : (Submonoid.centralizer (Submonoid.centralizer self.updates).carrier).carrier = self.updates

structure SubProbFootprint (m : Type u_1) : Type u_1

Analogue of DetermFootprint where updates are sub-probability kernels m → SubProbability m composed via Kleisli composition for SubProbability.

• updates : Set (m → GaudisCrypt.SubProbability m)
• one_mem : 1 ∈ self.updates
• mul_mem {f g : m → GaudisCrypt.SubProbability m} : f ∈ self.updates → g ∈ self.updates → f * g ∈ self.updates
• double_commutant : (Submonoid.centralizer (Submonoid.centralizer self.updates).carrier).carrier = self.updates

noncomputable def SubProbability.ofVector {a : Type u_1} [Fintype a] (v : a → NNReal) (hv : ∑ x : a, v x ≤ 1) : GaudisCrypt.SubProbability a

Convert a vector of non-negative weights (summing to at most 1) into a sub-probability measure on a finite type. The resulting measure assigns mass v x to the point x.

Equations

• SubProbability.ofVector v hv = ⟨∑ x : a, ↑(v x) • MeasureTheory.Measure.dirac x, ⋯⟩

noncomputable def SubProbability.ofMatrix {a : Type u_1} {b : Type u_2} [Fintype a] (M : Matrix a b NNReal) (hM : ∀ (j : b), ∑ i : a, M i j ≤ 1) : b → GaudisCrypt.SubProbability a

Convert a column-sub-stochastic matrix (each column sums to at most 1) into a probabilistic function b → SubProbability a. Column j of M gives the distribution ofMatrix M hM j.

With this convention ofMatrix is a monoid homomorphism: ofMatrix (M * N) = ofMatrix M * ofMatrix N.

Equations

• SubProbability.ofMatrix M hM j = SubProbability.ofVector (fun (i : a) => M i j) ⋯

theorem SubProbability.ofVector_inj {a : Type u_1} [Fintype a] {v w : a → NNReal} {hv : ∑ x : a, v x ≤ 1} {hw : ∑ x : a, w x ≤ 1} : ofVector v hv = ofVector w hw ↔ v = w

ofVector is injective: equal sub-probability measures imply equal weight vectors.

theorem SubProbability.ofMatrix_inj {a : Type u_1} {b : Type u_2} [Fintype a] {M N : Matrix a b NNReal} {hM : ∀ (j : b), ∑ i : a, M i j ≤ 1} {hN : ∀ (j : b), ∑ i : a, N i j ≤ 1} : ofMatrix M hM = ofMatrix N hN ↔ M = N

ofMatrix is injective.

theorem SubProbability.ofMatrix_zero {a : Type u_1} {b : Type u_2} [Fintype a] : ofMatrix 0 ⋯ = fun (x : b) => ⊥

The zero matrix maps to the zero (bottom) sub-probability kernel.

theorem SubProbability.ofMatrix_one {a : Type u_1} [Fintype a] : ofMatrix 1 ⋯ = pure

The identity matrix maps to pure (the Kleisli identity).

theorem SubProbability.ofMatrix_mul {a : Type u_1} [Fintype a] {M N : Matrix a a NNReal} {hM : ∀ (j : a), ∑ i : a, M i j ≤ 1} {hN : ∀ (j : a), ∑ i : a, N i j ≤ 1} {hMN : ∀ (j : a), ∑ i : a, (M * N) i j ≤ 1} : ofMatrix M hM * ofMatrix N hN = ofMatrix (M * N) hMN

ofMatrix is a monoid homomorphism: it maps matrix products to Kleisli products. The Kleisli product ofMatrix M * ofMatrix N applies N first then M, which corresponds to the matrix product M * N.

noncomputable def CE1.p_matrix : Matrix (Fin 3) (Fin 3) NNReal

The matrix for p from Counterexample 1 (column convention: column j = distribution over outputs given input j).

• Column 0: uniform on {1, 2}
• Column 1: uniform on {0, 1}
• Column 2: uniform on {0, 2}

Equations

• CE1.p_matrix = !![0, 1 / 2, 1 / 2; 1 / 2, 1 / 2, 0; 1 / 2, 0, 1 / 2]

noncomputable def CE1.q_matrix : Matrix (Fin 3) (Fin 3) NNReal

The matrix for q from Counterexample 1 (column convention).

• Column 0: uniform on {1, 2}
• Column 1: Dirac at 0
• Column 2: Dirac at 0

Equations

• CE1.q_matrix = !![0, 1, 1; 1 / 2, 0, 0; 1 / 2, 0, 0]

noncomputable def CE1.p : Fin 3 → GaudisCrypt.SubProbability (Fin 3)

The probabilistic function p from Counterexample 1, as SubProbability.ofMatrix p_matrix.

Equations

• CE1.p = SubProbability.ofMatrix CE1.p_matrix CE1.p._proof_1

noncomputable def CE1.q : Fin 3 → GaudisCrypt.SubProbability (Fin 3)

The probabilistic function q from Counterexample 1, as SubProbability.ofMatrix q_matrix.

Equations

• CE1.q = SubProbability.ofMatrix CE1.q_matrix CE1.q._proof_1

theorem CE1.matrices_not_commute : p_matrix * q_matrix ≠ q_matrix * p_matrix

p_matrix and q_matrix do not commute as matrices. Witness: entry (0, 0) is 1/2 in p_matrix * q_matrix but 1 in q_matrix * p_matrix.

theorem CE1.pq_not_commute : p * q ≠ q * p

p and q do not commute in the Kleisli monoid, because p_matrix and q_matrix do not commute as matrices.

def Centralizer {α : Type u_1} {β : Type u_2} (commutes : α → β → Prop) (S : Set α) : Set β

The centralizer of a set S ⊆ α with respect to a binary relation commutes : α → β → Prop: the set of all b : β that commute with every element of S.

Equations

• Centralizer commutes S = {b : β | ∀ a ∈ S, commutes a b}

def functionMatrix {m : Type u_1} [DecidableEq m] (f : m → m) : Matrix m m NNReal

The function matrix of f : m → m in column convention: column j is the Dirac distribution at f j, i.e., P_f i j = 1 iff i = f j.

Equations

• functionMatrix f = Matrix.of fun (i j : m) => if i = f j then 1 else 0

def commuteMT {m : Type u_1} [Fintype m] [DecidableEq m] (M : Matrix m m NNReal) (f : Function.End m) : Prop

A stochastic matrix M commutes with a total function f : m → m if M * P_f = P_f * M, where P_f is the function matrix of f.

Equations

• commuteMT M f = (M * functionMatrix f = functionMatrix f * M)

def commuteST {m : Type u_1} (F : m → GaudisCrypt.SubProbability m) (f : Function.End m) : Prop

A stochastic map F : m → SubProbability m commutes with a total function f : m → m if F * (pure ∘ f) = (pure ∘ f) * F in the Kleisli monoid, i.e., ∀ x, F (f x) = F x >>= fun y => pure (f y).

Equations

• commuteST F f = (F * pure ∘ f = pure ∘ f * F)

def partialFunctionMatrix {m : Type u_1} [DecidableEq m] (f : m → Option m) : Matrix m m NNReal

The partial-function matrix of f : m → Option m in column convention: column j is the Dirac column at i when f j = some i, and the zero column when f j = none, i.e. P_f i j = 1 iff f j = some i.

Equations

• partialFunctionMatrix f = Matrix.of fun (i j : m) => if f j = some i then 1 else 0

def commuteMP {m : Type u_1} [Fintype m] [DecidableEq m] (M : Matrix m m NNReal) (f : m → Option m) : Prop

A stochastic matrix M commutes with a partial function f : m → Option m if M * P_f = P_f * M, where P_f is the partial-function matrix of f.

Equations

• commuteMP M f = (M * partialFunctionMatrix f = partialFunctionMatrix f * M)

noncomputable def partialToKernel {m : Type u_1} (f : m → Option m) : m → GaudisCrypt.SubProbability m

The sub-probability kernel of a partial function f : m → Option m: f x = some y maps to pure y (Dirac at y), and f x = none maps to ⊥ (the zero sub-probability measure).

Equations

• partialToKernel f x = (f x).elim ⊥ pure

def commuteSP {m : Type u_1} (F : m → GaudisCrypt.SubProbability m) (f : m → Option m) : Prop

A stochastic map F : m → SubProbability m commutes with a partial function f : m → Option m if F * partialToKernel f = partialToKernel f * F in the Kleisli monoid.

Equations

• commuteSP F f = (F * partialToKernel f = partialToKernel f * F)

theorem functionMatrix_colSum {a : Type u_1} [Fintype a] [DecidableEq a] (f : a → a) (j : a) : ∑ i : a, functionMatrix f i j = 1

Each column of functionMatrix f sums to 1 (it is a Dirac column).

theorem pure_comp_eq_ofMatrix {a : Type u_1} [Fintype a] [DecidableEq a] (f : a → a) (hf : ∀ (j : a), ∑ i : a, functionMatrix f i j ≤ 1) : pure ∘ f = SubProbability.ofMatrix (functionMatrix f) hf

The Kleisli identity pure ∘ f of a total function is the sub-probability kernel of its function matrix functionMatrix f.

theorem commuteST_ofMatrix_iff {a : Type u_1} [Fintype a] [DecidableEq a] (M : Matrix a a NNReal) (hM : ∀ (j : a), ∑ i : a, M i j ≤ 1) (f : a → a) : commuteST (SubProbability.ofMatrix M hM) f ↔ commuteMT M f

commuteST (ofMatrix M) f reduces to the matrix-level commuteMT M f, via multiplicativity (ofMatrix_mul) and injectivity (ofMatrix_inj) of ofMatrix.

theorem partialFunctionMatrix_colSum_le {a : Type u_1} [Fintype a] [DecidableEq a] (f : a → Option a) (j : a) : ∑ i : a, partialFunctionMatrix f i j ≤ 1

Each column of partialFunctionMatrix f sums to at most 1 (a Dirac column, or the zero column when f j = none).

theorem partialToKernel_eq_ofMatrix {a : Type u_1} [Fintype a] [DecidableEq a] (f : a → Option a) (hf : ∀ (j : a), ∑ i : a, partialFunctionMatrix f i j ≤ 1) : partialToKernel f = SubProbability.ofMatrix (partialFunctionMatrix f) hf

The kernel partialToKernel f of a partial function is the sub-probability kernel of its partial-function matrix.

theorem commuteSP_ofMatrix_iff {a : Type u_1} [Fintype a] [DecidableEq a] (M : Matrix a a NNReal) (hM : ∀ (j : a), ∑ i : a, M i j ≤ 1) (f : a → Option a) : commuteSP (SubProbability.ofMatrix M hM) f ↔ commuteMP M f

commuteSP (ofMatrix M) f reduces to the matrix-level commuteMP M f, via multiplicativity (ofMatrix_mul) and injectivity (ofMatrix_inj) of ofMatrix.

def hullST {m : Type u_1} (S : Set (m → GaudisCrypt.SubProbability m)) : Set (Function.End m)

The deterministic bicommutant C(C(S)) of a set of stochastic kernels S: the Submonoid.centralizer (in the composition monoid m → m) of the deterministic centralizer Centralizer commuteST S. Returned as a Set (m → m) (the submonoid carrier) so it can feed DetermFootprint.from.

Equations

• hullST S = (Submonoid.centralizer (Centralizer commuteST S)).carrier

def hullSP {m : Type u_1} (S : Set (m → GaudisCrypt.SubProbability m)) : Set (m → Option m)

The partial-function bicommutant C(C(S)) of a set of stochastic kernels S: the Submonoid.centralizer (in the Kleisli-Option monoid m → Option m) of the partial centralizer Centralizer commuteSP S. The partial analogue of hullST.

Equations

• hullSP S = (Submonoid.centralizer (Centralizer commuteSP S)).carrier

def CE1.tau : Function.End (Fin 3)

The swap permutation τ = (2 3), swapping indices 1 and 2 (0-indexed), as a total function on Fin 3.

Equations

• CE1.tau = ![0, 2, 1]

theorem CE1.centralizer_p_matrix : Centralizer commuteMT {p_matrix} = {id, tau}

The deterministic centralizer of {p_matrix} is exactly {id, τ}, matching the claim C({p}) = {id, τ} in Counterexample 1.

Forward direction is a finite case bash over all 27 functions Fin 3 → Fin 3 (decide is unavailable since NNReal has no computable DecidableEq): only id and τ satisfy the matrix commutation p_matrix * P_f = P_f * p_matrix.

theorem CE1.centralizer_q_matrix : Centralizer commuteMT {q_matrix} = {id, tau}

The deterministic centralizer of {q_matrix} is exactly {id, τ}, matching the claim C({q}) = {id, τ} in Counterexample 1.

Same finite case bash over all 27 functions Fin 3 → Fin 3 as centralizer_p_matrix: only id and τ satisfy q_matrix * P_f = P_f * q_matrix.

theorem CE1.centralizer_p : Centralizer commuteST {p} = {id, tau}

The stochastic centralizer of {p} equals {id, τ}, by reduction to the matrix-level centralizer_p_matrix through commuteST_ofMatrix_iff.

theorem CE1.centralizer_q : Centralizer commuteST {q} = {id, tau}

The stochastic centralizer of {q} equals {id, τ}, by reduction to the matrix-level centralizer_q_matrix through commuteST_ofMatrix_iff.

def CE1.c₁ : Fin 3 → Fin 3

The constant map to 0, the unique fixed point of τ = (2 3).

Equations

• CE1.c₁ x✝ = 0

theorem CE1.centralizer_id_tau : ↑(Submonoid.centralizer {id, tau}) = {id, tau, c₁}

Helper for the deterministic bicommutant: the total functions commuting under composition with both id and τ are exactly {id, τ, c₁}, where c₁ is the constant map to τ's fixed point 0.

Stated over Function.End (Fin 3) to pin the composition monoid unambiguously: the bare type Fin 3 → Fin 3 carries two Monoid instances here (pointwise and composition), and the composition one is definitionally equal to Function.End's, so this transfers by defeq.

theorem CE1.hullST_p_commutes_q (f : Function.End (Fin 3)) : f ∈ hullST {p} → ∀ g ∈ hullST {q}, f * g = g * f

Both deterministic bicommutants C(C({p})) and C(C({q})) equal {id, τ, c₁}, an abelian set under composition; hence every element of hullST {p} commutes with every element of hullST {q}. This is the (satisfied) hypothesis of the implication that Counterexample 1 refutes — even though p and q themselves do not commute (not_commute).

theorem CE1.from_hullST_updates {m : Type u_1} (S : Set (m → GaudisCrypt.SubProbability m)) : (DetermFootprint.from (hullST S)).updates = hullST S

hullST S is already double-commutant closed, i.e. it is a genuine DetermFootprint: the DetermFootprint.from it generates returns exactly hullST S. This holds because hullST S is a single centralizer and C∘C∘C = C (Set.centralizer_centralizer_centralizer).

theorem CE1.theorem_negated : ¬∀ (m : Type) (p q : m → GaudisCrypt.SubProbability m), (∀ f ∈ hullST {p}, ∀ g ∈ hullST {q}, f * g = g * f) → p * q = q * p

noncomputable def CE2.p_matrix : Matrix (Fin 4) (Fin 4) NNReal

The matrix for p from Counterexample 2: the simple random walk on the 4-cycle 0-1-2-3-0 (column convention: column j is the output distribution from state j). p_matrix i j = 1/2 exactly when i and j are adjacent on the cycle. It is symmetric, so it coincides with the row-stochastic matrix in the text.

Equations

• CE2.p_matrix = !![0, 1 / 2, 0, 1 / 2; 1 / 2, 0, 1 / 2, 0; 0, 1 / 2, 0, 1 / 2; 1 / 2, 0, 1 / 2, 0]

noncomputable def CE2.q_matrix : Matrix (Fin 4) (Fin 4) NNReal

The matrix for q from Counterexample 2: the "forgetful" kernel that ignores the current state and jumps to 0 or 2 with equal probability (column convention). Every column is (1/2, 0, 1/2, 0)ᵀ; this is the transpose of the row-stochastic q = 𝟙 rᵀ, r = (1/2, 0, 1/2, 0), in the text.

Equations

• CE2.q_matrix = !![1 / 2, 1 / 2, 1 / 2, 1 / 2; 0, 0, 0, 0; 1 / 2, 1 / 2, 1 / 2, 1 / 2; 0, 0, 0, 0]

theorem CE2.matrices_not_commute : p_matrix * q_matrix ≠ q_matrix * p_matrix

p_matrix and q_matrix do not commute as matrices. Witness: entry (0, 1) is 0 in p_matrix * q_matrix but 1/2 in q_matrix * p_matrix.

noncomputable def CE2.p : Fin 4 → GaudisCrypt.SubProbability (Fin 4)

The probabilistic kernel p from Counterexample 2, as SubProbability.ofMatrix p_matrix.

Equations

• CE2.p = SubProbability.ofMatrix CE2.p_matrix CE2.p._proof_1

noncomputable def CE2.q : Fin 4 → GaudisCrypt.SubProbability (Fin 4)

The probabilistic kernel q from Counterexample 2, as SubProbability.ofMatrix q_matrix.

Equations

• CE2.q = SubProbability.ofMatrix CE2.q_matrix CE2.q._proof_1

theorem CE2.pq_not_commute : p * q ≠ q * p

def CE2.Aadj : Matrix (Fin 4) (Fin 4) ℕ

The integer cycle-adjacency matrix A = 2 · p_matrix (entries in {0,1}).

Equations

• CE2.Aadj = !![0, 1, 0, 1; 1, 0, 1, 0; 0, 1, 0, 1; 1, 0, 1, 0]

def CE2.pfNat (f : Fin 4 → Option (Fin 4)) : Matrix (Fin 4) (Fin 4) ℕ

The integer {0,1} partial-function matrix (column convention), the ℕ-valued analogue of partialFunctionMatrix.

Equations

• CE2.pfNat f = Matrix.of fun (i j : Fin 4) => if f j = some i then 1 else 0

def CE2.Badj : Matrix (Fin 4) (Fin 4) ℕ

The integer "forgetful" matrix B = 2 · q_matrix (entries in {0,1}).

Equations

• CE2.Badj = !![1, 1, 1, 1; 0, 0, 0, 0; 1, 1, 1, 1; 0, 0, 0, 0]

theorem CE2.commuteMP_iff_intAdj {M : Matrix (Fin 4) (Fin 4) NNReal} {A : Matrix (Fin 4) (Fin 4) ℕ} (hM : M = (1 / 2) • A.map Nat.cast) (f : Fin 4 → Option (Fin 4)) : commuteMP M f ↔ A * pfNat f = pfNat f * A

General bridge: if a stochastic matrix is ½ · A for an integer matrix A, then commuteMP M f is equivalent to the integer matrix equation A · P_f = P_f · A. Since the {0,1}-matrix partialFunctionMatrix f is the Nat.cast image of pfNat f, scaling by the nonzero ½ and the injectivity of ℕ ↪ ℝ≥0 reduce the NNReal commutation to a decidable condition over ℕ.

theorem CE2.commuteMP_p_iff (f : Fin 4 → Option (Fin 4)) : commuteMP p_matrix f ↔ Aadj * pfNat f = pfNat f * Aadj

commuteMP p_matrix f is the decidable integer equation A · P_f = P_f · A.

theorem CE2.commuteMP_q_iff (f : Fin 4 → Option (Fin 4)) : commuteMP q_matrix f ↔ Badj * pfNat f = pfNat f * Badj

commuteMP q_matrix f is the decidable integer equation B · P_f = P_f · B.

theorem CE2.centralizer_p_matrix : Centralizer commuteMP {p_matrix} = {![none, none, none, none], ![some 0, some 1, some 2, some 3], ![some 0, some 3, some 2, some 1], ![some 1, some 0, some 3, some 2], ![some 1, some 2, some 3, some 0], ![some 2, some 1, some 0, some 3], ![some 2, some 3, some 0, some 1], ![some 3, some 0, some 1, some 2], ![some 3, some 2, some 1, some 0]}

The deterministic-partial centralizer of {p_matrix} is exactly D₄ ∪ {∅}: the eight dihedral symmetries of the 4-cycle (all total bijections) together with the empty partial function ∅. This is the partial-function first centralizer A_p of Counterexample 2: D₄ ⊆ A_p holds, and the only proper partial map commuting with p is ∅.

def CE2.qCentralizerSet : Finset (Fin 4 → Option (Fin 4))

The 33 partial functions making up Centralizer commuteMP {q_matrix}, as a Finset (a flat-decidable carrier keeps the decide below tractable): the empty partial function ∅, plus every total map sending the antipodal pair {0, 2} to itself (f 0, f 2 equal to 0, 2 in some order) with f 1, f 3 arbitrary.

Equations

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

theorem CE2.centralizer_q_matrix : Centralizer commuteMP {q_matrix} = ↑qCentralizerSet

The deterministic-partial centralizer of {q_matrix} is A_q of Counterexample 2: the empty partial function ∅ together with the 32 total maps that fix the antipodal pair {0, 2} setwise (identity or swap on it) and are arbitrary on {1, 3}. In particular it contains ρ = (0 2)(1 3), the fact the text uses (ρ ∈ A_q).

def CE2.pBicommutantSet : Finset (Fin 4 → Option (Fin 4))

The partial-function bicommutant B_p = {∅, id, ρ} of Counterexample 2, where ρ = (0 2)(1 3), as a Finset (the Kleisli-Option monoid is decidable, and a Finset target keeps the decide below tractable).

Equations

• CE2.pBicommutantSet = {![none, none, none, none], ![some 0, some 1, some 2, some 3], ![some 2, some 3, some 0, some 1]}

def CE2.qBicommutantSet : Finset (Fin 4 → Option (Fin 4))

The partial-function bicommutant B_q = {∅, id} of Counterexample 2, as a Finset.

Equations

• CE2.qBicommutantSet = {![none, none, none, none], ![some 0, some 1, some 2, some 3]}

theorem CE2.centralizer_p_SP : Centralizer commuteSP {p} = {![none, none, none, none], ![some 0, some 1, some 2, some 3], ![some 0, some 3, some 2, some 1], ![some 1, some 0, some 3, some 2], ![some 1, some 2, some 3, some 0], ![some 2, some 1, some 0, some 3], ![some 2, some 3, some 0, some 1], ![some 3, some 0, some 1, some 2], ![some 3, some 2, some 1, some 0]}

The partial-function centralizer of the kernel p equals that of its matrix p_matrix (= A_p = D₄ ∪ {∅}), via commuteSP_ofMatrix_iff and centralizer_p_matrix.

theorem CE2.centralizer_q_SP : Centralizer commuteSP {q} = ↑qCentralizerSet

The partial-function centralizer of the kernel q equals that of its matrix q_matrix (= A_q = ↑qCentralizerSet), via commuteSP_ofMatrix_iff and centralizer_q_matrix.

theorem CE2.hullSP_p : hullSP {p} = ↑pBicommutantSet

The partial-function bicommutant B_p = hullSP {p} of the kernel p (in the Kleisli-Option monoid) is exactly {∅, id, ρ} with ρ = (0 2)(1 3), as claimed in Counterexample 2. Rewrites A_p = Centralizer commuteSP {p} to its explicit 9-element value (centralizer_p_SP); the centralizer is then a decidable computation.

theorem CE2.hullSP_q : hullSP {q} = ↑qBicommutantSet

The partial-function bicommutant B_q = hullSP {q} of the kernel q (in the Kleisli-Option monoid) is exactly {∅, id}: A_q is so large that its centralizer collapses to the trivial maps. In particular ρ = (0 2)(1 3) ∈ A_q commutes with all of B_q — the key step in Counterexample 2 (combined with ρ ∈ B_p).

theorem CE2.bicommutants_commute (f : Fin 4 → Option (Fin 4)) : f ∈ hullSP {p} → ∀ g ∈ hullSP {q}, f * g = g * f

Counterexample 2, the punchline. The partial-function bicommutants B_p = hullSP {p} and B_q = hullSP {q} commute elementwise (under Kleisli composition): every f ∈ B_p = {∅,id,ρ} commutes with every g ∈ B_q = {∅, id}. Yet p and q do not commute (matrices_not_commute) — so the bicommutants commuting does not imply the underlying kernels commute, even in the partial setting.

theorem CE2.from_hullSP_updates {m : Type u_1} (S : Set (m → GaudisCrypt.SubProbability m)) : (OptionLensRange.from (hullSP S)).updates = hullSP S

theorem CE2.theorem_negated : ¬∀ (m : Type) (p q : m → GaudisCrypt.SubProbability m), (∀ f ∈ hullSP {p}, ∀ g ∈ hullSP {q}, f * g = g * f) → p * q = q * p