Definitions for Bipartite Units of Non-Locality

Definition

QAlgorithms_Papers_Independent_Intakethird100_P78

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

The objects the formalized statements of Bipartite Units of Non-Locality (arXiv:0808.0651) are stated in. Each was checked against the paper by a blind read-back and a moderator.

BipartiteConditionalArray: PDF p.2: a conditional array, before imposing probability and no-signaling conditions. The two input and two output alphabets may differ.
BipartiteSystem: PDF pp.2–3: the finite bipartite systems considered in this paper. Nonempty alphabets are imposed at each theorem using this structure. The two marginal equalities express no-signaling for both proper subsets.
simulationDistance: PDF p.2, Definition 1: worst-input total variation. The range whose supremum is taken is finite and nonempty, hence bounded and nonempty; there is no default empty/unbounded real supremum in the stated domain.
graphKernel: PDF p.3, Definition 3: uniform graph law of a family of maps. This raw array belongs to D precisely when d > 1 and the maps are permutations; that condition is stated by IsPermutationSystem below.
IsPermutationSystem: PDF p.3, Definition 3: membership in D, without presupposing that a constructed candidate map is bijective.
liftLabel: PDF p.4, (8): zero-based form of r_hat, which exchanges the omitted label with the last label. Here d = m + 1.
dropLabel: PDF p.4, inverse of (8), on the complement of hat. Modulo gives a specified total extension off that complement. For a valid complement label the swapped value is less than m, so modulo does not change it. All uses in the reduction have this valid-complement property as a consequence of the given permutation, rather than an extra hypothesis.
reducedMap: PDF p.4, corrected (7): set u = r_ahat(a), replace f(u) by f(ahat) exactly when f(u) = bhat, then apply r_bhat inverse. Printed (7) instead tests f(a) = bhat, a != ahat; this fails when f(last) = bhat and ahat is not last. This definition implements the deletion-and-splicing construction described in the text and Figures 4–5.
reducedKernel: PDF pp.4–5: the computed smaller resource has augmented local inputs (x,ahat) and (y,bhat), and m outputs on each side.
roundKernel: PDF p.5, four-step round: a fresh shared coin, independent of the resource, keeps (ahat,bhat) with mass 1/(m+1). Otherwise, the smaller resource's outputs are relabeled separately. The sum explicitly uses that resource; no unconstrained transition probability is supplied.
finiteRoundKernel: PDF pp.5,7, exact-resource experiment: start from independent uniform local labels and apply n rounds. The convolution uses a fresh coin and an independent exact resource copy in each round. This specifies this particular synchronous construction, not the general wiring model.
relabeledKernel: PDF p.8, Lemma 5 proof: one permutation resource followed by local relabelings depending solely on the corresponding test input.
IsRational: PDF p.8: entirely rational probabilities; zeros and ones are allowed.
HasCommonProbabilityDenominator: PDF p.8: a padded common denominator d, not necessarily the least one. Nonnegative integer numerators are appropriate because these are probabilities. Padding to d >= 2 retains deterministic target systems in Definition 3.

Definition code

import Mathlib

/-!
# Bipartite Units of Nonlocality (arXiv:0808.0651v4)

Finite-law statements from PDF pp.4–8. Equation (7) is corrected by testing
f(r_hat(a)) rather than f(a); the deleted edge is spliced as described in the
plan. The printed R in the rational-case paragraph on p.8 is corrected to D.
Both corrections require independent moderation. General wiring results and
the disputed adaptive lemmas are explicitly deferred in the unit artifacts.
No unreviewed module or paper-specific quantum-information predicate is used.
-/

noncomputable section

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P78

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.2: a conditional array, before imposing probability and no-signaling
conditions. The two input and two output alphabets may differ. -/
abbrev BipartiteConditionalArray (X Y A B : Type) := X → Y → A → B → ℝ

