Notation by work
Certified Bayesian Inference
All notation · Glossary · Source coverage
273 symbol spellings in 606 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 273 entries are available below.
=Definition passage · 172 passages
Search aliases: =
Definition passage: Cache validity · solver.tex, line 44
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
c=(B,(G_a),(e_a),t)
ADefinition passage · 14 passages
Search aliases: A
Definition passage: Cache validity · solver.tex, line 45
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
G_a=Q_aF(B),\qquad e_a=E(G_a),\qquad t=\sum_{a\in A}e_a. \label{eq:solver-invariant}
aDefinition passage · 61 passages
Search aliases: a
Definition passage: Cache validity · solver.tex, line 44
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
c=(B,(G_a),(e_a),t)
BDefinition passage · 123 passages
Search aliases: B
Definition passage: Cache validity · solver.tex, line 44
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
c=(B,(G_a),(e_a),t)
cDefinition passage · 11 passages
Search aliases: c
Definition passage: Cache validity · solver.tex, line 44
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
c=(B,(G_a),(e_a),t)
EDefinition passage · 31 passages
Search aliases: E
Definition passage: Cache validity · solver.tex, line 45
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
G_a=Q_aF(B),\qquad e_a=E(G_a),\qquad t=\sum_{a\in A}e_a. \label{eq:solver-invariant}
eDefinition passage · 10 passages
Search aliases: e
Definition passage: Cache validity · solver.tex, line 44
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
c=(B,(G_a),(e_a),t)
e_aDefinition passage · 6 passages
Search aliases: e_a
Definition passage: Cache validity · solver.tex, line 44
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
c=(B,(G_a),(e_a),t)
FDefinition passage · 52 passages
Search aliases: F
Definition passage: Cache validity · solver.tex, line 45
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
G_a=Q_aF(B),\qquad e_a=E(G_a),\qquad t=\sum_{a\in A}e_a. \label{eq:solver-invariant}
GDefinition passage · 11 passages
Search aliases: G
Definition passage: Cache validity · solver.tex, line 44
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
c=(B,(G_a),(e_a),t)
G_aDefinition passage · 9 passages
Search aliases: G_a
Definition passage: Cache validity · solver.tex, line 44
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
c=(B,(G_a),(e_a),t)
QDefinition passage · 38 passages
Search aliases: Q
Definition passage: Cache validity · solver.tex, line 45
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
G_a=Q_aF(B),\qquad e_a=E(G_a),\qquad t=\sum_{a\in A}e_a. \label{eq:solver-invariant}
Q_aDefinition passage · 22 passages
Search aliases: Q_a
Definition passage: Cache validity · solver.tex, line 45
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
G_a=Q_aF(B),\qquad e_a=E(G_a),\qquad t=\sum_{a\in A}e_a. \label{eq:solver-invariant}
sDefinition passage · 4 passages
Search aliases: s
Definition passage: Cache validity · solver.tex, line 49
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
s(c)=tw
tDefinition passage · 10 passages
Search aliases: t
Definition passage: Cache validity · solver.tex, line 44
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
c=(B,(G_a),(e_a),t)
wDefinition passage · 6 passages
Search aliases: w
Definition passage: Cache validity · solver.tex, line 49
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
s(c)=tw
\inDefinition passage · 21 passages
Search aliases: ∈ in
Definition passage: Cache validity · solver.tex, line 45
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
G_a=Q_aF(B),\qquad e_a=E(G_a),\qquad t=\sum_{a\in A}e_a. \label{eq:solver-invariant}
\sumDefinition passage · 12 passages
Search aliases: ∑ sum
Definition passage: Cache validity · solver.tex, line 45
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
G_a=Q_aF(B),\qquad e_a=E(G_a),\qquad t=\sum_{a\in A}e_a. \label{eq:solver-invariant}
\sum_{a\in A}Definition passage · 2 passages
Search aliases: ∑_a∈ A sum in
Definition passage: Cache validity · solver.tex, line 45
[Cache validity] A cache state is a tuple c=(B,(G_a),(e_a),t) satisfying G_a=Q_aF(B), e_a=E(G_a), t=∑_a∈ Ae_a. The cached score is s(c)=tw.
Exact mathematical passage
G_a=Q_aF(B),\qquad e_a=E(G_a),\qquad t=\sum_{a\in A}e_a. \label{eq:solver-invariant}
+Introduction passage · 58 passages
Search aliases: +
Introduction passage · solver.tex, line 170
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
\rho=1-\frac{\sigma}{\sigma+\tr S},\qquad q=\rho^2,\qquad r=1-\frac{1-q}{A_{\mathrm{count}}}. \label{eq:solver-rates}
A_{\mathrm{count}}Introduction passage · 3 passages
Search aliases: A_count mathrm
Introduction passage · solver.tex, line 169
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
A_{\mathrm{count}}=|A|
CIntroduction passage · 27 passages
Search aliases: C
Introduction passage · solver.tex, line 292
The common precision selector is the computable integer expression precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
\operatorname{precisionFor}(C,d) =\log^{\N}_2\left(\left\lceil C/d\right\rceil_{\N}\right)+1, \qquad d>0, \label{eq:solver-precision}
\mathrm{count}Introduction passage · 3 passages
Search aliases: count mathrm
Introduction passage · solver.tex, line 169
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
A_{\mathrm{count}}=|A|
dIntroduction passage · 28 passages
Search aliases: d
Introduction passage · solver.tex, line 292
The common precision selector is the computable integer expression precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
\operatorname{precisionFor}(C,d) =\log^{\N}_2\left(\left\lceil C/d\right\rceil_{\N}\right)+1, \qquad d>0, \label{eq:solver-precision}
\lceilIntroduction passage · 3 passages
Search aliases: lceil
Introduction passage · solver.tex, line 292
The common precision selector is the computable integer expression precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
\operatorname{precisionFor}(C,d) =\log^{\N}_2\left(\left\lceil C/d\right\rceil_{\N}\right)+1, \qquad d>0, \label{eq:solver-precision}
\logIntroduction passage · 2 passages
Search aliases: log
Introduction passage · solver.tex, line 292
The common precision selector is the computable integer expression precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
\operatorname{precisionFor}(C,d) =\log^{\N}_2\left(\left\lceil C/d\right\rceil_{\N}\right)+1, \qquad d>0, \label{eq:solver-precision}
\log^{\N}_2Introduction passage · 2 passages
Search aliases: log^N_2 log N
Introduction passage · solver.tex, line 292
The common precision selector is the computable integer expression precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
\operatorname{precisionFor}(C,d) =\log^{\N}_2\left(\left\lceil C/d\right\rceil_{\N}\right)+1, \qquad d>0, \label{eq:solver-precision}
\NIntroduction passage · 5 passages
Search aliases: N
Introduction passage · solver.tex, line 292
The common precision selector is the computable integer expression precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
\operatorname{precisionFor}(C,d) =\log^{\N}_2\left(\left\lceil C/d\right\rceil_{\N}\right)+1, \qquad d>0, \label{eq:solver-precision}
pIntroduction passage · 23 passages
Search aliases: p
Introduction passage · solver.tex, line 300
inequation precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
C2^{-p}\le d
\operatorname{precisionFor}Introduction passage · 2 passages
Search aliases: precisionFor operatorname
Introduction passage · solver.tex, line 292
The common precision selector is the computable integer expression precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
\operatorname{precisionFor}(C,d) =\log^{\N}_2\left(\left\lceil C/d\right\rceil_{\N}\right)+1, \qquad d>0, \label{eq:solver-precision}
qIntroduction passage · 6 passages
Search aliases: q
Introduction passage · solver.tex, line 170
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
\rho=1-\frac{\sigma}{\sigma+\tr S},\qquad q=\rho^2,\qquad r=1-\frac{1-q}{A_{\mathrm{count}}}. \label{eq:solver-rates}
rIntroduction passage · 16 passages
Search aliases: r
Introduction passage · solver.tex, line 170
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
\rho=1-\frac{\sigma}{\sigma+\tr S},\qquad q=\rho^2,\qquad r=1-\frac{1-q}{A_{\mathrm{count}}}. \label{eq:solver-rates}
\rceilIntroduction passage · 3 passages
Search aliases: rceil
Introduction passage · solver.tex, line 292
The common precision selector is the computable integer expression precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
\operatorname{precisionFor}(C,d) =\log^{\N}_2\left(\left\lceil C/d\right\rceil_{\N}\right)+1, \qquad d>0, \label{eq:solver-precision}
\rceil_{\N}Introduction passage · 3 passages
Search aliases: rceil_N rceil N
Introduction passage · solver.tex, line 292
The common precision selector is the computable integer expression precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
\operatorname{precisionFor}(C,d) =\log^{\N}_2\left(\left\lceil C/d\right\rceil_{\N}\right)+1, \qquad d>0, \label{eq:solver-precision}
SIntroduction passage · 66 passages
Search aliases: S
Introduction passage · solver.tex, line 170
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
\rho=1-\frac{\sigma}{\sigma+\tr S},\qquad q=\rho^2,\qquad r=1-\frac{1-q}{A_{\mathrm{count}}}. \label{eq:solver-rates}
\trIntroduction passage · 13 passages
Search aliases: tr
Introduction passage · solver.tex, line 170
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
\rho=1-\frac{\sigma}{\sigma+\tr S},\qquad q=\rho^2,\qquad r=1-\frac{1-q}{A_{\mathrm{count}}}. \label{eq:solver-rates}
yIntroduction passage · 32 passages
Search aliases: y
Introduction passage · foundations.tex, line 151
For a supplied rational observation y, the executable contract uses the explicit version ν_y. That version is defined at every such y and is already proved to disintegrate the model. The solver's distance theorem is pointwise against this version. It does not prove pointwise equality to every possible modification of a canonical posterior kernel on evidence-null sets. The distinction is standard for conditional laws and does not weaken the law-level certificate that the program actually returns.
Exact mathematical passage
y
|Introduction passage · 2 passages
Search aliases: |
Introduction passage · solver.tex, line 169
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
A_{\mathrm{count}}=|A|
\nuIntroduction passage · 16 passages
Search aliases: ν nu
Introduction passage · foundations.tex, line 151
For a supplied rational observation y, the executable contract uses the explicit version ν_y. That version is defined at every such y and is already proved to disintegrate the model. The solver's distance theorem is pointwise against this version. It does not prove pointwise equality to every possible modification of a canonical posterior kernel on evidence-null sets. The distinction is standard for conditional laws and does not weaken the law-level certificate that the program actually returns.
Exact mathematical passage
\nu_y
\nu_yIntroduction passage · 12 passages
Search aliases: ν_y nu
Introduction passage · foundations.tex, line 151
For a supplied rational observation y, the executable contract uses the explicit version ν_y. That version is defined at every such y and is already proved to disintegrate the model. The solver's distance theorem is pointwise against this version. It does not prove pointwise equality to every possible modification of a canonical posterior kernel on evidence-null sets. The distinction is standard for conditional laws and does not weaken the law-level certificate that the program actually returns.
Exact mathematical passage
\nu_y
\rhoIntroduction passage · 3 passages
Search aliases: ρ rho
Introduction passage · solver.tex, line 170
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
\rho=1-\frac{\sigma}{\sigma+\tr S},\qquad q=\rho^2,\qquad r=1-\frac{1-q}{A_{\mathrm{count}}}. \label{eq:solver-rates}
\rho^2Introduction passage · 1 passage
Search aliases: ρ^2 rho
Introduction passage · solver.tex, line 170
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
\rho=1-\frac{\sigma}{\sigma+\tr S},\qquad q=\rho^2,\qquad r=1-\frac{1-q}{A_{\mathrm{count}}}. \label{eq:solver-rates}
\sigmaIntroduction passage · 42 passages
Search aliases: σ sigma
Introduction passage · solver.tex, line 170
Write A_count=|A| for the positive number of output labels, and set ρ=1-fracσσ+tr S, q=ρ^2, r=1-frac1-qA_count. The model factorization and positive noise floor imply that S is positive semidefinite with quadratic lower bound σ. Its trace is nonnegative, and σ+tr S is a valid positive spectral cap. Thus 0≤ρ<1, 0≤ q<1, and 0≤ r<1. No eigenvalue oracle is needed to construct these rational constants.
Exact mathematical passage
\rho=1-\frac{\sigma}{\sigma+\tr S},\qquad q=\rho^2,\qquad r=1-\frac{1-q}{A_{\mathrm{count}}}. \label{eq:solver-rates}
\leIntroduction passage · 42 passages
Search aliases: ≤ le
Introduction passage · solver.tex, line 300
inequation precisionFor(C,d) =log^N_2(lceil C/drceil_N)+1, d>0, where log^N_2 denotes the natural-number logarithm pathNat.log, including its specified value at zero. It is not a floating-point logarithm. For every precision at least this selected count, pathcoefficient_mesh_le gives C2^-p≤ d. The proof uses integer power and ceiling inequalities. The additional bit is a sufficient choice, not a claim that the bit count is minimal.
Exact mathematical passage
C2^{-p}\le d
*Use in source · 19 passages
Search aliases: *
Use in source · foundations.tex, line 74
The exact posterior formula is ν_y= N(m+Kd,C_*), C_*=P-KHP. Writing this formula does not by itself establish conditional probability semantics. A matrix identity could describe a plausible mean and covariance without proving that its Gaussian is a disintegration of the prior and likelihood. The source constructs that disintegration at the level of probability measures. This section records the argument and the precise meaning of the word posterior.
Exact mathematical passage
\nu_y=\mathcal N(m+Kd,C_*),\qquad C_*=P-KHP. \label{eq:foundation-exact-posterior}
\mathcal AUse in source · 5 passages
Search aliases: A mathcal
Use in source · foundations.tex, line 324
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'),
Exact mathematical passage
\{Q_a:a\in\mathcal A\}
a'Use in source · 3 passages
Search aliases: a'
Use in source · foundations.tex, line 325
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'), D_b^top · =D_b, · D_b^2 · =D_b, · D_bD_b' · =0 (b≠ b'). Completeness is a separate condition: ∑_a∈ AQ_a=I_n, ∑_b∈ BD_b=I_p. The self-adjoint condition makes these Euclidean orthogonal projectors. Idempot…
Exact mathematical passage
Q_a^\top&=Q_a,& Q_a^2&=Q_a,& Q_aQ_{a'}&=0\quad(a\ne a'),\label{eq:foundation-output-packets}\\ D_b^\top&=D_b,& D_b^2&=D_b,& D_bD_{b'}&=0\quad(b\ne b').\label{eq:foundation-input-packets}
A^\topUse in source · 3 passages
Search aliases: A^top top
Use in source · foundations.tex, line 346
Use the Frobenius inner product ⟨ A,C⟩_ F=tr(A^top C). For a≠ a', self-adjointness and disjointness give ⟨ Q_aA,Q_a'A⟩_ F =tr(A^top Q_aQ_a'A)=0. Consequently the energy of a finite sum of output packets is the sum of their energies. The input analogue follows by transposing the matrices. Applying the two decompositions successively gives complete two-sided accounting.
Exact mathematical passage
\langle A,C\rangle_{\mathrm F}=\tr(A^\top C)
A_{ij}^2Use in source · 1 passage
Search aliases: A_ij^2
Use in source · foundations.tex, line 12
We use Euclidean vector norms and the squared Frobenius energy E(A)=FrobA^2=∑_i,jA_ij^2. The distinction between these norms matters. A matrix energy is a finite sum of scalar squares that can be evaluated exactly on rational inputs. An operator norm is used in the proof that this energy controls distribution error. The certificate never asks a producer to supply an unverified operator norm or an approximate eigenvalue calculation.
Exact mathematical passage
E(A)=\Frob{A}^2=\sum_{i,j}A_{ij}^2. \label{eq:foundation-energy}
\mathrm{approximation}Use in source · 1 passage
Search aliases: approximation mathrm
Use in source · foundations.tex, line 458
andidate checking] Let M be a factor-coded rational model, Q,D rational packet families, and c a rational candidate. If both pathcheckCandidate M Q D c and pathcheckTolerance M c epsilon return true, then the exact real posterior version represented by M and the exact real Joseph Gaussian represented by the gain of c satisfy Wtwo(M.posterior,M.approximation(c.gain)) ≤ε. Here ε is the real interpretation of the rational tolerance. The first check gives positivity of the floor and the four finite …
Exact mathematical passage
\Wtwo(M.\mathrm{posterior},M.\mathrm{approximation}(c.\mathrm{gain})) \le\varepsilon. \label{eq:foundation-rational-soundness}
\mathcal BUse in source · 5 passages
Search aliases: B mathcal
Use in source · foundations.tex, line 324
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'),
Exact mathematical passage
\{D_b:b\in\mathcal B\}
bUse in source · 22 passages
Search aliases: b
Use in source · foundations.tex, line 324
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'),
Exact mathematical passage
\{D_b:b\in\mathcal B\}
B'Use in source · 9 passages
Search aliases: B'
Use in source · solver.tex, line 75
For a selected label a, the executed update is B' · =B+τ G_a, · G'_a · =G_aT, · e'_a · =E(G'_a),nonumber G'_b · =G_b (b≠ a), · e'_b · =e_b (b≠ a), · t' · =t-e_a+e'_a. This is the definition pathKomorebi.CachedPosterior.step. It computes the new selected residual from the old selected residual and the precomputed transition. It retains unselected entries and updates the scalar total by a difference. The implementation does not define its new state by recomputing F(B') and projecting that matrix o…
Exact mathematical passage
B'&=B+\tau G_a, &G'_a&=G_aT, &e'_a&=E(G'_a),\nonumber\\ G'_b&=G_b\quad(b\ne a), &e'_b&=e_b\quad(b\ne a), &t'&=t-e_a+e'_a. \label{eq:solver-cache-step}
b'Use in source · 1 passage
Search aliases: b'
Use in source · foundations.tex, line 325
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'), D_b^top · =D_b, · D_b^2 · =D_b, · D_bD_b' · =0 (b≠ b'). Completeness is a separate condition: ∑_a∈ AQ_a=I_n, ∑_b∈ BD_b=I_p. The self-adjoint condition makes these Euclidean orthogonal projectors. Idempot…
Exact mathematical passage
Q_a^\top&=Q_a,& Q_a^2&=Q_a,& Q_aQ_{a'}&=0\quad(a\ne a'),\label{eq:foundation-output-packets}\\ D_b^\top&=D_b,& D_b^2&=D_b,& D_bD_{b'}&=0\quad(b\ne b').\label{eq:foundation-input-packets}
B^{\mathsf T}Use in source · 3 passages
Search aliases: B^ T mathsf
Use in source · introduction.tex, line 30
For a rational gain B, the Joseph approximation has mean and covariance m_B · =m+B(y-Hm), P_B · =(I-BH)P(I-BH)^ T+BRB^ T. Its covariance is positive semidefinite by construction. The approximation is a measure, rather than a collection of unqualified decimal entries. The exact gain K=PH^ TS^-1 identifies the familiar Gaussian posterior parameters. Later sections prove that this explicit Gaussian kernel disintegrates the actual forward joint law. This gives a posterior version defined at every su…
Exact mathematical passage
m_B&=m+B(y-Hm),\\ P_B&=(I-BH)P(I-BH)^{\mathsf T}+BRB^{\mathsf T}.
B^\topUse in source · 3 passages
Search aliases: B^top top
Use in source · foundations.tex, line 159
Let B∈R^n× p be an arbitrary gain candidate. It need not solve the innovation equation and need not have been produced by the packet algorithm. Define m_B · =m+Bd, C_B · =(I_n-BH)P(I_n-BH)^top+BRB^top, μ_B · = N(m_B,C_B). Every C_B is positive semidefinite, since it is a sum of covariance congruences. Thus every candidate gain determines a genuine Gaussian law. This is useful for certification: an imperfect candidate is a valid distribution with a measurable error, rather than a covariance formu…
Exact mathematical passage
m_B&=m+Bd,\label{eq:foundation-approx-mean}\\ C_B&=(I_n-BH)P(I_n-BH)^\top+BRB^\top,\label{eq:foundation-approx-cov}\\ \mu_B&=\mathcal N(m_B,C_B).\label{eq:foundation-approx-law}
B_*Use in source · 3 passages
Search aliases: B_*
Use in source · solver.tex, line 512
-2/3 · 5/6). If B_*=(2/3,1/6)^ T is the exact gain, expansion of the Joseph expression gives V_B_6=V_*+6(B_6-B_*)(B_6-B_*)^ T. The gain discrepancy is B_*-B_6=(2/1029,1/2058)^ T, which produces the displayed matrix. This second calculation checks the sign of the off-diagonal entries and explains why the approximate covariance has an additional positive semidefinite term. The posterior accuracy certificate concerns the complete mean-covariance law, while the dyadic output stage faithfully represe…
Exact mathematical passage
B_*=(2/3,1/6)^{\mathsf T}
B_0Use in source · 9 passages
Search aliases: B_0
Use in source · solver.tex, line 54
Validity is an exact equality invariant. It does not mean that a stored residual is approximately near a true residual, nor that its energy is merely an upper bound. Initialization evaluates F(B_0) once, projects it onto every output packet, computes every energy, and sums them. The theorem pathinitialState_valid follows directly from the definitions. It requires no prediction about future iterates.
Exact mathematical passage
F(B_0)
B_1Use in source · 1 passage
Search aliases: B_1
Use in source · solver.tex, line 613
Exact cache validity cannot be reused unchanged after independently rounding its components. The release contains a scalar counterexample with P=H=R=1, σ=1, m=0, y=1, and B_0=0. Then S=2, τ=1/3, w=2, and the first exact update is B_1=1/3, F(B_1)=1/3. The naive route separately rounds the gain center and residual center downward to zero fractional bits. Both become zero. It then computes the stored energy from the rounded residual, obtaining a stored score of zero.
Exact mathematical passage
B_1=1/3,\qquad F(B_1)=1/3.
B_4Use in source · 2 passages
Search aliases: B_4
Use in source · solver.tex, line 573
After four updates, B_4=frac203625J, F(B_4)=frac16625J, a(B_4)=frac3072390625. The score weight is w=3, because lVert yrVert^2=2. The strict margin is ε^2/4=1/64. At the previous state the score is 768/15625>1/64; after the fourth it is below 1/64. The computed fuel is 4267. Precision 4 produces score 435/64 and fails; precision 12 produces 9111/1048576 and passes the final threshold 1/16.
Exact mathematical passage
B_4=\frac{203}{625}J,\qquad F(B_4)=\frac{16}{625}J, \qquad a(B_4)=\frac{3072}{390625}.
B_5Use in source · 1 passage
Search aliases: B_5
Use in source · solver.tex, line 468
1/343, a(B_6)=frac34117649. The strict search threshold is ε^2/4=1/1600. At the previous state, a(B_5)=130/117649>1/1600, while a(B_6)<1/1600. Thus six is the actual update count for this stopping rule. The formal fuel is 410093; the program uses only six of these allowed updates. This large difference illustrates the conservative fuel construction, not an ambiguity in the observed trace.
Exact mathematical passage
a(B_5)=130/117649>1/1600
B_6Use in source · 8 passages
Search aliases: B_6
Use in source · solver.tex, line 462
After six updates, each coordinate has been selected three times. The geometric sum in its gain gives B_6=228/343 57/343, F(B_6)=4/343 1/343, a(B_6)=frac34117649. The strict search threshold is ε^2/4=1/1600. At the previous state, a(B_5)=130/117649>1/1600, while a(B_6)<1/1600. Thus six is the actual update count for this stopping rule. The formal fuel is 410093; the program uses only six of these allowed updates. This large difference illustrates the conservative fuel construction, not an ambigu…
Exact mathematical passage
B_6=\begin{pmatrix}228/343\\57/343\end{pmatrix},\qquad F(B_6)=\begin{pmatrix}4/343\\1/343\end{pmatrix},\qquad a(B_6)=\frac{34}{117649}.
B_nUse in source · 2 passages
Search aliases: B_n
Use in source · solver.tex, line 191
The transition contracts every residual matrix: E(XT)≤ qE(X). If label a is updated, its residual energy contracts by this inequality and all other output residuals remain unchanged. Orthogonal energy accounting gives E(F(B'))≤ E(F(B))-(1-q)e_a. Because a is a maximum, e_a≥ E(F(B))/A_count. It follows that E(F(B'))≤ rE(F(B)), a(B_n)≤ r^na(B_0). The energy share is pathselected_energy_share; one-step contraction is pathgreedy_energy_contract; and the score estimate is pathgreedy_score_geometric. …
Exact mathematical passage
E(F(B'))\le rE(F(B)),\qquad a(B_n)\le r^na(B_0). \label{eq:solver-geometric}
B_{n+1}^{\mathrm{ideal}}Use in source · 2 passages
Search aliases: B_n+1^ideal mathrm
Use in source · solver.tex, line 644
Core 1.0.0 already retains a different, completed rounded solver. Its update is a genuinely rounded full-gain Richardson step. It neither claims exact selective cache invariants nor selects a largest cached packet. Its declarations expose the whole-update defect instead. If widetilde B_n+1 is the rounded update and B_n+1^ideal is the exact full step at the current gain, then F(widetilde B_n+1)=F(widetilde B_n)T -(widetilde B_n+1-B_n+1^ideal)S. This is pathrounded_residual_step. The defect is exp…
Exact mathematical passage
B_{n+1}^{\mathrm{ideal}}
B_n^{\mathrm{exact}}Use in source · 2 passages
Search aliases: B_n^exact mathrm
Use in source · solver.tex, line 654
Writing d for the number of gain entries and h_t=2^-t, the source establishes an all-iteration tracking bound E(widetilde B_n-B_n^exact) ≤frac6d h_t^2(1-q)^2. Its residual-score comparison has the form a(widetilde B_n)≤2a(B_n^exact)+C_roundh_t^2, C_round= frac12dE(S)w(1-q)^2. The source names are pathroundedGain_tracking, pathroundoffScoreCoeff, and pathrounded_score_compare. The first term is ideal progress. The second is a precision-dependent floor. Both are needed.
Exact mathematical passage
E(\widetilde B_n-B_n^{\mathrm{exact}}) \le\frac{6d h_t^2}{(1-q)^2}.
C_*Use in source · 11 passages
Search aliases: C_*
Use in source · foundations.tex, line 74
The exact posterior formula is ν_y= N(m+Kd,C_*), C_*=P-KHP. Writing this formula does not by itself establish conditional probability semantics. A matrix identity could describe a plausible mean and covariance without proving that its Gaussian is a disintegration of the prior and likelihood. The source constructs that disintegration at the level of probability measures. This section records the argument and the precise meaning of the word posterior.
Exact mathematical passage
\nu_y=\mathcal N(m+Kd,C_*),\qquad C_*=P-KHP. \label{eq:foundation-exact-posterior}
C_*^{-1}Use in source · 1 passage
Search aliases: C_*^-1
Use in source · foundations.tex, line 87
The covariance C_* admits the Joseph representation C_*=(I_n-KH)P(I_n-KH)^top+KRK^top. Each term on the right is positive semidefinite. Therefore C_*succeq0, including at the singular boundary. This avoids any proof based on P^-1 or C_*^-1.
Exact mathematical passage
C_*^{-1}
C_BUse in source · 8 passages
Search aliases: C_B
Use in source · foundations.tex, line 159
Let B∈R^n× p be an arbitrary gain candidate. It need not solve the innovation equation and need not have been produced by the packet algorithm. Define m_B · =m+Bd, C_B · =(I_n-BH)P(I_n-BH)^top+BRB^top, μ_B · = N(m_B,C_B). Every C_B is positive semidefinite, since it is a sum of covariance congruences. Thus every candidate gain determines a genuine Gaussian law. This is useful for certification: an imperfect candidate is a valid distribution with a measurable error, rather than a covariance formu…
Exact mathematical passage
m_B&=m+Bd,\label{eq:foundation-approx-mean}\\ C_B&=(I_n-BH)P(I_n-BH)^\top+BRB^\top,\label{eq:foundation-approx-cov}\\ \mu_B&=\mathcal N(m_B,C_B).\label{eq:foundation-approx-law}
C_{\mathrm{out}}Use in source · 2 passages
Search aliases: C_out mathrm
Use in source · solver.tex, line 376
Each output arithmetic expression has a precision-independent budget coefficient. The source sums all mean coefficients and all covariance coefficients to obtain C_out, defined by pathoutputCoefficient. Every individual coefficient is nonnegative and no greater than this sum. It chooses p_out=precisionFor(C_out,δ) and evaluates the output graph at that precision. Since every entry radius is bounded by its coefficient times 2^-p_out, the same integer precision bounds all radii by δ. The declarati…
Exact mathematical passage
C_{\mathrm{out}}
C_{\mathrm{round}}Use in source · 1 passage
Search aliases: C_round mathrm
Use in source · solver.tex, line 659
Writing d for the number of gain entries and h_t=2^-t, the source establishes an all-iteration tracking bound E(widetilde B_n-B_n^exact) ≤frac6d h_t^2(1-q)^2. Its residual-score comparison has the form a(widetilde B_n)≤2a(B_n^exact)+C_roundh_t^2, C_round= frac12dE(S)w(1-q)^2. The source names are pathroundedGain_tracking, pathroundoffScoreCoeff, and pathrounded_score_compare. The first term is ideal progress. The second is a precision-dependent floor. Both are needed.
Exact mathematical passage
a(\widetilde B_n)\le2a(B_n^{\mathrm{exact}})+C_{\mathrm{round}}h_t^2, \qquad C_{\mathrm{round}}= \frac{12dE(S)w}{(1-q)^2}.
C_{\mathrm{ver}}Use in source · 2 passages
Search aliases: C_ver mathrm
Use in source · solver.tex, line 280
Let h_p=2^-p. The dyadic evaluator propagates rational centers and outward radii through its arithmetic graph. Its budget calculation supplies a nonnegative coefficient C_ver(M,Q,D,B) independent of p, with widehat a_p(B)≤ a(B)+C_ver(M,Q,D,B)h_p. Here widehat a_p is the actual rounded candidate score. The full expression for the coefficient is pathscoreRoundCoeff, built from packet residual energy and innovation-vector magnitude and radius budgets. It bounds the entire score graph, rather than r…
Exact mathematical passage
C_{\mathrm{ver}}(M,Q,D,B)
DUse in source · 15 passages
Search aliases: D
Use in source · foundations.tex, line 324
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'),
Exact mathematical passage
\{D_b:b\in\mathcal B\}
D_bUse in source · 10 passages
Search aliases: D_b
Use in source · foundations.tex, line 324
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'),
Exact mathematical passage
\{D_b:b\in\mathcal B\}
D_{b'}Use in source · 1 passage
Search aliases: D_b'
Use in source · foundations.tex, line 325
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'), D_b^top · =D_b, · D_b^2 · =D_b, · D_bD_b' · =0 (b≠ b'). Completeness is a separate condition: ∑_a∈ AQ_a=I_n, ∑_b∈ BD_b=I_p. The self-adjoint condition makes these Euclidean orthogonal projectors. Idempot…
Exact mathematical passage
Q_a^\top&=Q_a,& Q_a^2&=Q_a,& Q_aQ_{a'}&=0\quad(a\ne a'),\label{eq:foundation-output-packets}\\ D_b^\top&=D_b,& D_b^2&=D_b,& D_bD_{b'}&=0\quad(b\ne b').\label{eq:foundation-input-packets}
D_b^2Use in source · 1 passage
Search aliases: D_b^2
Use in source · foundations.tex, line 325
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'), D_b^top · =D_b, · D_b^2 · =D_b, · D_bD_b' · =0 (b≠ b'). Completeness is a separate condition: ∑_a∈ AQ_a=I_n, ∑_b∈ BD_b=I_p. The self-adjoint condition makes these Euclidean orthogonal projectors. Idempot…
Exact mathematical passage
Q_a^\top&=Q_a,& Q_a^2&=Q_a,& Q_aQ_{a'}&=0\quad(a\ne a'),\label{eq:foundation-output-packets}\\ D_b^\top&=D_b,& D_b^2&=D_b,& D_bD_{b'}&=0\quad(b\ne b').\label{eq:foundation-input-packets}
D_b^\topUse in source · 1 passage
Search aliases: D_b^top top
Use in source · foundations.tex, line 325
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'), D_b^top · =D_b, · D_b^2 · =D_b, · D_bD_b' · =0 (b≠ b'). Completeness is a separate condition: ∑_a∈ AQ_a=I_n, ∑_b∈ BD_b=I_p. The self-adjoint condition makes these Euclidean orthogonal projectors. Idempot…
Exact mathematical passage
Q_a^\top&=Q_a,& Q_a^2&=Q_a,& Q_aQ_{a'}&=0\quad(a\ne a'),\label{eq:foundation-output-packets}\\ D_b^\top&=D_b,& D_b^2&=D_b,& D_bD_{b'}&=0\quad(b\ne b').\label{eq:foundation-input-packets}
\operatorname{diag}Use in source · 1 passage
Search aliases: diag operatorname
Use in source · solver.tex, line 435
0, y=1. It is represented by L=diag(2,1), N=0, and σ=1. The two output projectors select the coordinate axes, and the single input projector is 1. Start with B_0=0, seed 0, scan [0,1], probes [4,12], ε=1/20, and δ=1/1000.
Exact mathematical passage
L=\operatorname{diag}(2,1)
\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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\downarrow
\EUse in source · 1 passage
Search aliases: E
Use in source · foundations.tex, line 217
Let Δ=K-B. Subtraction in [source reference] gives T_K-T_B=Δ d-Δ(HU+V). The random vector HU+V is centered and has covariance S. The difference therefore has mean Δ d and covariance Δ SΔ^top. Its expected squared Euclidean norm is E T_K-T_B ^2 = Δ d ^2+tr(Δ SΔ^top). The source proves both marginals and this cost. It does not assume that a producer has supplied a coupling with the desired properties. The load-bearing declarations are pathgainSample_law, pathgainSample_exact_posterior_law, and pat…
Exact mathematical passage
\E\|T_K-T_B\|^2 =\|\Delta d\|^2+\tr(\Delta S\Delta^\top). \label{eq:foundation-coupling-cost}
e'_aUse in source · 2 passages
Search aliases: e'_a
Use in source · solver.tex, line 75
For a selected label a, the executed update is B' · =B+τ G_a, · G'_a · =G_aT, · e'_a · =E(G'_a),nonumber G'_b · =G_b (b≠ a), · e'_b · =e_b (b≠ a), · t' · =t-e_a+e'_a. This is the definition pathKomorebi.CachedPosterior.step. It computes the new selected residual from the old selected residual and the precomputed transition. It retains unselected entries and updates the scalar total by a difference. The implementation does not define its new state by recomputing F(B') and projecting that matrix o…
Exact mathematical passage
B'&=B+\tau G_a, &G'_a&=G_aT, &e'_a&=E(G'_a),\nonumber\\ G'_b&=G_b\quad(b\ne a), &e'_b&=e_b\quad(b\ne a), &t'&=t-e_a+e'_a. \label{eq:solver-cache-step}
e'_bUse in source · 2 passages
Search aliases: e'_b
Use in source · solver.tex, line 75
For a selected label a, the executed update is B' · =B+τ G_a, · G'_a · =G_aT, · e'_a · =E(G'_a),nonumber G'_b · =G_b (b≠ a), · e'_b · =e_b (b≠ a), · t' · =t-e_a+e'_a. This is the definition pathKomorebi.CachedPosterior.step. It computes the new selected residual from the old selected residual and the precomputed transition. It retains unselected entries and updates the scalar total by a difference. The implementation does not define its new state by recomputing F(B') and projecting that matrix o…
Exact mathematical passage
B'&=B+\tau G_a, &G'_a&=G_aT, &e'_a&=E(G'_a),\nonumber\\ G'_b&=G_b\quad(b\ne a), &e'_b&=e_b\quad(b\ne a), &t'&=t-e_a+e'_a. \label{eq:solver-cache-step}
E_*Use in source · 2 passages
Search aliases: E_*
Use in source · foundations.tex, line 121
For the reverse construction, sample Y∼ N(Hm,S) and an independent E_*∼ N(0,C_*). Define Z=m+K(Y-Hm)+E_*. Conditional on Y=y, the law of Z is precisely ν_y. The joint mean of (Y,Z) is again (Hm,m). Its cross covariance is SK^top=HP, and its state covariance is KSK^top+C_*=KHP+(P-KHP)=P. It therefore has exactly the covariance in [source reference]. Both constructions yield Gaussian measures with the same mean and covariance, so they yield the same joint probability measure. This is a full law id…
Exact mathematical passage
E_*\sim\mathcal N(0,C_*)
e_+Use in source · 1 passage
Search aliases: e_+
Use in source · solver.tex, line 566
Take B_0=0, seed 0, scan [0,1], probes [4,12], ε=1/4, and δ=1/1000. Here tr S=4, τ=1/5, and T=I-(I+J)/5. The initial residual is J, entirely in the Q_+ output packet. Since JS=3J, each selected update multiplies this residual by 2/5. The Q_- residual remains zero. Thus every selected label is 0 and (e_+,e_-)=(4(4/25)^n,0), B_n=frac1-(2/5)^n3J. The first four pre-update energy pairs are (4,0), (16/25,0), (64/625,0), and (256/15625,0).
Exact mathematical passage
(e_+,e_-)=(4(4/25)^n,0),\qquad B_n=\frac{1-(2/5)^n}{3}J.
e_-Use in source · 1 passage
Search aliases: e_-
Use in source · solver.tex, line 566
Take B_0=0, seed 0, scan [0,1], probes [4,12], ε=1/4, and δ=1/1000. Here tr S=4, τ=1/5, and T=I-(I+J)/5. The initial residual is J, entirely in the Q_+ output packet. Since JS=3J, each selected update multiplies this residual by 2/5. The Q_- residual remains zero. Thus every selected label is 0 and (e_+,e_-)=(4(4/25)^n,0), B_n=frac1-(2/5)^n3J. The first four pre-update energy pairs are (4,0), (16/25,0), (64/625,0), and (256/15625,0).
Exact mathematical passage
(e_+,e_-)=(4(4/25)^n,0),\qquad B_n=\frac{1-(2/5)^n}{3}J.
e_0Use in source · 1 passage
Search aliases: e_0
Use in source · solver.tex, line 448
al residual is (4,1)^ T, with packet energies 16 and 1. Updating one coordinate multiplies its residual by 1/7 and its energy by 1/49. The other coordinate remains exactly unchanged. The maximum-energy schedule therefore alternates between labels 0 and 1. The complete pre-update trace is rrrrr Updates already made · Selected label · e_0 · e_1 · t
Exact mathematical passage
e_0
e_1Use in source · 1 passage
Search aliases: e_1
Use in source · solver.tex, line 448
ual is (4,1)^ T, with packet energies 16 and 1. Updating one coordinate multiplies its residual by 1/7 and its energy by 1/49. The other coordinate remains exactly unchanged. The maximum-energy schedule therefore alternates between labels 0 and 1. The complete pre-update trace is rrrrr Updates already made · Selected label · e_0 · e_1 · t
Exact mathematical passage
e_1
e_bUse in source · 1 passage
Search aliases: e_b
Use in source · solver.tex, line 75
For a selected label a, the executed update is B' · =B+τ G_a, · G'_a · =G_aT, · e'_a · =E(G'_a),nonumber G'_b · =G_b (b≠ a), · e'_b · =e_b (b≠ a), · t' · =t-e_a+e'_a. This is the definition pathKomorebi.CachedPosterior.step. It computes the new selected residual from the old selected residual and the precomputed transition. It retains unselected entries and updates the scalar total by a difference. The implementation does not define its new state by recomputing F(B') and projecting that matrix o…
Exact mathematical passage
B'&=B+\tau G_a, &G'_a&=G_aT, &e'_a&=E(G'_a),\nonumber\\ G'_b&=G_b\quad(b\ne a), &e'_b&=e_b\quad(b\ne a), &t'&=t-e_a+e'_a. \label{eq:solver-cache-step}
\mathrm{exact}Use in source · 2 passages
Search aliases: exact mathrm
Use in source · solver.tex, line 654
Writing d for the number of gain entries and h_t=2^-t, the source establishes an all-iteration tracking bound E(widetilde B_n-B_n^exact) ≤frac6d h_t^2(1-q)^2. Its residual-score comparison has the form a(widetilde B_n)≤2a(B_n^exact)+C_roundh_t^2, C_round= frac12dE(S)w(1-q)^2. The source names are pathroundedGain_tracking, pathroundoffScoreCoeff, and pathrounded_score_compare. The first term is ideal progress. The second is a precision-dependent floor. Both are needed.
Exact mathematical passage
E(\widetilde B_n-B_n^{\mathrm{exact}}) \le\frac{6d h_t^2}{(1-q)^2}.
\mathrm FUse in source · 3 passages
Search aliases: F mathrm
Use in source · foundations.tex, line 346
Use the Frobenius inner product ⟨ A,C⟩_ F=tr(A^top C). For a≠ a', self-adjointness and disjointness give ⟨ Q_aA,Q_a'A⟩_ F =tr(A^top Q_aQ_a'A)=0. Consequently the energy of a finite sum of output packets is the sum of their energies. The input analogue follows by transposing the matrices. Applying the two decompositions successively gives complete two-sided accounting.
Exact mathematical passage
\langle A,C\rangle_{\mathrm F}=\tr(A^\top C)
fUse in source · 2 passages
Search aliases: f
Use in source · foundations.tex, line 275
sigma^-2 d ^2). For a vector v, rowwise Cauchy--Schwarz gives Fv ^2=∑_i(∑_jF_ijv_j)^2 ≤∑_i(∑_jF_ij^2) v ^2 =E(F) v ^2. Apply this with v=S^-1d and use [source reference] to obtain FS^-1d ^2≤ E(F)σ^-2 d ^2. If f_i is the transpose of the ith row of F, then tr(FS^-1F^top)=∑_i f_i^top S^-1f_i ≤∑_i f_i S^-1f_i ≤σ^-1∑_i f_i ^2. The last sum is E(F). Adding the two estimates proves the result.
Exact mathematical passage
f_i
F^\topUse in source · 2 passages
Search aliases: F^top top
Use in source · foundations.tex, line 258
[Frobenius energy controls the residual cost] If F∈R^n× p and Ssucceqσ I_psucc0, then FS^-1d ^2+tr(FS^-1F^top) ≤ E(F)(σ^-1+σ^-2 d ^2). For a vector v, rowwise Cauchy--Schwarz gives Fv ^2=∑_i(∑_jF_ijv_j)^2 ≤∑_i(∑_jF_ij^2) v ^2 =E(F) v ^2. Apply this with v=S^-1d and use [source reference] to obtain FS^-1d ^2≤ E(F)σ^-2 d ^2. If f_i is the transpose of the ith row of F, then tr(FS^-1F^top)=∑_i f_i^top S^-1f_i ≤∑_i f_i S^-1f_i ≤σ^-1∑_i f_i ^2. The last sum is E(F). Adding the two estimates proves th…
Exact mathematical passage
\|FS^{-1}d\|^2+\tr(FS^{-1}F^\top) \le E(F)\left(\sigma^{-1}+\sigma^{-2}\|d\|^2\right). \label{eq:foundation-cost-majorant}
F_{ab}Use in source · 3 passages
Search aliases: F_ab
Use in source · foundations.tex, line 338
The two-sided residual packet is F_ab(B)=Q_aF(B)D_b. Each packet remains an n× p matrix, although it is supported on the output and input subspaces selected by its projectors. The notation does not assume a coordinate partition or require projectors to be diagonal. Rational rotated projectors are allowed when their exact entries satisfy the declared identities.
Exact mathematical passage
F_{ab}(B)=Q_aF(B)D_b. \label{eq:foundation-packet-residual}
f_iUse in source · 2 passages
Search aliases: f_i
Use in source · foundations.tex, line 275
sigma^-2 d ^2). For a vector v, rowwise Cauchy--Schwarz gives Fv ^2=∑_i(∑_jF_ijv_j)^2 ≤∑_i(∑_jF_ij^2) v ^2 =E(F) v ^2. Apply this with v=S^-1d and use [source reference] to obtain FS^-1d ^2≤ E(F)σ^-2 d ^2. If f_i is the transpose of the ith row of F, then tr(FS^-1F^top)=∑_i f_i^top S^-1f_i ≤∑_i f_i S^-1f_i ≤σ^-1∑_i f_i ^2. The last sum is E(F). Adding the two estimates proves the result.
Exact mathematical passage
f_i
f_i^\topUse in source · 1 passage
Search aliases: f_i^top top
Use in source · foundations.tex, line 276
ajorant For a vector v, rowwise Cauchy--Schwarz gives Fv ^2=∑_i(∑_jF_ijv_j)^2 ≤∑_i(∑_jF_ij^2) v ^2 =E(F) v ^2. Apply this with v=S^-1d and use [source reference] to obtain FS^-1d ^2≤ E(F)σ^-2 d ^2. If f_i is the transpose of the ith row of F, then tr(FS^-1F^top)=∑_i f_i^top S^-1f_i ≤∑_i f_i S^-1f_i ≤σ^-1∑_i f_i ^2. The last sum is E(F). Adding the two estimates proves the result.
Exact mathematical passage
\tr(FS^{-1}F^\top)=\sum_i f_i^\top S^{-1}f_i \le\sum_i\|f_i\|\|S^{-1}f_i\| \le\sigma^{-1}\sum_i\|f_i\|^2.
F_{ij}Use in source · 1 passage
Search aliases: F_ij
Use in source · foundations.tex, line 266
[Frobenius energy controls the residual cost] If F∈R^n× p and Ssucceqσ I_psucc0, then FS^-1d ^2+tr(FS^-1F^top) ≤ E(F)(σ^-1+σ^-2 d ^2). For a vector v, rowwise Cauchy--Schwarz gives Fv ^2=∑_i(∑_jF_ijv_j)^2 ≤∑_i(∑_jF_ij^2) v ^2 =E(F) v ^2. Apply this with v=S^-1d and use [source reference] to obtain FS^-1d ^2≤ E(F)σ^-2 d ^2. If f_i is the transpose of the ith row of F, then tr(FS^-1F^top)=∑_i f_i^top S^-1f_i ≤∑_i f_i S^-1f_i ≤σ^-1∑_i f_i ^2. The last sum is E(F). Adding the two estimates proves th…
Exact mathematical passage
\|Fv\|^2=\sum_i\left(\sum_jF_{ij}v_j\right)^2 \le\sum_i\left(\sum_jF_{ij}^2\right)\|v\|^2 =E(F)\|v\|^2.
F_{ij}^2Use in source · 1 passage
Search aliases: F_ij^2
Use in source · foundations.tex, line 266
[Frobenius energy controls the residual cost] If F∈R^n× p and Ssucceqσ I_psucc0, then FS^-1d ^2+tr(FS^-1F^top) ≤ E(F)(σ^-1+σ^-2 d ^2). For a vector v, rowwise Cauchy--Schwarz gives Fv ^2=∑_i(∑_jF_ijv_j)^2 ≤∑_i(∑_jF_ij^2) v ^2 =E(F) v ^2. Apply this with v=S^-1d and use [source reference] to obtain FS^-1d ^2≤ E(F)σ^-2 d ^2. If f_i is the transpose of the ith row of F, then tr(FS^-1F^top)=∑_i f_i^top S^-1f_i ≤∑_i f_i S^-1f_i ≤σ^-1∑_i f_i ^2. The last sum is E(F). Adding the two estimates proves th…
Exact mathematical passage
\|Fv\|^2=\sum_i\left(\sum_jF_{ij}v_j\right)^2 \le\sum_i\left(\sum_jF_{ij}^2\right)\|v\|^2 =E(F)\|v\|^2.
\FrobUse in source · 2 passages
Search aliases: Frob
Use in source · foundations.tex, line 12
We use Euclidean vector norms and the squared Frobenius energy E(A)=FrobA^2=∑_i,jA_ij^2. The distinction between these norms matters. A matrix energy is a finite sum of scalar squares that can be evaluated exactly on rational inputs. An operator norm is used in the proof that this energy controls distribution error. The certificate never asks a producer to supply an unverified operator norm or an approximate eigenvalue calculation.
Exact mathematical passage
E(A)=\Frob{A}^2=\sum_{i,j}A_{ij}^2. \label{eq:foundation-energy}
G'_aUse in source · 1 passage
Search aliases: G'_a
Use in source · solver.tex, line 75
For a selected label a, the executed update is B' · =B+τ G_a, · G'_a · =G_aT, · e'_a · =E(G'_a),nonumber G'_b · =G_b (b≠ a), · e'_b · =e_b (b≠ a), · t' · =t-e_a+e'_a. This is the definition pathKomorebi.CachedPosterior.step. It computes the new selected residual from the old selected residual and the precomputed transition. It retains unselected entries and updates the scalar total by a difference. The implementation does not define its new state by recomputing F(B') and projecting that matrix o…
Exact mathematical passage
B'&=B+\tau G_a, &G'_a&=G_aT, &e'_a&=E(G'_a),\nonumber\\ G'_b&=G_b\quad(b\ne a), &e'_b&=e_b\quad(b\ne a), &t'&=t-e_a+e'_a. \label{eq:solver-cache-step}
G'_bUse in source · 1 passage
Search aliases: G'_b
Use in source · solver.tex, line 75
For a selected label a, the executed update is B' · =B+τ G_a, · G'_a · =G_aT, · e'_a · =E(G'_a),nonumber G'_b · =G_b (b≠ a), · e'_b · =e_b (b≠ a), · t' · =t-e_a+e'_a. This is the definition pathKomorebi.CachedPosterior.step. It computes the new selected residual from the old selected residual and the precomputed transition. It retains unselected entries and updates the scalar total by a difference. The implementation does not define its new state by recomputing F(B') and projecting that matrix o…
Exact mathematical passage
B'&=B+\tau G_a, &G'_a&=G_aT, &e'_a&=E(G'_a),\nonumber\\ G'_b&=G_b\quad(b\ne a), &e'_b&=e_b\quad(b\ne a), &t'&=t-e_a+e'_a. \label{eq:solver-cache-step}
G_bUse in source · 2 passages
Search aliases: G_b
Use in source · solver.tex, line 75
For a selected label a, the executed update is B' · =B+τ G_a, · G'_a · =G_aT, · e'_a · =E(G'_a),nonumber G'_b · =G_b (b≠ a), · e'_b · =e_b (b≠ a), · t' · =t-e_a+e'_a. This is the definition pathKomorebi.CachedPosterior.step. It computes the new selected residual from the old selected residual and the precomputed transition. It retains unselected entries and updates the scalar total by a difference. The implementation does not define its new state by recomputing F(B') and projecting that matrix o…
Exact mathematical passage
B'&=B+\tau G_a, &G'_a&=G_aT, &e'_a&=E(G'_a),\nonumber\\ G'_b&=G_b\quad(b\ne a), &e'_b&=e_b\quad(b\ne a), &t'&=t-e_a+e'_a. \label{eq:solver-cache-step}
\mathrm{gain}Use in source · 1 passage
Search aliases: gain mathrm
Use in source · foundations.tex, line 458
andidate checking] Let M be a factor-coded rational model, Q,D rational packet families, and c a rational candidate. If both pathcheckCandidate M Q D c and pathcheckTolerance M c epsilon return true, then the exact real posterior version represented by M and the exact real Joseph Gaussian represented by the gain of c satisfy Wtwo(M.posterior,M.approximation(c.gain)) ≤ε. Here ε is the real interpretation of the rational tolerance. The first check gives positivity of the floor and the four finite …
Exact mathematical passage
\Wtwo(M.\mathrm{posterior},M.\mathrm{approximation}(c.\mathrm{gain})) \le\varepsilon. \label{eq:foundation-rational-soundness}
HUse in source · 52 passages
Search aliases: H
Use in source · foundations.tex, line 5
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
Y=HX+V,\qquad V\sim\mathcal N(0,R),\qquad V\text{ independent of }X. \label{eq:foundation-model}
hUse in source · 5 passages
Search aliases: h
Use in source · solver.tex, line 278
Let h_p=2^-p. The dyadic evaluator propagates rational centers and outward radii through its arithmetic graph. Its budget calculation supplies a nonnegative coefficient C_ver(M,Q,D,B) independent of p, with widehat a_p(B)≤ a(B)+C_ver(M,Q,D,B)h_p. Here widehat a_p is the actual rounded candidate score. The full expression for the coefficient is pathscoreRoundCoeff, built from packet residual energy and innovation-vector magnitude and radius budgets. It bounds the entire score graph, rather than r…
Exact mathematical passage
h_p=2^{-p}
H^{\mathsf T}Use in source · 6 passages
Search aliases: H^ T mathsf
Use in source · introduction.tex, line 24
. The representation uses rational factors P=LL^ T, R=NN^ T+σ I, σ>0. All data supplied to the executable construction, including m,H,L,N,σ and the observation y, are rational. Finite state and observation index types determine the matrix shapes. There is no requirement that H be square or that P be invertible. The innovation matrix is S=HPH^ T+R. Its positive noise floor supports the inverse used in the exact posterior semantics. The executable iterative solver avoids computing that inverse to …
Exact mathematical passage
S=HPH^{\mathsf T}+R.
H^\topUse in source · 11 passages
Search aliases: H^top top
Use in source · foundations.tex, line 19
For an observed value y, put d=y-Hm, S=HPH^top+R, K=PH^top S^-1. The matrix S is the innovation covariance. It is positive definite because, for every nonzero z∈R^p, z^top Sz=(H^top z)^top P(H^top z)+z^top Rz>0. Consequently the inverse in the definition of K exists even when P has a nontrivial nullspace or H has deficient rank. Every inverse used by the posterior argument is an inverse on the observation space. This is the structural reason singular priors are supported.
Exact mathematical passage
d=y-Hm,\qquad S=HPH^\top+R,\qquad K=PH^\top S^{-1}. \label{eq:foundation-innovation}
h_pUse in source · 2 passages
Search aliases: h_p
Use in source · solver.tex, line 278
Let h_p=2^-p. The dyadic evaluator propagates rational centers and outward radii through its arithmetic graph. Its budget calculation supplies a nonnegative coefficient C_ver(M,Q,D,B) independent of p, with widehat a_p(B)≤ a(B)+C_ver(M,Q,D,B)h_p. Here widehat a_p is the actual rounded candidate score. The full expression for the coefficient is pathscoreRoundCoeff, built from packet residual energy and innovation-vector magnitude and radius budgets. It bounds the entire score graph, rather than r…
Exact mathematical passage
h_p=2^{-p}
h_tUse in source · 1 passage
Search aliases: h_t
Use in source · solver.tex, line 652
Writing d for the number of gain entries and h_t=2^-t, the source establishes an all-iteration tracking bound E(widetilde B_n-B_n^exact) ≤frac6d h_t^2(1-q)^2. Its residual-score comparison has the form a(widetilde B_n)≤2a(B_n^exact)+C_roundh_t^2, C_round= frac12dE(S)w(1-q)^2. The source names are pathroundedGain_tracking, pathroundoffScoreCoeff, and pathrounded_score_compare. The first term is ideal progress. The second is a precision-dependent floor. Both are needed.
Exact mathematical passage
h_t=2^{-t}
h_t^2Use in source · 2 passages
Search aliases: h_t^2
Use in source · solver.tex, line 654
Writing d for the number of gain entries and h_t=2^-t, the source establishes an all-iteration tracking bound E(widetilde B_n-B_n^exact) ≤frac6d h_t^2(1-q)^2. Its residual-score comparison has the form a(widetilde B_n)≤2a(B_n^exact)+C_roundh_t^2, C_round= frac12dE(S)w(1-q)^2. The source names are pathroundedGain_tracking, pathroundoffScoreCoeff, and pathrounded_score_compare. The first term is ideal progress. The second is a precision-dependent floor. Both are needed.
Exact mathematical passage
E(\widetilde B_n-B_n^{\mathrm{exact}}) \le\frac{6d h_t^2}{(1-q)^2}.
IUse in source · 20 passages
Search aliases: I
Use in source · foundations.tex, line 32
The completed executable contract represents its model by rational matrices and vectors. Its input consists of H, m, y, a prior factor L∈Q^n× r, a noise factor N∈Q^p× s, and a rational number σ. The covariance matrices are derived from these inputs: P=LL^top, R=NN^top+σ I_p, σ>0. The factor dimensions r and s are finite and need not equal the state or observation dimension. The factors may have dependent columns or zero entries. The prior factor is allowed to have rank below n. The positive floo…
Exact mathematical passage
P=LL^\top,\qquad R=NN^\top+\sigma I_p,\qquad \sigma>0. \label{eq:foundation-factor-model}
iUse in source · 5 passages
Search aliases: i
Use in source · foundations.tex, line 12
We use Euclidean vector norms and the squared Frobenius energy E(A)=FrobA^2=∑_i,jA_ij^2. The distinction between these norms matters. A matrix energy is a finite sum of scalar squares that can be evaluated exactly on rational inputs. An operator norm is used in the proof that this energy controls distribution error. The certificate never asks a producer to supply an unverified operator norm or an approximate eigenvalue calculation.
Exact mathematical passage
E(A)=\Frob{A}^2=\sum_{i,j}A_{ij}^2. \label{eq:foundation-energy}
I_nUse in source · 5 passages
Search aliases: I_n
Use in source · foundations.tex, line 83
The covariance C_* admits the Joseph representation C_*=(I_n-KH)P(I_n-KH)^top+KRK^top. Each term on the right is positive semidefinite. Therefore C_*succeq0, including at the singular boundary. This avoids any proof based on P^-1 or C_*^-1.
Exact mathematical passage
C_*=(I_n-KH)P(I_n-KH)^\top+KRK^\top. \label{eq:foundation-exact-joseph}
I_pUse in source · 5 passages
Search aliases: I_p
Use in source · foundations.tex, line 32
The completed executable contract represents its model by rational matrices and vectors. Its input consists of H, m, y, a prior factor L∈Q^n× r, a noise factor N∈Q^p× s, and a rational number σ. The covariance matrices are derived from these inputs: P=LL^top, R=NN^top+σ I_p, σ>0. The factor dimensions r and s are finite and need not equal the state or observation dimension. The factors may have dependent columns or zero entries. The prior factor is allowed to have rank below n. The positive floo…
Exact mathematical passage
P=LL^\top,\qquad R=NN^\top+\sigma I_p,\qquad \sigma>0. \label{eq:foundation-factor-model}
\mathrm{ideal}Use in source · 2 passages
Search aliases: ideal mathrm
Use in source · solver.tex, line 644
Core 1.0.0 already retains a different, completed rounded solver. Its update is a genuinely rounded full-gain Richardson step. It neither claims exact selective cache invariants nor selects a largest cached packet. Its declarations expose the whole-update defect instead. If widetilde B_n+1 is the rounded update and B_n+1^ideal is the exact full step at the current gain, then F(widetilde B_n+1)=F(widetilde B_n)T -(widetilde B_n+1-B_n+1^ideal)S. This is pathrounded_residual_step. The defect is exp…
Exact mathematical passage
B_{n+1}^{\mathrm{ideal}}
\infUse in source · 1 passage
Search aliases: inf
Use in source · foundations.tex, line 240
For probability laws with finite second moment, write Wtwo(ν,μ)^2 =inf_π∈Π(ν,μ)∫ x-z ^2 dπ(x,z), where Π(ν,μ) is the set of transport plans with the stated marginals. The formal source defines the squared quantity as a nonnegative extended-real infimum and obtains the distance by a square-root operation. The explicit finite Gaussian coupling proves that the quantities considered here are finite. The notation Wtwo in the paper is the corresponding finite distance.
Exact mathematical passage
\Wtwo(\nu,\mu)^2 =\inf_{\pi\in\Pi(\nu,\mu)}\int\|x-z\|^2\,d\pi(x,z),
\inf_{\pi\in\Pi(\nu,\mu)}Use in source · 1 passage
Search aliases: inf_π∈Π(ν,μ) inf pi in Pi nu mu
Use in source · foundations.tex, line 240
For probability laws with finite second moment, write Wtwo(ν,μ)^2 =inf_π∈Π(ν,μ)∫ x-z ^2 dπ(x,z), where Π(ν,μ) is the set of transport plans with the stated marginals. The formal source defines the squared quantity as a nonnegative extended-real infimum and obtains the distance by a square-root operation. The explicit finite Gaussian coupling proves that the quantities considered here are finite. The notation Wtwo in the paper is the corresponding finite distance.
Exact mathematical passage
\Wtwo(\nu,\mu)^2 =\inf_{\pi\in\Pi(\nu,\mu)}\int\|x-z\|^2\,d\pi(x,z),
JUse in source · 10 passages
Search aliases: J
Use in source · solver.tex, line 547
The rotated fixture makes the prior singular and the packets non-coordinate: P=J=1 · 1 1 · 1, H=I, R=I, m=0, y=1 -1. It uses the rectangular prior factor L=(1,1)^ T, zero noise factor, and σ=1. Both output and input packet families are Q_+=frac121 · 1
Exact mathematical passage
P=J=\begin{pmatrix}1&1\\1&1\end{pmatrix},\quad H=I, \quad R=I,\quad m=0,\quad y=\begin{pmatrix}1\\-1\end{pmatrix}.
jUse in source · 2 passages
Search aliases: j
Use in source · foundations.tex, line 12
We use Euclidean vector norms and the squared Frobenius energy E(A)=FrobA^2=∑_i,jA_ij^2. The distinction between these norms matters. A matrix energy is a finite sum of scalar squares that can be evaluated exactly on rational inputs. An operator norm is used in the proof that this energy controls distribution error. The certificate never asks a producer to supply an unverified operator norm or an approximate eigenvalue calculation.
Exact mathematical passage
E(A)=\Frob{A}^2=\sum_{i,j}A_{ij}^2. \label{eq:foundation-energy}
KUse in source · 30 passages
Search aliases: K
Use in source · foundations.tex, line 19
For an observed value y, put d=y-Hm, S=HPH^top+R, K=PH^top S^-1. The matrix S is the innovation covariance. It is positive definite because, for every nonzero z∈R^p, z^top Sz=(H^top z)^top P(H^top z)+z^top Rz>0. Consequently the inverse in the definition of K exists even when P has a nontrivial nullspace or H has deficient rank. Every inverse used by the posterior argument is an inverse on the observation space. This is the structural reason singular priors are supported.
Exact mathematical passage
d=y-Hm,\qquad S=HPH^\top+R,\qquad K=PH^\top S^{-1}. \label{eq:foundation-innovation}
kUse in source · 1 passage
Search aliases: k
Use in source · solver.tex, line 243
st ε^2/4 at the current state. If the test fails and fuel remains, it advances once and decrements fuel. At fuel zero it still tests the last permitted state. This convention permits success after exactly N updates. pathsearch_score proves that every returned state passes the score condition. pathsearch_origin proves that a returned state is an actual trajectory state at some k≤ N. Finally, pathsearch_complete proves that a passing score at the last permitted state forces the search to return so…
Exact mathematical passage
k\le N
K^\topUse in source · 8 passages
Search aliases: K^top top
Use in source · foundations.tex, line 83
The covariance C_* admits the Joseph representation C_*=(I_n-KH)P(I_n-KH)^top+KRK^top. Each term on the right is positive semidefinite. Therefore C_*succeq0, including at the singular boundary. This avoids any proof based on P^-1 or C_*^-1.
Exact mathematical passage
C_*=(I_n-KH)P(I_n-KH)^\top+KRK^\top. \label{eq:foundation-exact-joseph}
LUse in source · 9 passages
Search aliases: L
Use in source · foundations.tex, line 31
The completed executable contract represents its model by rational matrices and vectors. Its input consists of H, m, y, a prior factor L∈Q^n× r, a noise factor N∈Q^p× s, and a rational number σ. The covariance matrices are derived from these inputs: P=LL^top, R=NN^top+σ I_p, σ>0. The factor dimensions r and s are finite and need not equal the state or observation dimension. The factors may have dependent columns or zero entries. The prior factor is allowed to have rank below n. The positive floo…
Exact mathematical passage
L\in\Q^{n\times r}
L^{\mathsf T}Use in source · 2 passages
Search aliases: L^ T mathsf
Use in source · introduction.tex, line 19
The problem is one Gaussian observation update. Write the prior as X∼ N(m,P), Y=HX+η, where the centered Gaussian noise η is independent of X. The representation uses rational factors P=LL^ T, R=NN^ T+σ I, σ>0. All data supplied to the executable construction, including m,H,L,N,σ and the observation y, are rational. Finite state and observation index types determine the matrix shapes. There is no requirement that H be square or that P be invertible. The innovation matrix is S=HPH^ T+R. Its posit…
Exact mathematical passage
P=LL^{\mathsf T},\qquad R=NN^{\mathsf T}+\sigma I, \qquad \sigma>0.
L^\topUse in source · 2 passages
Search aliases: L^top top
Use in source · foundations.tex, line 32
The completed executable contract represents its model by rational matrices and vectors. Its input consists of H, m, y, a prior factor L∈Q^n× r, a noise factor N∈Q^p× s, and a rational number σ. The covariance matrices are derived from these inputs: P=LL^top, R=NN^top+σ I_p, σ>0. The factor dimensions r and s are finite and need not equal the state or observation dimension. The factors may have dependent columns or zero entries. The prior factor is allowed to have rank below n. The positive floo…
Exact mathematical passage
P=LL^\top,\qquad R=NN^\top+\sigma I_p,\qquad \sigma>0. \label{eq:foundation-factor-model}
\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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\land
\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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\lor
\lVertUse in source · 3 passages
Search aliases: lVert
Use in source · solver.tex, line 31
Preprocessing forms three model-dependent constants: τ=frac1σ+tr S, T=I-τ S, w=fracσ+lVert vrVert^2σ^2. All are rational. They are the fields of the record pathKomorebi.CachedPosterior.Kernel, produced by pathKomorebi.CachedPosterior.prepare. The correctness theorems use this actual preparation, rather than an arbitrary record whose fields happen to have the same names. A wrong transition matrix or weight would invalidate the correspondence between the stored score and the posterior certificate.
Exact mathematical passage
\tau=\frac{1}{\sigma+\tr S},\qquad T=I-\tau S, \qquad w=\frac{\sigma+\lVert v\rVert^{2}}{\sigma^{2}}. \label{eq:solver-kernel}
MUse in source · 7 passages
Search aliases: M
Use in source · foundations.tex, line 442
The first Boolean function is checkCandidate(M,Q,D,c) =decide(ValidCandidate(M,Q,D,c)). It recomputes the finite obligations for the explicit model, packets, and candidate. A claimed successful producer run is not one of its inputs. The equivalence pathcheckCandidate_eq_true states that its true result is exactly candidate validity.
Exact mathematical passage
\texttt{checkCandidate}(M,Q,D,c) =\texttt{decide}(\texttt{ValidCandidate}(M,Q,D,c)).
mUse in source · 31 passages
Search aliases: m
Use in source · foundations.tex, line 4
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
\mathcal N(m,P)
m_BUse in source · 7 passages
Search aliases: m_B
Use in source · foundations.tex, line 159
Let B∈R^n× p be an arbitrary gain candidate. It need not solve the innovation equation and need not have been produced by the packet algorithm. Define m_B · =m+Bd, C_B · =(I_n-BH)P(I_n-BH)^top+BRB^top, μ_B · = N(m_B,C_B). Every C_B is positive semidefinite, since it is a sum of covariance congruences. Thus every candidate gain determines a genuine Gaussian law. This is useful for certification: an imperfect candidate is a valid distribution with a measurable error, rather than a covariance formu…
Exact mathematical passage
m_B&=m+Bd,\label{eq:foundation-approx-mean}\\ C_B&=(I_n-BH)P(I_n-BH)^\top+BRB^\top,\label{eq:foundation-approx-cov}\\ \mu_B&=\mathcal N(m_B,C_B).\label{eq:foundation-approx-law}
\midUse in source · 1 passage
Search aliases: mid
Use in source · common.tex, line 48
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\mid
NUse in source · 11 passages
Search aliases: N
Use in source · foundations.tex, line 31
The completed executable contract represents its model by rational matrices and vectors. Its input consists of H, m, y, a prior factor L∈Q^n× r, a noise factor N∈Q^p× s, and a rational number σ. The covariance matrices are derived from these inputs: P=LL^top, R=NN^top+σ I_p, σ>0. The factor dimensions r and s are finite and need not equal the state or observation dimension. The factors may have dependent columns or zero entries. The prior factor is allowed to have rank below n. The positive floo…
Exact mathematical passage
N\in\Q^{p\times s}
\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
\mathcal NUse in source · 15 passages
Search aliases: N mathcal
Use in source · foundations.tex, line 4
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
\mathcal N(m,P)
nUse in source · 34 passages
Search aliases: n
Use in source · foundations.tex, line 4
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
\R^n
N^{\mathsf T}Use in source · 2 passages
Search aliases: N^ T mathsf
Use in source · introduction.tex, line 19
The problem is one Gaussian observation update. Write the prior as X∼ N(m,P), Y=HX+η, where the centered Gaussian noise η is independent of X. The representation uses rational factors P=LL^ T, R=NN^ T+σ I, σ>0. All data supplied to the executable construction, including m,H,L,N,σ and the observation y, are rational. Finite state and observation index types determine the matrix shapes. There is no requirement that H be square or that P be invertible. The innovation matrix is S=HPH^ T+R. Its posit…
Exact mathematical passage
P=LL^{\mathsf T},\qquad R=NN^{\mathsf T}+\sigma I, \qquad \sigma>0.
N^\topUse in source · 2 passages
Search aliases: N^top top
Use in source · foundations.tex, line 32
The completed executable contract represents its model by rational matrices and vectors. Its input consists of H, m, y, a prior factor L∈Q^n× r, a noise factor N∈Q^p× s, and a rational number σ. The covariance matrices are derived from these inputs: P=LL^top, R=NN^top+σ I_p, σ>0. The factor dimensions r and s are finite and need not equal the state or observation dimension. The factors may have dependent columns or zero entries. The prior factor is allowed to have rank below n. The positive floo…
Exact mathematical passage
P=LL^\top,\qquad R=NN^\top+\sigma I_p,\qquad \sigma>0. \label{eq:foundation-factor-model}
\negUse in source · 1 passage
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\neg
\mathrm{op}Use in source · 2 passages
Search aliases: op mathrm
Use in source · foundations.tex, line 62
p gives z^top Sz≥σ z ^2 for all z∈R^p. Let x=S^-1v. Then Sx=v, and the Cauchy--Schwarz inequality yields σ x ^2≤ x^top Sx=x^top v≤ x v . If x=0 the desired bound is immediate. Otherwise division by σ x gives S^-1v ≤σ^-1 v . Hence S^-1 _op≤σ^-1. This elementary estimate supplies an explicit certificate constant without computing the inverse. The inverse exists in the semantic proof, while the executable stopping test uses σ, an innovation vector, and a residual. This separation allows an approxim…
Exact mathematical passage
\|S^{-1}\|_{\mathrm{op}}\le\sigma^{-1}. \label{eq:foundation-inverse-bound}
\mathrm{out}Use in source · 3 passages
Search aliases: out mathrm
Use in source · solver.tex, line 376
Each output arithmetic expression has a precision-independent budget coefficient. The source sums all mean coefficients and all covariance coefficients to obtain C_out, defined by pathoutputCoefficient. Every individual coefficient is nonnegative and no greater than this sum. It chooses p_out=precisionFor(C_out,δ) and evaluates the output graph at that precision. Since every entry radius is bounded by its coefficient times 2^-p_out, the same integer precision bounds all radii by δ. The declarati…
Exact mathematical passage
C_{\mathrm{out}}
PUse in source · 52 passages
Search aliases: P
Use in source · foundations.tex, line 4
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
\mathcal N(m,P)
P^{-1}Use in source · 1 passage
Search aliases: P^-1
Use in source · foundations.tex, line 87
The covariance C_* admits the Joseph representation C_*=(I_n-KH)P(I_n-KH)^top+KRK^top. Each term on the right is positive semidefinite. Therefore C_*succeq0, including at the singular boundary. This avoids any proof based on P^-1 or C_*^-1.
Exact mathematical passage
P^{-1}
p_*Use in source · 2 passages
Search aliases: p_*
Use in source · solver.tex, line 305
For final verification, the solver appends p_* = sufficientPrecision(M,Q,D,B,ε^2/4). At its returned search state, a(B)≤ε^2/4. The fallback guarantees inflation at most another ε^2/4, so widehat a_p_*(B)≤ε^2/2≤ε^2. Positive ε gives a positive inflation allowance. Valid model and packet setup give the candidate check, while this inequality gives the tolerance check. The declarations pathcertifyRounded_of_slack and pathcertifyGain_complete establish that the fallback must succeed.
Exact mathematical passage
p_* = \operatorname{sufficientPrecision}(M,Q,D,B,\varepsilon^2/4).
P_BUse in source · 3 passages
Search aliases: P_B
Use in source · introduction.tex, line 30
For a rational gain B, the Joseph approximation has mean and covariance m_B · =m+B(y-Hm), P_B · =(I-BH)P(I-BH)^ T+BRB^ T. Its covariance is positive semidefinite by construction. The approximation is a measure, rather than a collection of unqualified decimal entries. The exact gain K=PH^ TS^-1 identifies the familiar Gaussian posterior parameters. Later sections prove that this explicit Gaussian kernel disintegrates the actual forward joint law. This gives a posterior version defined at every su…
Exact mathematical passage
m_B&=m+B(y-Hm),\\ P_B&=(I-BH)P(I-BH)^{\mathsf T}+BRB^{\mathsf T}.
p_{\mathrm{out}}Use in source · 2 passages
Search aliases: p_out mathrm
Use in source · solver.tex, line 378
Each output arithmetic expression has a precision-independent budget coefficient. The source sums all mean coefficients and all covariance coefficients to obtain C_out, defined by pathoutputCoefficient. Every individual coefficient is nonnegative and no greater than this sum. It chooses p_out=precisionFor(C_out,δ) and evaluates the output graph at that precision. Since every entry radius is bounded by its coefficient times 2^-p_out, the same integer precision bounds all radii by δ. The declarati…
Exact mathematical passage
p_{\mathrm{out}}=\operatorname{precisionFor}(C_{\mathrm{out}},\delta)
\mathrm{posterior}Use in source · 1 passage
Search aliases: posterior mathrm
Use in source · foundations.tex, line 458
andidate checking] Let M be a factor-coded rational model, Q,D rational packet families, and c a rational candidate. If both pathcheckCandidate M Q D c and pathcheckTolerance M c epsilon return true, then the exact real posterior version represented by M and the exact real Joseph Gaussian represented by the gain of c satisfy Wtwo(M.posterior,M.approximation(c.gain)) ≤ε. Here ε is the real interpretation of the rational tolerance. The first check gives positivity of the floor and the four finite …
Exact mathematical passage
\Wtwo(M.\mathrm{posterior},M.\mathrm{approximation}(c.\mathrm{gain})) \le\varepsilon. \label{eq:foundation-rational-soundness}
\QUse in source · 3 passages
Search aliases: Q
Use in source · foundations.tex, line 31
The completed executable contract represents its model by rational matrices and vectors. Its input consists of H, m, y, a prior factor L∈Q^n× r, a noise factor N∈Q^p× s, and a rational number σ. The covariance matrices are derived from these inputs: P=LL^top, R=NN^top+σ I_p, σ>0. The factor dimensions r and s are finite and need not equal the state or observation dimension. The factors may have dependent columns or zero entries. The prior factor is allowed to have rank below n. The positive floo…
Exact mathematical passage
L\in\Q^{n\times r}
\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
\Q^{n\times r}Use in source · 1 passage
Search aliases: Q^n× r Q times
Use in source · foundations.tex, line 31
The completed executable contract represents its model by rational matrices and vectors. Its input consists of H, m, y, a prior factor L∈Q^n× r, a noise factor N∈Q^p× s, and a rational number σ. The covariance matrices are derived from these inputs: P=LL^top, R=NN^top+σ I_p, σ>0. The factor dimensions r and s are finite and need not equal the state or observation dimension. The factors may have dependent columns or zero entries. The prior factor is allowed to have rank below n. The positive floo…
Exact mathematical passage
L\in\Q^{n\times r}
\Q^{p\times s}Use in source · 1 passage
Search aliases: Q^p× s Q times
Use in source · foundations.tex, line 31
The completed executable contract represents its model by rational matrices and vectors. Its input consists of H, m, y, a prior factor L∈Q^n× r, a noise factor N∈Q^p× s, and a rational number σ. The covariance matrices are derived from these inputs: P=LL^top, R=NN^top+σ I_p, σ>0. The factor dimensions r and s are finite and need not equal the state or observation dimension. The factors may have dependent columns or zero entries. The prior factor is allowed to have rank below n. The positive floo…
Exact mathematical passage
N\in\Q^{p\times s}
Q_+Use in source · 2 passages
Search aliases: Q_+
Use in source · solver.tex, line 553
-1. It uses the rectangular prior factor L=(1,1)^ T, zero noise factor, and σ=1. Both output and input packet families are Q_+=frac121 · 1 1 · 1, Q_-=frac121 · -1 -1 · 1. These project onto the common and antisymmetric directions. They are rational, self-adjoint, orthogonal, and complete. The prior has rank one, but the innovation matrix S=I+J is positive definite because of the positive noise floor.
Exact mathematical passage
Q_+=\frac12\begin{pmatrix}1&1\\1&1\end{pmatrix},\qquad Q_-=\frac12\begin{pmatrix}1&-1\\-1&1\end{pmatrix}.
Q_-Use in source · 2 passages
Search aliases: Q_-
Use in source · solver.tex, line 553
-1. It uses the rectangular prior factor L=(1,1)^ T, zero noise factor, and σ=1. Both output and input packet families are Q_+=frac121 · 1 1 · 1, Q_-=frac121 · -1 -1 · 1. These project onto the common and antisymmetric directions. They are rational, self-adjoint, orthogonal, and complete. The prior has rank one, but the innovation matrix S=I+J is positive definite because of the positive noise floor.
Exact mathematical passage
Q_+=\frac12\begin{pmatrix}1&1\\1&1\end{pmatrix},\qquad Q_-=\frac12\begin{pmatrix}1&-1\\-1&1\end{pmatrix}.
Q_{a'}Use in source · 2 passages
Search aliases: Q_a'
Use in source · foundations.tex, line 325
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'), D_b^top · =D_b, · D_b^2 · =D_b, · D_bD_b' · =0 (b≠ b'). Completeness is a separate condition: ∑_a∈ AQ_a=I_n, ∑_b∈ BD_b=I_p. The self-adjoint condition makes these Euclidean orthogonal projectors. Idempot…
Exact mathematical passage
Q_a^\top&=Q_a,& Q_a^2&=Q_a,& Q_aQ_{a'}&=0\quad(a\ne a'),\label{eq:foundation-output-packets}\\ D_b^\top&=D_b,& D_b^2&=D_b,& D_bD_{b'}&=0\quad(b\ne b').\label{eq:foundation-input-packets}
Q_a^2Use in source · 2 passages
Search aliases: Q_a^2
Use in source · foundations.tex, line 325
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'), D_b^top · =D_b, · D_b^2 · =D_b, · D_bD_b' · =0 (b≠ b'). Completeness is a separate condition: ∑_a∈ AQ_a=I_n, ∑_b∈ BD_b=I_p. The self-adjoint condition makes these Euclidean orthogonal projectors. Idempot…
Exact mathematical passage
Q_a^\top&=Q_a,& Q_a^2&=Q_a,& Q_aQ_{a'}&=0\quad(a\ne a'),\label{eq:foundation-output-packets}\\ D_b^\top&=D_b,& D_b^2&=D_b,& D_bD_{b'}&=0\quad(b\ne b').\label{eq:foundation-input-packets}
Q_a^\topUse in source · 1 passage
Search aliases: Q_a^top top
Use in source · foundations.tex, line 325
A packet family in this release is a finite collection of self-adjoint, pairwise disjoint idempotent matrices. Let {Q_a:a∈ A} act on the state space and {D_b:b∈ B} act on the observation space. For each family, the structural conditions are Q_a^top · =Q_a, · Q_a^2 · =Q_a, · Q_aQ_a' · =0 (a≠ a'), D_b^top · =D_b, · D_b^2 · =D_b, · D_bD_b' · =0 (b≠ b'). Completeness is a separate condition: ∑_a∈ AQ_a=I_n, ∑_b∈ BD_b=I_p. The self-adjoint condition makes these Euclidean orthogonal projectors. Idempot…
Exact mathematical passage
Q_a^\top&=Q_a,& Q_a^2&=Q_a,& Q_aQ_{a'}&=0\quad(a\ne a'),\label{eq:foundation-output-packets}\\ D_b^\top&=D_b,& D_b^2&=D_b,& D_bD_{b'}&=0\quad(b\ne b').\label{eq:foundation-input-packets}
Q_bUse in source · 2 passages
Search aliases: Q_b
Use in source · solver.tex, line 103
in [source reference] is valid. By cache validity, G_a=Q_aF(B), so the gain update is the exact packet step B'=B+τ Q_aF(B). Expand its residual: F(B')=F(B)-τ Q_aF(B)S. Multiplication on the left by the selected projector gives Q_aF(B')=Q_aF(B)-τ Q_a^2F(B)S =G_a(I-τ S)=G_aT. For b≠ a, mutual orthogonality gives Q_bQ_a=0 and hence Q_bF(B')=Q_bF(B)=G_b. This proves every residual equality in the new cache. Its energy equalities hold because the selected energy is evaluated from its new residual and…
Exact mathematical passage
Q_bQ_a=0
RUse in source · 26 passages
Search aliases: R
Use in source · foundations.tex, line 5
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
Y=HX+V,\qquad V\sim\mathcal N(0,R),\qquad V\text{ independent of }X. \label{eq:foundation-model}
\RUse in source · 12 passages
Search aliases: R
Use in source · foundations.tex, line 4
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
\R^n
\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^2Use in source · 1 passage
Search aliases: R^2 R
Use in source · foundations.tex, line 426
For example, take the coordinate projectors onto the two axes of R^2. A residual matrix with a nonzero second row has zero energy in the first output packet. Certifying that first packet alone says nothing about the omitted row. Completeness and a bound for every packet are what change local information into a global posterior guarantee. The exact checker tests those structural and local obligations; it does not accept a producer's assertion that a chosen subset happened to be representative.
Exact mathematical passage
\R^2
\R^nUse in source · 1 passage
Search aliases: R^n R
Use in source · foundations.tex, line 4
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
\R^n
r^nUse in source · 4 passages
Search aliases: r^n
Use in source · solver.tex, line 191
The transition contracts every residual matrix: E(XT)≤ qE(X). If label a is updated, its residual energy contracts by this inequality and all other output residuals remain unchanged. Orthogonal energy accounting gives E(F(B'))≤ E(F(B))-(1-q)e_a. Because a is a maximum, e_a≥ E(F(B))/A_count. It follows that E(F(B'))≤ rE(F(B)), a(B_n)≤ r^na(B_0). The energy share is pathselected_energy_share; one-step contraction is pathgreedy_energy_contract; and the score estimate is pathgreedy_score_geometric. …
Exact mathematical passage
E(F(B'))\le rE(F(B)),\qquad a(B_n)\le r^na(B_0). \label{eq:solver-geometric}
\R^{n\times n}Use in source · 1 passage
Search aliases: R^n× n R times
Use in source · foundations.tex, line 9
e inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approxim…
Exact mathematical passage
P\in\R^{n\times n}
\R^{n\times p}Use in source · 3 passages
Search aliases: R^n× p R times
Use in source · foundations.tex, line 158
Let B∈R^n× p be an arbitrary gain candidate. It need not solve the innovation equation and need not have been produced by the packet algorithm. Define m_B · =m+Bd,
Exact mathematical passage
B\in\R^{n\times p}
\R^pUse in source · 3 passages
Search aliases: R^p R
Use in source · foundations.tex, line 4
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
\R^p
\R^{p\times n}Use in source · 1 passage
Search aliases: R^p× n R times
Use in source · foundations.tex, line 9
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
H\in\R^{p\times n}
\mathrm{round}Use in source · 1 passage
Search aliases: round mathrm
Use in source · solver.tex, line 659
Writing d for the number of gain entries and h_t=2^-t, the source establishes an all-iteration tracking bound E(widetilde B_n-B_n^exact) ≤frac6d h_t^2(1-q)^2. Its residual-score comparison has the form a(widetilde B_n)≤2a(B_n^exact)+C_roundh_t^2, C_round= frac12dE(S)w(1-q)^2. The source names are pathroundedGain_tracking, pathroundoffScoreCoeff, and pathrounded_score_compare. The first term is ideal progress. The second is a precision-dependent floor. Both are needed.
Exact mathematical passage
a(\widetilde B_n)\le2a(B_n^{\mathrm{exact}})+C_{\mathrm{round}}h_t^2, \qquad C_{\mathrm{round}}= \frac{12dE(S)w}{(1-q)^2}.
\rVertUse in source · 3 passages
Search aliases: rVert
Use in source · solver.tex, line 31
Preprocessing forms three model-dependent constants: τ=frac1σ+tr S, T=I-τ S, w=fracσ+lVert vrVert^2σ^2. All are rational. They are the fields of the record pathKomorebi.CachedPosterior.Kernel, produced by pathKomorebi.CachedPosterior.prepare. The correctness theorems use this actual preparation, rather than an arbitrary record whose fields happen to have the same names. A wrong transition matrix or weight would invalidate the correspondence between the stored score and the posterior certificate.
Exact mathematical passage
\tau=\frac{1}{\sigma+\tr S},\qquad T=I-\tau S, \qquad w=\frac{\sigma+\lVert v\rVert^{2}}{\sigma^{2}}. \label{eq:solver-kernel}
\rVert^2Use in source · 2 passages
Search aliases: rVert^2 rVert
Use in source · solver.tex, line 64
Orthogonal complete packets account for the whole energy: ∑_a∈ AE(Q_aF)=E(F). Consequently a valid cache has t=E(F(B)) and s(c)=E(F(B))fracσ+lVert vrVert^2σ^2=a(B). The right-hand side is the exact residual score used by the posterior error certificate. The declarations pathtotal_eq_residual_energy and pathscore_eq establish these two identifications. The total is therefore a meaningful global stopping signal even though only one of its summands changes in an iteration.
Exact mathematical passage
s(c)=E(F(B))\frac{\sigma+\lVert v\rVert^2}{\sigma^2}=a(B). \label{eq:solver-score}
\rVert^{2}Use in source · 1 passage
Search aliases: rVert^2 rVert
Use in source · solver.tex, line 31
Preprocessing forms three model-dependent constants: τ=frac1σ+tr S, T=I-τ S, w=fracσ+lVert vrVert^2σ^2. All are rational. They are the fields of the record pathKomorebi.CachedPosterior.Kernel, produced by pathKomorebi.CachedPosterior.prepare. The correctness theorems use this actual preparation, rather than an arbitrary record whose fields happen to have the same names. A wrong transition matrix or weight would invalidate the correspondence between the stored score and the posterior certificate.
Exact mathematical passage
\tau=\frac{1}{\sigma+\tr S},\qquad T=I-\tau S, \qquad w=\frac{\sigma+\lVert v\rVert^{2}}{\sigma^{2}}. \label{eq:solver-kernel}
S^{-1}Use in source · 14 passages
Search aliases: S^-1
Use in source · foundations.tex, line 19
For an observed value y, put d=y-Hm, S=HPH^top+R, K=PH^top S^-1. The matrix S is the innovation covariance. It is positive definite because, for every nonzero z∈R^p, z^top Sz=(H^top z)^top P(H^top z)+z^top Rz>0. Consequently the inverse in the definition of K exists even when P has a nontrivial nullspace or H has deficient rank. Every inverse used by the posterior argument is an inverse on the observation space. This is the structural reason singular priors are supported.
Exact mathematical passage
d=y-Hm,\qquad S=HPH^\top+R,\qquad K=PH^\top S^{-1}. \label{eq:foundation-innovation}
\succUse in source · 4 passages
Search aliases: succ
Use in source · foundations.tex, line 9
t state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approximation or assign an artificial inverse to its covariance.
Exact mathematical passage
R\succ0
\succeqUse in source · 6 passages
Search aliases: succeq
Use in source · foundations.tex, line 9
imensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approximation or assign an artificial inverse to its covariance.
Exact mathematical passage
P\succeq0
\operatorname{sufficientPrecision}Use in source · 1 passage
Search aliases: sufficientPrecision operatorname
Use in source · solver.tex, line 305
For final verification, the solver appends p_* = sufficientPrecision(M,Q,D,B,ε^2/4). At its returned search state, a(B)≤ε^2/4. The fallback guarantees inflation at most another ε^2/4, so widehat a_p_*(B)≤ε^2/2≤ε^2. Positive ε gives a positive inflation allowance. Valid model and packet setup give the candidate check, while this inequality gives the tolerance check. The declarations pathcertifyRounded_of_slack and pathcertifyGain_complete establish that the fallback must succeed.
Exact mathematical passage
p_* = \operatorname{sufficientPrecision}(M,Q,D,B,\varepsilon^2/4).
TUse in source · 11 passages
Search aliases: T
Use in source · foundations.tex, line 204
Take independent centered Gaussian variables U∼ N(0,P) and V∼ N(0,R). For each gain B, define the mathematical affine random variable T_B=m+Bd+(I_n-BH)U-BV. Its mean is m_B and its covariance is C_B, so its law is μ_B. At B=K, the exact Joseph identity identifies its law with ν_y. The pair (T_K,T_B), using the same inputs (U,V), is therefore an actual transport plan between the exact posterior version and the approximate law.
Exact mathematical passage
T_B=m+Bd+(I_n-BH)U-BV. \label{eq:foundation-shared-sample}
\mathsf TUse in source · 16 passages
Search aliases: T mathsf
Use in source · introduction.tex, line 19
The problem is one Gaussian observation update. Write the prior as X∼ N(m,P), Y=HX+η, where the centered Gaussian noise η is independent of X. The representation uses rational factors P=LL^ T, R=NN^ T+σ I, σ>0. All data supplied to the executable construction, including m,H,L,N,σ and the observation y, are rational. Finite state and observation index types determine the matrix shapes. There is no requirement that H be square or that P be invertible. The innovation matrix is S=HPH^ T+R. Its posit…
Exact mathematical passage
P=LL^{\mathsf T},\qquad R=NN^{\mathsf T}+\sigma I, \qquad \sigma>0.
t'Use in source · 2 passages
Search aliases: t'
Use in source · solver.tex, line 75
For a selected label a, the executed update is B' · =B+τ G_a, · G'_a · =G_aT, · e'_a · =E(G'_a),nonumber G'_b · =G_b (b≠ a), · e'_b · =e_b (b≠ a), · t' · =t-e_a+e'_a. This is the definition pathKomorebi.CachedPosterior.step. It computes the new selected residual from the old selected residual and the precomputed transition. It retains unselected entries and updates the scalar total by a difference. The implementation does not define its new state by recomputing F(B') and projecting that matrix o…
Exact mathematical passage
B'&=B+\tau G_a, &G'_a&=G_aT, &e'_a&=E(G'_a),\nonumber\\ G'_b&=G_b\quad(b\ne a), &e'_b&=e_b\quad(b\ne a), &t'&=t-e_a+e'_a. \label{eq:solver-cache-step}
T_BUse in source · 4 passages
Search aliases: T_B
Use in source · foundations.tex, line 204
Take independent centered Gaussian variables U∼ N(0,P) and V∼ N(0,R). For each gain B, define the mathematical affine random variable T_B=m+Bd+(I_n-BH)U-BV. Its mean is m_B and its covariance is C_B, so its law is μ_B. At B=K, the exact Joseph identity identifies its law with ν_y. The pair (T_K,T_B), using the same inputs (U,V), is therefore an actual transport plan between the exact posterior version and the approximate law.
Exact mathematical passage
T_B=m+Bd+(I_n-BH)U-BV. \label{eq:foundation-shared-sample}
T_KUse in source · 3 passages
Search aliases: T_K
Use in source · foundations.tex, line 208
independent centered Gaussian variables U∼ N(0,P) and V∼ N(0,R). For each gain B, define the mathematical affine random variable T_B=m+Bd+(I_n-BH)U-BV. Its mean is m_B and its covariance is C_B, so its law is μ_B. At B=K, the exact Joseph identity identifies its law with ν_y. The pair (T_K,T_B), using the same inputs (U,V), is therefore an actual transport plan between the exact posterior version and the approximate law.
Exact mathematical passage
(T_K,T_B)
\topUse in source · 39 passages
Search aliases: top
Use in source · foundations.tex, line 19
For an observed value y, put d=y-Hm, S=HPH^top+R, K=PH^top S^-1. The matrix S is the innovation covariance. It is positive definite because, for every nonzero z∈R^p, z^top Sz=(H^top z)^top P(H^top z)+z^top Rz>0. Consequently the inverse in the definition of K exists even when P has a nontrivial nullspace or H has deficient rank. Every inverse used by the posterior argument is an inverse on the observation space. This is the structural reason singular priors are supported.
Exact mathematical passage
d=y-Hm,\qquad S=HPH^\top+R,\qquad K=PH^\top S^{-1}. \label{eq:foundation-innovation}
\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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\triangleright
UUse in source · 15 passages
Search aliases: U
Use in source · foundations.tex, line 203
Take independent centered Gaussian variables U∼ N(0,P) and V∼ N(0,R). For each gain B, define the mathematical affine random variable T_B=m+Bd+(I_n-BH)U-BV. Its mean is m_B and its covariance is C_B, so its law is μ_B. At B=K, the exact Joseph identity identifies its law with ν_y. The pair (T_K,T_B), using the same inputs (U,V), is therefore an actual transport plan between the exact posterior version and the approximate law.
Exact mathematical passage
U\sim\mathcal N(0,P)
uUse in source · 7 passages
Search aliases: u
Use in source · foundations.tex, line 382
Suppose a producer supplies values u_ab and v with proved inequalities E(F_ab(B))≤ u_ab, d ^2≤ v. Completeness and nonnegative energy imply E(F(B))≤ U, U=∑_a,bu_ab. Each u_ab is nonnegative because it bounds a nonnegative quantity. Likewise v≥0. The score widehat a(B)=Ufracσ+vσ^2 therefore bounds a(B) and hence the squared posterior distance. If U(σ+v)≤ε^2σ^2, ε≥0, the same law tolerance follows.
Exact mathematical passage
u_{ab}
u_{ab}Use in source · 7 passages
Search aliases: u_ab
Use in source · foundations.tex, line 382
Suppose a producer supplies values u_ab and v with proved inequalities E(F_ab(B))≤ u_ab, d ^2≤ v. Completeness and nonnegative energy imply E(F(B))≤ U, U=∑_a,bu_ab. Each u_ab is nonnegative because it bounds a nonnegative quantity. Likewise v≥0. The score widehat a(B)=Ufracσ+vσ^2 therefore bounds a(B) and hence the squared posterior distance. If U(σ+v)≤ε^2σ^2, ε≥0, the same law tolerance follows.
Exact mathematical passage
u_{ab}
\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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\uparrow
VUse in source · 15 passages
Search aliases: V
Use in source · foundations.tex, line 5
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
Y=HX+V,\qquad V\sim\mathcal N(0,R),\qquad V\text{ independent of }X. \label{eq:foundation-model}
vUse in source · 18 passages
Search aliases: v
Use in source · foundations.tex, line 57
The same σ that certifies positive noise also bounds the inverse innovation operator. Adding the positive semidefinite term HPH^top gives z^top Sz≥σ z ^2 for all z∈R^p. Let x=S^-1v. Then Sx=v, and the Cauchy--Schwarz inequality yields σ x ^2≤ x^top Sx=x^top v≤ x v . If x=0 the desired bound is immediate. Otherwise division by σ x gives S^-1v ≤σ^-1 v . Hence S^-1 _op≤σ^-1. This elementary estimate supplies an explicit certificate constant without computing the inverse. The inverse exists in the s…
Exact mathematical passage
x=S^{-1}v
V_*Use in source · 2 passages
Search aliases: V_*
Use in source · solver.tex, line 511
-78432 · 98041. It can be checked directly by substituting B_6 into [source reference]. Another useful check starts from the exact posterior covariance V_* = (4/3 · -2/3 -2/3 · 5/6). If B_*=(2/3,1/6)^ T is the exact gain, expansion of the Joseph expression gives V_B_6=V_*+6(B_6-B_*)(B_6-B_*)^ T. The gain discrepancy is B_*-B_6=(2/1029,1/2058)^ T, which produces the displayed matrix. This second calculation checks the sign of the off-diagonal entries and explains why the approximate covariance ha…
Exact mathematical passage
V_* = \left(\begin{smallmatrix}4/3&-2/3\\-2/3&5/6\end{smallmatrix}\right)
V_BUse in source · 1 passage
Search aliases: V_B
Use in source · solver.tex, line 357
A useful posterior output contains more than a passing gain. For the returned rational gain B, the parameter stage represents μ_B · =m+B(y-Hm),nonumber V_B · =(I-BH)P(I-BH)^ T+BRB^ T. These are the mean and Joseph covariance of the same Gaussian law certified by the Wasserstein statement. The covariance is positive semidefinite under the model hypotheses even when the prior is singular. The declaration pathapproximation_eq_output_gaussian identifies this parameterized Gaussian with the approxima…
Exact mathematical passage
\mu_B&=m+B(y-Hm),\nonumber\\ V_B&=(I-BH)P(I-BH)^{\mathsf T}+BRB^{\mathsf T}. \label{eq:solver-joseph-output}
V_{B_4}Use in source · 1 passage
Search aliases: V_B_4
Use in source · solver.tex, line 585
The exact posterior mean is zero because Jy=0, and the returned approximation's mean is also zero. Its Joseph covariance is V_B_4=frac130379390625J. The exact posterior covariance is J/3. Both laws remain supported in the prior's one-dimensional common-direction subspace. This example therefore combines a singular prior, rotated packet selection, a nontrivial covariance approximation, and a zero mean without using an inverse of the singular prior covariance.
Exact mathematical passage
V_{B_4}=\frac{130379}{390625}J.
V_{B_6}Use in source · 2 passages
Search aliases: V_B_6
Use in source · solver.tex, line 504
The exact rational matrix enclosed by those covariance balls is V_B_6=frac1117649 156868 · -78432 -78432 · 98041. It can be checked directly by substituting B_6 into [source reference]. Another useful check starts from the exact posterior covariance V_* = (4/3 · -2/3
Exact mathematical passage
V_{B_6}=\frac{1}{117649} \begin{pmatrix}156868&-78432\\-78432&98041\end{pmatrix}.
v_jUse in source · 1 passage
Search aliases: v_j
Use in source · foundations.tex, line 266
[Frobenius energy controls the residual cost] If F∈R^n× p and Ssucceqσ I_psucc0, then FS^-1d ^2+tr(FS^-1F^top) ≤ E(F)(σ^-1+σ^-2 d ^2). For a vector v, rowwise Cauchy--Schwarz gives Fv ^2=∑_i(∑_jF_ijv_j)^2 ≤∑_i(∑_jF_ij^2) v ^2 =E(F) v ^2. Apply this with v=S^-1d and use [source reference] to obtain FS^-1d ^2≤ E(F)σ^-2 d ^2. If f_i is the transpose of the ith row of F, then tr(FS^-1F^top)=∑_i f_i^top S^-1f_i ≤∑_i f_i S^-1f_i ≤σ^-1∑_i f_i ^2. The last sum is E(F). Adding the two estimates proves th…
Exact mathematical passage
\|Fv\|^2=\sum_i\left(\sum_jF_{ij}v_j\right)^2 \le\sum_i\left(\sum_jF_{ij}^2\right)\|v\|^2 =E(F)\|v\|^2.
\mathrm{ver}Use in source · 2 passages
Search aliases: ver mathrm
Use in source · solver.tex, line 280
Let h_p=2^-p. The dyadic evaluator propagates rational centers and outward radii through its arithmetic graph. Its budget calculation supplies a nonnegative coefficient C_ver(M,Q,D,B) independent of p, with widehat a_p(B)≤ a(B)+C_ver(M,Q,D,B)h_p. Here widehat a_p is the actual rounded candidate score. The full expression for the coefficient is pathscoreRoundCoeff, built from packet residual energy and innovation-vector magnitude and radius budgets. It bounds the entire score graph, rather than r…
Exact mathematical passage
C_{\mathrm{ver}}(M,Q,D,B)
WUse in source · 2 passages
Search aliases: W
Use in source · closing.tex, line 15
Joseph gain · A valid Gaussian approximation and residual-based W_2 bound · Common-noise coupling and matrix bounds
Exact mathematical passage
W_2
W_2Use in source · 2 passages
Search aliases: W_2
Use in source · closing.tex, line 15
Joseph gain · A valid Gaussian approximation and residual-based W_2 bound · Common-noise coupling and matrix bounds
Exact mathematical passage
W_2
\widehat aUse in source · 4 passages
Search aliases: widehat a widehat
Use in source · foundations.tex, line 392
Suppose a producer supplies values u_ab and v with proved inequalities E(F_ab(B))≤ u_ab, d ^2≤ v. Completeness and nonnegative energy imply E(F(B))≤ U, U=∑_a,bu_ab. Each u_ab is nonnegative because it bounds a nonnegative quantity. Likewise v≥0. The score widehat a(B)=Ufracσ+vσ^2 therefore bounds a(B) and hence the squared posterior distance. If U(σ+v)≤ε^2σ^2, ε≥0, the same law tolerance follows.
Exact mathematical passage
\widehat a(B)=U\frac{\sigma+v}{\sigma^2} \label{eq:foundation-majorant-score}
\widehat a_pUse in source · 2 passages
Search aliases: widehat a_p widehat
Use in source · solver.tex, line 281
Let h_p=2^-p. The dyadic evaluator propagates rational centers and outward radii through its arithmetic graph. Its budget calculation supplies a nonnegative coefficient C_ver(M,Q,D,B) independent of p, with widehat a_p(B)≤ a(B)+C_ver(M,Q,D,B)h_p. Here widehat a_p is the actual rounded candidate score. The full expression for the coefficient is pathscoreRoundCoeff, built from packet residual energy and innovation-vector magnitude and radius budgets. It bounds the entire score graph, rather than r…
Exact mathematical passage
\widehat a_p(B)\le a(B)+C_{\mathrm{ver}}(M,Q,D,B)h_p. \label{eq:solver-inflation}
\widehat a_{p_*}Use in source · 1 passage
Search aliases: widehat a_p_* widehat
Use in source · solver.tex, line 310
For final verification, the solver appends p_* = sufficientPrecision(M,Q,D,B,ε^2/4). At its returned search state, a(B)≤ε^2/4. The fallback guarantees inflation at most another ε^2/4, so widehat a_p_*(B)≤ε^2/2≤ε^2. Positive ε gives a positive inflation allowance. Valid model and packet setup give the candidate check, while this inequality gives the tolerance check. The declarations pathcertifyRounded_of_slack and pathcertifyGain_complete establish that the fallback must succeed.
Exact mathematical passage
\widehat a_{p_*}(B)\le\varepsilon^2/2\le\varepsilon^2.
\widetilde BUse in source · 4 passages
Search aliases: widetilde B widetilde
Use in source · solver.tex, line 643
Core 1.0.0 already retains a different, completed rounded solver. Its update is a genuinely rounded full-gain Richardson step. It neither claims exact selective cache invariants nor selects a largest cached packet. Its declarations expose the whole-update defect instead. If widetilde B_n+1 is the rounded update and B_n+1^ideal is the exact full step at the current gain, then F(widetilde B_n+1)=F(widetilde B_n)T -(widetilde B_n+1-B_n+1^ideal)S. This is pathrounded_residual_step. The defect is exp…
Exact mathematical passage
\widetilde B_{n+1}
\widetilde B_nUse in source · 3 passages
Search aliases: widetilde B_n widetilde
Use in source · solver.tex, line 645
Core 1.0.0 already retains a different, completed rounded solver. Its update is a genuinely rounded full-gain Richardson step. It neither claims exact selective cache invariants nor selects a largest cached packet. Its declarations expose the whole-update defect instead. If widetilde B_n+1 is the rounded update and B_n+1^ideal is the exact full step at the current gain, then F(widetilde B_n+1)=F(widetilde B_n)T -(widetilde B_n+1-B_n+1^ideal)S. This is pathrounded_residual_step. The defect is exp…
Exact mathematical passage
F(\widetilde B_{n+1})=F(\widetilde B_n)T -(\widetilde B_{n+1}-B_{n+1}^{\mathrm{ideal}})S.
\widetilde B_{n+1}Use in source · 2 passages
Search aliases: widetilde B_n+1 widetilde
Use in source · solver.tex, line 643
Core 1.0.0 already retains a different, completed rounded solver. Its update is a genuinely rounded full-gain Richardson step. It neither claims exact selective cache invariants nor selects a largest cached packet. Its declarations expose the whole-update defect instead. If widetilde B_n+1 is the rounded update and B_n+1^ideal is the exact full step at the current gain, then F(widetilde B_n+1)=F(widetilde B_n)T -(widetilde B_n+1-B_n+1^ideal)S. This is pathrounded_residual_step. The defect is exp…
Exact mathematical passage
\widetilde B_{n+1}
\WtwoUse in source · 10 passages
Search aliases: Wtwo
Use in source · foundations.tex, line 240
For probability laws with finite second moment, write Wtwo(ν,μ)^2 =inf_π∈Π(ν,μ)∫ x-z ^2 dπ(x,z), where Π(ν,μ) is the set of transport plans with the stated marginals. The formal source defines the squared quantity as a nonnegative extended-real infimum and obtains the distance by a square-root operation. The explicit finite Gaussian coupling proves that the quantities considered here are finite. The notation Wtwo in the paper is the corresponding finite distance.
Exact mathematical passage
\Wtwo(\nu,\mu)^2 =\inf_{\pi\in\Pi(\nu,\mu)}\int\|x-z\|^2\,d\pi(x,z),
\Wtwo^2Use in source · 1 passage
Search aliases: Wtwo^2 Wtwo
Use in source · foundations.tex, line 305
ns are pathposterior_wasserstein2Sq_le_residual_energy and pathposterior_wasserstein2_le_of_residual_tolerance. Their hypotheses include the covariance assumptions, positivity of the floor, and the floor's quadratic interpretation. In the factor-coded program, those hypotheses are discharged by the represented factors and the checked positive scalar. The user does not supply the conclusion a(B)≥Wtwo^2 as an input promise.
Exact mathematical passage
a(B)\ge\Wtwo^2
XUse in source · 9 passages
Search aliases: X
Use in source · foundations.tex, line 4
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
X
xUse in source · 12 passages
Search aliases: x
Use in source · foundations.tex, line 38
This representation makes the covariance hypotheses concrete. For every x, x^top LL^top x= L^top x ^2≥0, x^top Rx= N^top x ^2+σ x ^2. Thus P is positive semidefinite and Rsucceqσ I_psucc0. These conclusions are proved from the factors; they are not additional statistical assumptions hidden inside a covariance record. The real semantics interprets each rational coordinate through the exact inclusion Q↪R. There is no intermediate conversion through hardware floating point.
Exact mathematical passage
x
x^\topUse in source · 2 passages
Search aliases: x^top top
Use in source · foundations.tex, line 39
This representation makes the covariance hypotheses concrete. For every x, x^top LL^top x= L^top x ^2≥0, x^top Rx= N^top x ^2+σ x ^2. Thus P is positive semidefinite and Rsucceqσ I_psucc0. These conclusions are proved from the factors; they are not additional statistical assumptions hidden inside a covariance record. The real semantics interprets each rational coordinate through the exact inclusion Q↪R. There is no intermediate conversion through hardware floating point.
Exact mathematical passage
x^\top LL^\top x=\|L^\top x\|^2\ge0, \qquad x^\top Rx=\|N^\top x\|^2+\sigma\|x\|^2.
YUse in source · 9 passages
Search aliases: Y
Use in source · foundations.tex, line 5
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
Y=HX+V,\qquad V\sim\mathcal N(0,R),\qquad V\text{ independent of }X. \label{eq:foundation-model}
ZUse in source · 3 passages
Search aliases: Z
Use in source · foundations.tex, line 122
For the reverse construction, sample Y∼ N(Hm,S) and an independent E_*∼ N(0,C_*). Define Z=m+K(Y-Hm)+E_*. Conditional on Y=y, the law of Z is precisely ν_y. The joint mean of (Y,Z) is again (Hm,m). Its cross covariance is SK^top=HP, and its state covariance is KSK^top+C_*=KHP+(P-KHP)=P. It therefore has exactly the covariance in [source reference]. Both constructions yield Gaussian measures with the same mean and covariance, so they yield the same joint probability measure. This is a full law id…
Exact mathematical passage
Z=m+K(Y-Hm)+E_*.
\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 · 4 passages
Search aliases: z
Use in source · foundations.tex, line 23
For an observed value y, put d=y-Hm, S=HPH^top+R, K=PH^top S^-1. The matrix S is the innovation covariance. It is positive definite because, for every nonzero z∈R^p, z^top Sz=(H^top z)^top P(H^top z)+z^top Rz>0. Consequently the inverse in the definition of K exists even when P has a nontrivial nullspace or H has deficient rank. Every inverse used by the posterior argument is an inverse on the observation space. This is the structural reason singular priors are supported.
Exact mathematical passage
z\in\R^p
z^\topUse in source · 2 passages
Search aliases: z^top top
Use in source · foundations.tex, line 24
For an observed value y, put d=y-Hm, S=HPH^top+R, K=PH^top S^-1. The matrix S is the innovation covariance. It is positive definite because, for every nonzero z∈R^p, z^top Sz=(H^top z)^top P(H^top z)+z^top Rz>0. Consequently the inverse in the definition of K exists even when P has a nontrivial nullspace or H has deficient rank. Every inverse used by the posterior argument is an inverse on the observation space. This is the structural reason singular priors are supported.
Exact mathematical passage
z^\top Sz=(H^\top z)^\top P(H^\top z)+z^\top Rz>0.
\cdotUse in source · 3 passages
Search aliases: · cdot
Use in source · common.tex, line 42
note[2]textcolorteal#1 #2 newcommandfig[3][H]centeringincludegraphics[width=linewidth]#1caption#2 graphicspath../figures/figures/ pagestylefancyfancyhf fancyhead[L]smalltextcolornavyCertified Bayesian inference fancyhead[R]smallPublication edition fancyfoot[L]small Komorebi P. · 7 October 2026 fancyfoot[R]smallthepage / pagerefLastPage renewcommand0.3pt0.3pt hypersetuppdfauthor=Komorebi P.,pdftitle=Certified Bayesian Inference: Packet Updates, Posterior Guarantees, and Arithmetic Certificates,pd…
Exact mathematical passage
\cdot
\timesUse in source · 9 passages
Search aliases: × times
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\times
\alphaUse in source · 1 passage
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
\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 · 1 passage
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\Gamma
\DeltaUse in source · 5 passages
Search aliases: Δ Delta
Use in source · foundations.tex, line 212
Let Δ=K-B. Subtraction in [source reference] gives T_K-T_B=Δ d-Δ(HU+V). The random vector HU+V is centered and has covariance S. The difference therefore has mean Δ d and covariance Δ SΔ^top. Its expected squared Euclidean norm is E T_K-T_B ^2 = Δ d ^2+tr(Δ SΔ^top). The source proves both marginals and this cost. It does not assume that a producer has supplied a coupling with the desired properties. The load-bearing declarations are pathgainSample_law, pathgainSample_exact_posterior_law, and pat…
Exact mathematical passage
\Delta=K-B
\deltaUse in source · 18 passages
Search aliases: δ delta
Use in source · closing.tex, line 19
Parameter arrays · Enclose this approximation's parameters, with radii at most δ · Declared evaluator and precision theorem
Exact mathematical passage
\delta
\Delta^\topUse in source · 2 passages
Search aliases: Δ^top Delta top
Use in source · foundations.tex, line 216
Let Δ=K-B. Subtraction in [source reference] gives T_K-T_B=Δ d-Δ(HU+V). The random vector HU+V is centered and has covariance S. The difference therefore has mean Δ d and covariance Δ SΔ^top. Its expected squared Euclidean norm is E T_K-T_B ^2 = Δ d ^2+tr(Δ SΔ^top). The source proves both marginals and this cost. It does not assume that a producer has supplied a coupling with the desired properties. The load-bearing declarations are pathgainSample_law, pathgainSample_exact_posterior_law, and pat…
Exact mathematical passage
\Delta S\Delta^\top
\epsilonUse in source · 3 passages
Search aliases: ϵ epsilon
Use in source · introduction.tex, line 37
[Publication contract of the canonical solver] Fix a finite-dimensional rational factor-coded model with σ>0, and complete, mutually orthogonal self-adjoint rational output and input packet families. Supply an output-packet seed and a finite scan containing every output label. Let ϵ,δ>0 be rational. An arbitrary rational initial gain and an arbitrary finite list of requested precision probes are permitted.
Exact mathematical passage
\epsilon,\delta>0
\varepsilonUse in source · 42 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 newcommandbayescover[2]
Exact mathematical passage
\varepsilon
\varepsilon^2Use in source · 21 passages
Search aliases: ε^2 varepsilon
Use in source · foundations.tex, line 295
osterior certificate] For the model in [source reference], with Rsucceqσ I_p and σ>0, every gain B satisfies Wtwo(ν_y,μ_B)^2≤ a(B), a(B)=E(F(B))fracσ+ d ^2σ^2. In particular, for ε≥0, the stopping condition E(F(B))(σ+ d ^2)≤ε^2σ^2 implies Wtwo(ν_y,μ_B)≤ε. The common-noise transport plan gives [source reference]. Lemma~[source reference] bounds its cost by a(B), establishing the first statement. Since σ^2>0, [source reference] is equivalent to a(B)≤ε^2. Taking the nonnegative square root gives th…
Exact mathematical passage
E(F(B))(\sigma+\|d\|^2)\le\varepsilon^2\sigma^2 \label{eq:foundation-stop}
\etaUse in source · 6 passages
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 newcommandbayescover[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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CAL…
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI /qu…
Exact mathematical passage
\lambda
\muUse in source · 12 passages
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMO…
Exact mathematical passage
\mu
\mu_BUse in source · 9 passages
Search aliases: μ_B mu
Use in source · foundations.tex, line 159
Let B∈R^n× p be an arbitrary gain candidate. It need not solve the innovation equation and need not have been produced by the packet algorithm. Define m_B · =m+Bd, C_B · =(I_n-BH)P(I_n-BH)^top+BRB^top, μ_B · = N(m_B,C_B). Every C_B is positive semidefinite, since it is a sum of covariance congruences. Thus every candidate gain determines a genuine Gaussian law. This is useful for certification: an imperfect candidate is a valid distribution with a measurable error, rather than a covariance formu…
Exact mathematical passage
m_B&=m+Bd,\label{eq:foundation-approx-mean}\\ C_B&=(I_n-BH)P(I_n-BH)^\top+BRB^\top,\label{eq:foundation-approx-cov}\\ \mu_B&=\mathcal N(m_B,C_B).\label{eq:foundation-approx-law}
\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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS vspa…
Exact mathematical passage
\xi
\PiUse in source · 4 passages
Search aliases: Π Pi
Use in source · foundations.tex, line 240
For probability laws with finite second moment, write Wtwo(ν,μ)^2 =inf_π∈Π(ν,μ)∫ x-z ^2 dπ(x,z), where Π(ν,μ) is the set of transport plans with the stated marginals. The formal source defines the squared quantity as a nonnegative extended-real infimum and obtains the distance by a square-root operation. The explicit finite Gaussian coupling proves that the quantities considered here are finite. The notation Wtwo in the paper is the corresponding finite distance.
Exact mathematical passage
\Wtwo(\nu,\mu)^2 =\inf_{\pi\in\Pi(\nu,\mu)}\int\|x-z\|^2\,d\pi(x,z),
\piUse in source · 2 passages
Search aliases: π pi
Use in source · common.tex, line 48
.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 newcommandbayescover[2]hypersetuppageanchor=…
Exact mathematical passage
\pi
\Pi_yUse in source · 2 passages
Search aliases: Π_y Pi
Use in source · introduction.tex, line 39
The canonical program pathKomorebi.CachedPosterior.runCached returns a result r. If B is its candidate gain and Π_y is the explicitly proved Gaussian posterior version, then Wtwo(Π_y, N(m_B,P_B))≤ϵ. The candidate and tolerance predicates hold. The reported mean and covariance intervals enclose m_B and P_B, respectively, and every reported radius is at most δ. Its parameter precision is the program's computed output precision, and its arrays equal the declared evaluator at that precision.
Exact mathematical passage
\Pi_y
\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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\Sigma
\sigma^{-1}Use in source · 4 passages
Search aliases: σ^-1 sigma
Use in source · foundations.tex, line 61
perator. Adding the positive semidefinite term HPH^top gives z^top Sz≥σ z ^2 for all z∈R^p. Let x=S^-1v. Then Sx=v, and the Cauchy--Schwarz inequality yields σ x ^2≤ x^top Sx=x^top v≤ x v . If x=0 the desired bound is immediate. Otherwise division by σ x gives S^-1v ≤σ^-1 v . Hence S^-1 _op≤σ^-1. This elementary estimate supplies an explicit certificate constant without computing the inverse. The inverse exists in the semantic proof, while the executable stopping test uses σ, an innovation vecto…
Exact mathematical passage
\|S^{-1}v\|\le\sigma^{-1}\|v\|
\sigma^{-2}Use in source · 2 passages
Search aliases: σ^-2 sigma
Use in source · foundations.tex, line 258
[Frobenius energy controls the residual cost] If F∈R^n× p and Ssucceqσ I_psucc0, then FS^-1d ^2+tr(FS^-1F^top) ≤ E(F)(σ^-1+σ^-2 d ^2). For a vector v, rowwise Cauchy--Schwarz gives Fv ^2=∑_i(∑_jF_ijv_j)^2 ≤∑_i(∑_jF_ij^2) v ^2 =E(F) v ^2. Apply this with v=S^-1d and use [source reference] to obtain FS^-1d ^2≤ E(F)σ^-2 d ^2. If f_i is the transpose of the ith row of F, then tr(FS^-1F^top)=∑_i f_i^top S^-1f_i ≤∑_i f_i S^-1f_i ≤σ^-1∑_i f_i ^2. The last sum is E(F). Adding the two estimates proves th…
Exact mathematical passage
\|FS^{-1}d\|^2+\tr(FS^{-1}F^\top) \le E(F)\left(\sigma^{-1}+\sigma^{-2}\|d\|^2\right). \label{eq:foundation-cost-majorant}
\sigma^2Use in source · 8 passages
Search aliases: σ^2 sigma
Use in source · foundations.tex, line 289
[Residual-energy posterior certificate] For the model in [source reference], with Rsucceqσ I_p and σ>0, every gain B satisfies Wtwo(ν_y,μ_B)^2≤ a(B), a(B)=E(F(B))fracσ+ d ^2σ^2. In particular, for ε≥0, the stopping condition E(F(B))(σ+ d ^2)≤ε^2σ^2 implies Wtwo(ν_y,μ_B)≤ε. The common-noise transport plan gives [source reference]. Lemma~[source reference] bounds its cost by a(B), establishing the first statement. Since σ^2>0, [source reference] is equivalent to a(B)≤ε^2. Taking the nonnegative sq…
Exact mathematical passage
\Wtwo(\nu_y,\mu_B)^2\le a(B),\qquad a(B)=E(F(B))\frac{\sigma+\|d\|^2}{\sigma^2}. \label{eq:foundation-score}
\sigma^{2}Use in source · 1 passage
Search aliases: σ^2 sigma
Use in source · solver.tex, line 31
Preprocessing forms three model-dependent constants: τ=frac1σ+tr S, T=I-τ S, w=fracσ+lVert vrVert^2σ^2. All are rational. They are the fields of the record pathKomorebi.CachedPosterior.Kernel, produced by pathKomorebi.CachedPosterior.prepare. The correctness theorems use this actual preparation, rather than an arbitrary record whose fields happen to have the same names. A wrong transition matrix or weight would invalidate the correspondence between the stored score and the posterior certificate.
Exact mathematical passage
\tau=\frac{1}{\sigma+\tr S},\qquad T=I-\tau S, \qquad w=\frac{\sigma+\lVert v\rVert^{2}}{\sigma^{2}}. \label{eq:solver-kernel}
\tauUse in source · 12 passages
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy vspace*16…
Exact mathematical passage
\tau
\phiUse in source · 1 passage
Search aliases: ϕ phi
Use in source · introduction.tex, line 69
Relation to established methods. Maximum-energy packet selection has a direct optimization interpretation. For the quadratic objective ϕ(B)=tfrac12tr(BSB^ T)-⟨ B,PH^ T⟩_ F, the gradient is BS-PH^ T=-F(B). The selected packet has largest projected-gradient norm. This is a block Gauss--Southwell mechanism, and the residual cache is maintained by exact linear identities. Greedy coordinate and block selection are established methods [source reference]. Pathwise Gaussian conditioning and Wasserstein …
Exact mathematical passage
\phi(B)=\tfrac12\tr(BSB^{\mathsf T})-\langle B,PH^{\mathsf T}\rangle_{\mathrm F},
\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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\chi
\OmegaUse in source · 1 passage
Search aliases: Ω Omega
Use in source · common.tex, line 48
le,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 ₆_61 ₇_7…
Exact mathematical passage
\Omega
\omegaUse in source · 1 passage
Search aliases: ω omega
Use in source · common.tex, line 48
e=∀∀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 newcommandbayescover[2]hypersetuppageanchor=falsebegint…
Exact mathematical passage
\omega
\ellUse in source · 2 passages
Search aliases: ℓ ell
Use in source · foundations.tex, line 133
[Gaussian disintegration] Let ℓ(x,·)= N(Hx,R) be the observation kernel and let η= N(Hm,S) be the evidence law. Then the explicit kernel y↦ν_y satisfies η(dy) ν_y(dx) = N(m,P)(dx) ℓ(x,dy) after exchanging the order of the two coordinates on the right. In particular, η is the actual observation marginal and ν is a posterior version for this prior and likelihood. The forward and reverse constructions just described have the same joint Gaussian mean and covariance. The reverse construction is the p…
Exact mathematical passage
\ell(x,\cdot)=\mathcal N(Hx,R)
\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
\toUse in source · 1 passage
Search aliases: → to
Use in source · common.tex, line 48
--,morecomment=[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 ×…
Exact mathematical passage
\to
\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
\mapstoUse in source · 1 passage
Search aliases: ↦ mapsto
Use in source · foundations.tex, line 133
[Gaussian disintegration] Let ℓ(x,·)= N(Hx,R) be the observation kernel and let η= N(Hm,S) be the evidence law. Then the explicit kernel y↦ν_y satisfies η(dy) ν_y(dx) = N(m,P)(dx) ℓ(x,dy) after exchanging the order of the two coordinates on the right. In particular, η is the actual observation marginal and ν is a posterior version for this prior and likelihood. The forward and reverse constructions just described have the same joint Gaussian mean and covariance. The reverse construction is the p…
Exact mathematical passage
y\mapsto\nu_y
\hookrightarrowUse in source · 1 passage
Search aliases: ↪ hookrightarrow
Use in source · foundations.tex, line 44
s concrete. For every x, x^top LL^top x= L^top x ^2≥0, x^top Rx= N^top x ^2+σ x ^2. Thus P is positive semidefinite and Rsucceqσ I_psucc0. These conclusions are proved from the factors; they are not additional statistical assumptions hidden inside a covariance record. The real semantics interprets each rational coordinate through the exact inclusion Q↪R. There is no intermediate conversion through hardware floating point.
Exact mathematical passage
\Q\hookrightarrow\R
\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
\forallUse in source · 1 passage
Search aliases: ∀ forall
Use in source · common.tex, line 48
ving,sensitive=true,morecomment=[l]--,morecomment=[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 θ…
Exact mathematical passage
\forall
\existsUse in source · 1 passage
Search aliases: ∃ exists
Use in source · common.tex, line 48
ue,morecomment=[l]--,morecomment=[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 ∧l…
Exact mathematical passage
\exists
\notinUse in source · 1 passage
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\prod
\sum_{a,b}Use in source · 2 passages
Search aliases: ∑_a,b sum
Use in source · foundations.tex, line 388
Suppose a producer supplies values u_ab and v with proved inequalities E(F_ab(B))≤ u_ab, d ^2≤ v. Completeness and nonnegative energy imply E(F(B))≤ U, U=∑_a,bu_ab. Each u_ab is nonnegative because it bounds a nonnegative quantity. Likewise v≥0. The score widehat a(B)=Ufracσ+vσ^2 therefore bounds a(B) and hence the squared posterior distance. If U(σ+v)≤ε^2σ^2, ε≥0, the same law tolerance follows.
Exact mathematical passage
E(F(B))\le U,\qquad U=\sum_{a,b}u_{ab}.
\sum_{a\in\mathcal A}Use in source · 2 passages
Search aliases: ∑_a∈ A sum in mathcal
Use in source · foundations.tex, line 330
D_b^top · =D_b, · D_b^2 · =D_b, · D_bD_b' · =0 (b≠ b'). Completeness is a separate condition: ∑_a∈ AQ_a=I_n, ∑_b∈ BD_b=I_p. The self-adjoint condition makes these Euclidean orthogonal projectors. Idempotence alone would not give the required energy geometry. Completeness prevents a certificate from forgetting a residual direction outside the selected packet spans.
Exact mathematical passage
\sum_{a\in\mathcal A}Q_a=I_n,\qquad \sum_{b\in\mathcal B}D_b=I_p. \label{eq:foundation-packet-complete}
\sum_{a\in U}Use in source · 1 passage
Search aliases: ∑_a∈ U sum in
Use in source · foundations.tex, line 361
lthm:foundation-packet-energy If both families satisfy [source reference]--[source reference], then every A∈R^n× p satisfies E(A)=∑_a∈ A∑_b∈ BE(Q_aAD_b). More generally, for subsets U⊆ A and V⊆ B, E ((∑_a∈ UQ_a)A (∑_b∈ VD_b)) =∑_a∈ U∑_b∈ VE(Q_aAD_b). The sum of any subfamily of the Q_a is again self-adjoint and idempotent: expansion of its square removes the off-diagonal products, and the remaining diagonal products equal the original projectors. For a self-adjoint idempotent Q, E(QA)=tr((QA)^to…
Exact mathematical passage
E\!\left(\left(\sum_{a\in U}Q_a\right)A \left(\sum_{b\in V}D_b\right)\right) =\sum_{a\in U}\sum_{b\in V}E(Q_aAD_b). \label{eq:foundation-parent-energy}
\sum_bUse in source · 1 passage
Search aliases: ∑_b sum
Use in source · solver.tex, line 108
=G_a(I-τ S)=G_aT. For b≠ a, mutual orthogonality gives Q_bQ_a=0 and hence Q_bF(B')=Q_bF(B)=G_b. This proves every residual equality in the new cache. Its energy equalities hold because the selected energy is evaluated from its new residual and the remaining residual-energy pairs are retained. Finally, replacing one term in a finite sum changes that sum by exactly -e_a+e'_a. Thus t'=∑_b e'_b. All three clauses of validity are preserved.
Exact mathematical passage
t'=\sum_b e'_b
\sum_{b\in\mathcal B}Use in source · 2 passages
Search aliases: ∑_b∈ B sum in mathcal
Use in source · foundations.tex, line 330
D_b^top · =D_b, · D_b^2 · =D_b, · D_bD_b' · =0 (b≠ b'). Completeness is a separate condition: ∑_a∈ AQ_a=I_n, ∑_b∈ BD_b=I_p. The self-adjoint condition makes these Euclidean orthogonal projectors. Idempotence alone would not give the required energy geometry. Completeness prevents a certificate from forgetting a residual direction outside the selected packet spans.
Exact mathematical passage
\sum_{a\in\mathcal A}Q_a=I_n,\qquad \sum_{b\in\mathcal B}D_b=I_p. \label{eq:foundation-packet-complete}
\sum_{b\in V}Use in source · 1 passage
Search aliases: ∑_b∈ V sum in
Use in source · foundations.tex, line 361
lthm:foundation-packet-energy If both families satisfy [source reference]--[source reference], then every A∈R^n× p satisfies E(A)=∑_a∈ A∑_b∈ BE(Q_aAD_b). More generally, for subsets U⊆ A and V⊆ B, E ((∑_a∈ UQ_a)A (∑_b∈ VD_b)) =∑_a∈ U∑_b∈ VE(Q_aAD_b). The sum of any subfamily of the Q_a is again self-adjoint and idempotent: expansion of its square removes the off-diagonal products, and the remaining diagonal products equal the original projectors. For a self-adjoint idempotent Q, E(QA)=tr((QA)^to…
Exact mathematical passage
E\!\left(\left(\sum_{a\in U}Q_a\right)A \left(\sum_{b\in V}D_b\right)\right) =\sum_{a\in U}\sum_{b\in V}E(Q_aAD_b). \label{eq:foundation-parent-energy}
\sum_iUse in source · 2 passages
Search aliases: ∑_i sum
Use in source · foundations.tex, line 266
[Frobenius energy controls the residual cost] If F∈R^n× p and Ssucceqσ I_psucc0, then FS^-1d ^2+tr(FS^-1F^top) ≤ E(F)(σ^-1+σ^-2 d ^2). For a vector v, rowwise Cauchy--Schwarz gives Fv ^2=∑_i(∑_jF_ijv_j)^2 ≤∑_i(∑_jF_ij^2) v ^2 =E(F) v ^2. Apply this with v=S^-1d and use [source reference] to obtain FS^-1d ^2≤ E(F)σ^-2 d ^2. If f_i is the transpose of the ith row of F, then tr(FS^-1F^top)=∑_i f_i^top S^-1f_i ≤∑_i f_i S^-1f_i ≤σ^-1∑_i f_i ^2. The last sum is E(F). Adding the two estimates proves th…
Exact mathematical passage
\|Fv\|^2=\sum_i\left(\sum_jF_{ij}v_j\right)^2 \le\sum_i\left(\sum_jF_{ij}^2\right)\|v\|^2 =E(F)\|v\|^2.
\sum_{i,j}Use in source · 1 passage
Search aliases: ∑_i,j sum
Use in source · foundations.tex, line 12
We use Euclidean vector norms and the squared Frobenius energy E(A)=FrobA^2=∑_i,jA_ij^2. The distinction between these norms matters. A matrix energy is a finite sum of scalar squares that can be evaluated exactly on rational inputs. An operator norm is used in the proof that this energy controls distribution error. The certificate never asks a producer to supply an unverified operator norm or an approximate eigenvalue calculation.
Exact mathematical passage
E(A)=\Frob{A}^2=\sum_{i,j}A_{ij}^2. \label{eq:foundation-energy}
\sum_jUse in source · 1 passage
Search aliases: ∑_j sum
Use in source · foundations.tex, line 266
[Frobenius energy controls the residual cost] If F∈R^n× p and Ssucceqσ I_psucc0, then FS^-1d ^2+tr(FS^-1F^top) ≤ E(F)(σ^-1+σ^-2 d ^2). For a vector v, rowwise Cauchy--Schwarz gives Fv ^2=∑_i(∑_jF_ijv_j)^2 ≤∑_i(∑_jF_ij^2) v ^2 =E(F) v ^2. Apply this with v=S^-1d and use [source reference] to obtain FS^-1d ^2≤ E(F)σ^-2 d ^2. If f_i is the transpose of the ith row of F, then tr(FS^-1F^top)=∑_i f_i^top S^-1f_i ≤∑_i f_i S^-1f_i ≤σ^-1∑_i f_i ^2. The last sum is E(F). Adding the two estimates proves th…
Exact mathematical passage
\|Fv\|^2=\sum_i\left(\sum_jF_{ij}v_j\right)^2 \le\sum_i\left(\sum_jF_{ij}^2\right)\|v\|^2 =E(F)\|v\|^2.
\circUse in source · 1 passage
Search aliases: ∘ circ
Use in source · common.tex, line 48
a1 σσ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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\circ
\intUse in source · 1 passage
Search aliases: ∫ int
Use in source · foundations.tex, line 240
For probability laws with finite second moment, write Wtwo(ν,μ)^2 =inf_π∈Π(ν,μ)∫ x-z ^2 dπ(x,z), where Π(ν,μ) is the set of transport plans with the stated marginals. The formal source defines the squared quantity as a nonnegative extended-real infimum and obtains the distance by a square-root operation. The explicit finite Gaussian coupling proves that the quantities considered here are finite. The notation Wtwo in the paper is the corresponding finite distance.
Exact mathematical passage
\Wtwo(\nu,\mu)^2 =\inf_{\pi\in\Pi(\nu,\mu)}\int\|x-z\|^2\,d\pi(x,z),
\simUse in source · 7 passages
Search aliases: ∼ sim
Use in source · foundations.tex, line 5
The inference problem concerns one observation of a finite-dimensional latent state. Let the state space be R^n and the observation space be R^p. A state X has prior law N(m,P), and its observation is Y=HX+V, V∼ N(0,R), V independent of X. Here H∈R^p× n may be rectangular, and P∈R^n× n may be singular. The assumptions are Psucceq0 and Rsucc0. A singular prior is an ordinary Gaussian probability law concentrated on an affine subspace. The argument does not replace that law by a nonsingular approx…
Exact mathematical passage
Y=HX+V,\qquad V\sim\mathcal N(0,R),\qquad V\text{ independent of }X. \label{eq:foundation-model}
\neUse in source · 5 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 · 1 passage
Search aliases: ≤ leq
Use in source · introduction.tex, line 40
The canonical program pathKomorebi.CachedPosterior.runCached returns a result r. If B is its candidate gain and Π_y is the explicitly proved Gaussian posterior version, then Wtwo(Π_y, N(m_B,P_B))≤ϵ. The candidate and tolerance predicates hold. The reported mean and covariance intervals enclose m_B and P_B, respectively, and every reported radius is at most δ. Its parameter precision is the program's computed output precision, and its arrays equal the declared evaluator at that precision.
Exact mathematical passage
\Wtwo(\Pi_y,\mathcal N(m_B,P_B))\leq\epsilon.
\geUse in source · 12 passages
Search aliases: ≥ ge
Use in source · common.tex, line 48
es=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 ↓downarrow1 ▸triangleri…
Exact mathematical passage
\ge
\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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\subset
\subseteqUse in source · 3 passages
Search aliases: ⊆ subseteq
Use in source · common.tex, line 48
a1 αα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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\subseteq
\langleUse in source · 4 passages
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\langle
\rangleUse in source · 4 passages
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 newcommandbayescover[2]hypersetuppageanchor=falsecolornavy large KOMOREBI / REALIZATION CALCULUS Hugebfseries Certified Bayesian
Exact mathematical passage
\rangle
\rangle_{\mathrm F}Use in source · 3 passages
Search aliases: ⟩_ F rangle mathrm
Use in source · foundations.tex, line 346
Use the Frobenius inner product ⟨ A,C⟩_ F=tr(A^top C). For a≠ a', self-adjointness and disjointness give ⟨ Q_aA,Q_a'A⟩_ F =tr(A^top Q_aQ_a'A)=0. Consequently the energy of a finite sum of output packets is the sum of their energies. The input analogue follows by transposing the matrices. Applying the two decompositions successively gives complete two-sided accounting.
Exact mathematical passage
\langle A,C\rangle_{\mathrm F}=\tr(A^\top C)
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/certified-bayesian-inference/Certified_Bayesian_Publication_1.0/README.md · 0 mathematical passages
- research/certified-bayesian-inference/Certified_Bayesian_Publication_1.0/manuscripts/closing.tex · 3 mathematical passages
- research/certified-bayesian-inference/Certified_Bayesian_Publication_1.0/manuscripts/common.tex · 62 mathematical passages
- research/certified-bayesian-inference/Certified_Bayesian_Publication_1.0/manuscripts/foundations.tex · 253 mathematical passages
- research/certified-bayesian-inference/Certified_Bayesian_Publication_1.0/manuscripts/introduction.tex · 36 mathematical passages
- research/certified-bayesian-inference/Certified_Bayesian_Publication_1.0/manuscripts/main.tex · 0 mathematical passages
- research/certified-bayesian-inference/Certified_Bayesian_Publication_1.0/manuscripts/solver.tex · 252 mathematical passages
- research/certified-bayesian-inference/Certified_Bayesian_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.