Notation by work
AVOC
All notation · Glossary · Source coverage
312 symbol spellings in 623 mathematical passages across 8 selected source files. Subscripts and superscripts have their own entries alongside their base symbols.
The same symbol can have several meanings here. A passage classified as a definition may define another part of its expression. Read the linked context before assigning a meaning.
All 312 entries are available below.
*Definition passage · 6 passages
Search aliases: *
Definition passage: Deterministic experiment value · core_chapters.tex, line 69
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
J_b^*(\phi)=\max_{\pi:Z\to A}J_b(\phi,\pi)
+Definition passage · 46 passages
Search aliases: +
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 363
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
x\mapsto Ax+b
=Definition passage · 135 passages
Search aliases: =
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 8
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi\succeq T \quad\Longleftrightarrow\quad \exists d:Z\to Y\ \ \forall x\in X,\ d(\phi(x))=T(x).
ADefinition passage · 30 passages
Search aliases: A
Definition passage: Deterministic experiment value · core_chapters.tex, line 65
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
A
aDefinition passage · 44 passages
Search aliases: a
Definition passage: Deterministic control sufficiency · core_chapters.tex, line 179
[Deterministic control sufficiency] Let A_0 be a finite nonempty set of admissible actions, let f:S× A_0→ S be transition, and let r:S× A_0→Q be reward. A representation ϕ:S→ Z is control sufficient if, whenever ϕ(s)=ϕ(t), every admissible action satisfies r(s,a)=r(t,a), ϕ(f(s,a))=ϕ(f(t,a)). The global action set is common to all states in this definition.
Exact mathematical passage
r(s,a)=r(t,a),\qquad \phi(f(s,a))=\phi(f(t,a)).
A'Definition passage · 1 passage
Search aliases: A'
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 364
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
(B,c)\circ(A,b)=(BA,Bb+c),\qquad (A,b)+(A',b')=(A+A',b+b').
A_0Definition passage · 5 passages
Search aliases: A_0
Definition passage: Deterministic control sufficiency · core_chapters.tex, line 178
[Deterministic control sufficiency] Let A_0 be a finite nonempty set of admissible actions, let f:S× A_0→ S be transition, and let r:S× A_0→Q be reward. A representation ϕ:S→ Z is control sufficient if, whenever ϕ(s)=ϕ(t), every admissible action satisfies r(s,a)=r(t,a), ϕ(f(s,a))=ϕ(f(t,a)). The global action set is common to all states in this definition.
Exact mathematical passage
A_0
BDefinition passage · 15 passages
Search aliases: B
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 364
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
(B,c)\circ(A,b)=(BA,Bb+c),\qquad (A,b)+(A',b')=(A+A',b+b').
bDefinition passage · 39 passages
Search aliases: b
Definition passage: Deterministic experiment value · core_chapters.tex, line 65
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
b:\Omega\to\Q
b'Definition passage · 4 passages
Search aliases: b'
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 364
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
(B,c)\circ(A,b)=(BA,Bb+c),\qquad (A,b)+(A',b')=(A+A',b+b').
cDefinition passage · 19 passages
Search aliases: c
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 364
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
(B,c)\circ(A,b)=(BA,Bb+c),\qquad (A,b)+(A',b')=(A+A',b+b').
dDefinition passage · 24 passages
Search aliases: d
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 8
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi\succeq T \quad\Longleftrightarrow\quad \exists d:Z\to Y\ \ \forall x\in X,\ d(\phi(x))=T(x).
EDefinition passage · 18 passages
Search aliases: E
Definition passage: Finite rational channel · core_chapters.tex, line 87
[Finite rational channel] A channel from Ω to a finite observation alphabet O consists of rational entries E(omidω)≥0 with ∑_o E(omidω)=1 for every ω. Given a second channel K(ymid o), their composite is (EK)(ymidω)=∑_o E(omidω)K(ymid o). The composite is a garbling of E.
Exact mathematical passage
E(o\mid\omega)\ge0
fDefinition passage · 13 passages
Search aliases: f
Definition passage: Deterministic control sufficiency · core_chapters.tex, line 178
[Deterministic control sufficiency] Let A_0 be a finite nonempty set of admissible actions, let f:S× A_0→ S be transition, and let r:S× A_0→Q be reward. A representation ϕ:S→ Z is control sufficient if, whenever ϕ(s)=ϕ(t), every admissible action satisfies r(s,a)=r(t,a), ϕ(f(s,a))=ϕ(f(t,a)). The global action set is common to all states in this definition.
Exact mathematical passage
f:S\times A_0\to S
hDefinition passage · 25 passages
Search aliases: h
Definition passage: Guarded rational system · planning_chapters.tex, line 20
[Guarded rational system] Let S be a state space, A(s) a finite nonempty set of actions, and O a finite observation space. A guarded system consists of a rational reward r(s,a), a transition T(s,a,o), and rational probabilities P(omid s,a) satisfying P(omid s,a)≥0, ∑_o∈ OP(omid s,a)=1. Its finite-horizon Bellman values are V_0(s) · =0, Q_h(s,a) · =r(s,a)+∑_oP(omid s,a)V_h(T(s,a,o)), V_h+1(s) · =max_a∈ A(s)Q_h(s,a).
Exact mathematical passage
V_0(s)&=0,\label{eq:bellmanzero}\\ Q_h(s,a)&=r(s,a)+\sum_oP(o\mid s,a)V_h(T(s,a,o)),\label{eq:qvalue}\\ V_{h+1}(s)&=\max_{a\in A(s)}Q_h(s,a).\label{eq:bellman}
JDefinition passage · 15 passages
Search aliases: J
Definition passage: Deterministic experiment value · core_chapters.tex, line 66
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
J_b(\phi,\pi)=\sum_{\omega\in\Omega}b(\omega)u(\omega,\pi(\phi(\omega))).
J_bDefinition passage · 5 passages
Search aliases: J_b
Definition passage: Deterministic experiment value · core_chapters.tex, line 66
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
J_b(\phi,\pi)=\sum_{\omega\in\Omega}b(\omega)u(\omega,\pi(\phi(\omega))).
J_b^*Definition passage · 3 passages
Search aliases: J_b^*
Definition passage: Deterministic experiment value · core_chapters.tex, line 69
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
J_b^*(\phi)=\max_{\pi:Z\to A}J_b(\phi,\pi)
KDefinition passage · 12 passages
Search aliases: K
Definition passage: Finite rational channel · core_chapters.tex, line 87
[Finite rational channel] A channel from Ω to a finite observation alphabet O consists of rational entries E(omidω)≥0 with ∑_o E(omidω)=1 for every ω. Given a second channel K(ymid o), their composite is (EK)(ymidω)=∑_o E(omidω)K(ymid o). The composite is a garbling of E.
Exact mathematical passage
K(y\mid o)
\LongleftrightarrowDefinition passage · 2 passages
Search aliases: Longleftrightarrow
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 8
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi\succeq T \quad\Longleftrightarrow\quad \exists d:Z\to Y\ \ \forall x\in X,\ d(\phi(x))=T(x).
mDefinition passage · 19 passages
Search aliases: m
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 363
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
m
\maxDefinition passage · 4 passages
Search aliases: max
Definition passage: Deterministic experiment value · core_chapters.tex, line 69
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
J_b^*(\phi)=\max_{\pi:Z\to A}J_b(\phi,\pi)
\max_{a\in A(s)}Definition passage · 1 passage
Search aliases: max_a∈ A(s) max in
Definition passage: Guarded rational system · planning_chapters.tex, line 20
[Guarded rational system] Let S be a state space, A(s) a finite nonempty set of actions, and O a finite observation space. A guarded system consists of a rational reward r(s,a), a transition T(s,a,o), and rational probabilities P(omid s,a) satisfying P(omid s,a)≥0, ∑_o∈ OP(omid s,a)=1. Its finite-horizon Bellman values are V_0(s) · =0, Q_h(s,a) · =r(s,a)+∑_oP(omid s,a)V_h(T(s,a,o)), V_h+1(s) · =max_a∈ A(s)Q_h(s,a).
Exact mathematical passage
V_0(s)&=0,\label{eq:bellmanzero}\\ Q_h(s,a)&=r(s,a)+\sum_oP(o\mid s,a)V_h(T(s,a,o)),\label{eq:qvalue}\\ V_{h+1}(s)&=\max_{a\in A(s)}Q_h(s,a).\label{eq:bellman}
\max_{\pi:Z\to A}Definition passage · 1 passage
Search aliases: max_π:Z→ A max pi to
Definition passage: Deterministic experiment value · core_chapters.tex, line 69
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
J_b^*(\phi)=\max_{\pi:Z\to A}J_b(\phi,\pi)
\midDefinition passage · 15 passages
Search aliases: mid
Definition passage: Finite rational channel · core_chapters.tex, line 87
[Finite rational channel] A channel from Ω to a finite observation alphabet O consists of rational entries E(omidω)≥0 with ∑_o E(omidω)=1 for every ω. Given a second channel K(ymid o), their composite is (EK)(ymidω)=∑_o E(omidω)K(ymid o). The composite is a garbling of E.
Exact mathematical passage
E(o\mid\omega)\ge0
nDefinition passage · 41 passages
Search aliases: n
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 363
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
n
ODefinition passage · 3 passages
Search aliases: O
Definition passage: Finite rational channel · core_chapters.tex, line 87
[Finite rational channel] A channel from Ω to a finite observation alphabet O consists of rational entries E(omidω)≥0 with ∑_o E(omidω)=1 for every ω. Given a second channel K(ymid o), their composite is (EK)(ymidω)=∑_o E(omidω)K(ymid o). The composite is a garbling of E.
Exact mathematical passage
O
oDefinition passage · 28 passages
Search aliases: o
Definition passage: Finite rational channel · core_chapters.tex, line 87
[Finite rational channel] A channel from Ω to a finite observation alphabet O consists of rational entries E(omidω)≥0 with ∑_o E(omidω)=1 for every ω. Given a second channel K(ymid o), their composite is (EK)(ymidω)=∑_o E(omidω)K(ymid o). The composite is a garbling of E.
Exact mathematical passage
E(o\mid\omega)\ge0
PDefinition passage · 13 passages
Search aliases: P
Definition passage: Projected stochastic control sufficiency · core_chapters.tex, line 215
[Projected stochastic control sufficiency] A representation ϕ:S→ Z is projected stochastically sufficient if equal represented current states have equal immediate rewards and, for every admissible a and every rational fiber-constant function W:S→Q, ∑_s'P_a(s,s')W(s')=∑_s'P_a(t,s')W(s') whenever ϕ(s)=ϕ(t).
Exact mathematical passage
\sum_{s'}P_a(s,s')W(s')=\sum_{s'}P_a(t,s')W(s') \quad\text{whenever }\phi(s)=\phi(t).
P_aDefinition passage · 7 passages
Search aliases: P_a
Definition passage: Projected stochastic control sufficiency · core_chapters.tex, line 215
[Projected stochastic control sufficiency] A representation ϕ:S→ Z is projected stochastically sufficient if equal represented current states have equal immediate rewards and, for every admissible a and every rational fiber-constant function W:S→Q, ∑_s'P_a(s,s')W(s')=∑_s'P_a(t,s')W(s') whenever ϕ(s)=ϕ(t).
Exact mathematical passage
\sum_{s'}P_a(s,s')W(s')=\sum_{s'}P_a(t,s')W(s') \quad\text{whenever }\phi(s)=\phi(t).
QDefinition passage · 15 passages
Search aliases: Q
Definition passage: Guarded rational system · planning_chapters.tex, line 20
[Guarded rational system] Let S be a state space, A(s) a finite nonempty set of actions, and O a finite observation space. A guarded system consists of a rational reward r(s,a), a transition T(s,a,o), and rational probabilities P(omid s,a) satisfying P(omid s,a)≥0, ∑_o∈ OP(omid s,a)=1. Its finite-horizon Bellman values are V_0(s) · =0, Q_h(s,a) · =r(s,a)+∑_oP(omid s,a)V_h(T(s,a,o)), V_h+1(s) · =max_a∈ A(s)Q_h(s,a).
Exact mathematical passage
V_0(s)&=0,\label{eq:bellmanzero}\\ Q_h(s,a)&=r(s,a)+\sum_oP(o\mid s,a)V_h(T(s,a,o)),\label{eq:qvalue}\\ V_{h+1}(s)&=\max_{a\in A(s)}Q_h(s,a).\label{eq:bellman}
\QDefinition passage · 6 passages
Search aliases: Q
Definition passage: Deterministic experiment value · core_chapters.tex, line 65
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
b:\Omega\to\Q
Q_hDefinition passage · 6 passages
Search aliases: Q_h
Definition passage: Guarded rational system · planning_chapters.tex, line 20
[Guarded rational system] Let S be a state space, A(s) a finite nonempty set of actions, and O a finite observation space. A guarded system consists of a rational reward r(s,a), a transition T(s,a,o), and rational probabilities P(omid s,a) satisfying P(omid s,a)≥0, ∑_o∈ OP(omid s,a)=1. Its finite-horizon Bellman values are V_0(s) · =0, Q_h(s,a) · =r(s,a)+∑_oP(omid s,a)V_h(T(s,a,o)), V_h+1(s) · =max_a∈ A(s)Q_h(s,a).
Exact mathematical passage
V_0(s)&=0,\label{eq:bellmanzero}\\ Q_h(s,a)&=r(s,a)+\sum_oP(o\mid s,a)V_h(T(s,a,o)),\label{eq:qvalue}\\ V_{h+1}(s)&=\max_{a\in A(s)}Q_h(s,a).\label{eq:bellman}
RDefinition passage · 9 passages
Search aliases: R
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 363
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
R
rDefinition passage · 12 passages
Search aliases: r
Definition passage: Deterministic control sufficiency · core_chapters.tex, line 178
[Deterministic control sufficiency] Let A_0 be a finite nonempty set of admissible actions, let f:S× A_0→ S be transition, and let r:S× A_0→Q be reward. A representation ϕ:S→ Z is control sufficient if, whenever ϕ(s)=ϕ(t), every admissible action satisfies r(s,a)=r(t,a), ϕ(f(s,a))=ϕ(f(t,a)). The global action set is common to all states in this definition.
Exact mathematical passage
r:S\times A_0\to\Q
R^mDefinition passage · 3 passages
Search aliases: R^m
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 363
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
b\in R^m
R^{m\times n}Definition passage · 1 passage
Search aliases: R^m× n times
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 363
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
A\in R^{m\times n}
SDefinition passage · 16 passages
Search aliases: S
Definition passage: Deterministic control sufficiency · core_chapters.tex, line 178
[Deterministic control sufficiency] Let A_0 be a finite nonempty set of admissible actions, let f:S× A_0→ S be transition, and let r:S× A_0→Q be reward. A representation ϕ:S→ Z is control sufficient if, whenever ϕ(s)=ϕ(t), every admissible action satisfies r(s,a)=r(t,a), ϕ(f(s,a))=ϕ(f(t,a)). The global action set is common to all states in this definition.
Exact mathematical passage
f:S\times A_0\to S
sDefinition passage · 45 passages
Search aliases: s
Definition passage: Deterministic control sufficiency · core_chapters.tex, line 178
[Deterministic control sufficiency] Let A_0 be a finite nonempty set of admissible actions, let f:S× A_0→ S be transition, and let r:S× A_0→Q be reward. A representation ϕ:S→ Z is control sufficient if, whenever ϕ(s)=ϕ(t), every admissible action satisfies r(s,a)=r(t,a), ϕ(f(s,a))=ϕ(f(t,a)). The global action set is common to all states in this definition.
Exact mathematical passage
\phi(s)=\phi(t)
s'Definition passage · 7 passages
Search aliases: s'
Definition passage: Projected stochastic control sufficiency · core_chapters.tex, line 215
[Projected stochastic control sufficiency] A representation ϕ:S→ Z is projected stochastically sufficient if equal represented current states have equal immediate rewards and, for every admissible a and every rational fiber-constant function W:S→Q, ∑_s'P_a(s,s')W(s')=∑_s'P_a(t,s')W(s') whenever ϕ(s)=ϕ(t).
Exact mathematical passage
\sum_{s'}P_a(s,s')W(s')=\sum_{s'}P_a(t,s')W(s') \quad\text{whenever }\phi(s)=\phi(t).
\succeqDefinition passage · 5 passages
Search aliases: succeq
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 8
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi\succeq T \quad\Longleftrightarrow\quad \exists d:Z\to Y\ \ \forall x\in X,\ d(\phi(x))=T(x).
TDefinition passage · 28 passages
Search aliases: T
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 7
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
T:X\to Y
tDefinition passage · 10 passages
Search aliases: t
Definition passage: Deterministic control sufficiency · core_chapters.tex, line 178
[Deterministic control sufficiency] Let A_0 be a finite nonempty set of admissible actions, let f:S× A_0→ S be transition, and let r:S× A_0→Q be reward. A representation ϕ:S→ Z is control sufficient if, whenever ϕ(s)=ϕ(t), every admissible action satisfies r(s,a)=r(t,a), ϕ(f(s,a))=ϕ(f(t,a)). The global action set is common to all states in this definition.
Exact mathematical passage
\phi(s)=\phi(t)
uDefinition passage · 14 passages
Search aliases: u
Definition passage: Deterministic experiment value · core_chapters.tex, line 65
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
u:\Omega\times A\to\Q
VDefinition passage · 21 passages
Search aliases: V
Definition passage: Guarded rational system · planning_chapters.tex, line 20
[Guarded rational system] Let S be a state space, A(s) a finite nonempty set of actions, and O a finite observation space. A guarded system consists of a rational reward r(s,a), a transition T(s,a,o), and rational probabilities P(omid s,a) satisfying P(omid s,a)≥0, ∑_o∈ OP(omid s,a)=1. Its finite-horizon Bellman values are V_0(s) · =0, Q_h(s,a) · =r(s,a)+∑_oP(omid s,a)V_h(T(s,a,o)), V_h+1(s) · =max_a∈ A(s)Q_h(s,a).
Exact mathematical passage
V_0(s)&=0,\label{eq:bellmanzero}\\ Q_h(s,a)&=r(s,a)+\sum_oP(o\mid s,a)V_h(T(s,a,o)),\label{eq:qvalue}\\ V_{h+1}(s)&=\max_{a\in A(s)}Q_h(s,a).\label{eq:bellman}
V_0Definition passage · 3 passages
Search aliases: V_0
Definition passage: Guarded rational system · planning_chapters.tex, line 20
[Guarded rational system] Let S be a state space, A(s) a finite nonempty set of actions, and O a finite observation space. A guarded system consists of a rational reward r(s,a), a transition T(s,a,o), and rational probabilities P(omid s,a) satisfying P(omid s,a)≥0, ∑_o∈ OP(omid s,a)=1. Its finite-horizon Bellman values are V_0(s) · =0, Q_h(s,a) · =r(s,a)+∑_oP(omid s,a)V_h(T(s,a,o)), V_h+1(s) · =max_a∈ A(s)Q_h(s,a).
Exact mathematical passage
V_0(s)&=0,\label{eq:bellmanzero}\\ Q_h(s,a)&=r(s,a)+\sum_oP(o\mid s,a)V_h(T(s,a,o)),\label{eq:qvalue}\\ V_{h+1}(s)&=\max_{a\in A(s)}Q_h(s,a).\label{eq:bellman}
V_hDefinition passage · 2 passages
Search aliases: V_h
Definition passage: Guarded rational system · planning_chapters.tex, line 20
[Guarded rational system] Let S be a state space, A(s) a finite nonempty set of actions, and O a finite observation space. A guarded system consists of a rational reward r(s,a), a transition T(s,a,o), and rational probabilities P(omid s,a) satisfying P(omid s,a)≥0, ∑_o∈ OP(omid s,a)=1. Its finite-horizon Bellman values are V_0(s) · =0, Q_h(s,a) · =r(s,a)+∑_oP(omid s,a)V_h(T(s,a,o)), V_h+1(s) · =max_a∈ A(s)Q_h(s,a).
Exact mathematical passage
V_0(s)&=0,\label{eq:bellmanzero}\\ Q_h(s,a)&=r(s,a)+\sum_oP(o\mid s,a)V_h(T(s,a,o)),\label{eq:qvalue}\\ V_{h+1}(s)&=\max_{a\in A(s)}Q_h(s,a).\label{eq:bellman}
V_{h+1}Definition passage · 2 passages
Search aliases: V_h+1
Definition passage: Guarded rational system · planning_chapters.tex, line 20
[Guarded rational system] Let S be a state space, A(s) a finite nonempty set of actions, and O a finite observation space. A guarded system consists of a rational reward r(s,a), a transition T(s,a,o), and rational probabilities P(omid s,a) satisfying P(omid s,a)≥0, ∑_o∈ OP(omid s,a)=1. Its finite-horizon Bellman values are V_0(s) · =0, Q_h(s,a) · =r(s,a)+∑_oP(omid s,a)V_h(T(s,a,o)), V_h+1(s) · =max_a∈ A(s)Q_h(s,a).
Exact mathematical passage
V_0(s)&=0,\label{eq:bellmanzero}\\ Q_h(s,a)&=r(s,a)+\sum_oP(o\mid s,a)V_h(T(s,a,o)),\label{eq:qvalue}\\ V_{h+1}(s)&=\max_{a\in A(s)}Q_h(s,a).\label{eq:bellman}
WDefinition passage · 6 passages
Search aliases: W
Definition passage: Projected stochastic control sufficiency · core_chapters.tex, line 214
[Projected stochastic control sufficiency] A representation ϕ:S→ Z is projected stochastically sufficient if equal represented current states have equal immediate rewards and, for every admissible a and every rational fiber-constant function W:S→Q, ∑_s'P_a(s,s')W(s')=∑_s'P_a(t,s')W(s') whenever ϕ(s)=ϕ(t).
Exact mathematical passage
W:S\to\Q
XDefinition passage · 17 passages
Search aliases: X
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 7
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
X
xDefinition passage · 25 passages
Search aliases: x
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 8
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi\succeq T \quad\Longleftrightarrow\quad \exists d:Z\to Y\ \ \forall x\in X,\ d(\phi(x))=T(x).
YDefinition passage · 6 passages
Search aliases: Y
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 7
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
T:X\to Y
yDefinition passage · 12 passages
Search aliases: y
Definition passage: Finite rational channel · core_chapters.tex, line 87
[Finite rational channel] A channel from Ω to a finite observation alphabet O consists of rational entries E(omidω)≥0 with ∑_o E(omidω)=1 for every ω. Given a second channel K(ymid o), their composite is (EK)(ymidω)=∑_o E(omidω)K(ymid o). The composite is a garbling of E.
Exact mathematical passage
K(y\mid o)
ZDefinition passage · 14 passages
Search aliases: Z
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 7
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi:X\to Z
\timesDefinition passage · 8 passages
Search aliases: × times
Definition passage: Deterministic experiment value · core_chapters.tex, line 65
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
u:\Omega\times A\to\Q
\piDefinition passage · 11 passages
Search aliases: π pi
Definition passage: Deterministic experiment value · core_chapters.tex, line 65
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
\pi:Z\to A
\phiDefinition passage · 49 passages
Search aliases: ϕ phi
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 7
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi:X\to Z
\psiDefinition passage · 13 passages
Search aliases: ψ psi
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 13
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi\succeq\psi
\OmegaDefinition passage · 9 passages
Search aliases: Ω Omega
Definition passage: Deterministic experiment value · core_chapters.tex, line 65
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
\Omega
\omegaDefinition passage · 23 passages
Search aliases: ω omega
Definition passage: Deterministic experiment value · core_chapters.tex, line 66
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
J_b(\phi,\pi)=\sum_{\omega\in\Omega}b(\omega)u(\omega,\pi(\phi(\omega))).
\toDefinition passage · 28 passages
Search aliases: → to
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 7
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi:X\to Z
\mapstoDefinition passage · 2 passages
Search aliases: ↦ mapsto
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 363
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
x\mapsto Ax+b
\forallDefinition passage · 3 passages
Search aliases: ∀ forall
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 8
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi\succeq T \quad\Longleftrightarrow\quad \exists d:Z\to Y\ \ \forall x\in X,\ d(\phi(x))=T(x).
\existsDefinition passage · 2 passages
Search aliases: ∃ exists
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 8
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi\succeq T \quad\Longleftrightarrow\quad \exists d:Z\to Y\ \ \forall x\in X,\ d(\phi(x))=T(x).
\inDefinition passage · 31 passages
Search aliases: ∈ in
Definition passage: Deterministic refinement and task sufficiency · core_chapters.tex, line 8
[Deterministic refinement and task sufficiency] Let X be a raw state space and let ϕ:X→ Z and T:X→ Y be functions. We write ϕsucceq T Longleftrightarrow ∃ d:Z→ Y ∀ x∈ X, d(ϕ(x))=T(x). More generally, ϕsucceqψ means that ψ factors through ϕ. The relation is called refinement. The representation ϕ is task sufficient for T when ϕsucceq T. Two representations are information equivalent when each refines the other.
Exact mathematical passage
\phi\succeq T \quad\Longleftrightarrow\quad \exists d:Z\to Y\ \ \forall x\in X,\ d(\phi(x))=T(x).
\sumDefinition passage · 32 passages
Search aliases: ∑ sum
Definition passage: Deterministic experiment value · core_chapters.tex, line 66
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
J_b(\phi,\pi)=\sum_{\omega\in\Omega}b(\omega)u(\omega,\pi(\phi(\omega))).
\sum_oDefinition passage · 7 passages
Search aliases: ∑_o sum
Definition passage: Finite rational channel · core_chapters.tex, line 87
[Finite rational channel] A channel from Ω to a finite observation alphabet O consists of rational entries E(omidω)≥0 with ∑_o E(omidω)=1 for every ω. Given a second channel K(ymid o), their composite is (EK)(ymidω)=∑_o E(omidω)K(ymid o). The composite is a garbling of E.
Exact mathematical passage
\sum_o E(o\mid\omega)=1
\sum_{o\in O}Definition passage · 1 passage
Search aliases: ∑_o∈ O sum in
Definition passage: Guarded rational system · planning_chapters.tex, line 16
[Guarded rational system] Let S be a state space, A(s) a finite nonempty set of actions, and O a finite observation space. A guarded system consists of a rational reward r(s,a), a transition T(s,a,o), and rational probabilities P(omid s,a) satisfying P(omid s,a)≥0, ∑_o∈ OP(omid s,a)=1. Its finite-horizon Bellman values are V_0(s) · =0,
Exact mathematical passage
P(o\mid s,a)\geq0,\qquad \sum_{o\in O}P(o\mid s,a)=1.
\sum_{s'}Definition passage · 4 passages
Search aliases: ∑_s' sum
Definition passage: Projected stochastic control sufficiency · core_chapters.tex, line 215
[Projected stochastic control sufficiency] A representation ϕ:S→ Z is projected stochastically sufficient if equal represented current states have equal immediate rewards and, for every admissible a and every rational fiber-constant function W:S→Q, ∑_s'P_a(s,s')W(s')=∑_s'P_a(t,s')W(s') whenever ϕ(s)=ϕ(t).
Exact mathematical passage
\sum_{s'}P_a(s,s')W(s')=\sum_{s'}P_a(t,s')W(s') \quad\text{whenever }\phi(s)=\phi(t).
\sum_{\omega\in\Omega}Definition passage · 1 passage
Search aliases: ∑_ω∈Ω sum omega in Omega
Definition passage: Deterministic experiment value · core_chapters.tex, line 66
[Deterministic experiment value] Let Ω be finite, A be a finite nonempty action set, b:Ω→Q be a prior, and u:Ω× A→Q be utility. For an observation ϕ:Ω→ Z and policy π:Z→ A, define J_b(ϕ,π)=∑_ω∈Ωb(ω)u(ω,π(ϕ(ω))). When Z is finite, write J_b^*(ϕ)=max_π:Z→ AJ_b(ϕ,π).
Exact mathematical passage
J_b(\phi,\pi)=\sum_{\omega\in\Omega}b(\omega)u(\omega,\pi(\phi(\omega))).
\circDefinition passage · 7 passages
Search aliases: ∘ circ
Definition passage: Dimension-indexed affine signature · core_chapters.tex, line 364
[Dimension-indexed affine signature] Over a ring R, a signature from dimension n to dimension m is a pair (A,b) with A∈ R^m× n and b∈ R^m, denoting x↦ Ax+b. Dimensions are part of the type. Composition and pointwise addition are (B,c)∘(A,b)=(BA,Bb+c), (A,b)+(A',b')=(A+A',b+b').
Exact mathematical passage
(B,c)\circ(A,b)=(BA,Bb+c),\qquad (A,b)+(A',b')=(A+A',b+b').
\geDefinition passage · 5 passages
Search aliases: ≥ ge
Definition passage: Finite rational channel · core_chapters.tex, line 87
[Finite rational channel] A channel from Ω to a finite observation alphabet O consists of rational entries E(omidω)≥0 with ∑_o E(omidω)=1 for every ω. Given a second channel K(ymid o), their composite is (EK)(ymidω)=∑_o E(omidω)K(ymid o). The composite is a garbling of E.
Exact mathematical passage
E(o\mid\omega)\ge0
\geqDefinition passage · 1 passage
Search aliases: ≥ geq
Definition passage: Guarded rational system · planning_chapters.tex, line 16
[Guarded rational system] Let S be a state space, A(s) a finite nonempty set of actions, and O a finite observation space. A guarded system consists of a rational reward r(s,a), a transition T(s,a,o), and rational probabilities P(omid s,a) satisfying P(omid s,a)≥0, ∑_o∈ OP(omid s,a)=1. Its finite-horizon Bellman values are V_0(s) · =0,
Exact mathematical passage
P(o\mid s,a)\geq0,\qquad \sum_{o\in O}P(o\mid s,a)=1.
c_DIntroduction passage · 2 passages
Search aliases: c_D
Introduction passage · core_chapters.tex, line 34
[Finite data processing] For a finite sample D⊆ X, let c_D(ϕ)=|ϕ(D)| denote the number of reached representation states. If ϕsucceqψ, then c_D(ψ)≤ c_D(ϕ). Choose d with ψ=d∘ϕ. Then ψ(D)=d(ϕ(D)), and the image of a finite set under a function has cardinality at most that of the original set.
Exact mathematical passage
c_D(\phi)=|\phi(D)|
DIntroduction passage · 19 passages
Search aliases: D
Introduction passage · core_chapters.tex, line 34
[Finite data processing] For a finite sample D⊆ X, let c_D(ϕ)=|ϕ(D)| denote the number of reached representation states. If ϕsucceqψ, then c_D(ψ)≤ c_D(ϕ). Choose d with ψ=d∘ϕ. Then ψ(D)=d(ϕ(D)), and the image of a finite set under a function has cardinality at most that of the original set.
Exact mathematical passage
D\subseteq X
|Introduction passage · 9 passages
Search aliases: |
Introduction passage · core_chapters.tex, line 34
[Finite data processing] For a finite sample D⊆ X, let c_D(ϕ)=|ϕ(D)| denote the number of reached representation states. If ϕsucceqψ, then c_D(ψ)≤ c_D(ϕ). Choose d with ψ=d∘ϕ. Then ψ(D)=d(ϕ(D)), and the image of a finite set under a function has cardinality at most that of the original set.
Exact mathematical passage
c_D(\phi)=|\phi(D)|
\leIntroduction passage · 15 passages
Search aliases: ≤ le
Introduction passage · core_chapters.tex, line 35
[Finite data processing] For a finite sample D⊆ X, let c_D(ϕ)=|ϕ(D)| denote the number of reached representation states. If ϕsucceqψ, then c_D(ψ)≤ c_D(ϕ). Choose d with ψ=d∘ϕ. Then ψ(D)=d(ϕ(D)), and the image of a finite set under a function has cardinality at most that of the original set.
Exact mathematical passage
c_D(\psi)\le c_D(\phi).
\subseteqIntroduction passage · 2 passages
Search aliases: ⊆ subseteq
Introduction passage · core_chapters.tex, line 34
[Finite data processing] For a finite sample D⊆ X, let c_D(ϕ)=|ϕ(D)| denote the number of reached representation states. If ϕsucceqψ, then c_D(ψ)≤ c_D(ϕ). Choose d with ψ=d∘ϕ. Then ψ(D)=d(ϕ(D)), and the image of a finite set under a function has cardinality at most that of the original set.
Exact mathematical passage
D\subseteq X
a^*Use in source · 2 passages
Search aliases: a^*
Use in source · planning_chapters.tex, line 288
Let a_h(s) maximize L_h(s,a) and let a^* maximize the true Q_h. Then V_h+1(s)-Q_h(s,a_h(s)) · ≤ U_h(s,a^*)-L_h(s,a_h(s))
Exact mathematical passage
a^*
a_hUse in source · 2 passages
Search aliases: a_h
Use in source · planning_chapters.tex, line 288
Let a_h(s) maximize L_h(s,a) and let a^* maximize the true Q_h. Then V_h+1(s)-Q_h(s,a_h(s)) · ≤ U_h(s,a^*)-L_h(s,a_h(s))
Exact mathematical passage
a_h(s)
a_oUse in source · 4 passages
Search aliases: a_o
Use in source · core_chapters.tex, line 105
[Finite stochastic information-value monotonicity] Every deterministic policy on EK is weakly dominated in value by some deterministic policy on E. Consequently the best deterministic value of EK is at most that of E. For each fine observation o, select a_o∈ A maximizing S_E(o,a). Such a selection exists because A is finite and nonempty. For a coarse policy π, expand the channel composition and rearrange finite sums: J_b(EK,π)=∑_o∑_y K(ymid o)S_E(o,π(y)). Every inner score is at most S_E(o,a_o).…
Exact mathematical passage
a_o\in A
B_0Use in source · 2 passages
Search aliases: B_0
Use in source · core_chapters.tex, line 304
The initial grammar layer has five atoms: two literals and three variables. If a layer is L, expansion retains L, adds all negations, and adds all ordered pairs under each of the three binary operations. Let M_d count emitted list entries at depth d. The source proves M_0=5, M_d+1=2M_d+3M_d^2. The entries can contain duplicates. The node bound is B_0=1, B_d+1=2B_d+1, and every expression of height at most d occurs in the depth-d list. In particular M_1=85 and M_2=21845.
Exact mathematical passage
B_0=1
B_1Use in source · 1 passage
Search aliases: B_1
Use in source · planning_chapters.tex, line 447
[Why the schedule's total allowance is necessary] Take a fair Boolean outcome ω and two checkpoint bad events B_0={ω=0} and B_1={ω=1}. Each has probability 1/2. Selecting j(ω)=ω makes selected failure certain. The total allowance 1/2+1/2=1 remains valid, while either single checkpoint's allowance fails. This is the exact obstruction proved by pathfairBool_adaptive_exceeds_single_budget.
Exact mathematical passage
B_1=\{\omega=1\}
B_dUse in source · 2 passages
Search aliases: B_d
Use in source · core_chapters.tex, line 304
The initial grammar layer has five atoms: two literals and three variables. If a layer is L, expansion retains L, adds all negations, and adds all ordered pairs under each of the three binary operations. Let M_d count emitted list entries at depth d. The source proves M_0=5, M_d+1=2M_d+3M_d^2. The entries can contain duplicates. The node bound is B_0=1, B_d+1=2B_d+1, and every expression of height at most d occurs in the depth-d list. In particular M_1=85 and M_2=21845.
Exact mathematical passage
B_{d+1}=2B_d+1
B_{d+1}Use in source · 1 passage
Search aliases: B_d+1
Use in source · core_chapters.tex, line 304
The initial grammar layer has five atoms: two literals and three variables. If a layer is L, expansion retains L, adds all negations, and adds all ordered pairs under each of the three binary operations. Let M_d count emitted list entries at depth d. The source proves M_0=5, M_d+1=2M_d+3M_d^2. The entries can contain duplicates. The node bound is B_0=1, B_d+1=2B_d+1, and every expression of height at most d occurs in the depth-d list. In particular M_1=85 and M_2=21845.
Exact mathematical passage
B_{d+1}=2B_d+1
b_fUse in source · 1 passage
Search aliases: b_f
Use in source · core_chapters.tex, line 374
[Complete zero-and-basis probes] Two affine signatures f,g:R^n→ R^m are equal if and only if they agree at 0 and at every standard basis vector e_j. Thus n+1 vector probes establish equality on all inputs. A mismatch in signatures has a mismatch among these probes. The zero probe identifies the offsets because f(0)=b_f. At e_j, the output is the jth matrix column plus the offset. After canceling the now-equal offsets, equality of the basis probes identifies every column. Equal coefficients give …
Exact mathematical passage
f(0)=b_f
B_jUse in source · 2 passages
Search aliases: B_j
Use in source · planning_chapters.tex, line 416
[Scheduled and selected failure bounds] Let B_j be the event that checkpoint j's interval excludes p_j. Then Prob(⋃_j∈ JB_j) ≤∑_j∈ Jα_j. For any data-dependent selector j(ω)∈ J, Prob{ω∈ B_j(ω)}≤∑_j∈ Jα_j. For each outcome ω, the indicator of a union is at most the sum of the individual indicators. Multiply by the nonnegative rational weight of ω and sum over the finite probability space. Interchange the two finite sums to obtain the union bound. Each checkpoint has failure mass at most its alloc…
Exact mathematical passage
B_j
B_{j(\omega)}Use in source · 1 passage
Search aliases: B_j(ω) omega
Use in source · planning_chapters.tex, line 422
[Scheduled and selected failure bounds] Let B_j be the event that checkpoint j's interval excludes p_j. Then Prob(⋃_j∈ JB_j) ≤∑_j∈ Jα_j. For any data-dependent selector j(ω)∈ J, Prob{ω∈ B_j(ω)}≤∑_j∈ Jα_j. For each outcome ω, the indicator of a union is at most the sum of the individual indicators. Multiply by the nonnegative rational weight of ω and sum over the finite probability space. Interchange the two finite sums to obtain the union bound. Each checkpoint has failure mass at most its alloc…
Exact mathematical passage
\Prob\{\omega\in B_{j(\omega)}\}\leq\sum_{j\in J}\alpha_j.
b_{n,k}Use in source · 3 passages
Search aliases: b_n,k
Use in source · planning_chapters.tex, line 343
Let K be the number of successes in n Bernoulli trials with rational parameter p∈[0,1]. Define b_n,k(p)=binom nk p^k(1-p)^n-k, 0≤ k≤ n. Choose a positive integer grid size m and nonnegative rational allowance α. The grid cells have endpoints ℓ_i=fracim, u_i=fraci+1m, 0≤ i<m. For observed count k, the envelope of its point mass over cell i is B_n,k,i=binom nk u_i^k(1-ℓ_i)^n-k. Retain the cell exactly when B_n,k,i>fracαn+1. Return the closed interval spanning all retained cells. If there are no re…
Exact mathematical passage
b_{n,k}(p)=\binom nk p^k(1-p)^{n-k},\qquad 0\leq k\leq n.
B_{n,k,i}Use in source · 4 passages
Search aliases: B_n,k,i
Use in source · planning_chapters.tex, line 352
uccesses in n Bernoulli trials with rational parameter p∈[0,1]. Define b_n,k(p)=binom nk p^k(1-p)^n-k, 0≤ k≤ n. Choose a positive integer grid size m and nonnegative rational allowance α. The grid cells have endpoints ℓ_i=fracim, u_i=fraci+1m, 0≤ i<m. For observed count k, the envelope of its point mass over cell i is B_n,k,i=binom nk u_i^k(1-ℓ_i)^n-k. Retain the cell exactly when B_n,k,i>fracαn+1. Return the closed interval spanning all retained cells. If there are no retained cells, return [0,…
Exact mathematical passage
B_{n,k,i}=\binom nk u_i^k(1-\ell_i)^{n-k}.
b_oUse in source · 4 passages
Search aliases: b_o
Use in source · core_chapters.tex, line 126
A rational belief is a nonnegative vector b on finite Ω with ∑_ω b(ω)=1. For a channel E, define the predictive mass p(o)=∑_ω b(ω)E(omidω). For p(o)>0, the posterior is b_o(ω)=b(ω)E(omidω)/p(o). The total updater in the source uses b_o=b when p(o)=0. This fallback is normalized and has zero coefficient in predictive expectations. Nonnegativity of every summand implies that each Bayes numerator also vanishes on such an impossible observation. Hence, with the total-update convention, the division-…
Exact mathematical passage
b_o(\omega)=b(\omega)E(o\mid\omega)/p(o)
\bar bUse in source · 3 passages
Search aliases: bar b bar
Use in source · core_chapters.tex, line 151
[Conditioning commutes with exact compression] Let ϕ:Ω→ Z map between finite spaces, and define the pushforward belief bar b(z)=∑_ϕ(ω)=zb(ω). Suppose L=bar L∘ϕ for a nonnegative likelihood bar L:Z→Q, and the evidence mass is positive. Then ϕ_*C_L(b)=C_bar L(ϕ_*b). Such an exact bar L exists if and only if L is constant on every fiber of ϕ. Grouping the normalizer by fibers gives M_b(L)=M_bar b(bar L). On each fiber ϕ^-1(z), the likelihood can be factored outside the sum. Thus ∑_ϕ(ω)=zfracb(ω)L(ω…
Exact mathematical passage
\bar b(z)=\sum_{\phi(\omega)=z}b(\omega)
\bar LUse in source · 6 passages
Search aliases: bar L bar
Use in source · core_chapters.tex, line 151
[Conditioning commutes with exact compression] Let ϕ:Ω→ Z map between finite spaces, and define the pushforward belief bar b(z)=∑_ϕ(ω)=zb(ω). Suppose L=bar L∘ϕ for a nonnegative likelihood bar L:Z→Q, and the evidence mass is positive. Then ϕ_*C_L(b)=C_bar L(ϕ_*b). Such an exact bar L exists if and only if L is constant on every fiber of ϕ. Grouping the normalizer by fibers gives M_b(L)=M_bar b(bar L). On each fiber ϕ^-1(z), the likelihood can be factored outside the sum. Thus ∑_ϕ(ω)=zfracb(ω)L(ω…
Exact mathematical passage
L=\bar L\circ\phi
\bar PUse in source · 2 passages
Search aliases: bar P bar
Use in source · core_chapters.tex, line 229
[Exact stochastic quotient] Suppose ϕ:S→ Z is surjective and projected stochastically sufficient, with S,Z finite. Choose a representative s_z of every fiber, and define bar r(z,a)=r(s_z,a), bar P_a(z,z')=∑_ϕ(s')=z'P_a(s_z,s'). These quantities give a normalized rational stochastic control system, independent of the representative choices for admissible actions. For every finite horizon, bar V_n(ϕ(s))=V_n(s). Nonnegative fiber masses give nonnegative quotient probabilities; partitioning S by the…
Exact mathematical passage
\bar r(z,a)=r(s_z,a),\qquad \bar P_a(z,z')=\sum_{\phi(s')=z'}P_a(s_z,s').
\bar P_aUse in source · 2 passages
Search aliases: bar P_a bar
Use in source · core_chapters.tex, line 229
[Exact stochastic quotient] Suppose ϕ:S→ Z is surjective and projected stochastically sufficient, with S,Z finite. Choose a representative s_z of every fiber, and define bar r(z,a)=r(s_z,a), bar P_a(z,z')=∑_ϕ(s')=z'P_a(s_z,s'). These quantities give a normalized rational stochastic control system, independent of the representative choices for admissible actions. For every finite horizon, bar V_n(ϕ(s))=V_n(s). Nonnegative fiber masses give nonnegative quotient probabilities; partitioning S by the…
Exact mathematical passage
\bar r(z,a)=r(s_z,a),\qquad \bar P_a(z,z')=\sum_{\phi(s')=z'}P_a(s_z,s').
\bar rUse in source · 1 passage
Search aliases: bar r bar
Use in source · core_chapters.tex, line 229
[Exact stochastic quotient] Suppose ϕ:S→ Z is surjective and projected stochastically sufficient, with S,Z finite. Choose a representative s_z of every fiber, and define bar r(z,a)=r(s_z,a), bar P_a(z,z')=∑_ϕ(s')=z'P_a(s_z,s'). These quantities give a normalized rational stochastic control system, independent of the representative choices for admissible actions. For every finite horizon, bar V_n(ϕ(s))=V_n(s). Nonnegative fiber masses give nonnegative quotient probabilities; partitioning S by the…
Exact mathematical passage
\bar r(z,a)=r(s_z,a),\qquad \bar P_a(z,z')=\sum_{\phi(s')=z'}P_a(s_z,s').
\bar VUse in source · 2 passages
Search aliases: bar V bar
Use in source · core_chapters.tex, line 234
Suppose ϕ:S→ Z is surjective and projected stochastically sufficient, with S,Z finite. Choose a representative s_z of every fiber, and define bar r(z,a)=r(s_z,a), bar P_a(z,z')=∑_ϕ(s')=z'P_a(s_z,s'). These quantities give a normalized rational stochastic control system, independent of the representative choices for admissible actions. For every finite horizon, bar V_n(ϕ(s))=V_n(s). Nonnegative fiber masses give nonnegative quotient probabilities; partitioning S by the fibers shows that each quot…
Exact mathematical passage
\bar V_n(\phi(s))=V_n(s).
\bar V_nUse in source · 2 passages
Search aliases: bar V_n bar
Use in source · core_chapters.tex, line 234
Suppose ϕ:S→ Z is surjective and projected stochastically sufficient, with S,Z finite. Choose a representative s_z of every fiber, and define bar r(z,a)=r(s_z,a), bar P_a(z,z')=∑_ϕ(s')=z'P_a(s_z,s'). These quantities give a normalized rational stochastic control system, independent of the representative choices for admissible actions. For every finite horizon, bar V_n(ϕ(s))=V_n(s). Nonnegative fiber masses give nonnegative quotient probabilities; partitioning S by the fibers shows that each quot…
Exact mathematical passage
\bar V_n(\phi(s))=V_n(s).
CUse in source · 6 passages
Search aliases: C
Use in source · core_chapters.tex, line 137
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
M_b(L)=\sum_\omega b(\omega)L(\omega),\qquad C_L(b)(\omega)=\frac{b(\omega)L(\omega)}{M_b(L)}
\mathsf cUse in source · 1 passage
Search aliases: c mathsf
Use in source · introduction.tex, line 29
Writing I for issuance and C for the specified episode certificate, the resulting conclusion is Prob(I∩ C^ c)≤∑_j∈ Jα_j. This is an unconditional probability over the original outcome space. It allows arbitrary dependence between scheduled checkpoints. It retains failed and unfinished runs in that space, with no plan issued on those runs. It does not assert a nominal bound conditional on issuance or completion, eventual issuance, or a productivity lower bound. The final recorder theorem derives …
Exact mathematical passage
\Prob(I\cap C^{\mathsf c})\leq\sum_{j\in J}\alpha_j.
C^{\mathsf c}Use in source · 1 passage
Search aliases: C^ c mathsf
Use in source · introduction.tex, line 29
Writing I for issuance and C for the specified episode certificate, the resulting conclusion is Prob(I∩ C^ c)≤∑_j∈ Jα_j. This is an unconditional probability over the original outcome space. It allows arbitrary dependence between scheduled checkpoints. It retains failed and unfinished runs in that space, with no plan issued on those runs. It does not assert a nominal bound conditional on issuance or completion, eventual issuance, or a productivity lower bound. The final recorder theorem derives …
Exact mathematical passage
\Prob(I\cap C^{\mathsf c})\leq\sum_{j\in J}\alpha_j.
C_{\bar L}Use in source · 1 passage
Search aliases: C_bar L bar
Use in source · core_chapters.tex, line 152
[Conditioning commutes with exact compression] Let ϕ:Ω→ Z map between finite spaces, and define the pushforward belief bar b(z)=∑_ϕ(ω)=zb(ω). Suppose L=bar L∘ϕ for a nonnegative likelihood bar L:Z→Q, and the evidence mass is positive. Then ϕ_*C_L(b)=C_bar L(ϕ_*b). Such an exact bar L exists if and only if L is constant on every fiber of ϕ. Grouping the normalizer by fibers gives M_b(L)=M_bar b(bar L). On each fiber ϕ^-1(z), the likelihood can be factored outside the sum. Thus ∑_ϕ(ω)=zfracb(ω)L(ω…
Exact mathematical passage
\phi_*C_L(b)=C_{\bar L}(\phi_*b).
c_c^+Use in source · 1 passage
Search aliases: c_c^+
Use in source · planning_chapters.tex, line 159
Let w_c(k)=c_k^+-c_k^-, w_g(k)=g_k^+-g_k^-, and w_p(k)=p_k^+-p_k^-. The source uses the uniform quantities ε · =w_c(w)+w_c(c)+w_g(w)+w_g(c), δ · =2(w_p(w)+w_p(c)), M · =c_w^++c_c^++g_w^++g_c^+. They bound reward error, Boolean-row L^1 error, and nominal one-step reward magnitude respectively. For an acquisition of kind k, the sharper local reward error is w_c(k) and its row error is 2w_p(k). For deployment of kind k, the local reward error is w_g(k) and its row error is zero. Stop has zero primi…
Exact mathematical passage
\varepsilon&=w_c(w)+w_c(c)+w_g(w)+w_g(c),\\ \delta&=2\bigl(w_p(w)+w_p(c)\bigr),\\ M&=c_w^++c_c^++g_w^++g_c^+.
c_kUse in source · 1 passage
Search aliases: c_k
Use in source · planning_chapters.tex, line 138
For kind k∈{w,c}, write c_k∈[c_k^-,c_k^+], g_k∈[g_k^-,g_k^+], p_k∈[p_k^-,p_k^+]. The formal nominal model reserves c_k^+, credits g_k^-, and uses p_k^-. A compatible realization supplies exact values inside these bands. In the true comparison system, rewards and report probabilities use those exact values, but the state transitions and action guards remain those of the nominal model. In particular, setup reservations continue to use the upper setup bound.
Exact mathematical passage
c_k\in[c_k^-,c_k^+],\qquad g_k\in[g_k^-,g_k^+],\qquad p_k\in[p_k^-,p_k^+].
c_k^+Use in source · 3 passages
Search aliases: c_k^+
Use in source · planning_chapters.tex, line 138
For kind k∈{w,c}, write c_k∈[c_k^-,c_k^+], g_k∈[g_k^-,g_k^+], p_k∈[p_k^-,p_k^+]. The formal nominal model reserves c_k^+, credits g_k^-, and uses p_k^-. A compatible realization supplies exact values inside these bands. In the true comparison system, rewards and report probabilities use those exact values, but the state transitions and action guards remain those of the nominal model. In particular, setup reservations continue to use the upper setup bound.
Exact mathematical passage
c_k\in[c_k^-,c_k^+],\qquad g_k\in[g_k^-,g_k^+],\qquad p_k\in[p_k^-,p_k^+].
c_k^-Use in source · 2 passages
Search aliases: c_k^-
Use in source · planning_chapters.tex, line 138
For kind k∈{w,c}, write c_k∈[c_k^-,c_k^+], g_k∈[g_k^-,g_k^+], p_k∈[p_k^-,p_k^+]. The formal nominal model reserves c_k^+, credits g_k^-, and uses p_k^-. A compatible realization supplies exact values inside these bands. In the true comparison system, rewards and report probabilities use those exact values, but the state transitions and action guards remain those of the nominal model. In particular, setup reservations continue to use the upper setup bound.
Exact mathematical passage
c_k\in[c_k^-,c_k^+],\qquad g_k\in[g_k^-,g_k^+],\qquad p_k\in[p_k^-,p_k^+].
C_LUse in source · 2 passages
Search aliases: C_L
Use in source · core_chapters.tex, line 137
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
M_b(L)=\sum_\omega b(\omega)L(\omega),\qquad C_L(b)(\omega)=\frac{b(\omega)L(\omega)}{M_b(L)}
C_{L_1}Use in source · 1 passage
Search aliases: C_L_1
Use in source · core_chapters.tex, line 142
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
M_b(L_1)M_{C_{L_1}(b)}(L_2)=M_b(L_1L_2),\qquad C_{L_2}(C_{L_1}(b))=C_{L_1L_2}(b).
C_{L_1L_2}Use in source · 1 passage
Search aliases: C_L_1L_2
Use in source · core_chapters.tex, line 142
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
M_b(L_1)M_{C_{L_1}(b)}(L_2)=M_b(L_1L_2),\qquad C_{L_2}(C_{L_1}(b))=C_{L_1L_2}(b).
C_{L_2}Use in source · 1 passage
Search aliases: C_L_2
Use in source · core_chapters.tex, line 142
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
M_b(L_1)M_{C_{L_1}(b)}(L_2)=M_b(L_1L_2),\qquad C_{L_2}(C_{L_1}(b))=C_{L_1L_2}(b).
c_w^+Use in source · 1 passage
Search aliases: c_w^+
Use in source · planning_chapters.tex, line 159
Let w_c(k)=c_k^+-c_k^-, w_g(k)=g_k^+-g_k^-, and w_p(k)=p_k^+-p_k^-. The source uses the uniform quantities ε · =w_c(w)+w_c(c)+w_g(w)+w_g(c), δ · =2(w_p(w)+w_p(c)), M · =c_w^++c_c^++g_w^++g_c^+. They bound reward error, Boolean-row L^1 error, and nominal one-step reward magnitude respectively. For an acquisition of kind k, the sharper local reward error is w_c(k) and its row error is 2w_p(k). For deployment of kind k, the local reward error is w_g(k) and its row error is zero. Stop has zero primi…
Exact mathematical passage
\varepsilon&=w_c(w)+w_c(c)+w_g(w)+w_g(c),\\ \delta&=2\bigl(w_p(w)+w_p(c)\bigr),\\ M&=c_w^++c_c^++g_w^++g_c^+.
c_\phiUse in source · 2 passages
Search aliases: c_ϕ phi
Use in source · core_chapters.tex, line 73
[Deterministic information-value monotonicity] If ϕsucceqψ, then J_b^*(ψ)≤ J_b^*(ϕ). If the acquisition costs satisfy c_ϕ≤ c_ψ, then J_b^*(ψ)-c_ψ≤ J_b^*(ϕ)-c_ϕ. Let d decode ψ from ϕ. Any coarse policy π lifts to π∘ d. For every world the lifted policy chooses exactly the same action, so its decision value is unchanged. A maximizing coarse policy exists because the policy space is finite and nonempty. Its lifted value is at most the best fine value. Subtracting the stated costs gives the second …
Exact mathematical passage
c_\phi\le c_\psi
c_\psiUse in source · 2 passages
Search aliases: c_ψ psi
Use in source · core_chapters.tex, line 73
[Deterministic information-value monotonicity] If ϕsucceqψ, then J_b^*(ψ)≤ J_b^*(ϕ). If the acquisition costs satisfy c_ϕ≤ c_ψ, then J_b^*(ψ)-c_ψ≤ J_b^*(ϕ)-c_ϕ. Let d decode ψ from ϕ. Any coarse policy π lifts to π∘ d. For every world the lifted policy chooses exactly the same action, so its decision value is unchanged. A maximizing coarse policy exists because the policy space is finite and nonempty. Its lifted value is at most the best fine value. Subtracting the stated costs gives the second …
Exact mathematical passage
c_\phi\le c_\psi
\operatorname{cost}Use in source · 1 passage
Search aliases: cost operatorname
Use in source · core_chapters.tex, line 464
The menu selector compares three equivalent implementations: the current program, its dense fused atom, and the accepted minimum-width two-stage plan. Its selected tariff is exactly min{cost(p), D(n,m), F(n,m,k)}. This proves a minimum over the explicit menu, and also comparison with every exact two-dense-stage factorization. It does not prove a globally cheapest affine program in the larger language. Sparse schedules, sharing, special primitives, and hardware-specific algorithms have different …
Exact mathematical passage
\min\{\operatorname{cost}(p),\ D(n,m),\ F(n,m,k)\}.
D_1Use in source · 1 passage
Search aliases: D_1
Use in source · planning_chapters.tex, line 260
mple[A deliberately conservative abstract quote fixture] The retained uncertainty example assigns zero setup to both kinds, warm gross 200, cold gross 60, warm success band [3/5,1], and exact cold success 1. Start with both statuses untried and use h=1, hence two total actions. The nominal scores are warm 120, cold 60, and stop 0. Here ε=0, δ=4/5, M=260, and D_1=0. The local warm radius is 208, while the cold and stop radii are zero: c|r|r|r action · widehat Q_1 · ρ_1 · L_1
Exact mathematical passage
D_1=0
D_hUse in source · 4 passages
Search aliases: D_h
Use in source · planning_chapters.tex, line 190
Induction on the Bellman recursion gives |widehat V_h(s)|≤ hM for the nominal value. The source's accumulated value radius and local Q radius are D_h · =∑_j=0^h-1(ε+δ jM), ρ_h(a) · =D_h+ε_a+δ_a hM, Γ_h · =D_h+ε+δ hM. The Bellman residual is zero here because the nominal tables are exact Bellman values. The broader model-error framework also allows a supplied table with a proved nonzero residual, but no residual term is silently introduced in these quote results.
Exact mathematical passage
D_h&=\sum_{j=0}^{h-1}(\varepsilon+\delta jM),\label{eq:value-radius}\\ \rho_h(a)&=D_h+\varepsilon_a+\delta_a hM,\label{eq:local-radius}\\ \Gamma_h&=D_h+\varepsilon+\delta hM.\label{eq:global-radius}
D_{h+1}Use in source · 1 passage
Search aliases: D_h+1
Use in source · planning_chapters.tex, line 215
inproof At horizon zero the value error is zero. In a single backup, insert and subtract the expectation of the nominal continuation under the true row. The reward error contributes at most ε_a, the continuation-value error at most D_h, and row transport at most δ_a hM. Taking a maximum over the same feasible action set is nonexpansive in the uniform score error. Therefore D_h+1≤ D_h+ε+δ hM, whose accumulated upper bound is [source reference]. The local Q statement follows from the same inserted…
Exact mathematical passage
D_{h+1}\leq D_h+\varepsilon+\delta hM
d_qUse in source · 2 passages
Search aliases: d_q
Use in source · core_chapters.tex, line 55
Suppose a family of tasks is given by T_q:X→ Y, indexed by q∈ Q. Define the joint target T_joint(x)=(T_q(x))_q∈ Q∈ Y^Q. Then ϕ is sufficient for the joint target if and only if it is sufficient for each individual task. The forward direction evaluates the decoded answer vector at q. For the reverse direction, choose a decoder d_q for each query and define d(z)(q)=d_q(z). The formal theorem permits an arbitrary query index type, and the simultaneous decoder selection uses classical choice.
Exact mathematical passage
d_q
\downarrowUse in source · 1 passage
Search aliases: downarrow
Use in source · common.tex, line 48
1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\downarrow
eUse in source · 6 passages
Search aliases: e
Use in source · core_chapters.tex, line 371
[Complete zero-and-basis probes] Two affine signatures f,g:R^n→ R^m are equal if and only if they agree at 0 and at every standard basis vector e_j. Thus n+1 vector probes establish equality on all inputs. A mismatch in signatures has a mismatch among these probes. The zero probe identifies the offsets because f(0)=b_f. At e_j, the output is the jth matrix column plus the offset. After canceling the now-equal offsets, equality of the basis probes identifies every column. Equal coefficients give …
Exact mathematical passage
e_j
e_jUse in source · 2 passages
Search aliases: e_j
Use in source · core_chapters.tex, line 371
[Complete zero-and-basis probes] Two affine signatures f,g:R^n→ R^m are equal if and only if they agree at 0 and at every standard basis vector e_j. Thus n+1 vector probes establish equality on all inputs. A mismatch in signatures has a mismatch among these probes. The zero probe identifies the offsets because f(0)=b_f. At e_j, the output is the jth matrix column plus the offset. After canceling the now-equal offsets, equality of the basis probes identifies every column. Equal coefficients give …
Exact mathematical passage
e_j
\operatorname{eval}Use in source · 1 passage
Search aliases: eval operatorname
Use in source · core_chapters.tex, line 386
Typed programs combine affine atoms, identities, sequential composition, and pointwise addition. Composition connects only matching intermediate dimensions. An independent recursive execution semantics and coefficient-normalization semantics are defined. Structural induction proves eval(normalize(p),x)=run(p,x) for all x. Hence two programs are equivalent if and only if their normal signatures coincide. Decidable coefficient comparison is a sound and complete checker when equality in R is decida…
Exact mathematical passage
\operatorname{eval}(\operatorname{normalize}(p),x)=\operatorname{run}(p,x) \qquad\text{for all }x.
\mathrm{evaluationSpent}Use in source · 1 passage
Search aliases: evaluationSpent mathrm
Use in source · planning_chapters.tex, line 788
For a successful paid trace with total evaluation debit e and switching debit u, the formal accounting identities are evaluationSpent_rm final · =evaluationSpent_rm initial+e, switchSpent_rm final · =switchSpent_rm initial+u. From a safe initial journal, their sum stays within protected credits. Successful replay also cannot decrease the protected utility of the active version. These are pathpaid_trace_exact_accounting, pathpaid_trace_no_overspend, and pathreplay_utility_nondecreasing in pathAVO…
Exact mathematical passage
\mathrm{evaluationSpent}_{\rm final} &=\mathrm{evaluationSpent}_{\rm initial}+e,\\ \mathrm{switchSpent}_{\rm final} &=\mathrm{switchSpent}_{\rm initial}+u.
\mathrm{evaluationSpent}_{\rm final}Use in source · 1 passage
Search aliases: evaluationSpent_rm final mathrm rm
Use in source · planning_chapters.tex, line 788
For a successful paid trace with total evaluation debit e and switching debit u, the formal accounting identities are evaluationSpent_rm final · =evaluationSpent_rm initial+e, switchSpent_rm final · =switchSpent_rm initial+u. From a safe initial journal, their sum stays within protected credits. Successful replay also cannot decrease the protected utility of the active version. These are pathpaid_trace_exact_accounting, pathpaid_trace_no_overspend, and pathreplay_utility_nondecreasing in pathAVO…
Exact mathematical passage
\mathrm{evaluationSpent}_{\rm final} &=\mathrm{evaluationSpent}_{\rm initial}+e,\\ \mathrm{switchSpent}_{\rm final} &=\mathrm{switchSpent}_{\rm initial}+u.
\mathrm{evaluationSpent}_{\rm initial}Use in source · 1 passage
Search aliases: evaluationSpent_rm initial mathrm rm
Use in source · planning_chapters.tex, line 788
For a successful paid trace with total evaluation debit e and switching debit u, the formal accounting identities are evaluationSpent_rm final · =evaluationSpent_rm initial+e, switchSpent_rm final · =switchSpent_rm initial+u. From a safe initial journal, their sum stays within protected credits. Successful replay also cannot decrease the protected utility of the active version. These are pathpaid_trace_exact_accounting, pathpaid_trace_no_overspend, and pathreplay_utility_nondecreasing in pathAVO…
Exact mathematical passage
\mathrm{evaluationSpent}_{\rm final} &=\mathrm{evaluationSpent}_{\rm initial}+e,\\ \mathrm{switchSpent}_{\rm final} &=\mathrm{switchSpent}_{\rm initial}+u.
FUse in source · 5 passages
Search aliases: F
Use in source · core_chapters.tex, line 257
[Checker soundness] If the inference checker accepts derivation p for target F under context Γ, then every valuation satisfying Γ satisfies F. Induct on the derivation. A used assumption belongs to Γ and is true by the context hypothesis. Conjunction introduction combines the two inductive conclusions, and its projections select the corresponding conclusion. Implication introduction applies the induction hypothesis in the extended context; implication elimination applies a proved implication to …
Exact mathematical passage
F
\mathbb FUse in source · 1 passage
Search aliases: F mathbb
Use in source · introduction.tex, line 45
A running computational example. Consider an affine map over F_5 with four inputs and four outputs, all-ones linear coefficient matrix, and offset (1,2,3,4). The direct dense evaluation tariff is 4(2·4+1)=36. Its rank-one factorization has a 4→1 stage followed by a 1→4 stage, with tariff 9+12=21. Thus each declared call saves 15 arithmetic cost units. For 1,000 calls the gross saving is 15,000.
Exact mathematical passage
\mathbb F_5
\mathbf FUse in source · 1 passage
Search aliases: F mathbf
Use in source · core_chapters.tex, line 454
[A checked rank-one bottleneck] In the archived finite-field example over F_5, A is the 4×4 all-ones matrix and b=(1,2,3,4). The first stage computes y=x_1+x_2+x_3+x_4. The second emits (y+1,y+2,y+3,y+4). Taking L to select the first output coordinate and H to select the first input coordinate gives LAH=(1). The width-one factorization is therefore exact and width minimal.
Exact mathematical passage
\mathbf F_5
\mathbb F_5Use in source · 1 passage
Search aliases: F_5 mathbb
Use in source · introduction.tex, line 45
A running computational example. Consider an affine map over F_5 with four inputs and four outputs, all-ones linear coefficient matrix, and offset (1,2,3,4). The direct dense evaluation tariff is 4(2·4+1)=36. Its rank-one factorization has a 4→1 stage followed by a 1→4 stage, with tariff 9+12=21. Thus each declared call saves 15 arithmetic cost units. For 1,000 calls the gross saving is 15,000.
Exact mathematical passage
\mathbb F_5
\mathbf F_5Use in source · 1 passage
Search aliases: F_5 mathbf
Use in source · core_chapters.tex, line 454
[A checked rank-one bottleneck] In the archived finite-field example over F_5, A is the 4×4 all-ones matrix and b=(1,2,3,4). The first stage computes y=x_1+x_2+x_3+x_4. The second emits (y+1,y+2,y+3,y+4). Taking L to select the first output coordinate and H to select the first input coordinate gives LAH=(1). The width-one factorization is therefore exact and width minimal.
Exact mathematical passage
\mathbf F_5
\mathrm{false}Use in source · 2 passages
Search aliases: false mathrm
Use in source · planning_chapters.tex, line 569
[Replay and faults do not create new evidence] Let an identity's source be [true,false]. Begin ID 7, report ID 7, then report ID 7 again. The sample list is [true] and the remaining source begins with false. Begin ID 8 and finish it as a fault. The sample list stays unchanged. Begin and report ID 9. It appends false, yielding [true,false]. A further fresh report rejects after source exhaustion, while a replay of ID 7 remains possible. The replay supplies no extra success and the fault supplies n…
Exact mathematical passage
[\mathrm{true},\mathrm{false}]
gUse in source · 11 passages
Search aliases: g
Use in source · core_chapters.tex, line 371
[Complete zero-and-basis probes] Two affine signatures f,g:R^n→ R^m are equal if and only if they agree at 0 and at every standard basis vector e_j. Thus n+1 vector probes establish equality on all inputs. A mismatch in signatures has a mismatch among these probes. The zero probe identifies the offsets because f(0)=b_f. At e_j, the output is the jth matrix column plus the offset. After canceling the now-equal offsets, equality of the basis probes identifies every column. Equal coefficients give …
Exact mathematical passage
f,g:R^n\to R^m
g_c^+Use in source · 1 passage
Search aliases: g_c^+
Use in source · planning_chapters.tex, line 159
Let w_c(k)=c_k^+-c_k^-, w_g(k)=g_k^+-g_k^-, and w_p(k)=p_k^+-p_k^-. The source uses the uniform quantities ε · =w_c(w)+w_c(c)+w_g(w)+w_g(c), δ · =2(w_p(w)+w_p(c)), M · =c_w^++c_c^++g_w^++g_c^+. They bound reward error, Boolean-row L^1 error, and nominal one-step reward magnitude respectively. For an acquisition of kind k, the sharper local reward error is w_c(k) and its row error is 2w_p(k). For deployment of kind k, the local reward error is w_g(k) and its row error is zero. Stop has zero primi…
Exact mathematical passage
\varepsilon&=w_c(w)+w_c(c)+w_g(w)+w_g(c),\\ \delta&=2\bigl(w_p(w)+w_p(c)\bigr),\\ M&=c_w^++c_c^++g_w^++g_c^+.
g_kUse in source · 1 passage
Search aliases: g_k
Use in source · planning_chapters.tex, line 138
For kind k∈{w,c}, write c_k∈[c_k^-,c_k^+], g_k∈[g_k^-,g_k^+], p_k∈[p_k^-,p_k^+]. The formal nominal model reserves c_k^+, credits g_k^-, and uses p_k^-. A compatible realization supplies exact values inside these bands. In the true comparison system, rewards and report probabilities use those exact values, but the state transitions and action guards remain those of the nominal model. In particular, setup reservations continue to use the upper setup bound.
Exact mathematical passage
c_k\in[c_k^-,c_k^+],\qquad g_k\in[g_k^-,g_k^+],\qquad p_k\in[p_k^-,p_k^+].
g_k^+Use in source · 2 passages
Search aliases: g_k^+
Use in source · planning_chapters.tex, line 138
For kind k∈{w,c}, write c_k∈[c_k^-,c_k^+], g_k∈[g_k^-,g_k^+], p_k∈[p_k^-,p_k^+]. The formal nominal model reserves c_k^+, credits g_k^-, and uses p_k^-. A compatible realization supplies exact values inside these bands. In the true comparison system, rewards and report probabilities use those exact values, but the state transitions and action guards remain those of the nominal model. In particular, setup reservations continue to use the upper setup bound.
Exact mathematical passage
c_k\in[c_k^-,c_k^+],\qquad g_k\in[g_k^-,g_k^+],\qquad p_k\in[p_k^-,p_k^+].
g_k^-Use in source · 3 passages
Search aliases: g_k^-
Use in source · planning_chapters.tex, line 138
For kind k∈{w,c}, write c_k∈[c_k^-,c_k^+], g_k∈[g_k^-,g_k^+], p_k∈[p_k^-,p_k^+]. The formal nominal model reserves c_k^+, credits g_k^-, and uses p_k^-. A compatible realization supplies exact values inside these bands. In the true comparison system, rewards and report probabilities use those exact values, but the state transitions and action guards remain those of the nominal model. In particular, setup reservations continue to use the upper setup bound.
Exact mathematical passage
c_k\in[c_k^-,c_k^+],\qquad g_k\in[g_k^-,g_k^+],\qquad p_k\in[p_k^-,p_k^+].
g_w^+Use in source · 1 passage
Search aliases: g_w^+
Use in source · planning_chapters.tex, line 159
Let w_c(k)=c_k^+-c_k^-, w_g(k)=g_k^+-g_k^-, and w_p(k)=p_k^+-p_k^-. The source uses the uniform quantities ε · =w_c(w)+w_c(c)+w_g(w)+w_g(c), δ · =2(w_p(w)+w_p(c)), M · =c_w^++c_c^++g_w^++g_c^+. They bound reward error, Boolean-row L^1 error, and nominal one-step reward magnitude respectively. For an acquisition of kind k, the sharper local reward error is w_c(k) and its row error is 2w_p(k). For deployment of kind k, the local reward error is w_g(k) and its row error is zero. Stop has zero primi…
Exact mathematical passage
\varepsilon&=w_c(w)+w_c(c)+w_g(w)+w_g(c),\\ \delta&=2\bigl(w_p(w)+w_p(c)\bigr),\\ M&=c_w^++c_c^++g_w^++g_c^+.
\mathrm{generateCold}Use in source · 2 passages
Search aliases: generateCold mathrm
Use in source · planning_chapters.tex, line 87
[The artifact-backed rank-one comparison] The exact quote model retained in pathAVOC/RobustQuoteExamples.lean has warm setup 133, cold setup 196, success probability 1 for both, and gross deployment value 15000 for each over 1000 calls. With initial credit 196 and two total actions available, Q_1(inspectWarm)=15000-133=14867, Q_1(generateCold)=15000-196=14804. Warm inspection is better by 63 in this exact model. At one total action, acquisition has only its negative immediate reward, and stoppin…
Exact mathematical passage
Q_1(\mathrm{inspectWarm})=15000-133=14867, \qquad Q_1(\mathrm{generateCold})=15000-196=14804.
HUse in source · 17 passages
Search aliases: H
Use in source · core_chapters.tex, line 425
Work over a field R. For reference f=(A,b):R^n→ R^m, a candidate supplies an intermediate width k, first and second affine signatures a(x)=Ux+u_0, d(y)=Vy+v_0, and matrices L∈ R^k× m, H∈ R^n× k. The checker verifies VU=A, Vu_0+v_0=b, LAH=I_k. The first two identities give the exact upper implementation. The third is an independently checkable lower witness. Validation uses polynomial matrix identities; an untrusted rank routine is not part of the logical justification.
Exact mathematical passage
H\in R^{n\times k}
\hlineUse in source · 2 passages
Search aliases: hline
Use in source · planning_chapters.tex, line 262
example assigns zero setup to both kinds, warm gross 200, cold gross 60, warm success band [3/5,1], and exact cold success 1. Start with both statuses untried and use h=1, hence two total actions. The nominal scores are warm 120, cold 60, and stop 0. Here ε=0, δ=4/5, M=260, and D_1=0. The local warm radius is 208, while the cold and stop radii are zero: c|r|r|r action · widehat Q_1 · ρ_1 · L_1 inspectWarm · 120 · 208 · -88 generateCold · 60 · 0 · 60 stop · 0 · 0 · 0 The lower-Q rule chooses cold…
Exact mathematical passage
\begin{array}{c|r|r|r} \text{action}&\widehat Q_1&\rho_1&L_1\\\hline \mathrm{inspectWarm}&120&208&-88\\ \mathrm{generateCold}&60&0&60\\ \mathrm{stop}&0&0&0 \end{array}
IUse in source · 8 passages
Search aliases: I
Use in source · core_chapters.tex, line 426
Work over a field R. For reference f=(A,b):R^n→ R^m, a candidate supplies an intermediate width k, first and second affine signatures a(x)=Ux+u_0, d(y)=Vy+v_0, and matrices L∈ R^k× m, H∈ R^n× k. The checker verifies VU=A, Vu_0+v_0=b, LAH=I_k. The first two identities give the exact upper implementation. The third is an independently checkable lower witness. Validation uses polynomial matrix identities; an untrusted rank routine is not part of the logical justification.
Exact mathematical passage
VU=A,\qquad Vu_0+v_0=b,\qquad LAH=I_k.
iUse in source · 10 passages
Search aliases: i
Use in source · planning_chapters.tex, line 348
Let K be the number of successes in n Bernoulli trials with rational parameter p∈[0,1]. Define b_n,k(p)=binom nk p^k(1-p)^n-k, 0≤ k≤ n. Choose a positive integer grid size m and nonnegative rational allowance α. The grid cells have endpoints ℓ_i=fracim, u_i=fraci+1m, 0≤ i<m. For observed count k, the envelope of its point mass over cell i is B_n,k,i=binom nk u_i^k(1-ℓ_i)^n-k. Retain the cell exactly when B_n,k,i>fracαn+1. Return the closed interval spanning all retained cells. If there are no re…
Exact mathematical passage
\ell_i=\frac{i}{m},\qquad u_i=\frac{i+1}{m},\qquad 0\leq i<m.
I_kUse in source · 4 passages
Search aliases: I_k
Use in source · core_chapters.tex, line 426
Work over a field R. For reference f=(A,b):R^n→ R^m, a candidate supplies an intermediate width k, first and second affine signatures a(x)=Ux+u_0, d(y)=Vy+v_0, and matrices L∈ R^k× m, H∈ R^n× k. The checker verifies VU=A, Vu_0+v_0=b, LAH=I_k. The first two identities give the exact upper implementation. The third is an independently checkable lower witness. Validation uses polynomial matrix identities; an untrusted rank routine is not part of the logical justification.
Exact mathematical passage
VU=A,\qquad Vu_0+v_0=b,\qquad LAH=I_k.
\mathrm{inspectWarm}Use in source · 2 passages
Search aliases: inspectWarm mathrm
Use in source · planning_chapters.tex, line 87
[The artifact-backed rank-one comparison] The exact quote model retained in pathAVOC/RobustQuoteExamples.lean has warm setup 133, cold setup 196, success probability 1 for both, and gross deployment value 15000 for each over 1000 calls. With initial credit 196 and two total actions available, Q_1(inspectWarm)=15000-133=14867, Q_1(generateCold)=15000-196=14804. Warm inspection is better by 63 in this exact model. At one total action, acquisition has only its negative immediate reward, and stoppin…
Exact mathematical passage
Q_1(\mathrm{inspectWarm})=15000-133=14867, \qquad Q_1(\mathrm{generateCold})=15000-196=14804.
jUse in source · 23 passages
Search aliases: j
Use in source · core_chapters.tex, line 334
A complete finite semantic algebra supports a stronger conclusion than searching a deeper finite layer. Let D be a semantic domain with interpretations of the Boolean constructors. A cost function c:D→N is a lower certificate if it satisfies the constructor inequalities c(literal b) · ≤1, · c(variable j) · ≤1, c(neg s) · ≤ c(s)+1, · c(smathbin∘t) · ≤ c(s)+c(t)+1 (∘∈{wedge,vee,⊕}).
Exact mathematical passage
c(\text{literal }b)&\le1,& c(\text{variable }j)&\le1,\\ c(\neg s)&\le c(s)+1,& c(s\mathbin{\circ}t)&\le c(s)+c(t)+1 \quad(\circ\in\{\wedge,\vee,\oplus\}).
J_H^{\rm lower}Use in source · 2 passages
Search aliases: J_H^rm lower rm
Use in source · planning_chapters.tex, line 300
[Expected frozen-policy regret] For a horizon H, let J_H^rm lower(s) be the expected value of the complete adaptive policy induced by robust lower-Q selection. Under any compatible realization, 0≤ V_H(s)-J_H^rm lower(s) ≤∑_h=0^H-12Γ_h. The comparator is the true optimal legal adaptive plan with the same conservative reservation guards. Write the regret at a node with h+1 remaining steps as its local Bellman loss plus the expected regret of the selected continuation. The local term is at most 2Γ_…
Exact mathematical passage
J_H^{\rm lower}(s)
\mathrm{joint}Use in source · 1 passage
Search aliases: joint mathrm
Use in source · core_chapters.tex, line 52
Suppose a family of tasks is given by T_q:X→ Y, indexed by q∈ Q. Define the joint target T_joint(x)=(T_q(x))_q∈ Q∈ Y^Q. Then ϕ is sufficient for the joint target if and only if it is sufficient for each individual task. The forward direction evaluates the decoded answer vector at q. For the reverse direction, choose a decoder d_q for each query and define d(z)(q)=d_q(z). The formal theorem permits an arbitrary query index type, and the simultaneous decoder selection uses classical choice.
Exact mathematical passage
T_{\mathrm{joint}}(x)=(T_q(x))_{q\in Q}\in Y^Q.
kUse in source · 44 passages
Search aliases: k
Use in source · core_chapters.tex, line 402
An exact normal form can improve verification without improving evaluation. The affine backend therefore checks semantics and cost separately. Its dense arithmetic tariff is D(n,m)=m(2n+1), charging n multiplications, n accumulations, and one bias addition per output row. The coefficient-composition tariff is C(n,m,k)=2knm+D(m,k). These are declared scalar-operation tariffs. They exclude bit complexity, memory traffic, allocation, and physical timing.
Exact mathematical passage
C(n,m,k)=2knm+D(m,k).
LUse in source · 32 passages
Search aliases: L
Use in source · core_chapters.tex, line 136
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
L
lUse in source · 3 passages
Search aliases: l
Use in source · planning_chapters.tex, line 300
[Expected frozen-policy regret] For a horizon H, let J_H^rm lower(s) be the expected value of the complete adaptive policy induced by robust lower-Q selection. Under any compatible realization, 0≤ V_H(s)-J_H^rm lower(s) ≤∑_h=0^H-12Γ_h. The comparator is the true optimal legal adaptive plan with the same conservative reservation guards. Write the regret at a node with h+1 remaining steps as its local Bellman loss plus the expected regret of the selected continuation. The local term is at most 2Γ_…
Exact mathematical passage
J_H^{\rm lower}(s)
L^1Use in source · 2 passages
Search aliases: L^1
Use in source · core_chapters.tex, line 169
[Rare evidence can reverse a posterior completely] Under the uniform prior on {0,1}, take L_0=(ε,0) and L_1=(0,ε) with rational ε>0. The two likelihoods differ pointwise by at most ε, and both evidence masses equal ε/2. Their posteriors are respectively (1,0) and (0,1), with full L^1 distance 2. Arbitrarily small positive likelihood perturbations therefore do not imply uniform pointwise posterior stability without an additional evidence condition. The later model-error chapter uses weighted cont…
Exact mathematical passage
L^1
L_0Use in source · 1 passage
Search aliases: L_0
Use in source · core_chapters.tex, line 169
[Rare evidence can reverse a posterior completely] Under the uniform prior on {0,1}, take L_0=(ε,0) and L_1=(0,ε) with rational ε>0. The two likelihoods differ pointwise by at most ε, and both evidence masses equal ε/2. Their posteriors are respectively (1,0) and (0,1), with full L^1 distance 2. Arbitrarily small positive likelihood perturbations therefore do not imply uniform pointwise posterior stability without an additional evidence condition. The later model-error chapter uses weighted cont…
Exact mathematical passage
L_0=(\varepsilon,0)
L_1Use in source · 4 passages
Search aliases: L_1
Use in source · core_chapters.tex, line 141
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
L_1,L_2
L_2Use in source · 2 passages
Search aliases: L_2
Use in source · core_chapters.tex, line 141
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
L_1,L_2
L_hUse in source · 6 passages
Search aliases: L_h
Use in source · planning_chapters.tex, line 206
|Q_h(s,a)-widehat Q_h(s,a)| · ≤ρ_h(a)≤Γ_h. Thus L_h(s,a)=widehat Q_h(s,a)-ρ_h(a) and U_h(s,a)=widehat Q_h(s,a)+ρ_h(a) enclose the true Q value. At horizon zero the value error is zero. In a single backup, insert and subtract the expectation of the nominal continuation under the true row. The reward error contributes at most ε_a, the continuation-value error at most D_h, and row transport at most δ_a hM. Taking a maximum over the same feasible action set is nonexpansive in the uniform score error…
Exact mathematical passage
L_h(s,a)=\widehat Q_h(s,a)-\rho_h(a)
\landUse in source · 1 passage
Search aliases: land
Use in source · common.tex, line 48
athbb Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\land
\LongrightarrowUse in source · 1 passage
Search aliases: Longrightarrow
Use in source · core_chapters.tex, line 21
[Exact fiber criterion] Suppose Y is nonempty. Then ϕ is sufficient for T if and only if ϕ(x)=ϕ(y) Longrightarrow T(x)=T(y) (x,y∈ X). In particular, a single pair with ϕ(x)=ϕ(y) and T(x)≠ T(y) proves insufficiency. If T=d∘ϕ, equality of the two representations gives equality after applying d. Conversely, fix a default y_0∈ Y. For every reachable z∈ϕ(X) choose x_z with ϕ(x_z)=z and set d(z)=T(x_z). Set d(z)=y_0 on unreachable representation states. The fiber hypothesis ensures that T(x_z)=T(x) wh…
Exact mathematical passage
\phi(x)=\phi(y)\quad\Longrightarrow\quad T(x)=T(y) \qquad(x,y\in X).
\lorUse in source · 1 passage
Search aliases: lor
Use in source · common.tex, line 48
R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\lor
MUse in source · 16 passages
Search aliases: M
Use in source · core_chapters.tex, line 137
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
M_b(L)=\sum_\omega b(\omega)L(\omega),\qquad C_L(b)(\omega)=\frac{b(\omega)L(\omega)}{M_b(L)}
M_0Use in source · 1 passage
Search aliases: M_0
Use in source · core_chapters.tex, line 301
The initial grammar layer has five atoms: two literals and three variables. If a layer is L, expansion retains L, adds all negations, and adds all ordered pairs under each of the three binary operations. Let M_d count emitted list entries at depth d. The source proves M_0=5, M_d+1=2M_d+3M_d^2. The entries can contain duplicates. The node bound is B_0=1, B_d+1=2B_d+1, and every expression of height at most d occurs in the depth-d list. In particular M_1=85 and M_2=21845.
Exact mathematical passage
M_0=5,\qquad M_{d+1}=2M_d+3M_d^2.
M_1Use in source · 1 passage
Search aliases: M_1
Use in source · core_chapters.tex, line 304
is L, expansion retains L, adds all negations, and adds all ordered pairs under each of the three binary operations. Let M_d count emitted list entries at depth d. The source proves M_0=5, M_d+1=2M_d+3M_d^2. The entries can contain duplicates. The node bound is B_0=1, B_d+1=2B_d+1, and every expression of height at most d occurs in the depth-d list. In particular M_1=85 and M_2=21845.
Exact mathematical passage
M_1=85
M_2Use in source · 1 passage
Search aliases: M_2
Use in source · core_chapters.tex, line 304
sion retains L, adds all negations, and adds all ordered pairs under each of the three binary operations. Let M_d count emitted list entries at depth d. The source proves M_0=5, M_d+1=2M_d+3M_d^2. The entries can contain duplicates. The node bound is B_0=1, B_d+1=2B_d+1, and every expression of height at most d occurs in the depth-d list. In particular M_1=85 and M_2=21845.
Exact mathematical passage
M_2=21845
M_bUse in source · 5 passages
Search aliases: M_b
Use in source · core_chapters.tex, line 137
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
M_b(L)=\sum_\omega b(\omega)L(\omega),\qquad C_L(b)(\omega)=\frac{b(\omega)L(\omega)}{M_b(L)}
M_{\bar b}Use in source · 2 passages
Search aliases: M_bar b bar
Use in source · core_chapters.tex, line 158
te spaces, and define the pushforward belief bar b(z)=∑_ϕ(ω)=zb(ω). Suppose L=bar L∘ϕ for a nonnegative likelihood bar L:Z→Q, and the evidence mass is positive. Then ϕ_*C_L(b)=C_bar L(ϕ_*b). Such an exact bar L exists if and only if L is constant on every fiber of ϕ. Grouping the normalizer by fibers gives M_b(L)=M_bar b(bar L). On each fiber ϕ^-1(z), the likelihood can be factored outside the sum. Thus ∑_ϕ(ω)=zfracb(ω)L(ω)M_b(L) =fracbar b(z)bar L(z)M_bar b(bar L). The factorization criterion i…
Exact mathematical passage
M_b(L)=M_{\bar b}(\bar L)
M_{C_{L_1}(b)}Use in source · 1 passage
Search aliases: M_C_L_1(b)
Use in source · core_chapters.tex, line 142
For any nonnegative likelihood weight L, write M_b(L)=∑_ω b(ω)L(ω), C_L(b)(ω)=fracb(ω)L(ω)M_b(L) when M_b(L)>0. Given nonnegative L_1,L_2 and positive successive evidence masses, the source proves M_b(L_1)M_C_L_1(b)(L_2)=M_b(L_1L_2), C_L_2(C_L_1(b))=C_L_1L_2(b). These identities follow by expanding the finite sums and canceling the positive normalizers. Both conditioning orders agree when their respective intermediate masses are positive. Applying this algebra to physical observations requires t…
Exact mathematical passage
M_b(L_1)M_{C_{L_1}(b)}(L_2)=M_b(L_1L_2),\qquad C_{L_2}(C_{L_1}(b))=C_{L_1L_2}(b).
M_dUse in source · 2 passages
Search aliases: M_d
Use in source · core_chapters.tex, line 300
The initial grammar layer has five atoms: two literals and three variables. If a layer is L, expansion retains L, adds all negations, and adds all ordered pairs under each of the three binary operations. Let M_d count emitted list entries at depth d. The source proves M_0=5, M_d+1=2M_d+3M_d^2. The entries can contain duplicates. The node bound is B_0=1, B_d+1=2B_d+1, and every expression of height at most d occurs in the depth-d list. In particular M_1=85 and M_2=21845.
Exact mathematical passage
M_d
M_{d+1}Use in source · 1 passage
Search aliases: M_d+1
Use in source · core_chapters.tex, line 301
The initial grammar layer has five atoms: two literals and three variables. If a layer is L, expansion retains L, adds all negations, and adds all ordered pairs under each of the three binary operations. Let M_d count emitted list entries at depth d. The source proves M_0=5, M_d+1=2M_d+3M_d^2. The entries can contain duplicates. The node bound is B_0=1, B_d+1=2B_d+1, and every expression of height at most d occurs in the depth-d list. In particular M_1=85 and M_2=21845.
Exact mathematical passage
M_0=5,\qquad M_{d+1}=2M_d+3M_d^2.
M_d^2Use in source · 1 passage
Search aliases: M_d^2
Use in source · core_chapters.tex, line 301
The initial grammar layer has five atoms: two literals and three variables. If a layer is L, expansion retains L, adds all negations, and adds all ordered pairs under each of the three binary operations. Let M_d count emitted list entries at depth d. The source proves M_0=5, M_d+1=2M_d+3M_d^2. The entries can contain duplicates. The node bound is B_0=1, B_d+1=2B_d+1, and every expression of height at most d occurs in the depth-d list. In particular M_1=85 and M_2=21845.
Exact mathematical passage
M_0=5,\qquad M_{d+1}=2M_d+3M_d^2.
m_jUse in source · 1 passage
Search aliases: m_j
Use in source · planning_chapters.tex, line 410
A schedule is a finite set J of checkpoints. Each checkpoint fixes an identity stratum, sample size n_j, grid m_j>0, true parameter p_j, and nonnegative error allocation α_j. Its count statistic has the stated binomial marginal. Counts can be dependent, including different prefixes of one source and checkpoints that share other underlying randomness.
Exact mathematical passage
m_j>0
\mathbinUse in source · 1 passage
Search aliases: mathbin
Use in source · core_chapters.tex, line 334
A complete finite semantic algebra supports a stronger conclusion than searching a deeper finite layer. Let D be a semantic domain with interpretations of the Boolean constructors. A cost function c:D→N is a lower certificate if it satisfies the constructor inequalities c(literal b) · ≤1, · c(variable j) · ≤1, c(neg s) · ≤ c(s)+1, · c(smathbin∘t) · ≤ c(s)+c(t)+1 (∘∈{wedge,vee,⊕}).
Exact mathematical passage
c(\text{literal }b)&\le1,& c(\text{variable }j)&\le1,\\ c(\neg s)&\le c(s)+1,& c(s\mathbin{\circ}t)&\le c(s)+c(t)+1 \quad(\circ\in\{\wedge,\vee,\oplus\}).
\max_{a\in A_0}Use in source · 2 passages
Search aliases: max_a∈ A_0 max in
Use in source · core_chapters.tex, line 186
Define the finite-horizon values by V_0(s)=0, Q_n(s,a)=r(s,a)+V_n(f(s,a)), V_n+1(s)=max_a∈ A_0Q_n(s,a).
Exact mathematical passage
V_0(s)=0,\qquad Q_n(s,a)=r(s,a)+V_n(f(s,a)),\qquad V_{n+1}(s)=\max_{a\in A_0}Q_n(s,a).
\minUse in source · 2 passages
Search aliases: min
Use in source · core_chapters.tex, line 464
The menu selector compares three equivalent implementations: the current program, its dense fused atom, and the accepted minimum-width two-stage plan. Its selected tariff is exactly min{cost(p), D(n,m), F(n,m,k)}. This proves a minimum over the explicit menu, and also comparison with every exact two-dense-stage factorization. It does not prove a globally cheapest affine program in the larger language. Sparse schedules, sharing, special primitives, and hardware-specific algorithms have different …
Exact mathematical passage
\min\{\operatorname{cost}(p),\ D(n,m),\ F(n,m,k)\}.
NUse in source · 6 passages
Search aliases: N
Use in source · core_chapters.tex, line 282
Programs are finite abstract syntax trees built from Boolean literals, three input variables, negation, conjunction, disjunction, and exclusive-or. The input domain is the eight triples in {0,1}^3. Let N(p) be the tree-node count: each literal or variable contributes one, negation adds one to its child, and a binary constructor adds one to the sum of its child counts.
Exact mathematical passage
N(p)
\NUse in source · 3 passages
Search aliases: N
Use in source · core_chapters.tex, line 192
[Exact preservation of controlled value] If ϕ is control sufficient, then V_n is constant on every fiber of ϕ for every n∈N. The same is true of Q_n(·,a) for each admissible a, and Bellman-optimal action sets coincide within each fiber. At horizon zero the values vanish. If V_n is fiber constant and ϕ(s)=ϕ(t), control sufficiency gives equal rewards and equal represented successors. Hence Q_n(s,a)=Q_n(t,a) for every admissible a. Taking the maximum over the common action set proves equality of V…
Exact mathematical passage
n\in\N
\mathbb NUse in source · 1 passage
Search aliases: N mathbb
Use in source · common.tex, line 48
,keepspaces=true,showstringspaces=false,backgroundcolor=colorlight,frame=single,rulecolor=colorlight,keywordstyle=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_…
Exact mathematical passage
\mathbb N
n_jUse in source · 3 passages
Search aliases: n_j
Use in source · planning_chapters.tex, line 410
A schedule is a finite set J of checkpoints. Each checkpoint fixes an identity stratum, sample size n_j, grid m_j>0, true parameter p_j, and nonnegative error allocation α_j. Its count statistic has the stated binomial marginal. Counts can be dependent, including different prefixes of one source and checkpoints that share other underlying randomness.
Exact mathematical passage
n_j
N_kUse in source · 1 passage
Search aliases: N_k
Use in source · planning_chapters.tex, line 463
The primitive model uses a finite rational probability space and, for each identity k, a finite latent Boolean vector of length N_k. Its success parameter p_k is fixed. The fresh-outcome contract states that after agreement with any specified pattern on a previously revealed set of positions, a fresh position's joint success mass is p_k times that history mass. In notation, Prob{H matches and X_i=1}=p_kProb{H matches}, i fresh. The multiplication-only form is meaningful for histories of mass zer…
Exact mathematical passage
N_k
\negUse in source · 3 passages
Search aliases: neg
Use in source · common.tex, line 48
ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\neg
\operatorname{normalize}Use in source · 1 passage
Search aliases: normalize operatorname
Use in source · core_chapters.tex, line 386
Typed programs combine affine atoms, identities, sequential composition, and pointwise addition. Composition connects only matching intermediate dimensions. An independent recursive execution semantics and coefficient-normalization semantics are defined. Structural induction proves eval(normalize(p),x)=run(p,x) for all x. Hence two programs are equivalent if and only if their normal signatures coincide. Decidable coefficient comparison is a sound and complete checker when equality in R is decida…
Exact mathematical passage
\operatorname{eval}(\operatorname{normalize}(p),x)=\operatorname{run}(p,x) \qquad\text{for all }x.
pUse in source · 44 passages
Search aliases: p
Use in source · core_chapters.tex, line 123
A rational belief is a nonnegative vector b on finite Ω with ∑_ω b(ω)=1. For a channel E, define the predictive mass p(o)=∑_ω b(ω)E(omidω). For p(o)>0, the posterior is b_o(ω)=b(ω)E(omidω)/p(o). The total updater in the source uses b_o=b when p(o)=0. This fallback is normalized and has zero coefficient in predictive expectations. Nonnegativity of every summand implies that each Bayes numerator also vanishes on such an impossible observation. Hence, with the total-update convention, the division-…
Exact mathematical passage
p(o)=\sum_\omega b(\omega)E(o\mid\omega).
p^kUse in source · 1 passage
Search aliases: p^k
Use in source · planning_chapters.tex, line 343
Let K be the number of successes in n Bernoulli trials with rational parameter p∈[0,1]. Define b_n,k(p)=binom nk p^k(1-p)^n-k, 0≤ k≤ n. Choose a positive integer grid size m and nonnegative rational allowance α. The grid cells have endpoints ℓ_i=fracim, u_i=fraci+1m, 0≤ i<m. For observed count k, the envelope of its point mass over cell i is B_n,k,i=binom nk u_i^k(1-ℓ_i)^n-k. Retain the cell exactly when B_n,k,i>fracαn+1. Return the closed interval spanning all retained cells. If there are no re…
Exact mathematical passage
b_{n,k}(p)=\binom nk p^k(1-p)^{n-k},\qquad 0\leq k\leq n.
p_jUse in source · 2 passages
Search aliases: p_j
Use in source · planning_chapters.tex, line 410
A schedule is a finite set J of checkpoints. Each checkpoint fixes an identity stratum, sample size n_j, grid m_j>0, true parameter p_j, and nonnegative error allocation α_j. Its count statistic has the stated binomial marginal. Counts can be dependent, including different prefixes of one source and checkpoints that share other underlying randomness.
Exact mathematical passage
p_j
p_kUse in source · 4 passages
Search aliases: p_k
Use in source · planning_chapters.tex, line 138
For kind k∈{w,c}, write c_k∈[c_k^-,c_k^+], g_k∈[g_k^-,g_k^+], p_k∈[p_k^-,p_k^+]. The formal nominal model reserves c_k^+, credits g_k^-, and uses p_k^-. A compatible realization supplies exact values inside these bands. In the true comparison system, rewards and report probabilities use those exact values, but the state transitions and action guards remain those of the nominal model. In particular, setup reservations continue to use the upper setup bound.
Exact mathematical passage
c_k\in[c_k^-,c_k^+],\qquad g_k\in[g_k^-,g_k^+],\qquad p_k\in[p_k^-,p_k^+].
p_k^+Use in source · 2 passages
Search aliases: p_k^+
Use in source · planning_chapters.tex, line 138
For kind k∈{w,c}, write c_k∈[c_k^-,c_k^+], g_k∈[g_k^-,g_k^+], p_k∈[p_k^-,p_k^+]. The formal nominal model reserves c_k^+, credits g_k^-, and uses p_k^-. A compatible realization supplies exact values inside these bands. In the true comparison system, rewards and report probabilities use those exact values, but the state transitions and action guards remain those of the nominal model. In particular, setup reservations continue to use the upper setup bound.
Exact mathematical passage
c_k\in[c_k^-,c_k^+],\qquad g_k\in[g_k^-,g_k^+],\qquad p_k\in[p_k^-,p_k^+].
p_k^-Use in source · 3 passages
Search aliases: p_k^-
Use in source · planning_chapters.tex, line 138
For kind k∈{w,c}, write c_k∈[c_k^-,c_k^+], g_k∈[g_k^-,g_k^+], p_k∈[p_k^-,p_k^+]. The formal nominal model reserves c_k^+, credits g_k^-, and uses p_k^-. A compatible realization supplies exact values inside these bands. In the true comparison system, rewards and report probabilities use those exact values, but the state transitions and action guards remain those of the nominal model. In particular, setup reservations continue to use the upper setup bound.
Exact mathematical passage
c_k\in[c_k^-,c_k^+],\qquad g_k\in[g_k^-,g_k^+],\qquad p_k\in[p_k^-,p_k^+].
P_pUse in source · 1 passage
Search aliases: P_p
Use in source · planning_chapters.tex, line 172
[Bernoulli row error and expectation transport] For Bernoulli parameters p,q, ∑_o∈{0,1}|P_p(o)-P_q(o)|=2|p-q|. If |W(t)|≤ B, then replacing an observation row P by widehat P changes its expected continuation by at most |∑_o(P(o)-widehat P(o))W(T(s,a,o))| ≤ B∑_o|P(o)-widehat P(o)|. The two Bernoulli row differences are p-q and q-p, which have equal absolute values. For the second statement, apply the triangle inequality to the finite sum and use the uniform bound on each continuation value.
Exact mathematical passage
\sum_{o\in\{0,1\}}|P_p(o)-P_q(o)|=2|p-q|.
P_qUse in source · 1 passage
Search aliases: P_q
Use in source · planning_chapters.tex, line 172
[Bernoulli row error and expectation transport] For Bernoulli parameters p,q, ∑_o∈{0,1}|P_p(o)-P_q(o)|=2|p-q|. If |W(t)|≤ B, then replacing an observation row P by widehat P changes its expected continuation by at most |∑_o(P(o)-widehat P(o))W(T(s,a,o))| ≤ B∑_o|P(o)-widehat P(o)|. The two Bernoulli row differences are p-q and q-p, which have equal absolute values. For the second statement, apply the triangle inequality to the finite sum and use the uniform bound on each continuation value.
Exact mathematical passage
\sum_{o\in\{0,1\}}|P_p(o)-P_q(o)|=2|p-q|.
\ProbUse in source · 7 passages
Search aliases: Prob
Use in source · introduction.tex, line 29
Writing I for issuance and C for the specified episode certificate, the resulting conclusion is Prob(I∩ C^ c)≤∑_j∈ Jα_j. This is an unconditional probability over the original outcome space. It allows arbitrary dependence between scheduled checkpoints. It retains failed and unfinished runs in that space, with no plan issued on those runs. It does not assert a nominal bound conditional on issuance or completion, eventual issuance, or a productivity lower bound. The final recorder theorem derives …
Exact mathematical passage
\Prob(I\cap C^{\mathsf c})\leq\sum_{j\in J}\alpha_j.
\operatorname{Prop}Use in source · 1 passage
Search aliases: Prop operatorname
Use in source · core_chapters.tex, line 254
The concrete binding layer uses a small data-only propositional language. Formulas contain numbered atoms, truth, falsity, conjunction, disjunction, and implication. Derivations contain the corresponding introduction and elimination rules. Atoms are interpreted as arbitrary propositions under a valuation v:N→Prop. A recursive inference function either returns a formula or rejects. It accepts data representing a derivation, rather than executable tactics or imported source code.
Exact mathematical passage
v:\N\to\operatorname{Prop}
\mathbb QUse in source · 1 passage
Search aliases: Q mathbb
Use in source · common.tex, line 48
wstringspaces=false,backgroundcolor=colorlight,frame=single,rulecolor=colorlight,keywordstyle=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 …
Exact mathematical passage
\mathbb Q
qUse in source · 18 passages
Search aliases: q
Use in source · core_chapters.tex, line 51
Suppose a family of tasks is given by T_q:X→ Y, indexed by q∈ Q. Define the joint target T_joint(x)=(T_q(x))_q∈ Q∈ Y^Q. Then ϕ is sufficient for the joint target if and only if it is sufficient for each individual task. The forward direction evaluates the decoded answer vector at q. For the reverse direction, choose a decoder d_q for each query and define d(z)(q)=d_q(z). The formal theorem permits an arbitrary query index type, and the simultaneous decoder selection uses classical choice.
Exact mathematical passage
T_q:X\to Y
Q_0Use in source · 1 passage
Search aliases: Q_0
Use in source · planning_chapters.tex, line 29
Here h in Q_h counts continuation steps. Choosing an acquisition action and then deploying a successful artifact requires two total actions, so its first-action score is Q_1, not Q_0. This indexing also applies to robustChoice md h s in the formal source.
Exact mathematical passage
Q_0
Q_1Use in source · 2 passages
Search aliases: Q_1
Use in source · planning_chapters.tex, line 29
Here h in Q_h counts continuation steps. Choosing an acquisition action and then deploying a successful artifact requires two total actions, so its first-action score is Q_1, not Q_0. This indexing also applies to robustChoice md h s in the formal source.
Exact mathematical passage
Q_1
Q_nUse in source · 4 passages
Search aliases: Q_n
Use in source · core_chapters.tex, line 186
Define the finite-horizon values by V_0(s)=0, Q_n(s,a)=r(s,a)+V_n(f(s,a)), V_n+1(s)=max_a∈ A_0Q_n(s,a).
Exact mathematical passage
V_0(s)=0,\qquad Q_n(s,a)=r(s,a)+V_n(f(s,a)),\qquad V_{n+1}(s)=\max_{a\in A_0}Q_n(s,a).
\mathbb RUse in source · 1 passage
Search aliases: R mathbb
Use in source · common.tex, line 48
backgroundcolor=colorlight,frame=single,rulecolor=colorlight,keywordstyle=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_4…
Exact mathematical passage
\mathbb R
R^{k\times m}Use in source · 1 passage
Search aliases: R^k× m times
Use in source · core_chapters.tex, line 425
Work over a field R. For reference f=(A,b):R^n→ R^m, a candidate supplies an intermediate width k, first and second affine signatures a(x)=Ux+u_0, d(y)=Vy+v_0, and matrices L∈ R^k× m, H∈ R^n× k. The checker verifies VU=A, Vu_0+v_0=b, LAH=I_k. The first two identities give the exact upper implementation. The third is an independently checkable lower witness. Validation uses polynomial matrix identities; an untrusted rank routine is not part of the logical justification.
Exact mathematical passage
L\in R^{k\times m}
R^nUse in source · 2 passages
Search aliases: R^n
Use in source · core_chapters.tex, line 371
[Complete zero-and-basis probes] Two affine signatures f,g:R^n→ R^m are equal if and only if they agree at 0 and at every standard basis vector e_j. Thus n+1 vector probes establish equality on all inputs. A mismatch in signatures has a mismatch among these probes. The zero probe identifies the offsets because f(0)=b_f. At e_j, the output is the jth matrix column plus the offset. After canceling the now-equal offsets, equality of the basis probes identifies every column. Equal coefficients give …
Exact mathematical passage
f,g:R^n\to R^m
R^{n\times k}Use in source · 1 passage
Search aliases: R^n× k times
Use in source · core_chapters.tex, line 425
Work over a field R. For reference f=(A,b):R^n→ R^m, a candidate supplies an intermediate width k, first and second affine signatures a(x)=Ux+u_0, d(y)=Vy+v_0, and matrices L∈ R^k× m, H∈ R^n× k. The checker verifies VU=A, Vu_0+v_0=b, LAH=I_k. The first two identities give the exact upper implementation. The third is an independently checkable lower witness. Validation uses polynomial matrix identities; an untrusted rank routine is not part of the logical justification.
Exact mathematical passage
H\in R^{n\times k}
\operatorname{rank}Use in source · 4 passages
Search aliases: rank operatorname
Use in source · core_chapters.tex, line 433
[Certified minimum affine width] An accepted candidate has k=rank(A). Every exact two-stage affine factorization of f through width ℓ satisfies k≤ℓ. Under the dense two-stage tariff, F(n,m,k)=D(n,k)+D(k,m), the accepted candidate is no more expensive than any such two-stage factorization. The upper factorization gives rank(A)=rank(VU)≤ k. The lower witness gives k=rank(I_k)=rank(LAH)≤rank(A). Thus rank equals k. Any exact factorization through ℓ has rank(A)≤ℓ, by the same upper rank inequality. …
Exact mathematical passage
k=\operatorname{rank}(A)
\rmUse in source · 3 passages
Search aliases: rm
Use in source · planning_chapters.tex, line 300
[Expected frozen-policy regret] For a horizon H, let J_H^rm lower(s) be the expected value of the complete adaptive policy induced by robust lower-Q selection. Under any compatible realization, 0≤ V_H(s)-J_H^rm lower(s) ≤∑_h=0^H-12Γ_h. The comparator is the true optimal legal adaptive plan with the same conservative reservation guards. Write the regret at a node with h+1 remaining steps as its local Bellman loss plus the expected regret of the selected continuation. The local term is at most 2Γ_…
Exact mathematical passage
J_H^{\rm lower}(s)
\operatorname{run}Use in source · 1 passage
Search aliases: run operatorname
Use in source · core_chapters.tex, line 386
Typed programs combine affine atoms, identities, sequential composition, and pointwise addition. Composition connects only matching intermediate dimensions. An independent recursive execution semantics and coefficient-normalization semantics are defined. Structural induction proves eval(normalize(p),x)=run(p,x) for all x. Hence two programs are equivalent if and only if their normal signatures coincide. Decidable coefficient comparison is a sound and complete checker when equality in R is decida…
Exact mathematical passage
\operatorname{eval}(\operatorname{normalize}(p),x)=\operatorname{run}(p,x) \qquad\text{for all }x.
S_EUse in source · 5 passages
Search aliases: S_E
Use in source · core_chapters.tex, line 95
The unnormalized signal-action score and policy value are S_E(o,a)=∑_ω b(ω)E(omidω)u(ω,a), J_b(E,π)=∑_o S_E(o,π(o)). This form avoids dividing by the evidence mass. In particular, it remains well defined on observations whose predictive probability is zero.
Exact mathematical passage
S_E(o,a)=\sum_\omega b(\omega)E(o\mid\omega)u(\omega,a), \qquad J_b(E,\pi)=\sum_o S_E(o,\pi(o)).
s_zUse in source · 3 passages
Search aliases: s_z
Use in source · core_chapters.tex, line 228
[Exact stochastic quotient] Suppose ϕ:S→ Z is surjective and projected stochastically sufficient, with S,Z finite. Choose a representative s_z of every fiber, and define bar r(z,a)=r(s_z,a), bar P_a(z,z')=∑_ϕ(s')=z'P_a(s_z,s'). These quantities give a normalized rational stochastic control system, independent of the representative choices for admissible actions. For every finite horizon, bar V_n(ϕ(s))=V_n(s). Nonnegative fiber masses give nonnegative quotient probabilities; partitioning S by the…
Exact mathematical passage
s_z
\mathrm{samples}Use in source · 1 passage
Search aliases: samples mathrm
Use in source · planning_chapters.tex, line 554
Every accepted generative step emits an ordinary recorder command and an effective reveal marker. Whole-run induction proves that the emitted commands reproduce the actual raw recorder state and that the reveal state equals the inherited reveal machine on its effective trace. In particular, for every identity, samples_k(terminalLog) =source_k.take (|samples_k(terminalLog)|).
Exact mathematical passage
\mathrm{samples}_k(\mathrm{terminalLog}) =\mathrm{source}_k.\mathrm{take} \bigl(|\mathrm{samples}_k(\mathrm{terminalLog})|\bigr). \label{eq:recorder-prefix}
\mathrm{samples}_kUse in source · 1 passage
Search aliases: samples_k mathrm
Use in source · planning_chapters.tex, line 554
Every accepted generative step emits an ordinary recorder command and an effective reveal marker. Whole-run induction proves that the emitted commands reproduce the actual raw recorder state and that the reveal state equals the inherited reveal machine on its effective trace. In particular, for every identity, samples_k(terminalLog) =source_k.take (|samples_k(terminalLog)|).
Exact mathematical passage
\mathrm{samples}_k(\mathrm{terminalLog}) =\mathrm{source}_k.\mathrm{take} \bigl(|\mathrm{samples}_k(\mathrm{terminalLog})|\bigr). \label{eq:recorder-prefix}
\operatorname{sem}Use in source · 1 passage
Search aliases: sem operatorname
Use in source · core_chapters.tex, line 350
uppose c satisfies those inequalities and, for every semantic state s, a witness expression w_s has semantics s and node count c(s). Then for every expression p with semantics s, N(w_s)=c(s)≤ N(p). No expression-height bound appears in this conclusion. Two such attained cost certificates have identical cost functions. Structural induction proves c(sem(p))≤ N(p). The leaf inequalities give the base cases. For a unary constructor, use its inequality and the child's induction hypothesis. For a bina…
Exact mathematical passage
c(\operatorname{sem}(p))\le N(p)
\mathrm{source}Use in source · 1 passage
Search aliases: source mathrm
Use in source · planning_chapters.tex, line 554
Every accepted generative step emits an ordinary recorder command and an effective reveal marker. Whole-run induction proves that the emitted commands reproduce the actual raw recorder state and that the reveal state equals the inherited reveal machine on its effective trace. In particular, for every identity, samples_k(terminalLog) =source_k.take (|samples_k(terminalLog)|).
Exact mathematical passage
\mathrm{samples}_k(\mathrm{terminalLog}) =\mathrm{source}_k.\mathrm{take} \bigl(|\mathrm{samples}_k(\mathrm{terminalLog})|\bigr). \label{eq:recorder-prefix}
\mathrm{source}_kUse in source · 1 passage
Search aliases: source_k mathrm
Use in source · planning_chapters.tex, line 554
Every accepted generative step emits an ordinary recorder command and an effective reveal marker. Whole-run induction proves that the emitted commands reproduce the actual raw recorder state and that the reveal state equals the inherited reveal machine on its effective trace. In particular, for every identity, samples_k(terminalLog) =source_k.take (|samples_k(terminalLog)|).
Exact mathematical passage
\mathrm{samples}_k(\mathrm{terminalLog}) =\mathrm{source}_k.\mathrm{take} \bigl(|\mathrm{samples}_k(\mathrm{terminalLog})|\bigr). \label{eq:recorder-prefix}
\mathrm{stop}Use in source · 1 passage
Search aliases: stop mathrm
Use in source · planning_chapters.tex, line 262
example assigns zero setup to both kinds, warm gross 200, cold gross 60, warm success band [3/5,1], and exact cold success 1. Start with both statuses untried and use h=1, hence two total actions. The nominal scores are warm 120, cold 60, and stop 0. Here ε=0, δ=4/5, M=260, and D_1=0. The local warm radius is 208, while the cold and stop radii are zero: c|r|r|r action · widehat Q_1 · ρ_1 · L_1 inspectWarm · 120 · 208 · -88 generateCold · 60 · 0 · 60 stop · 0 · 0 · 0 The lower-Q rule chooses cold…
Exact mathematical passage
\begin{array}{c|r|r|r} \text{action}&\widehat Q_1&\rho_1&L_1\\\hline \mathrm{inspectWarm}&120&208&-88\\ \mathrm{generateCold}&60&0&60\\ \mathrm{stop}&0&0&0 \end{array}
\mathrm{switchSpent}Use in source · 1 passage
Search aliases: switchSpent mathrm
Use in source · planning_chapters.tex, line 788
For a successful paid trace with total evaluation debit e and switching debit u, the formal accounting identities are evaluationSpent_rm final · =evaluationSpent_rm initial+e, switchSpent_rm final · =switchSpent_rm initial+u. From a safe initial journal, their sum stays within protected credits. Successful replay also cannot decrease the protected utility of the active version. These are pathpaid_trace_exact_accounting, pathpaid_trace_no_overspend, and pathreplay_utility_nondecreasing in pathAVO…
Exact mathematical passage
\mathrm{evaluationSpent}_{\rm final} &=\mathrm{evaluationSpent}_{\rm initial}+e,\\ \mathrm{switchSpent}_{\rm final} &=\mathrm{switchSpent}_{\rm initial}+u.
\mathrm{switchSpent}_{\rm final}Use in source · 1 passage
Search aliases: switchSpent_rm final mathrm rm
Use in source · planning_chapters.tex, line 788
For a successful paid trace with total evaluation debit e and switching debit u, the formal accounting identities are evaluationSpent_rm final · =evaluationSpent_rm initial+e, switchSpent_rm final · =switchSpent_rm initial+u. From a safe initial journal, their sum stays within protected credits. Successful replay also cannot decrease the protected utility of the active version. These are pathpaid_trace_exact_accounting, pathpaid_trace_no_overspend, and pathreplay_utility_nondecreasing in pathAVO…
Exact mathematical passage
\mathrm{evaluationSpent}_{\rm final} &=\mathrm{evaluationSpent}_{\rm initial}+e,\\ \mathrm{switchSpent}_{\rm final} &=\mathrm{switchSpent}_{\rm initial}+u.
\mathrm{switchSpent}_{\rm initial}Use in source · 1 passage
Search aliases: switchSpent_rm initial mathrm rm
Use in source · planning_chapters.tex, line 788
For a successful paid trace with total evaluation debit e and switching debit u, the formal accounting identities are evaluationSpent_rm final · =evaluationSpent_rm initial+e, switchSpent_rm final · =switchSpent_rm initial+u. From a safe initial journal, their sum stays within protected credits. Successful replay also cannot decrease the protected utility of the active version. These are pathpaid_trace_exact_accounting, pathpaid_trace_no_overspend, and pathreplay_utility_nondecreasing in pathAVO…
Exact mathematical passage
\mathrm{evaluationSpent}_{\rm final} &=\mathrm{evaluationSpent}_{\rm initial}+e,\\ \mathrm{switchSpent}_{\rm final} &=\mathrm{switchSpent}_{\rm initial}+u.
T_{\mathrm{joint}}Use in source · 1 passage
Search aliases: T_joint mathrm
Use in source · core_chapters.tex, line 52
Suppose a family of tasks is given by T_q:X→ Y, indexed by q∈ Q. Define the joint target T_joint(x)=(T_q(x))_q∈ Q∈ Y^Q. Then ϕ is sufficient for the joint target if and only if it is sufficient for each individual task. The forward direction evaluates the decoded answer vector at q. For the reverse direction, choose a decoder d_q for each query and define d(z)(q)=d_q(z). The formal theorem permits an arbitrary query index type, and the simultaneous decoder selection uses classical choice.
Exact mathematical passage
T_{\mathrm{joint}}(x)=(T_q(x))_{q\in Q}\in Y^Q.
T_qUse in source · 2 passages
Search aliases: T_q
Use in source · core_chapters.tex, line 51
Suppose a family of tasks is given by T_q:X→ Y, indexed by q∈ Q. Define the joint target T_joint(x)=(T_q(x))_q∈ Q∈ Y^Q. Then ϕ is sufficient for the joint target if and only if it is sufficient for each individual task. The forward direction evaluates the decoded answer vector at q. For the reverse direction, choose a decoder d_q for each query and define d(z)(q)=d_q(z). The formal theorem permits an arbitrary query index type, and the simultaneous decoder selection uses classical choice.
Exact mathematical passage
T_q:X\to Y
\mathrm{take}Use in source · 1 passage
Search aliases: take mathrm
Use in source · planning_chapters.tex, line 554
Every accepted generative step emits an ordinary recorder command and an effective reveal marker. Whole-run induction proves that the emitted commands reproduce the actual raw recorder state and that the reveal state equals the inherited reveal machine on its effective trace. In particular, for every identity, samples_k(terminalLog) =source_k.take (|samples_k(terminalLog)|).
Exact mathematical passage
\mathrm{samples}_k(\mathrm{terminalLog}) =\mathrm{source}_k.\mathrm{take} \bigl(|\mathrm{samples}_k(\mathrm{terminalLog})|\bigr). \label{eq:recorder-prefix}
\mathrm{terminalLog}Use in source · 1 passage
Search aliases: terminalLog mathrm
Use in source · planning_chapters.tex, line 554
Every accepted generative step emits an ordinary recorder command and an effective reveal marker. Whole-run induction proves that the emitted commands reproduce the actual raw recorder state and that the reveal state equals the inherited reveal machine on its effective trace. In particular, for every identity, samples_k(terminalLog) =source_k.take (|samples_k(terminalLog)|).
Exact mathematical passage
\mathrm{samples}_k(\mathrm{terminalLog}) =\mathrm{source}_k.\mathrm{take} \bigl(|\mathrm{samples}_k(\mathrm{terminalLog})|\bigr). \label{eq:recorder-prefix}
\trianglerightUse in source · 1 passage
Search aliases: triangleright
Use in source · common.tex, line 48
λ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\triangleright
\mathrm{true}Use in source · 3 passages
Search aliases: true mathrm
Use in source · planning_chapters.tex, line 569
[Replay and faults do not create new evidence] Let an identity's source be [true,false]. Begin ID 7, report ID 7, then report ID 7 again. The sample list is [true] and the remaining source begins with false. Begin ID 8 and finish it as a fault. The sample list stays unchanged. Begin and report ID 9. It appends false, yielding [true,false]. A further fresh report rejects after source exhaustion, while a replay of ID 7 remains possible. The replay supplies no extra success and the fault supplies n…
Exact mathematical passage
[\mathrm{true},\mathrm{false}]
UUse in source · 9 passages
Search aliases: U
Use in source · core_chapters.tex, line 422
Work over a field R. For reference f=(A,b):R^n→ R^m, a candidate supplies an intermediate width k, first and second affine signatures a(x)=Ux+u_0, d(y)=Vy+v_0, and matrices L∈ R^k× m, H∈ R^n× k. The checker verifies VU=A, Vu_0+v_0=b, LAH=I_k. The first two identities give the exact upper implementation. The third is an independently checkable lower witness. Validation uses polynomial matrix identities; an untrusted rank routine is not part of the logical justification.
Exact mathematical passage
a(x)=Ux+u_0,\qquad d(y)=Vy+v_0,
u_0Use in source · 5 passages
Search aliases: u_0
Use in source · core_chapters.tex, line 422
Work over a field R. For reference f=(A,b):R^n→ R^m, a candidate supplies an intermediate width k, first and second affine signatures a(x)=Ux+u_0, d(y)=Vy+v_0, and matrices L∈ R^k× m, H∈ R^n× k. The checker verifies VU=A, Vu_0+v_0=b, LAH=I_k. The first two identities give the exact upper implementation. The third is an independently checkable lower witness. Validation uses polynomial matrix identities; an untrusted rank routine is not part of the logical justification.
Exact mathematical passage
a(x)=Ux+u_0,\qquad d(y)=Vy+v_0,
U_hUse in source · 4 passages
Search aliases: U_h
Use in source · planning_chapters.tex, line 207
|Q_h(s,a)-widehat Q_h(s,a)| · ≤ρ_h(a)≤Γ_h. Thus L_h(s,a)=widehat Q_h(s,a)-ρ_h(a) and U_h(s,a)=widehat Q_h(s,a)+ρ_h(a) enclose the true Q value. At horizon zero the value error is zero. In a single backup, insert and subtract the expectation of the nominal continuation under the true row. The reward error contributes at most ε_a, the continuation-value error at most D_h, and row transport at most δ_a hM. Taking a maximum over the same feasible action set is nonexpansive in the uniform score error…
Exact mathematical passage
U_h(s,a)=\widehat Q_h(s,a)+\rho_h(a)
u_iUse in source · 2 passages
Search aliases: u_i
Use in source · planning_chapters.tex, line 348
Let K be the number of successes in n Bernoulli trials with rational parameter p∈[0,1]. Define b_n,k(p)=binom nk p^k(1-p)^n-k, 0≤ k≤ n. Choose a positive integer grid size m and nonnegative rational allowance α. The grid cells have endpoints ℓ_i=fracim, u_i=fraci+1m, 0≤ i<m. For observed count k, the envelope of its point mass over cell i is B_n,k,i=binom nk u_i^k(1-ℓ_i)^n-k. Retain the cell exactly when B_n,k,i>fracαn+1. Return the closed interval spanning all retained cells. If there are no re…
Exact mathematical passage
\ell_i=\frac{i}{m},\qquad u_i=\frac{i+1}{m},\qquad 0\leq i<m.
u_i^kUse in source · 1 passage
Search aliases: u_i^k
Use in source · planning_chapters.tex, line 352
uccesses in n Bernoulli trials with rational parameter p∈[0,1]. Define b_n,k(p)=binom nk p^k(1-p)^n-k, 0≤ k≤ n. Choose a positive integer grid size m and nonnegative rational allowance α. The grid cells have endpoints ℓ_i=fracim, u_i=fraci+1m, 0≤ i<m. For observed count k, the envelope of its point mass over cell i is B_n,k,i=binom nk u_i^k(1-ℓ_i)^n-k. Retain the cell exactly when B_n,k,i>fracαn+1. Return the closed interval spanning all retained cells. If there are no retained cells, return [0,…
Exact mathematical passage
B_{n,k,i}=\binom nk u_i^k(1-\ell_i)^{n-k}.
\uparrowUse in source · 1 passage
Search aliases: uparrow
Use in source · common.tex, line 48
ma1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\uparrow
vUse in source · 5 passages
Search aliases: v
Use in source · core_chapters.tex, line 254
The concrete binding layer uses a small data-only propositional language. Formulas contain numbered atoms, truth, falsity, conjunction, disjunction, and implication. Derivations contain the corresponding introduction and elimination rules. Atoms are interpreted as arbitrary propositions under a valuation v:N→Prop. A recursive inference function either returns a formula or rejects. It accepts data representing a derivation, rather than executable tactics or imported source code.
Exact mathematical passage
v:\N\to\operatorname{Prop}
v_0Use in source · 2 passages
Search aliases: v_0
Use in source · core_chapters.tex, line 422
Work over a field R. For reference f=(A,b):R^n→ R^m, a candidate supplies an intermediate width k, first and second affine signatures a(x)=Ux+u_0, d(y)=Vy+v_0, and matrices L∈ R^k× m, H∈ R^n× k. The checker verifies VU=A, Vu_0+v_0=b, LAH=I_k. The first two identities give the exact upper implementation. The third is an independently checkable lower witness. Validation uses polynomial matrix identities; an untrusted rank routine is not part of the logical justification.
Exact mathematical passage
a(x)=Ux+u_0,\qquad d(y)=Vy+v_0,
v_0'Use in source · 2 passages
Search aliases: v_0'
Use in source · core_chapters.tex, line 472
Suppose a stored candidate has been validated for (A,b) and a later target is (A,b') with exactly the same linear matrix. Keep U,u_0,V,L,H and replace only the second-stage offset by v_0'=b'-Vu_0. Then VU=A is unchanged, Vu_0+v_0'=b', and LAH=I_k remains true. The same width and two-stage tariff are retained. A second retargeting overwrites the offset rather than accumulating prior offset changes.
Exact mathematical passage
v_0'=b'-Vu_0.
V_HUse in source · 4 passages
Search aliases: V_H
Use in source · planning_chapters.tex, line 40
[Optimality over complete adaptive plans] Every horizon H has a legal deterministic observation tree attaining V_H(s). Every other legal deterministic observation tree has value at most V_H(s). If each admissible transition preserves an invariant, the attaining tree preserves that invariant on every branch. At horizon zero, the empty tree has value zero. At horizon h+1, choose an action attaining the finite maximum in [source reference]; after each observation, attach an optimal horizon-h tree a…
Exact mathematical passage
V_H(s)
V_nUse in source · 6 passages
Search aliases: V_n
Use in source · core_chapters.tex, line 186
Define the finite-horizon values by V_0(s)=0, Q_n(s,a)=r(s,a)+V_n(f(s,a)), V_n+1(s)=max_a∈ A_0Q_n(s,a).
Exact mathematical passage
V_0(s)=0,\qquad Q_n(s,a)=r(s,a)+V_n(f(s,a)),\qquad V_{n+1}(s)=\max_{a\in A_0}Q_n(s,a).
V_{n+1}Use in source · 3 passages
Search aliases: V_n+1
Use in source · core_chapters.tex, line 186
Define the finite-horizon values by V_0(s)=0, Q_n(s,a)=r(s,a)+V_n(f(s,a)), V_n+1(s)=max_a∈ A_0Q_n(s,a).
Exact mathematical passage
V_0(s)=0,\qquad Q_n(s,a)=r(s,a)+V_n(f(s,a)),\qquad V_{n+1}(s)=\max_{a\in A_0}Q_n(s,a).
\veeUse in source · 2 passages
Search aliases: vee
Use in source · core_chapters.tex, line 315
[A smaller artifact need not repay its discovery] The reference neg(neg x_1veeneg x_2) has six nodes. The equivalent conjunction x_1wedge x_2 has three. The archived depth-one search examines the complete 85-entry layer under its stated limits and returns the conjunction, with modeled search charge 6890. Each eager evaluation subsequently saves three visits. A large deployment can repay the exploration cost; a single evaluation cannot. The synthesis theorem supplies semantic safety and a budget …
Exact mathematical passage
\neg(\neg x_1\vee\neg x_2)
wUse in source · 12 passages
Search aliases: w
Use in source · core_chapters.tex, line 343
[Attained global semantic minimum] Suppose c satisfies those inequalities and, for every semantic state s, a witness expression w_s has semantics s and node count c(s). Then for every expression p with semantics s, N(w_s)=c(s)≤ N(p). No expression-height bound appears in this conclusion. Two such attained cost certificates have identical cost functions. Structural induction proves c(sem(p))≤ N(p). The leaf inequalities give the base cases. For a unary constructor, use its inequality and the chil…
Exact mathematical passage
w_s
w_cUse in source · 3 passages
Search aliases: w_c
Use in source · planning_chapters.tex, line 157
Let w_c(k)=c_k^+-c_k^-, w_g(k)=g_k^+-g_k^-, and w_p(k)=p_k^+-p_k^-. The source uses the uniform quantities ε · =w_c(w)+w_c(c)+w_g(w)+w_g(c),
Exact mathematical passage
w_c(k)=c_k^+-c_k^-
w_gUse in source · 3 passages
Search aliases: w_g
Use in source · planning_chapters.tex, line 157
Let w_c(k)=c_k^+-c_k^-, w_g(k)=g_k^+-g_k^-, and w_p(k)=p_k^+-p_k^-. The source uses the uniform quantities ε · =w_c(w)+w_c(c)+w_g(w)+w_g(c),
Exact mathematical passage
w_g(k)=g_k^+-g_k^-
w_pUse in source · 3 passages
Search aliases: w_p
Use in source · planning_chapters.tex, line 158
Let w_c(k)=c_k^+-c_k^-, w_g(k)=g_k^+-g_k^-, and w_p(k)=p_k^+-p_k^-. The source uses the uniform quantities ε · =w_c(w)+w_c(c)+w_g(w)+w_g(c),
Exact mathematical passage
w_p(k)=p_k^+-p_k^-
w_sUse in source · 2 passages
Search aliases: w_s
Use in source · core_chapters.tex, line 343
[Attained global semantic minimum] Suppose c satisfies those inequalities and, for every semantic state s, a witness expression w_s has semantics s and node count c(s). Then for every expression p with semantics s, N(w_s)=c(s)≤ N(p). No expression-height bound appears in this conclusion. Two such attained cost certificates have identical cost functions. Structural induction proves c(sem(p))≤ N(p). The leaf inequalities give the base cases. For a unary constructor, use its inequality and the chil…
Exact mathematical passage
w_s
\wedgeUse in source · 3 passages
Search aliases: wedge
Use in source · core_chapters.tex, line 46
[A task must be declared before compression] Let X={0,1}^3 and let T(x_1,x_2,x_3)=x_1wedge x_2. The representation ϕ(x)=T(x) is sufficient for this target, although it discards x_3 and many distinctions among the first two coordinates. The representation ψ(x)=x_1⊕ x_2 is insufficient: (0,0,0) and (1,1,0) have the same ψ value and different T values. No decoder can repair this collision. Conversely, retaining all three coordinates refines T but retains more information than this task requires.
Exact mathematical passage
T(x_1,x_2,x_3)=x_1\wedge x_2
\widehat PUse in source · 2 passages
Search aliases: widehat P widehat
Use in source · planning_chapters.tex, line 175
[Bernoulli row error and expectation transport] For Bernoulli parameters p,q, ∑_o∈{0,1}|P_p(o)-P_q(o)|=2|p-q|. If |W(t)|≤ B, then replacing an observation row P by widehat P changes its expected continuation by at most |∑_o(P(o)-widehat P(o))W(T(s,a,o))| ≤ B∑_o|P(o)-widehat P(o)|. The two Bernoulli row differences are p-q and q-p, which have equal absolute values. For the second statement, apply the triangle inequality to the finite sum and use the uniform bound on each continuation value.
Exact mathematical passage
\widehat P
\widehat QUse in source · 4 passages
Search aliases: widehat Q widehat
Use in source · planning_chapters.tex, line 202
[Value and Q enclosures] For every compatible realization, every state, and every continuation horizon, |V_h(s)-widehat V_h(s)| · ≤ D_h, |Q_h(s,a)-widehat Q_h(s,a)| · ≤ρ_h(a)≤Γ_h. Thus L_h(s,a)=widehat Q_h(s,a)-ρ_h(a) and U_h(s,a)=widehat Q_h(s,a)+ρ_h(a) enclose the true Q value. At horizon zero the value error is zero. In a single backup, insert and subtract the expectation of the nominal continuation under the true row. The reward error contributes at most ε_a, the continuation-value error at …
Exact mathematical passage
|V_h(s)-\widehat V_h(s)|&\leq D_h,\\ |Q_h(s,a)-\widehat Q_h(s,a)|&\leq\rho_h(a)\leq\Gamma_h.
\widehat Q_1Use in source · 1 passage
Search aliases: widehat Q_1 widehat
Use in source · planning_chapters.tex, line 262
example assigns zero setup to both kinds, warm gross 200, cold gross 60, warm success band [3/5,1], and exact cold success 1. Start with both statuses untried and use h=1, hence two total actions. The nominal scores are warm 120, cold 60, and stop 0. Here ε=0, δ=4/5, M=260, and D_1=0. The local warm radius is 208, while the cold and stop radii are zero: c|r|r|r action · widehat Q_1 · ρ_1 · L_1 inspectWarm · 120 · 208 · -88 generateCold · 60 · 0 · 60 stop · 0 · 0 · 0 The lower-Q rule chooses cold…
Exact mathematical passage
\begin{array}{c|r|r|r} \text{action}&\widehat Q_1&\rho_1&L_1\\\hline \mathrm{inspectWarm}&120&208&-88\\ \mathrm{generateCold}&60&0&60\\ \mathrm{stop}&0&0&0 \end{array}
\widehat Q_hUse in source · 3 passages
Search aliases: widehat Q_h widehat
Use in source · planning_chapters.tex, line 202
[Value and Q enclosures] For every compatible realization, every state, and every continuation horizon, |V_h(s)-widehat V_h(s)| · ≤ D_h, |Q_h(s,a)-widehat Q_h(s,a)| · ≤ρ_h(a)≤Γ_h. Thus L_h(s,a)=widehat Q_h(s,a)-ρ_h(a) and U_h(s,a)=widehat Q_h(s,a)+ρ_h(a) enclose the true Q value. At horizon zero the value error is zero. In a single backup, insert and subtract the expectation of the nominal continuation under the true row. The reward error contributes at most ε_a, the continuation-value error at …
Exact mathematical passage
|V_h(s)-\widehat V_h(s)|&\leq D_h,\\ |Q_h(s,a)-\widehat Q_h(s,a)|&\leq\rho_h(a)\leq\Gamma_h.
\widehat VUse in source · 2 passages
Search aliases: widehat V widehat
Use in source · planning_chapters.tex, line 188
Induction on the Bellman recursion gives |widehat V_h(s)|≤ hM for the nominal value. The source's accumulated value radius and local Q radius are D_h · =∑_j=0^h-1(ε+δ jM),
Exact mathematical passage
|\widehat V_h(s)|\leq hM
\widehat V_hUse in source · 2 passages
Search aliases: widehat V_h widehat
Use in source · planning_chapters.tex, line 188
Induction on the Bellman recursion gives |widehat V_h(s)|≤ hM for the nominal value. The source's accumulated value radius and local Q radius are D_h · =∑_j=0^h-1(ε+δ jM),
Exact mathematical passage
|\widehat V_h(s)|\leq hM
X_1Use in source · 4 passages
Search aliases: X_1
Use in source · planning_chapters.tex, line 651
[Predictable availability still biases completed runs] Let (X_1,X_2) be independent fair bits. Reveal X_1, and reveal X_2 by the deadline only if X_1=1. Availability of the second report depends on the past, not on X_2. Completion probability is 1/2. Conditional on completion, X_1=1 with probability one, and the two-bit count has probability zero of being zero. A genuine two-trial binomial count with parameter 1/2 has zero count probability 1/4.
Exact mathematical passage
(X_1,X_2)
x_1Use in source · 5 passages
Search aliases: x_1
Use in source · core_chapters.tex, line 46
[A task must be declared before compression] Let X={0,1}^3 and let T(x_1,x_2,x_3)=x_1wedge x_2. The representation ϕ(x)=T(x) is sufficient for this target, although it discards x_3 and many distinctions among the first two coordinates. The representation ψ(x)=x_1⊕ x_2 is insufficient: (0,0,0) and (1,1,0) have the same ψ value and different T values. No decoder can repair this collision. Conversely, retaining all three coordinates refines T but retains more information than this task requires.
Exact mathematical passage
T(x_1,x_2,x_3)=x_1\wedge x_2
X_2Use in source · 3 passages
Search aliases: X_2
Use in source · planning_chapters.tex, line 651
[Predictable availability still biases completed runs] Let (X_1,X_2) be independent fair bits. Reveal X_1, and reveal X_2 by the deadline only if X_1=1. Availability of the second report depends on the past, not on X_2. Completion probability is 1/2. Conditional on completion, X_1=1 with probability one, and the two-bit count has probability zero of being zero. A genuine two-trial binomial count with parameter 1/2 has zero count probability 1/4.
Exact mathematical passage
(X_1,X_2)
x_2Use in source · 5 passages
Search aliases: x_2
Use in source · core_chapters.tex, line 46
[A task must be declared before compression] Let X={0,1}^3 and let T(x_1,x_2,x_3)=x_1wedge x_2. The representation ϕ(x)=T(x) is sufficient for this target, although it discards x_3 and many distinctions among the first two coordinates. The representation ψ(x)=x_1⊕ x_2 is insufficient: (0,0,0) and (1,1,0) have the same ψ value and different T values. No decoder can repair this collision. Conversely, retaining all three coordinates refines T but retains more information than this task requires.
Exact mathematical passage
T(x_1,x_2,x_3)=x_1\wedge x_2
x_3Use in source · 3 passages
Search aliases: x_3
Use in source · core_chapters.tex, line 46
[A task must be declared before compression] Let X={0,1}^3 and let T(x_1,x_2,x_3)=x_1wedge x_2. The representation ϕ(x)=T(x) is sufficient for this target, although it discards x_3 and many distinctions among the first two coordinates. The representation ψ(x)=x_1⊕ x_2 is insufficient: (0,0,0) and (1,1,0) have the same ψ value and different T values. No decoder can repair this collision. Conversely, retaining all three coordinates refines T but retains more information than this task requires.
Exact mathematical passage
T(x_1,x_2,x_3)=x_1\wedge x_2
x_4Use in source · 1 passage
Search aliases: x_4
Use in source · core_chapters.tex, line 454
[A checked rank-one bottleneck] In the archived finite-field example over F_5, A is the 4×4 all-ones matrix and b=(1,2,3,4). The first stage computes y=x_1+x_2+x_3+x_4. The second emits (y+1,y+2,y+3,y+4). Taking L to select the first output coordinate and H to select the first input coordinate gives LAH=(1). The width-one factorization is therefore exact and width minimal.
Exact mathematical passage
y=x_1+x_2+x_3+x_4
X_iUse in source · 1 passage
Search aliases: X_i
Use in source · planning_chapters.tex, line 467
The primitive model uses a finite rational probability space and, for each identity k, a finite latent Boolean vector of length N_k. Its success parameter p_k is fixed. The fresh-outcome contract states that after agreement with any specified pattern on a previously revealed set of positions, a fresh position's joint success mass is p_k times that history mass. In notation, Prob{H matches and X_i=1}=p_kProb{H matches}, i fresh. The multiplication-only form is meaningful for histories of mass zer…
Exact mathematical passage
\Prob\{H\text{ matches and }X_i=1\}=p_k\Prob\{H\text{ matches}\}, \qquad i\text{ fresh}.
x_zUse in source · 4 passages
Search aliases: x_z
Use in source · core_chapters.tex, line 28
fficient for T if and only if ϕ(x)=ϕ(y) Longrightarrow T(x)=T(y) (x,y∈ X). In particular, a single pair with ϕ(x)=ϕ(y) and T(x)≠ T(y) proves insufficiency. If T=d∘ϕ, equality of the two representations gives equality after applying d. Conversely, fix a default y_0∈ Y. For every reachable z∈ϕ(X) choose x_z with ϕ(x_z)=z and set d(z)=T(x_z). Set d(z)=y_0 on unreachable representation states. The fiber hypothesis ensures that T(x_z)=T(x) whenever z=ϕ(x), so d(ϕ(x))=T(x). The nonempty-codomain hypot…
Exact mathematical passage
x_z
Y^QUse in source · 1 passage
Search aliases: Y^Q
Use in source · core_chapters.tex, line 52
Suppose a family of tasks is given by T_q:X→ Y, indexed by q∈ Q. Define the joint target T_joint(x)=(T_q(x))_q∈ Q∈ Y^Q. Then ϕ is sufficient for the joint target if and only if it is sufficient for each individual task. The forward direction evaluates the decoded answer vector at q. For the reverse direction, choose a decoder d_q for each query and define d(z)(q)=d_q(z). The formal theorem permits an arbitrary query index type, and the simultaneous decoder selection uses classical choice.
Exact mathematical passage
T_{\mathrm{joint}}(x)=(T_q(x))_{q\in Q}\in Y^Q.
y_0Use in source · 2 passages
Search aliases: y_0
Use in source · core_chapters.tex, line 28
criterion Suppose Y is nonempty. Then ϕ is sufficient for T if and only if ϕ(x)=ϕ(y) Longrightarrow T(x)=T(y) (x,y∈ X). In particular, a single pair with ϕ(x)=ϕ(y) and T(x)≠ T(y) proves insufficiency. If T=d∘ϕ, equality of the two representations gives equality after applying d. Conversely, fix a default y_0∈ Y. For every reachable z∈ϕ(X) choose x_z with ϕ(x_z)=z and set d(z)=T(x_z). Set d(z)=y_0 on unreachable representation states. The fiber hypothesis ensures that T(x_z)=T(x) whenever z=ϕ(x),…
Exact mathematical passage
y_0\in Y
\mathbb ZUse in source · 1 passage
Search aliases: Z mathbb
Use in source · common.tex, line 48
orlight,frame=single,rulecolor=colorlight,keywordstyle=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆…
Exact mathematical passage
\mathbb Z
zUse in source · 16 passages
Search aliases: z
Use in source · core_chapters.tex, line 28
ty. Then ϕ is sufficient for T if and only if ϕ(x)=ϕ(y) Longrightarrow T(x)=T(y) (x,y∈ X). In particular, a single pair with ϕ(x)=ϕ(y) and T(x)≠ T(y) proves insufficiency. If T=d∘ϕ, equality of the two representations gives equality after applying d. Conversely, fix a default y_0∈ Y. For every reachable z∈ϕ(X) choose x_z with ϕ(x_z)=z and set d(z)=T(x_z). Set d(z)=y_0 on unreachable representation states. The fiber hypothesis ensures that T(x_z)=T(x) whenever z=ϕ(x), so d(ϕ(x))=T(x). The nonempt…
Exact mathematical passage
z\in\phi(X)
z'Use in source · 3 passages
Search aliases: z'
Use in source · core_chapters.tex, line 222
When Z is finite, this expectation condition is equivalent to equality of the mass sent to every abstract fiber: ∑_ϕ(s')=z'P_a(s,s')=∑_ϕ(s')=z'P_a(t,s') (z'∈ Z). To prove necessity, use the indicator of the fiber as W. To prove sufficiency, group the expectation by fibers and factor out the common value of W on each nonempty fiber. Empty fibers contribute zero. These arguments explain why raw states may have distinct next-state probabilities while having identical controlled abstract behavior.
Exact mathematical passage
\sum_{\phi(s')=z'}P_a(s,s')=\sum_{\phi(s')=z'}P_a(t,s')\qquad(z'\in Z).
\cdotUse in source · 3 passages
Search aliases: · cdot
Use in source · common.tex, line 42
[2]textcolorteal#1 #2 newcommandfig[3][H]centeringincludegraphics[width=linewidth]#1caption#2 graphicspath../figures/figures/ pagestylefancyfancyhf fancyhead[L]smalltextcolornavyAVOC / Certified artifact planning fancyhead[R]smallPublication edition fancyfoot[L]small Komorebi P. · 7 October 2026 fancyfoot[R]smallthepage / pagerefLastPage renewcommand0.3pt0.3pt hypersetuppdfauthor=Komorebi P.,pdftitle=AVOC: Certified Artifact Planning, Calibration, and Recoverable Execution,pdfsubject=Publication…
Exact mathematical passage
\cdot
\alphaUse in source · 15 passages
Search aliases: α alpha
Use in source · common.tex, line 48
orlight,keywordstyle=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 …
Exact mathematical passage
\alpha
\alpha_jUse in source · 7 passages
Search aliases: α_j alpha
Use in source · introduction.tex, line 29
Writing I for issuance and C for the specified episode certificate, the resulting conclusion is Prob(I∩ C^ c)≤∑_j∈ Jα_j. This is an unconditional probability over the original outcome space. It allows arbitrary dependence between scheduled checkpoints. It retains failed and unfinished runs in that space, with no plan issued on those runs. It does not assert a nominal bound conditional on issuance or completion, eventual issuance, or a productivity lower bound. The final recorder theorem derives …
Exact mathematical passage
\Prob(I\cap C^{\mathsf c})\leq\sum_{j\in J}\alpha_j.
\betaUse in source · 1 passage
Search aliases: β beta
Use in source · common.tex, line 48
style=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 ls…
Exact mathematical passage
\beta
\GammaUse in source · 10 passages
Search aliases: Γ Gamma
Use in source · common.tex, line 48
e1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning…
Exact mathematical passage
\Gamma
\Gamma_hUse in source · 5 passages
Search aliases: Γ_h Gamma
Use in source · planning_chapters.tex, line 190
Induction on the Bellman recursion gives |widehat V_h(s)|≤ hM for the nominal value. The source's accumulated value radius and local Q radius are D_h · =∑_j=0^h-1(ε+δ jM), ρ_h(a) · =D_h+ε_a+δ_a hM, Γ_h · =D_h+ε+δ hM. The Bellman residual is zero here because the nominal tables are exact Bellman values. The broader model-error framework also allows a supplied table with a proved nonzero residual, but no residual term is silently introduced in these quote results.
Exact mathematical passage
D_h&=\sum_{j=0}^{h-1}(\varepsilon+\delta jM),\label{eq:value-radius}\\ \rho_h(a)&=D_h+\varepsilon_a+\delta_a hM,\label{eq:local-radius}\\ \Gamma_h&=D_h+\varepsilon+\delta hM.\label{eq:global-radius}
\Gamma_jUse in source · 1 passage
Search aliases: Γ_j Gamma
Use in source · planning_chapters.tex, line 314
leq∑_h=0^H-12Γ_h. The comparator is the true optimal legal adaptive plan with the same conservative reservation guards. Write the regret at a node with h+1 remaining steps as its local Bellman loss plus the expected regret of the selected continuation. The local term is at most 2Γ_h. By induction, every child regret is bounded by the common sum ∑_j<h2Γ_j. Taking the expectation leaves that constant unchanged because probabilities sum to one. This yields the cumulative upper bound. Nonnegativity …
Exact mathematical passage
\sum_{j<h}2\Gamma_j
\deltaUse in source · 7 passages
Search aliases: δ delta
Use in source · common.tex, line 48
colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommand…
Exact mathematical passage
\delta
\delta_aUse in source · 2 passages
Search aliases: δ_a delta
Use in source · planning_chapters.tex, line 190
Induction on the Bellman recursion gives |widehat V_h(s)|≤ hM for the nominal value. The source's accumulated value radius and local Q radius are D_h · =∑_j=0^h-1(ε+δ jM), ρ_h(a) · =D_h+ε_a+δ_a hM, Γ_h · =D_h+ε+δ hM. The Bellman residual is zero here because the nominal tables are exact Bellman values. The broader model-error framework also allows a supplied table with a proved nonzero residual, but no residual term is silently introduced in these quote results.
Exact mathematical passage
D_h&=\sum_{j=0}^{h-1}(\varepsilon+\delta jM),\label{eq:value-radius}\\ \rho_h(a)&=D_h+\varepsilon_a+\delta_a hM,\label{eq:local-radius}\\ \Gamma_h&=D_h+\varepsilon+\delta hM.\label{eq:global-radius}
\varepsilonUse in source · 12 passages
Search aliases: ε varepsilon
Use in source · common.tex, line 48
skip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]h…
Exact mathematical passage
\varepsilon
\varepsilon_aUse in source · 2 passages
Search aliases: ε_a varepsilon
Use in source · planning_chapters.tex, line 190
Induction on the Bellman recursion gives |widehat V_h(s)|≤ hM for the nominal value. The source's accumulated value radius and local Q radius are D_h · =∑_j=0^h-1(ε+δ jM), ρ_h(a) · =D_h+ε_a+δ_a hM, Γ_h · =D_h+ε+δ hM. The Bellman residual is zero here because the nominal tables are exact Bellman values. The broader model-error framework also allows a supplied table with a proved nonzero residual, but no residual term is silently introduced in these quote results.
Exact mathematical passage
D_h&=\sum_{j=0}^{h-1}(\varepsilon+\delta jM),\label{eq:value-radius}\\ \rho_h(a)&=D_h+\varepsilon_a+\delta_a hM,\label{eq:local-radius}\\ \Gamma_h&=D_h+\varepsilon+\delta hM.\label{eq:global-radius}
\etaUse in source · 1 passage
Search aliases: η eta
Use in source · common.tex, line 48
rrow1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Huge
Exact mathematical passage
\eta
\ThetaUse in source · 1 passage
Search aliases: Θ Theta
Use in source · common.tex, line 48
⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALC…
Exact mathematical passage
\Theta
\thetaUse in source · 1 passage
Search aliases: θ theta
Use in source · common.tex, line 48
≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfse…
Exact mathematical passage
\theta
\kappaUse in source · 1 passage
Search aliases: κ kappa
Use in source · common.tex, line 48
y,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanC…
Exact mathematical passage
\kappa
\lambdaUse in source · 1 passage
Search aliases: λ lambda
Use in source · common.tex, line 48
rightarrow1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI /qua…
Exact mathematical passage
\lambda
\muUse in source · 1 passage
Search aliases: μ mu
Use in source · common.tex, line 48
1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOR…
Exact mathematical passage
\mu
\nuUse in source · 1 passage
Search aliases: ν nu
Use in source · common.tex, line 48
∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOCp…
Exact mathematical passage
\nu
\xiUse in source · 1 passage
Search aliases: ξ xi
Use in source · common.tex, line 48
1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS vspac…
Exact mathematical passage
\xi
\rhoUse in source · 6 passages
Search aliases: ρ rho
Use in source · common.tex, line 48
ge1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Ar…
Exact mathematical passage
\rho
\rho_1Use in source · 1 passage
Search aliases: ρ_1 rho
Use in source · planning_chapters.tex, line 262
example assigns zero setup to both kinds, warm gross 200, cold gross 60, warm success band [3/5,1], and exact cold success 1. Start with both statuses untried and use h=1, hence two total actions. The nominal scores are warm 120, cold 60, and stop 0. Here ε=0, δ=4/5, M=260, and D_1=0. The local warm radius is 208, while the cold and stop radii are zero: c|r|r|r action · widehat Q_1 · ρ_1 · L_1 inspectWarm · 120 · 208 · -88 generateCold · 60 · 0 · 60 stop · 0 · 0 · 0 The lower-Q rule chooses cold…
Exact mathematical passage
\begin{array}{c|r|r|r} \text{action}&\widehat Q_1&\rho_1&L_1\\\hline \mathrm{inspectWarm}&120&208&-88\\ \mathrm{generateCold}&60&0&60\\ \mathrm{stop}&0&0&0 \end{array}
\rho_hUse in source · 4 passages
Search aliases: ρ_h rho
Use in source · planning_chapters.tex, line 190
Induction on the Bellman recursion gives |widehat V_h(s)|≤ hM for the nominal value. The source's accumulated value radius and local Q radius are D_h · =∑_j=0^h-1(ε+δ jM), ρ_h(a) · =D_h+ε_a+δ_a hM, Γ_h · =D_h+ε+δ hM. The Bellman residual is zero here because the nominal tables are exact Bellman values. The broader model-error framework also allows a supplied table with a proved nonzero residual, but no residual term is silently introduced in these quote results.
Exact mathematical passage
D_h&=\sum_{j=0}^{h-1}(\varepsilon+\delta jM),\label{eq:value-radius}\\ \rho_h(a)&=D_h+\varepsilon_a+\delta_a hM,\label{eq:local-radius}\\ \Gamma_h&=D_h+\varepsilon+\delta hM.\label{eq:global-radius}
\SigmaUse in source · 1 passage
Search aliases: Σ Sigma
Use in source · common.tex, line 48
bb N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\Sigma
\sigmaUse in source · 3 passages
Search aliases: σ sigma
Use in source · common.tex, line 48
1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolorna…
Exact mathematical passage
\sigma
\tauUse in source · 1 passage
Search aliases: τ tau
Use in source · common.tex, line 48
1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy vspace*16m…
Exact mathematical passage
\tau
\phi^{-1}Use in source · 1 passage
Search aliases: ϕ^-1 phi
Use in source · core_chapters.tex, line 158
f bar b(z)=∑_ϕ(ω)=zb(ω). Suppose L=bar L∘ϕ for a nonnegative likelihood bar L:Z→Q, and the evidence mass is positive. Then ϕ_*C_L(b)=C_bar L(ϕ_*b). Such an exact bar L exists if and only if L is constant on every fiber of ϕ. Grouping the normalizer by fibers gives M_b(L)=M_bar b(bar L). On each fiber ϕ^-1(z), the likelihood can be factored outside the sum. Thus ∑_ϕ(ω)=zfracb(ω)L(ω)M_b(L) =fracbar b(z)bar L(z)M_bar b(bar L). The factorization criterion is Theorem~[source reference] applied to the…
Exact mathematical passage
\phi^{-1}(z)
\phi_*Use in source · 1 passage
Search aliases: ϕ_* phi
Use in source · core_chapters.tex, line 152
[Conditioning commutes with exact compression] Let ϕ:Ω→ Z map between finite spaces, and define the pushforward belief bar b(z)=∑_ϕ(ω)=zb(ω). Suppose L=bar L∘ϕ for a nonnegative likelihood bar L:Z→Q, and the evidence mass is positive. Then ϕ_*C_L(b)=C_bar L(ϕ_*b). Such an exact bar L exists if and only if L is constant on every fiber of ϕ. Grouping the normalizer by fibers gives M_b(L)=M_bar b(bar L). On each fiber ϕ^-1(z), the likelihood can be factored outside the sum. Thus ∑_ϕ(ω)=zfracb(ω)L(ω…
Exact mathematical passage
\phi_*C_L(b)=C_{\bar L}(\phi_*b).
\chiUse in source · 1 passage
Search aliases: χ chi
Use in source · common.tex, line 48
∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC vspace9…
Exact mathematical passage
\chi
\ellUse in source · 7 passages
Search aliases: ℓ ell
Use in source · core_chapters.tex, line 433
[Certified minimum affine width] An accepted candidate has k=rank(A). Every exact two-stage affine factorization of f through width ℓ satisfies k≤ℓ. Under the dense two-stage tariff, F(n,m,k)=D(n,k)+D(k,m), the accepted candidate is no more expensive than any such two-stage factorization. The upper factorization gives rank(A)=rank(VU)≤ k. The lower witness gives k=rank(I_k)=rank(LAH)≤rank(A). Thus rank equals k. Any exact factorization through ℓ has rank(A)≤ℓ, by the same upper rank inequality. …
Exact mathematical passage
\ell
\ell_iUse in source · 3 passages
Search aliases: ℓ_i ell
Use in source · planning_chapters.tex, line 348
Let K be the number of successes in n Bernoulli trials with rational parameter p∈[0,1]. Define b_n,k(p)=binom nk p^k(1-p)^n-k, 0≤ k≤ n. Choose a positive integer grid size m and nonnegative rational allowance α. The grid cells have endpoints ℓ_i=fracim, u_i=fraci+1m, 0≤ i<m. For observed count k, the envelope of its point mass over cell i is B_n,k,i=binom nk u_i^k(1-ℓ_i)^n-k. Retain the cell exactly when B_n,k,i>fracαn+1. Return the closed interval spanning all retained cells. If there are no re…
Exact mathematical passage
\ell_i=\frac{i}{m},\qquad u_i=\frac{i+1}{m},\qquad 0\leq i<m.
\leftarrowUse in source · 1 passage
Search aliases: ← leftarrow
Use in source · common.tex, line 48
LeanCodelanguage=Lean,basicstyle=ttfamilyfootnotesize,breaklines=true,columns=fullflexible,keepspaces=true,showstringspaces=false,backgroundcolor=colorlight,frame=single,rulecolor=colorlight,keywordstyle=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘
Exact mathematical passage
\leftarrow
\leftrightarrowUse in source · 1 passage
Search aliases: ↔ leftrightarrow
Use in source · common.tex, line 48
nt=[s]/--/,morestring=[b]" lstdefinestyleLeanCodelanguage=Lean,basicstyle=ttfamilyfootnotesize,breaklines=true,columns=fullflexible,keepspaces=true,showstringspaces=false,backgroundcolor=colorlight,frame=single,rulecolor=colorlight,keywordstyle=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨…
Exact mathematical passage
\leftrightarrow
\RightarrowUse in source · 1 passage
Search aliases: ⇒ Rightarrow
Use in source · common.tex, line 48
[b]" lstdefinestyleLeanCodelanguage=Lean,basicstyle=ttfamilyfootnotesize,breaklines=true,columns=fullflexible,keepspaces=true,showstringspaces=false,backgroundcolor=colorlight,frame=single,rulecolor=colorlight,keywordstyle=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 …
Exact mathematical passage
\Rightarrow
\notinUse in source · 2 passages
Search aliases: ∉ notin
Use in source · common.tex, line 48
ttfamilyfootnotesize,breaklines=true,columns=fullflexible,keepspaces=true,showstringspaces=false,backgroundcolor=colorlight,frame=single,rulecolor=colorlight,keywordstyle=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓
Exact mathematical passage
\notin
\prodUse in source · 1 passage
Search aliases: ∏ prod
Use in source · common.tex, line 48
n1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\prod
\sum_{h=0}^{H-1}Use in source · 1 passage
Search aliases: ∑_h=0^H-1 sum
Use in source · planning_chapters.tex, line 303
[Expected frozen-policy regret] For a horizon H, let J_H^rm lower(s) be the expected value of the complete adaptive policy induced by robust lower-Q selection. Under any compatible realization, 0≤ V_H(s)-J_H^rm lower(s) ≤∑_h=0^H-12Γ_h. The comparator is the true optimal legal adaptive plan with the same conservative reservation guards. Write the regret at a node with h+1 remaining steps as its local Bellman loss plus the expected regret of the selected continuation. The local term is at most 2Γ_…
Exact mathematical passage
0\leq V_H(s)-J_H^{\rm lower}(s) \leq\sum_{h=0}^{H-1}2\Gamma_h.
\sum_jUse in source · 1 passage
Search aliases: ∑_j sum
Use in source · planning_chapters.tex, line 642
The probability in [source reference] ranges over the original outcome space, including rejected, unresolved, and insufficient-data runs. There is no claim that a plan will be issued, that any operation finishes, or that collection is cheap. If the issuance probability is q>0, the generic conditional implication is only Prob{uncertifiedmidissued} ≤ min(1,frac∑_jα_jq). The same nominal allowance need not hold after conditioning on issuance.
Exact mathematical passage
\Prob\{\text{uncertified}\mid\text{issued}\} \leq \min\left(1,\frac{\sum_j\alpha_j}{q}\right).
\sum_{j<h}Use in source · 1 passage
Search aliases: ∑_j<h sum
Use in source · planning_chapters.tex, line 314
leq∑_h=0^H-12Γ_h. The comparator is the true optimal legal adaptive plan with the same conservative reservation guards. Write the regret at a node with h+1 remaining steps as its local Bellman loss plus the expected regret of the selected continuation. The local term is at most 2Γ_h. By induction, every child regret is bounded by the common sum ∑_j<h2Γ_j. Taking the expectation leaves that constant unchanged because probabilities sum to one. This yields the cumulative upper bound. Nonnegativity …
Exact mathematical passage
\sum_{j<h}2\Gamma_j
\sum_{j=0}^{h-1}Use in source · 1 passage
Search aliases: ∑_j=0^h-1 sum
Use in source · planning_chapters.tex, line 190
Induction on the Bellman recursion gives |widehat V_h(s)|≤ hM for the nominal value. The source's accumulated value radius and local Q radius are D_h · =∑_j=0^h-1(ε+δ jM), ρ_h(a) · =D_h+ε_a+δ_a hM, Γ_h · =D_h+ε+δ hM. The Bellman residual is zero here because the nominal tables are exact Bellman values. The broader model-error framework also allows a supplied table with a proved nonzero residual, but no residual term is silently introduced in these quote results.
Exact mathematical passage
D_h&=\sum_{j=0}^{h-1}(\varepsilon+\delta jM),\label{eq:value-radius}\\ \rho_h(a)&=D_h+\varepsilon_a+\delta_a hM,\label{eq:local-radius}\\ \Gamma_h&=D_h+\varepsilon+\delta hM.\label{eq:global-radius}
\sum_{j\in J}Use in source · 4 passages
Search aliases: ∑_j∈ J sum in
Use in source · introduction.tex, line 29
Writing I for issuance and C for the specified episode certificate, the resulting conclusion is Prob(I∩ C^ c)≤∑_j∈ Jα_j. This is an unconditional probability over the original outcome space. It allows arbitrary dependence between scheduled checkpoints. It retains failed and unfinished runs in that space, with no plan issued on those runs. It does not assert a nominal bound conditional on issuance or completion, eventual issuance, or a productivity lower bound. The final recorder theorem derives …
Exact mathematical passage
\Prob(I\cap C^{\mathsf c})\leq\sum_{j\in J}\alpha_j.
\sum_{k=10}^{20}Use in source · 1 passage
Search aliases: ∑_k=10^20 sum
Use in source · planning_chapters.tex, line 696
For the implemented interval, the stronger retained finite experiment starts twenty independent fair attempts and lets all successes complete before all rejections. If there are at least ten successes, the first ten completed reports are all true. Their interval is [3/5,1] and excludes 1/2. That event has mass frac12^20∑_k=10^20binom20k =frac308333524288>frac110. Thus actual interval failure exceeds its nominal allowance despite complete, fully resolved lifecycle records. The exact Python eviden…
Exact mathematical passage
\frac{1}{2^{20}}\sum_{k=10}^{20}\binom{20}{k} =\frac{308333}{524288}>\frac{1}{10}.
\sum_{o\in\{0,1\}}Use in source · 1 passage
Search aliases: ∑_o∈{0,1} sum in
Use in source · planning_chapters.tex, line 172
[Bernoulli row error and expectation transport] For Bernoulli parameters p,q, ∑_o∈{0,1}|P_p(o)-P_q(o)|=2|p-q|. If |W(t)|≤ B, then replacing an observation row P by widehat P changes its expected continuation by at most |∑_o(P(o)-widehat P(o))W(T(s,a,o))| ≤ B∑_o|P(o)-widehat P(o)|. The two Bernoulli row differences are p-q and q-p, which have equal absolute values. For the second statement, apply the triangle inequality to the finite sum and use the uniform bound on each continuation value.
Exact mathematical passage
\sum_{o\in\{0,1\}}|P_p(o)-P_q(o)|=2|p-q|.
\sum_yUse in source · 2 passages
Search aliases: ∑_y sum
Use in source · core_chapters.tex, line 106
licy on EK is weakly dominated in value by some deterministic policy on E. Consequently the best deterministic value of EK is at most that of E. For each fine observation o, select a_o∈ A maximizing S_E(o,a). Such a selection exists because A is finite and nonempty. For a coarse policy π, expand the channel composition and rearrange finite sums: J_b(EK,π)=∑_o∑_y K(ymid o)S_E(o,π(y)). Every inner score is at most S_E(o,a_o). Nonnegativity and normalization of the row of K give ∑_y K(ymid o)S_E(o,…
Exact mathematical passage
J_b(EK,\pi)=\sum_o\sum_y K(y\mid o)S_E(o,\pi(y)).
\sum_{z'}Use in source · 1 passage
Search aliases: ∑_z' sum
Use in source · core_chapters.tex, line 240
e actions. For every finite horizon, bar V_n(ϕ(s))=V_n(s). Nonnegative fiber masses give nonnegative quotient probabilities; partitioning S by the fibers shows that each quotient row sums to one. Sufficiency makes reward and projected mass unchanged when replacing s_z by another representative. Inductively assume the value equality at horizon n. Then ∑_z'bar P_a(ϕ(s),z')bar V_n(z') =∑_s'P_a(s,s')V_n(s'), by projected equality and fiberwise grouping. Immediate rewards agree, so every action backu…
Exact mathematical passage
\sum_{z'}\bar P_a(\phi(s),z')\bar V_n(z') =\sum_{s'}P_a(s,s')V_n(s'),
\sum_{\phi(s')=z'}Use in source · 2 passages
Search aliases: ∑_ϕ(s')=z' sum phi
Use in source · core_chapters.tex, line 222
When Z is finite, this expectation condition is equivalent to equality of the mass sent to every abstract fiber: ∑_ϕ(s')=z'P_a(s,s')=∑_ϕ(s')=z'P_a(t,s') (z'∈ Z). To prove necessity, use the indicator of the fiber as W. To prove sufficiency, group the expectation by fibers and factor out the common value of W on each nonempty fiber. Empty fibers contribute zero. These arguments explain why raw states may have distinct next-state probabilities while having identical controlled abstract behavior.
Exact mathematical passage
\sum_{\phi(s')=z'}P_a(s,s')=\sum_{\phi(s')=z'}P_a(t,s')\qquad(z'\in Z).
\sum_{\phi(\omega)=z}Use in source · 2 passages
Search aliases: ∑_ϕ(ω)=z sum phi omega
Use in source · core_chapters.tex, line 151
[Conditioning commutes with exact compression] Let ϕ:Ω→ Z map between finite spaces, and define the pushforward belief bar b(z)=∑_ϕ(ω)=zb(ω). Suppose L=bar L∘ϕ for a nonnegative likelihood bar L:Z→Q, and the evidence mass is positive. Then ϕ_*C_L(b)=C_bar L(ϕ_*b). Such an exact bar L exists if and only if L is constant on every fiber of ϕ. Grouping the normalizer by fibers gives M_b(L)=M_bar b(bar L). On each fiber ϕ^-1(z), the likelihood can be factored outside the sum. Thus ∑_ϕ(ω)=zfracb(ω)L(ω…
Exact mathematical passage
\bar b(z)=\sum_{\phi(\omega)=z}b(\omega)
\sum_\omegaUse in source · 5 passages
Search aliases: ∑_ω sum omega
Use in source · core_chapters.tex, line 95
The unnormalized signal-action score and policy value are S_E(o,a)=∑_ω b(ω)E(omidω)u(ω,a), J_b(E,π)=∑_o S_E(o,π(o)). This form avoids dividing by the evidence mass. In particular, it remains well defined on observations whose predictive probability is zero.
Exact mathematical passage
S_E(o,a)=\sum_\omega b(\omega)E(o\mid\omega)u(\omega,a), \qquad J_b(E,\pi)=\sum_o S_E(o,\pi(o)).
\capUse in source · 1 passage
Search aliases: ∩ cap
Use in source · introduction.tex, line 29
Writing I for issuance and C for the specified episode certificate, the resulting conclusion is Prob(I∩ C^ c)≤∑_j∈ Jα_j. This is an unconditional probability over the original outcome space. It allows arbitrary dependence between scheduled checkpoints. It retains failed and unfinished runs in that space, with no plan issued on those runs. It does not assert a nominal bound conditional on issuance or completion, eventual issuance, or a productivity lower bound. The final recorder theorem derives …
Exact mathematical passage
\Prob(I\cap C^{\mathsf c})\leq\sum_{j\in J}\alpha_j.
\neUse in source · 3 passages
Search aliases: ≠ ne
Use in source · common.tex, line 48
s=fullflexible,keepspaces=true,showstringspaces=false,backgroundcolor=colorlight,frame=single,rulecolor=colorlight,keywordstyle=colornavy,commentstyle=colorteal,aboveskip=0.7em,belowskip=0.7em, literate=∀∀1 ∃∃1 →→1 ↔↔1 ⇒⇒1 ←←1 ∈∈1 ∉∉1 ≤≤1 ≥≥1 ≠≠1 ℕ N1 ℚ Q1 ℝ R1 ℤ Z1 ΩΩ1 αα1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀…
Exact mathematical passage
\ne
\leqUse in source · 21 passages
Search aliases: ≤ leq
Use in source · introduction.tex, line 29
Writing I for issuance and C for the specified episode certificate, the resulting conclusion is Prob(I∩ C^ c)≤∑_j∈ Jα_j. This is an unconditional probability over the original outcome space. It allows arbitrary dependence between scheduled checkpoints. It retains failed and unfinished runs in that space, with no plan issued on those runs. It does not assert a nominal bound conditional on issuance or completion, eventual issuance, or a productivity lower bound. The final recorder theorem derives …
Exact mathematical passage
\Prob(I\cap C^{\mathsf c})\leq\sum_{j\in J}\alpha_j.
\subsetUse in source · 1 passage
Search aliases: ⊂ subset
Use in source · common.tex, line 48
1 ββ1 κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\subset
\oplusUse in source · 2 passages
Search aliases: ⊕ oplus
Use in source · core_chapters.tex, line 46
[A task must be declared before compression] Let X={0,1}^3 and let T(x_1,x_2,x_3)=x_1wedge x_2. The representation ϕ(x)=T(x) is sufficient for this target, although it discards x_3 and many distinctions among the first two coordinates. The representation ψ(x)=x_1⊕ x_2 is insufficient: (0,0,0) and (1,1,0) have the same ψ value and different T values. No decoder can repair this collision. Conversely, retaining all three coordinates refines T but retains more information than this task requires.
Exact mathematical passage
\psi(x)=x_1\oplus x_2
\bigcupUse in source · 1 passage
Search aliases: ⋃ bigcup
Use in source · planning_chapters.tex, line 417
[Scheduled and selected failure bounds] Let B_j be the event that checkpoint j's interval excludes p_j. Then Prob(⋃_j∈ JB_j) ≤∑_j∈ Jα_j. For any data-dependent selector j(ω)∈ J, Prob{ω∈ B_j(ω)}≤∑_j∈ Jα_j. For each outcome ω, the indicator of a union is at most the sum of the individual indicators. Multiply by the nonnegative rational weight of ω and sum over the finite probability space. Interchange the two finite sums to obtain the union bound. Each checkpoint has failure mass at most its alloc…
Exact mathematical passage
\Prob\Bigl(\bigcup_{j\in J}B_j\Bigr) \leq\sum_{j\in J}\alpha_j.
\bigcup_{j\in J}Use in source · 1 passage
Search aliases: ⋃_j∈ J bigcup in
Use in source · planning_chapters.tex, line 417
[Scheduled and selected failure bounds] Let B_j be the event that checkpoint j's interval excludes p_j. Then Prob(⋃_j∈ JB_j) ≤∑_j∈ Jα_j. For any data-dependent selector j(ω)∈ J, Prob{ω∈ B_j(ω)}≤∑_j∈ Jα_j. For each outcome ω, the indicator of a union is at most the sum of the individual indicators. Multiply by the nonnegative rational weight of ω and sum over the finite probability space. Interchange the two finite sums to obtain the union bound. Each checkpoint has failure mass at most its alloc…
Exact mathematical passage
\Prob\Bigl(\bigcup_{j\in J}B_j\Bigr) \leq\sum_{j\in J}\alpha_j.
\langleUse in source · 1 passage
Search aliases: ⟨ langle
Use in source · common.tex, line 48
κκ1 δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\langle
\rangleUse in source · 1 passage
Search aliases: ⟩ rangle
Use in source · common.tex, line 48
δδ1 εε1 ππ1 ωω1 σσ1 ττ1 μμ1 λλ1 ΘΘ1 ξξ1 ηη1 νν1 χχ1 θθ1 ρρ1 ΓΓ1 ΣΣ1 ∧land1 ∨lor1 ¬neg1 ××1 ⊆⊆1 ⊂⊂1 ⟨⟨1 ⟩⟩1 ∑∑1 ∏∏1 ∣mid1 ∘∘1 ↑uparrow1 ↓downarrow1 ▸triangleright1 ₀_01 ₁_11 ₂_21 ₃_31 ₄_41 ₅_51 ₆_61 ₇_71 ₈_81 ₉_91 lstsetstyle=LeanCode newcommandavoccover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries AVOC LARGEbfseries Certified Artifact Planning,
Exact mathematical passage
\rangle
Source coverage
Automatic extraction covers TeX and Markdown math delimiters and common equation environments in these selected files. It does not interpret diagrams, images, PDF text, program identifiers, or historical archives. Occurrences are navigation aids, not a proof review.
Download all entries, passages and source checksums (JSON) · Collection coverage
- research/avoc/AVOC_Publication_1.0/README.md · 0 mathematical passages
- research/avoc/AVOC_Publication_1.0/manuscripts/closing.tex · 10 mathematical passages
- research/avoc/AVOC_Publication_1.0/manuscripts/common.tex · 62 mathematical passages
- research/avoc/AVOC_Publication_1.0/manuscripts/core_chapters.tex · 329 mathematical passages
- research/avoc/AVOC_Publication_1.0/manuscripts/introduction.tex · 17 mathematical passages
- research/avoc/AVOC_Publication_1.0/manuscripts/main.tex · 0 mathematical passages
- research/avoc/AVOC_Publication_1.0/manuscripts/planning_chapters.tex · 205 mathematical passages
- research/avoc/AVOC_Publication_1.0/publication/README.txt · 0 mathematical passages
PDF reading editions (3)
The text index does not extract PDF glyphs. Check the reading edition for notation in figures, tables, and PDF-only material.