/-- PDF pp.2–3: the finite bipartite systems considered in this paper.
Nonempty alphabets are imposed at each theorem using this structure.
The two marginal equalities express no-signaling for both proper subsets. -/
structure BipartiteSystem (X Y A B : Type) [Fintype A] [Fintype B] where
  prob : BipartiteConditionalArray X Y A B
  nonnegative : ∀ x y a b, 0 ≤ prob x y a b
  normalized : ∀ x y, ∑ a, ∑ b, prob x y a b = 1
  aliceNS : ∀ x y z a, ∑ b, prob x y a b = ∑ b, prob x z a b
  bobNS : ∀ x z y b, ∑ a, prob x y a b = ∑ a, prob z y a b

/-- PDF p.2, Definition 1: worst-input total variation. The range whose
supremum is taken is finite and nonempty, hence bounded and nonempty;
there is no default empty/unbounded real supremum in the stated domain. -/
def simulationDistance {X Y A B : Type}
    [Fintype X] [Fintype Y] [Fintype A] [Fintype B]
    [Nonempty X] [Nonempty Y]
    (S T : BipartiteConditionalArray X Y A B) : ℝ :=
  sSup (Set.range fun xy : X × Y =>
    (∑ a, ∑ b, |S xy.1 xy.2 a b - T xy.1 xy.2 a b|) / 2)

/-- PDF p.3, Definition 3: uniform graph law of a family of maps.
This raw array belongs to D precisely when d > 1 and the maps are
permutations; that condition is stated by IsPermutationSystem below. -/
def graphKernel {X Y : Type} {d : ℕ}
    (F : X → Y → Fin d → Fin d) : BipartiteConditionalArray X Y (Fin d) (Fin d) :=
  fun x y a b => if F x y a = b then 1 / (d : ℝ) else 0

/-- PDF p.3, Definition 3: membership in D, without presupposing that a
constructed candidate map is bijective. -/
def IsPermutationSystem {X Y : Type} {d : ℕ}
    (P : BipartiteConditionalArray X Y (Fin d) (Fin d)) : Prop :=
  1 < d ∧ ∃ F : X → Y → Fin d → Fin d,
    (∀ x y, Function.Bijective (F x y)) ∧ P = graphKernel F

/-- PDF p.4, (8): zero-based form of r_hat, which exchanges the omitted
label with the last label. Here d = m + 1. -/
def liftLabel {m : ℕ} (hat : Fin (m + 1)) (a : Fin m) : Fin (m + 1) :=
  Equiv.swap hat (Fin.last m) a.castSucc

/-- PDF p.4, inverse of (8), on the complement of hat. Modulo gives a
specified total extension off that complement. For a valid complement
label the swapped value is less than m, so modulo does not change it.
All uses in the reduction have this valid-complement property as a
consequence of the given permutation, rather than an extra hypothesis. -/
def dropLabel {m : ℕ} (hm : 0 < m)
    (hat v : Fin (m + 1)) : Fin m :=
  ⟨(Equiv.swap hat (Fin.last m) v).val % m, Nat.mod_lt _ hm⟩

/-- PDF p.4, corrected (7): set u = r_ahat(a), replace f(u) by f(ahat)
exactly when f(u) = bhat, then apply r_bhat inverse. Printed (7) instead
tests f(a) = bhat, a != ahat; this fails when f(last) = bhat and ahat
is not last. This definition implements the deletion-and-splicing
construction described in the text and Figures 4–5. -/
def reducedMap {m : ℕ} (hm : 0 < m)
    (f : Equiv.Perm (Fin (m + 1)))
    (ahat bhat : Fin (m + 1)) (a : Fin m) : Fin m :=
  let u := liftLabel ahat a
  dropLabel hm bhat (if f u = bhat then f ahat else f u)

/-- PDF pp.4–5: the computed smaller resource has augmented local inputs
(x,ahat) and (y,bhat), and m outputs on each side. -/
def reducedKernel {X Y : Type} {m : ℕ} (hm : 0 < m)
    (F : X → Y → Equiv.Perm (Fin (m + 1))) :
    BipartiteConditionalArray (X × Fin (m + 1)) (Y × Fin (m + 1)) (Fin m) (Fin m) :=
  graphKernel (fun xa yb => reducedMap hm (F xa.1 yb.1) xa.2 yb.2)

/-- PDF p.5, four-step round: a fresh shared coin, independent of the
resource, keeps (ahat,bhat) with mass 1/(m+1). Otherwise, the smaller
resource's outputs are relabeled separately. The sum explicitly uses
that resource; no unconstrained transition probability is supplied. -/
def roundKernel {m : ℕ} (hm : 0 < m)
    (f : Equiv.Perm (Fin (m + 1)))
    (ahat bhat a b : Fin (m + 1)) : ℝ :=
  (if a = ahat ∧ b = bhat then 1 / ((m + 1 : ℕ) : ℝ) else 0) +
    (m : ℝ) / ((m + 1 : ℕ) : ℝ) *
      ∑ u : Fin m, ∑ v : Fin m,
        if liftLabel ahat u = a ∧ liftLabel bhat v = b then
          (if reducedMap hm f ahat bhat u = v then 1 / (m : ℝ) else 0)
        else 0

/-- PDF pp.5,7, exact-resource experiment: start from independent uniform
local labels and apply n rounds. The convolution uses a fresh coin and
an independent exact resource copy in each round. This specifies this
particular synchronous construction, not the general wiring model. -/
def finiteRoundKernel {X Y : Type} {m : ℕ} (hm : 0 < m)
    (F : X → Y → Equiv.Perm (Fin (m + 1))) :
    ℕ → BipartiteConditionalArray X Y (Fin (m + 1)) (Fin (m + 1))
  | 0 => fun _ _ _ _ => 1 / (((m + 1 : ℕ) : ℝ) ^ 2)
  | n + 1 => fun x y a b =>
      ∑ ahat, ∑ bhat,
        finiteRoundKernel hm F n x y ahat bhat *
          roundKernel hm (F x y) ahat bhat a b

/-- PDF p.8, Lemma 5 proof: one permutation resource followed by local
relabelings depending solely on the corresponding test input. -/
def relabeledKernel {X Y A B : Type} {d : ℕ}
    (F : X → Y → Equiv.Perm (Fin d))
    (alice : X → Fin d → A) (bob : Y → Fin d → B) : BipartiteConditionalArray X Y A B :=
  fun x y a b => ∑ u : Fin d,
    if alice x u = a ∧ bob y (F x y u) = b then 1 / (d : ℝ) else 0

/-- PDF p.8: entirely rational probabilities; zeros and ones are allowed. -/
def IsRational {X Y A B : Type} (P : BipartiteConditionalArray X Y A B) : Prop :=
  ∀ x y a b, ∃ q : ℚ, (q : ℝ) = P x y a b

/-- PDF p.8: a padded common denominator d, not necessarily the least one.
Nonnegative integer numerators are appropriate because these are probabilities.
Padding to d >= 2 retains deterministic target systems in Definition 3. -/
def HasCommonProbabilityDenominator {X Y A B : Type} (P : BipartiteConditionalArray X Y A B) (d : ℕ) : Prop :=
  ∀ x y a b, ∃ k : ℕ, P x y a b = (k : ℝ) / (d : ℝ)

-- Sanity: a deterministic singleton-output law is a legitimate no-signaling
-- system; the target alphabets need not have two distinct outputs.
example : BipartiteSystem Unit Unit Unit Unit where
  prob := fun _ _ _ _ => 1
  nonnegative := by intros; norm_num
  normalized := by intros; simp
  aliceNS := by intros; rfl
  bobNS := by intros; rfl

-- Sanity for (8): deleting the last label leaves the remaining labels fixed.
example {m : ℕ} (a : Fin m) : liftLabel (Fin.last m) a = a.castSucc := by
  simp [liftLabel]

-- Sanity for the total inverse on its valid domain.
example {m : ℕ} (hm : 0 < m) (a : Fin m) :
    dropLabel hm (Fin.last m) a.castSucc = a := by
  apply Fin.ext
  simp [dropLabel, Nat.mod_eq_of_lt a.isLt]

-- Sanity for the resource normalization constant, without enumeration.
example {d : ℕ} (F : Unit → Unit → Fin d → Fin d) (a : Fin d) :
    graphKernel F () () a (F () () a) = 1 / (d : ℝ) := by
  simp [graphKernel]

-- Sanity: n = 0 is an independent-uniform law, before any resource use.
example {X Y : Type} {m : ℕ} (hm : 0 < m)
    (F : X → Y → Equiv.Perm (Fin (m + 1))) (x : X) (y : Y)
    (a b : Fin (m + 1)) :
    finiteRoundKernel hm F 0 x y a b = 1 / (((m + 1 : ℕ) : ℝ) ^ 2) := by
  rfl

-- Sanity: relabeling all labels to the singleton output retains all d atoms.
example {d : ℕ} (F : Unit → Unit → Equiv.Perm (Fin d)) :
    relabeledKernel F (fun _ _ => ()) (fun _ _ => ()) () () () () =
      (d : ℝ) * (1 / (d : ℝ)) := by
  simp [relabeledKernel]

-- Sanity: arbitrary permutations on at least two labels satisfy the D predicate.
example {X Y : Type} {d : ℕ} (hd : 1 < d)
    (F : X → Y → Equiv.Perm (Fin d)) :
    IsPermutationSystem (graphKernel (fun x y => F x y)) := by
  exact ⟨hd, (fun x y => F x y), (fun x y => (F x y).bijective), rfl⟩

-- Sanity: the constant deterministic law is rational, including denominator one.
example : IsRational (fun (_ _ _ _ : Unit) => (1 : ℝ)) := by
  intro x y a b
  exact ⟨1, by norm_num⟩

-- Sanity: padding a deterministic probability to denominator two is allowed.
example : HasCommonProbabilityDenominator (fun (_ _ _ _ : Unit) => (1 : ℝ)) 2 := by
  intro x y a b
  exact ⟨2, by norm_num⟩

-- Sanity: worst-input distance vanishes for identical singleton laws.
example : simulationDistance (fun (_ _ _ _ : Unit) => (1 : ℝ))
    (fun (_ _ _ _ : Unit) => (1 : ℝ)) = 0 := by
  simp [simulationDistance]

end QAlgorithms.Papers.Independent.Intakethird100.P78

Source

Bipartite Units of Non-Locality, arXiv:0808.0651v4, https://arxiv.org/abs/0808.0651v4

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

`QAlgorithms.Papers.Independent.Intakethird100.P78.BipartiteConditionalArray`

For arbitrary types $X,Y,A,B$ , a bipartite conditional array is any real-valued function on $X\times Y\times A\times B$ , written $P(x,y,a,b)$ . No finiteness, nonemptiness, nonnegativity, normalization, or other condition is imposed.

`QAlgorithms.Papers.Independent.Intakethird100.P78.BipartiteSystem`

For arbitrary types $X,Y$ and finite types $A,B$ , a bipartite system consists of a real-valued function $P(x,y,a,b)$ , for $x\in X$ , $y\in Y$ , $a\in A$ , and $b\in B$ , together with the following properties:

\begin{aligned} &P(x,y,a,b)\ge 0 &&\text{for every }x,y,a,b,\\ &\sum_{a\in A}\sum_{b\in B}P(x,y,a,b)=1 &&\text{for every }x,y,\\ &\sum_{b\in B}P(x,y,a,b)=\sum_{b\in B}P(x,z,a,b) &&\text{for every }x\in X,\ y,z\in Y,\ a\in A,\\ &\sum_{a\in A}P(x,y,b_{\!A},b)=\sum_{a\in A}P(z,y,b_{\!A},b) &&\text{with the summation variable understood as below.} \end{aligned}

The last property, written without an auxiliary placeholder, is precisely

\sum_{a\in A}P(x,y,a,b)=\sum_{a\in A}P(z,y,a,b) \qquad \text{for every }x,z\in X,\ y\in Y,\ b\in B.

Neither $X$ nor $Y$ is required to be finite or nonempty, and $A,B$ may be empty. If $X$ or $Y$ is empty, all these conditions are vacuous; if both are nonempty and either output type is empty, normalization would require $0=1$ , so no such system exists.

`QAlgorithms.Papers.Independent.Intakethird100.P78.HasCommonProbabilityDenominator`

For arbitrary types $X,Y,A,B$ , an arbitrary real-valued array $P:X\times Y\times A\times B\to\mathbb R$ , and a natural number $d$ , the property $\operatorname{HasCommonProbabilityDenominator}(P,d)$ means that for every $x\in X$ , $y\in Y$ , $a\in A$ , and $b\in B$ , there exists a natural number $k$ , allowed to depend on all four indices, such that $P(x,y,a,b)=k/d$ , with numerator and denominator interpreted as real numbers. The value $d=0$ is included: division by zero here equals zero, so for $d=0$ the property says that every entry is zero. For positive $d$ , every entry is a nonnegative integer multiple of $1/d$ ; no normalization or upper bound is required. If any index type is empty, the property holds vacuously for every $d$ .

`QAlgorithms.Papers.Independent.Intakethird100.P78.IsPermutationSystem`

For arbitrary types $X,Y$ , a natural number $d$ , and a real-valued array $P$ on $X\times Y\times L_d\times L_d$ , where $L_d=\{0,\ldots,d-1\}$ , the property of being a permutation system means that $d>1$ and there exists a family of functions $F_{x,y}:L_d\to L_d$ , each bijective, such that

P(x,y,a,b)= \begin{cases} 1/d,&F_{x,y}(a)=b,\\ 0,&F_{x,y}(a)\ne b \end{cases}

for every $x\in X$ , $y\in Y$ , and $a,b\in L_d$ , with $1/d$ interpreted in the real numbers. The family is required to exist but is not required to be unique. The cases $d=0$ and $d=1$ are excluded even when $X$ or $Y$ is empty; neither input type is otherwise required to be finite or nonempty.

`QAlgorithms.Papers.Independent.Intakethird100.P78.IsRational`

For arbitrary types $X,Y,A,B$ and an arbitrary real-valued array $P:X\times Y\times A\times B\to\mathbb R$ , the property $\operatorname{IsRational}(P)$ means that for every $x\in X$ , $y\in Y$ , $a\in A$ , and $b\in B$ , there exists $q\in\mathbb Q$ whose image in $\mathbb R$ equals $P(x,y,a,b)$ . There are no finiteness, nonemptiness, nonnegativity, or normalization assumptions. If any of the four types is empty, this property holds vacuously.

`QAlgorithms.Papers.Independent.Intakethird100.P78.dropLabel`

For every natural number $m$ with a supplied hypothesis $m>0$ , and every pair of labels $h,v\in L_{m+1}=\{0,\ldots,m\}$ , the dropped label is the element of $L_m=\{0,\ldots,m-1\}$ whose integer value is

\delta_h(v)=\sigma_h(v)\bmod m,

where $\sigma_h$ interchanges $h$ and $m$ , fixes all other labels, and is the identity when $h=m$ . The remainder lies in $L_m$ because $m>0$ . The argument $v$ is unrestricted: in particular, $v=h$ is allowed and gives $\delta_h(h)=0$ . When $m=1$ , every value of this function is the sole label $0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P78.finiteRoundKernel`

For arbitrary types $X,Y$ , a natural number $m>0$ , and a family of permutations $F_{x,y}$ of $L_{m+1}=\{0,\ldots,m\}$ , this definition assigns a real-valued array $K_n(x,y,a,b)$ to every natural number $n$ , with $x\in X$ , $y\in Y$ , and $a,b\in L_{m+1}$ . To specify the recursion fully, let $L_m=\{0,\ldots,m-1\}$ , and let $\sigma_h$ interchange $h$ and $m$ , fixing all other labels and acting as the identity when $h=m$ . For a permutation $f$ of $L_{m+1}$ , labels $h,k\in L_{m+1}$ , and $u\in L_m$ regarded as a label in $L_{m+1}$ , put

r_{f,h,k}(u)= \sigma_k\!\left( \begin{cases} f(h),&f(\sigma_h(u))=k,\\ f(\sigma_h(u)),&f(\sigma_h(u))\ne k \end{cases} \right)\bmod m,

and define

W_f(h,k,a,b)= \begin{cases} \dfrac1{m+1},&a=h\ \text{and}\ b=k,\\ 0,&\text{otherwise} \end{cases} + \frac{m}{m+1} \sum_{u\in L_m}\sum_{v\in L_m} \begin{cases} \dfrac1m,& \sigma_h(u)=a,\ \sigma_k(v)=b,\ \text{and }r_{f,h,k}(u)=v,\\ 0,&\text{otherwise}. \end{cases}

The arrays are then defined by

K_0(x,y,a,b)=\frac1{(m+1)^2}, \qquad K_{n+1}(x,y,a,b)= \sum_{h\in L_{m+1}}\sum_{k\in L_{m+1}} K_n(x,y,h,k)\,W_{F_{x,y}}(h,k,a,b).

Every fraction is taken in the real numbers. Both $n=0$ and $m=1$ are included; $X,Y$ need not be finite or nonempty.

`QAlgorithms.Papers.Independent.Intakethird100.P78.graphKernel`

For arbitrary types $X,Y$ , a natural number $d$ , and a family of functions $F_{x,y}:L_d\to L_d$ , where $L_d=\{0,\ldots,d-1\}$ , the graph kernel is the real-valued array

G_F(x,y,a,b)= \begin{cases} 1/d,&F_{x,y}(a)=b,\\ 0,&F_{x,y}(a)\ne b, \end{cases} \qquad a,b\in L_d.

The reciprocal is taken in the real numbers. No bijectivity condition is imposed on the functions, and no finiteness or nonemptiness condition is imposed on $X,Y$ . The definition includes $d=0$ ; then $L_d$ is empty and the array has no output entries.

`QAlgorithms.Papers.Independent.Intakethird100.P78.liftLabel`

For every natural number $m$ , distinguished label $h\in L_{m+1}=\{0,\ldots,m\}$ , and label $a\in L_m=\{0,\ldots,m-1\}$ , the lifted label is obtained by regarding $a$ as the same integer in $L_{m+1}$ and then interchanging $h$ and $m$ :

\ell_h(a)=\sigma_h(a),

where $\sigma_h$ fixes every label other than $h,m$ and swaps those two labels; when $h=m$ , it is the identity. Equivalently, $\ell_h(a)=m$ if $a=h$ , and $\ell_h(a)=a$ otherwise. The definition includes $m=0$ , when there are no possible arguments $a$ .

`QAlgorithms.Papers.Independent.Intakethird100.P78.reducedKernel`

For arbitrary types $X,Y$ , a natural number $m>0$ , and a family of permutations $F_{x,y}$ of $L_{m+1}=\{0,\ldots,m\}$ , the reduced kernel is a real-valued array with inputs $(x,\widehat a)\in X\times L_{m+1}$ , $(y,\widehat b)\in Y\times L_{m+1}$ , and outputs $a,b\in L_m=\{0,\ldots,m-1\}$ . For $h\in L_{m+1}$ , let $\sigma_h$ swap $h$ and $m$ , fixing all other labels and acting as the identity if $h=m$ . Regard $a$ as a label in $L_{m+1}$ , and set

u=\sigma_{\widehat a}(a),\qquad w= \begin{cases} F_{x,y}(\widehat a),&F_{x,y}(u)=\widehat b,\\ F_{x,y}(u),&F_{x,y}(u)\ne\widehat b, \end{cases} \qquad r=\sigma_{\widehat b}(w)\bmod m.

The array is defined by

K((x,\widehat a),(y,\widehat b),a,b)= \begin{cases} 1/m,&r=b,\\ 0,&r\ne b, \end{cases}

with real-valued division. No finiteness or nonemptiness condition is imposed on $X,Y$ , and $m=1$ is allowed.

`QAlgorithms.Papers.Independent.Intakethird100.P78.reducedMap`

For every natural number $m>0$ , a permutation $f$ of $L_{m+1}=\{0,\ldots,m\}$ , distinguished labels $\widehat a,\widehat b\in L_{m+1}$ , and $a\in L_m=\{0,\ldots,m-1\}$ , define $\sigma_h$ to interchange $h$ and $m$ and fix every other label, with $\sigma_m$ the identity. The reduced map returns the element of $L_m$ with integer value

r_{f,\widehat a,\widehat b}(a) = \sigma_{\widehat b}\!\left( \begin{cases} f(\widehat a),&f(\sigma_{\widehat a}(a))=\widehat b,\\ f(\sigma_{\widehat a}(a)),&f(\sigma_{\widehat a}(a))\ne\widehat b \end{cases} \right)\bmod m,

where $a$ is regarded as the same integer in $L_{m+1}$ before applying the swap. The hypothesis $m>0$ ensures that the remainder is a label in $L_m$ ; the case $m=1$ is included and the output is then always $0$ . No relation between $f(\widehat a)$ and $\widehat b$ is assumed.

`QAlgorithms.Papers.Independent.Intakethird100.P78.relabeledKernel`

For arbitrary types $X,Y,A,B$ , a natural number $d$ , a family of permutations $F_{x,y}$ of $L_d=\{0,\ldots,d-1\}$ , and functions $\alpha_x:L_d\to A$ for each $x\in X$ and $\beta_y:L_d\to B$ for each $y\in Y$ , the relabeled kernel is the real-valued array

R(x,y,a,b)= \sum_{u\in L_d} \begin{cases} 1/d,&\alpha_x(u)=a\ \text{and}\ \beta_y(F_{x,y}(u))=b,\\ 0,&\text{otherwise}, \end{cases}

for every $x\in X$ , $y\in Y$ , $a\in A$ , and $b\in B$ , with real-valued division. The functions $\alpha_x,\beta_y$ need not be injective or surjective, and none of $X,Y,A,B$ is required to be finite or nonempty. The cases $d=0$ and $d=1$ are included; when $d=0$ , the sum is empty and every existing array entry equals zero.

`QAlgorithms.Papers.Independent.Intakethird100.P78.roundKernel`

For every natural number $m>0$ , permutation $f$ of $L_{m+1}=\{0,\ldots,m\}$ , and labels $\widehat a,\widehat b,a,b\in L_{m+1}$ , let $\sigma_h$ swap $h$ and $m$ , fix every other label, and be the identity if $h=m$ . For $u\in L_m=\{0,\ldots,m-1\}$ , regarded as a label in $L_{m+1}$ , define

r(u)= \sigma_{\widehat b}\!\left( \begin{cases} f(\widehat a),&f(\sigma_{\widehat a}(u))=\widehat b,\\ f(\sigma_{\widehat a}(u)),&f(\sigma_{\widehat a}(u))\ne\widehat b \end{cases} \right)\bmod m.

The round kernel is the real number

W_f(\widehat a,\widehat b,a,b)= \begin{cases} \dfrac1{m+1},&a=\widehat a\ \text{and}\ b=\widehat b,\\ 0,&\text{otherwise} \end{cases} + \frac{m}{m+1} \sum_{u\in L_m}\sum_{v\in L_m} \begin{cases} \dfrac1m,& \sigma_{\widehat a}(u)=a,\ \sigma_{\widehat b}(v)=b,\ \text{and }r(u)=v,\\ 0,&\text{otherwise}. \end{cases}

All fractions are real-valued, and the case $m=1$ is included. The four labels are unrestricted, and no relation between $f(\widehat a)$ and $\widehat b$ is assumed.

`QAlgorithms.Papers.Independent.Intakethird100.P78.simulationDistance`

For finite nonempty types $X,Y$ , finite types $A,B$ , and arbitrary real-valued arrays $S,T$ on $X\times Y\times A\times B$ , their simulation distance is the real number

D(S,T)= \sup\left\{ \frac12\sum_{a\in A}\sum_{b\in B} \left|S(x,y,a,b)-T(x,y,a,b)\right| :\ (x,y)\in X\times Y \right\}.

The set whose supremum is taken is finite and nonempty, so this is also its maximum. The arrays need not be nonnegative or normalized. Either $A$ or $B$ may be empty, in which case every displayed sum, and hence the distance, is zero.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph