Notation by work
Constructive Repair
All notation · Glossary · Source coverage
226 symbol spellings in 763 mathematical passages across 5 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 226 entries are available below.
+Definition passage · 50 passages
Search aliases: +
Definition passage: Correction and repair · Constructive_Repair.tex, line 170
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
\label{eq:repair} Du+Ew=-r.
=Definition passage · 246 passages
Search aliases: =
Definition passage: Correction and repair · Constructive_Repair.tex, line 166
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
\label{eq:correct} Du=-r.
ADefinition passage · 51 passages
Search aliases: A
Definition passage: Selection interval · Constructive_Repair.tex, line 1424
[Selection interval] For A⊆ B⊆ J, define I(A,B)={T⊆ J:A⊆ T⊆ B}. The set A contains candidates already required, and B contains all candidates still permitted by the branch decisions. The unresolved indices form B∖ A.
Exact mathematical passage
A\subseteq B\subseteq J
\mathcal ADefinition passage · 8 passages
Search aliases: A mathcal
Definition passage: Separating block · Constructive_Repair.tex, line 1234
[Separating block] A separating block is a pair (B,Y), where B⊆{0,…,q-1} and Y∈ℚ^1× m satisfy YD=0, Ywidetilde E_B=0, YR≠0. The set B need not itself belong to A.
Exact mathematical passage
\mathcal A
BDefinition passage · 56 passages
Search aliases: B
Definition passage: Faithfulness on a submodule · Constructive_Repair.tex, line 561
Faithfulness on precisely the required data. [Faithfulness on a submodule] For O≤ Q_D, the map B is faithful on O when ∀ z∈ O, Bz=0Longrightarrow z=0.
Exact mathematical passage
B
DDefinition passage · 182 passages
Search aliases: D
Definition passage: Correction and repair · Constructive_Repair.tex, line 165
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
D
EDefinition passage · 81 passages
Search aliases: E
Definition passage: Correction and repair · Constructive_Repair.tex, line 169
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
E:W\to V
IDefinition passage · 18 passages
Search aliases: I
Definition passage: Required obstruction span · Constructive_Repair.tex, line 242
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
r:I\to V
\mathcal IDefinition passage · 11 passages
Search aliases: I mathcal
Definition passage: Selection interval · Constructive_Repair.tex, line 1425
[Selection interval] For A⊆ B⊆ J, define I(A,B)={T⊆ J:A⊆ T⊆ B}. The set A contains candidates already required, and B contains all candidates still permitted by the branch decisions. The unresolved indices form B∖ A.
Exact mathematical passage
\mathcal I(A,B)=\{T\subseteq J:A\subseteq T\subseteq B\}.
iDefinition passage · 27 passages
Search aliases: i
Definition passage: Correction and repair · Constructive_Repair.tex, line 173
tion[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
r_i
JDefinition passage · 33 passages
Search aliases: J
Definition passage: Selection interval · Constructive_Repair.tex, line 1424
[Selection interval] For A⊆ B⊆ J, define I(A,B)={T⊆ J:A⊆ T⊆ B}. The set A contains candidates already required, and B contains all candidates still permitted by the branch decisions. The unresolved indices form B∖ A.
Exact mathematical passage
A\subseteq B\subseteq J
jDefinition passage · 30 passages
Search aliases: j
Definition passage: Accepted branch tree · Constructive_Repair.tex, line 1490
[Accepted branch tree] A tree for I(A,B) consists of one of the three terminal certificates above, or a split at j∈ B∖ A with accepted trees for both child intervals. In lower-bound mode a cost threshold is fixed throughout the tree. In infeasibility mode cost leaves are rejected.
Exact mathematical passage
j\in B\setminus A
\kkDefinition passage · 18 passages
Search aliases: kk 𝕜 Bbbk
Definition passage: Required obstruction span · Constructive_Repair.tex, line 243
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
O_D(r)=\Span_{\kk}\{q_D(r_i):i\in I\}\leq Q_D.
\LongrightarrowDefinition passage · 3 passages
Search aliases: Longrightarrow
Definition passage: Faithfulness on a submodule · Constructive_Repair.tex, line 562
Faithfulness on precisely the required data. [Faithfulness on a submodule] For O≤ Q_D, the map B is faithful on O when ∀ z∈ O, Bz=0Longrightarrow z=0.
Exact mathematical passage
\forall z\in O,\qquad Bz=0\Longrightarrow z=0.
mDefinition passage · 25 passages
Search aliases: m
Definition passage: Separating row · Constructive_Repair.tex, line 960
Separating obstructions. [Separating row] A separating certificate for S is a row Y∈ℚ^1× m satisfying YD=0, Ywidetilde E_S=0, YR≠0. The last condition asks that at least one original residual is detected. No residual index needs to be selected when the family is empty.
Exact mathematical passage
Y\in\Q^{1\times m}
ODefinition passage · 63 passages
Search aliases: O
Definition passage: Required obstruction span · Constructive_Repair.tex, line 243
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
O_D(r)=\Span_{\kk}\{q_D(r_i):i\in I\}\leq Q_D.
O_DDefinition passage · 8 passages
Search aliases: O_D
Definition passage: Required obstruction span · Constructive_Repair.tex, line 243
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
O_D(r)=\Span_{\kk}\{q_D(r_i):i\in I\}\leq Q_D.
QDefinition passage · 33 passages
Search aliases: Q
Definition passage: Required obstruction span · Constructive_Repair.tex, line 243
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
O_D(r)=\Span_{\kk}\{q_D(r_i):i\in I\}\leq Q_D.
\QDefinition passage · 29 passages
Search aliases: Q ℚ mathbb
Definition passage: Separating row · Constructive_Repair.tex, line 960
Separating obstructions. [Separating row] A separating certificate for S is a row Y∈ℚ^1× m satisfying YD=0, Ywidetilde E_S=0, YR≠0. The last condition asks that at least one original residual is detected. No residual index needs to be selected when the family is empty.
Exact mathematical passage
Y\in\Q^{1\times m}
qDefinition passage · 72 passages
Search aliases: q
Definition passage: Required obstruction span · Constructive_Repair.tex, line 243
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
O_D(r)=\Span_{\kk}\{q_D(r_i):i\in I\}\leq Q_D.
\Q^{1\times m}Definition passage · 2 passages
Search aliases: Q^1× m ℚ^1× m Q times mathbb times
Definition passage: Separating row · Constructive_Repair.tex, line 960
Separating obstructions. [Separating row] A separating certificate for S is a row Y∈ℚ^1× m satisfying YD=0, Ywidetilde E_S=0, YR≠0. The last condition asks that at least one original residual is detected. No residual index needs to be selected when the family is empty.
Exact mathematical passage
Y\in\Q^{1\times m}
Q_DDefinition passage · 16 passages
Search aliases: Q_D
Definition passage: Required obstruction span · Constructive_Repair.tex, line 243
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
O_D(r)=\Span_{\kk}\{q_D(r_i):i\in I\}\leq Q_D.
q_DDefinition passage · 57 passages
Search aliases: q_D
Definition passage: Required obstruction span · Constructive_Repair.tex, line 243
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
O_D(r)=\Span_{\kk}\{q_D(r_i):i\in I\}\leq Q_D.
RDefinition passage · 48 passages
Search aliases: R
Definition passage: Separating row · Constructive_Repair.tex, line 961
Separating obstructions. [Separating row] A separating certificate for S is a row Y∈ℚ^1× m satisfying YD=0, Ywidetilde E_S=0, YR≠0. The last condition asks that at least one original residual is detected. No residual index needs to be selected when the family is empty.
Exact mathematical passage
\label{eq:rational-separator} YD=0,\qquad Y\widetilde E_S=0,\qquad YR\ne0.
rDefinition passage · 85 passages
Search aliases: r
Definition passage: Correction and repair · Constructive_Repair.tex, line 165
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
r\in V
r_iDefinition passage · 20 passages
Search aliases: r_i
Definition passage: Correction and repair · Constructive_Repair.tex, line 173
tion[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
r_i
SDefinition passage · 65 passages
Search aliases: S
Definition passage: Separating row · Constructive_Repair.tex, line 960
Separating obstructions. [Separating row] A separating certificate for S is a row Y∈ℚ^1× m satisfying YD=0, Ywidetilde E_S=0, YR≠0. The last condition asks that at least one original residual is detected. No residual index needs to be selected when the family is empty.
Exact mathematical passage
S
\SpanDefinition passage · 6 passages
Search aliases: Span span operatorname
Definition passage: Required obstruction span · Constructive_Repair.tex, line 243
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
O_D(r)=\Span_{\kk}\{q_D(r_i):i\in I\}\leq Q_D.
\Span_{\kk}Definition passage · 2 passages
Search aliases: Span_kk span_𝕜 Span kk operatorname Bbbk
Definition passage: Required obstruction span · Constructive_Repair.tex, line 243
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
O_D(r)=\Span_{\kk}\{q_D(r_i):i\in I\}\leq Q_D.
TDefinition passage · 33 passages
Search aliases: T
Definition passage: Selection interval · Constructive_Repair.tex, line 1425
[Selection interval] For A⊆ B⊆ J, define I(A,B)={T⊆ J:A⊆ T⊆ B}. The set A contains candidates already required, and B contains all candidates still permitted by the branch decisions. The unresolved indices form B∖ A.
Exact mathematical passage
\mathcal I(A,B)=\{T\subseteq J:A\subseteq T\subseteq B\}.
UDefinition passage · 35 passages
Search aliases: U
Definition passage: Correction and repair · Constructive_Repair.tex, line 165
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
u\in U
uDefinition passage · 48 passages
Search aliases: u
Definition passage: Correction and repair · Constructive_Repair.tex, line 165
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
u\in U
VDefinition passage · 45 passages
Search aliases: V
Definition passage: Correction and repair · Constructive_Repair.tex, line 165
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
r\in V
WDefinition passage · 36 passages
Search aliases: W
Definition passage: Correction and repair · Constructive_Repair.tex, line 169
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
E:W\to V
wDefinition passage · 32 passages
Search aliases: w
Definition passage: Correction and repair · Constructive_Repair.tex, line 169
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
w\in W
\widetilde EDefinition passage · 13 passages
Search aliases: widetilde E widetilde
Definition passage: Separating row · Constructive_Repair.tex, line 961
Separating obstructions. [Separating row] A separating certificate for S is a row Y∈ℚ^1× m satisfying YD=0, Ywidetilde E_S=0, YR≠0. The last condition asks that at least one original residual is detected. No residual index needs to be selected when the family is empty.
Exact mathematical passage
\label{eq:rational-separator} YD=0,\qquad Y\widetilde E_S=0,\qquad YR\ne0.
\widetilde E_BDefinition passage · 2 passages
Search aliases: widetilde E_B widetilde
Definition passage: Separating block · Constructive_Repair.tex, line 1230
[Separating block] A separating block is a pair (B,Y), where B⊆{0,…,q-1} and Y∈ℚ^1× m satisfy YD=0, Ywidetilde E_B=0, YR≠0. The set B need not itself belong to A.
Exact mathematical passage
YD=0,\qquad Y\widetilde E_B=0,\qquad YR\ne0. \label{eq:menu-cover-dual}
\widetilde E_SDefinition passage · 9 passages
Search aliases: widetilde E_S widetilde
Definition passage: Separating row · Constructive_Repair.tex, line 961
Separating obstructions. [Separating row] A separating certificate for S is a row Y∈ℚ^1× m satisfying YD=0, Ywidetilde E_S=0, YR≠0. The last condition asks that at least one original residual is detected. No residual index needs to be selected when the family is empty.
Exact mathematical passage
\label{eq:rational-separator} YD=0,\qquad Y\widetilde E_S=0,\qquad YR\ne0.
YDefinition passage · 23 passages
Search aliases: Y
Definition passage: Separating row · Constructive_Repair.tex, line 960
Separating obstructions. [Separating row] A separating certificate for S is a row Y∈ℚ^1× m satisfying YD=0, Ywidetilde E_S=0, YR≠0. The last condition asks that at least one original residual is detected. No residual index needs to be selected when the family is empty.
Exact mathematical passage
Y\in\Q^{1\times m}
zDefinition passage · 8 passages
Search aliases: z
Definition passage: Faithfulness on a submodule · Constructive_Repair.tex, line 562
Faithfulness on precisely the required data. [Faithfulness on a submodule] For O≤ Q_D, the map B is faithful on O when ∀ z∈ O, Bz=0Longrightarrow z=0.
Exact mathematical passage
\forall z\in O,\qquad Bz=0\Longrightarrow z=0.
\timesDefinition passage · 15 passages
Search aliases: × times
Definition passage: Separating row · Constructive_Repair.tex, line 960
Separating obstructions. [Separating row] A separating certificate for S is a row Y∈ℚ^1× m satisfying YD=0, Ywidetilde E_S=0, YR≠0. The last condition asks that at least one original residual is detected. No residual index needs to be selected when the family is empty.
Exact mathematical passage
Y\in\Q^{1\times m}
\ldotsDefinition passage · 3 passages
Search aliases: … ldots
Definition passage: Separating block · Constructive_Repair.tex, line 1229
[Separating block] A separating block is a pair (B,Y), where B⊆{0,…,q-1} and Y∈ℚ^1× m satisfy YD=0, Ywidetilde E_B=0, YR≠0. The set B need not itself belong to A.
Exact mathematical passage
B\subseteq\{0,\ldots,q-1\}
\toDefinition passage · 32 passages
Search aliases: → to
Definition passage: Correction and repair · Constructive_Repair.tex, line 169
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
E:W\to V
\forallDefinition passage · 4 passages
Search aliases: ∀ forall
Definition passage: Faithfulness on a submodule · Constructive_Repair.tex, line 562
Faithfulness on precisely the required data. [Faithfulness on a submodule] For O≤ Q_D, the map B is faithful on O when ∀ z∈ O, Bz=0Longrightarrow z=0.
Exact mathematical passage
\forall z\in O,\qquad Bz=0\Longrightarrow z=0.
\inDefinition passage · 73 passages
Search aliases: ∈ in
Definition passage: Correction and repair · Constructive_Repair.tex, line 165
[Correction and repair] A residual r∈ V is correctable by D when there is u∈ U such that Du=-r. An added correction map E:W→ V repairs r when there are u∈ U and w∈ W with Du+Ew=-r. It repairs the family when this condition holds for every r_i. The witnesses may depend on i.
Exact mathematical passage
r\in V
\setminusDefinition passage · 6 passages
Search aliases: ∖ setminus
Definition passage: Selection interval · Constructive_Repair.tex, line 1428
[Selection interval] For A⊆ B⊆ J, define I(A,B)={T⊆ J:A⊆ T⊆ B}. The set A contains candidates already required, and B contains all candidates still permitted by the branch decisions. The unresolved indices form B∖ A.
Exact mathematical passage
B\setminus A
\neDefinition passage · 7 passages
Search aliases: ≠ ne
Definition passage: Separating row · Constructive_Repair.tex, line 961
Separating obstructions. [Separating row] A separating certificate for S is a row Y∈ℚ^1× m satisfying YD=0, Ywidetilde E_S=0, YR≠0. The last condition asks that at least one original residual is detected. No residual index needs to be selected when the family is empty.
Exact mathematical passage
\label{eq:rational-separator} YD=0,\qquad Y\widetilde E_S=0,\qquad YR\ne0.
\leqDefinition passage · 19 passages
Search aliases: ≤ leq
Definition passage: Required obstruction span · Constructive_Repair.tex, line 243
The obstruction span of a family. [Required obstruction span] For a residual family r:I→ V, put O_D(r)=span_𝕜{q_D(r_i):i∈ I}≤ Q_D. We write O when the family and correction map are understood.
Exact mathematical passage
O_D(r)=\Span_{\kk}\{q_D(r_i):i\in I\}\leq Q_D.
\subseteqDefinition passage · 24 passages
Search aliases: ⊆ subseteq
Definition passage: Separating block · Constructive_Repair.tex, line 1229
[Separating block] A separating block is a pair (B,Y), where B⊆{0,…,q-1} and Y∈ℚ^1× m satisfy YD=0, Ywidetilde E_B=0, YR≠0. The set B need not itself belong to A.
Exact mathematical passage
B\subseteq\{0,\ldots,q-1\}
aIntroduction passage · 39 passages
Search aliases: a
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
\arrowIntroduction passage · 2 passages
Search aliases: arrow
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
bIntroduction passage · 22 passages
Search aliases: b
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
cIntroduction passage · 40 passages
Search aliases: c
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
\operatorname{check}Introduction passage · 4 passages
Search aliases: check operatorname
Introduction passage · Constructive_Repair.tex, line 636
[The Boolean test has the intended meaning] The equality check(S)=true holds if and only if E_S repairs the residual family. The Boolean is defined by deciding precisely the quantified equations in [source reference] for the map E_S. No intermediate rank guess or unproved feasibility oracle replaces those equations. formalrepairMenuCheck_spec
Exact mathematical passage
\operatorname{check}(S)=\mathrm{true}
dIntroduction passage · 16 passages
Search aliases: d
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
D'Introduction passage · 16 passages
Search aliases: D'
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
eIntroduction passage · 25 passages
Search aliases: e
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
E_SIntroduction passage · 12 passages
Search aliases: E_S
Introduction passage · Constructive_Repair.tex, line 636
[The Boolean test has the intended meaning] The equality check(S)=true holds if and only if E_S repairs the residual family. The Boolean is defined by deciding precisely the quantified equations in [source reference] for the map E_S. No intermediate rank guess or unproved feasibility oracle replaces those equations. formalrepairMenuCheck_spec
Exact mathematical passage
E_S
gIntroduction passage · 2 passages
Search aliases: g
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
lIntroduction passage · 3 passages
Search aliases: l
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
nIntroduction passage · 13 passages
Search aliases: n
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
oIntroduction passage · 3 passages
Search aliases: o
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
pIntroduction passage · 27 passages
Search aliases: p
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
q_{D'}Introduction passage · 5 passages
Search aliases: q_D'
Introduction passage · Constructive_Repair.tex, line 530
U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
q_{D'}
sIntroduction passage · 29 passages
Search aliases: s
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
\mathrm{true}Introduction passage · 5 passages
Search aliases: true mathrm
Introduction passage · Constructive_Repair.tex, line 636
[The Boolean test has the intended meaning] The equality check(S)=true holds if and only if E_S repairs the residual family. The Boolean is defined by deciding precisely the quantified equations in [source reference] for the map E_S. No intermediate rank guess or unproved feasibility oracle replaces those equations. formalrepairMenuCheck_spec
Exact mathematical passage
\operatorname{check}(S)=\mathrm{true}
U'Introduction passage · 2 passages
Search aliases: U'
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
V'Introduction passage · 1 passage
Search aliases: V'
Introduction passage · Constructive_Repair.tex, line 523
Faithful transport of obstructions. The induced quotient map. Suppose two correction systems are related by a commuting square [column sep=large,row sep=large] U arrow[r,"D"] arrow[d,"a"'] · V arrow[d,"b"] U' arrow[r,"D'"'] · V'. bD=D'a. All four spaces are modules over the same commutative ring. Denote the quotient maps by q_D and q_D'.
Exact mathematical passage
\label{eq:square} \begin{tikzcd}[column sep=large,row sep=large] U \arrow[r,"D"] \arrow[d,"a"'] & V \arrow[d,"b"]\\ U' \arrow[r,"D'"'] & V'. \end{tikzcd} \qquad bD=D'a.
a^2Use in source · 3 passages
Search aliases: a^2
Use in source · Constructive_Repair.tex, line 872
[A nonlinear root with a nonzero first order obstruction] For a∈ℝ∖{0}, define F_a(x)=x^2-a^2. At zero, F_a'(0)=0, and the correction equation 0· u=a^2 has no solution. Nevertheless, F_a(a)=0. Differentiation gives F_a'(x)=2x, so the derivative at zero is zero. Since a≠0, its square is nonzero, while 0· u=0 for every u. Finally, F_a(a)=a^2-a^2=0. formalNonlinear.nonlinear_root_despite_first_order_obstruction
Exact mathematical passage
F_a(x)=x^2-a^2
a_0Use in source · 1 passage
Search aliases: a_0
Use in source · Constructive_Repair.tex, line 1537
Let b_1,b_2,b_3 be the standard basis of ℚ^3. Take D(u)=ub_1 and residual r=b_2+b_3. There are 24 candidate entries: a_0=b_2, a_1=b_3, a_j=b_1 (2≤ j<24). Their costs are two, three, and ten for each remaining entry. All subsets are admissible.
Exact mathematical passage
a_0=b_2,\qquad a_1=b_3,\qquad a_j=b_1\quad(2\leq j<24).
a_1Use in source · 1 passage
Search aliases: a_1
Use in source · Constructive_Repair.tex, line 1537
Let b_1,b_2,b_3 be the standard basis of ℚ^3. Take D(u)=ub_1 and residual r=b_2+b_3. There are 24 candidate entries: a_0=b_2, a_1=b_3, a_j=b_1 (2≤ j<24). Their costs are two, three, and ten for each remaining entry. All subsets are admissible.
Exact mathematical passage
a_0=b_2,\qquad a_1=b_3,\qquad a_j=b_1\quad(2\leq j<24).
a_iUse in source · 1 passage
Search aliases: a_i
Use in source · Constructive_Repair.tex, line 420
[Exact finite menu feasibility] The selected menu S repairs the family exactly when O_D(r)⊆ O_S. Equivalently, ∀ i∈ I ∃ u_i∈ U ∃ a_i∈𝕜^S, Du_i+∑_j∈ Sa_ije_j=-r_i. Apply [source reference] to the actual map E_S and use [source reference]. Its reverse direction supplies the original correction witnesses and the selected coefficients, rather than only an abstract statement about dimensions. formalfinite_menu_repair_iff_span
Exact mathematical passage
\forall i\in I\ \exists u_i\in U\ \exists a_i\in\kk^S, \qquad Du_i+\sum_{j\in S}a_{ij}e_j=-r_i.
a_{ij}Use in source · 1 passage
Search aliases: a_ij
Use in source · Constructive_Repair.tex, line 420
[Exact finite menu feasibility] The selected menu S repairs the family exactly when O_D(r)⊆ O_S. Equivalently, ∀ i∈ I ∃ u_i∈ U ∃ a_i∈𝕜^S, Du_i+∑_j∈ Sa_ije_j=-r_i. Apply [source reference] to the actual map E_S and use [source reference]. Its reverse direction supplies the original correction witnesses and the selected coefficients, rather than only an abstract statement about dimensions. formalfinite_menu_repair_iff_span
Exact mathematical passage
\forall i\in I\ \exists u_i\in U\ \exists a_i\in\kk^S, \qquad Du_i+\sum_{j\in S}a_{ij}e_j=-r_i.
a_jUse in source · 4 passages
Search aliases: a_j
Use in source · Constructive_Repair.tex, line 392
Finite menus and conservation. A menu is an actual coefficient map. Return to a commutative ring 𝕜 and modules U,V. Let e:J→ V be a family of candidate directions and let S⊆ J be finite. A coefficient vector is a function a:S→𝕜. Define E_S:𝕜^S⟶ V, E_S(a)=∑_j∈ Sa_je_j. Finite addition and scalar multiplication show that E_S is linear. The coefficient domain is the selected set itself, so no unselected direction appears in the equation.
Exact mathematical passage
\label{eq:menu} E_S:\kk^S\longrightarrow V,\qquad E_S(a)=\sum_{j\in S}a_je_j.
\operatorname{allowed}Use in source · 2 passages
Search aliases: allowed operatorname
Use in source · Constructive_Repair.tex, line 643
Additional admissibility is a supplied function allowed: P(J)→{false,true}. The cost is any supplied function c: P(J)→ℕ. The formal theorem does not require c to be additive in the selected entries.
Exact mathematical passage
\operatorname{allowed}:\mathcal P(J)\to\{\mathrm{false},\mathrm{true}\}
\mathcal BUse in source · 5 passages
Search aliases: B mathcal
Use in source · Constructive_Repair.tex, line 1272
Let B be a finite list of separating blocks. Say that B covers T when some (B,Y)∈ B satisfies T⊆ B. Validity of the block list and coverage of the relevant selections are separate obligations.
Exact mathematical passage
\mathcal B
B^{-1}Use in source · 2 passages
Search aliases: B^-1
Use in source · Constructive_Repair.tex, line 1118
How the Python producer obtains the matrices. The executable producer uses exact rational row reduction. It selects independent columns of D and extends them by standard basis vectors to a basis B of ℚ^m. The inverse B^-1 supplies the image coordinates and the complementary detector coordinates. The selected image coordinates are placed in the original domain to obtain P, while the complementary basis vectors form K and the corresponding rows of B^-1 form L.
Exact mathematical passage
B^{-1}
B_0Use in source · 3 passages
Search aliases: B_0
Use in source · Constructive_Repair.tex, line 1331
0=-R. Two separating blocks suffice: B_0={0}, Y_0=(0,1,-1), B_1={1}, Y_1=(0,1,0). Both satisfy Y_iD=0, annihilate their masked candidate matrices, and give Y_iR=1.
Exact mathematical passage
B_0=\{0\},\quad Y_0=(0,1,-1),\qquad B_1=\{1\},\quad Y_1=(0,1,0).
B_1Use in source · 3 passages
Search aliases: B_1
Use in source · Constructive_Repair.tex, line 1331
0=-R. Two separating blocks suffice: B_0={0}, Y_0=(0,1,-1), B_1={1}, Y_1=(0,1,0). Both satisfy Y_iD=0, annihilate their masked candidate matrices, and give Y_iR=1.
Exact mathematical passage
B_0=\{0\},\quad Y_0=(0,1,-1),\qquad B_1=\{1\},\quad Y_1=(0,1,0).
b_1Use in source · 3 passages
Search aliases: b_1
Use in source · Constructive_Repair.tex, line 1536
Let b_1,b_2,b_3 be the standard basis of ℚ^3. Take D(u)=ub_1 and residual r=b_2+b_3. There are 24 candidate entries: a_0=b_2, a_1=b_3, a_j=b_1 (2≤ j<24). Their costs are two, three, and ten for each remaining entry. All subsets are admissible.
Exact mathematical passage
b_1,b_2,b_3
b_2Use in source · 3 passages
Search aliases: b_2
Use in source · Constructive_Repair.tex, line 1536
Let b_1,b_2,b_3 be the standard basis of ℚ^3. Take D(u)=ub_1 and residual r=b_2+b_3. There are 24 candidate entries: a_0=b_2, a_1=b_3, a_j=b_1 (2≤ j<24). Their costs are two, three, and ten for each remaining entry. All subsets are admissible.
Exact mathematical passage
b_1,b_2,b_3
b_3Use in source · 3 passages
Search aliases: b_3
Use in source · Constructive_Repair.tex, line 1536
Let b_1,b_2,b_3 be the standard basis of ℚ^3. Take D(u)=ub_1 and residual r=b_2+b_3. There are 24 candidate entries: a_0=b_2, a_1=b_3, a_j=b_1 (2≤ j<24). Their costs are two, three, and ten for each remaining entry. All subsets are admissible.
Exact mathematical passage
b_1,b_2,b_3
\operatorname{bestByCheck}Use in source · 2 passages
Search aliases: bestByCheck operatorname
Use in source · Constructive_Repair.tex, line 656
For a finite list L of candidates, a Boolean predicate h, and a natural cost c, define bestByCheck(h,c, L) to filter by h and then return an argument of minimum cost. It returns codenone exactly when the filtered list is empty. Ties need not define a mathematically unique optimum.
Exact mathematical passage
\operatorname{bestByCheck}(h,c,\mathcal L)
\operatorname{bestRepairMenu}Use in source · 1 passage
Search aliases: bestRepairMenu operatorname
Use in source · Constructive_Repair.tex, line 667
The repair optimizer is bestRepairMenu =bestByCheck( S↦allowed(S)wedgecheck(S), c, L_J).
Exact mathematical passage
\operatorname{bestRepairMenu} =\operatorname{bestByCheck}\bigl( S\mapsto\operatorname{allowed}(S)\wedge\operatorname{check}(S),\ c,\ \mathcal L_J\bigr).
\bmodUse in source · 1 passage
Search aliases: bmod
Use in source · Constructive_Repair.tex, line 808
@rrrrr@ k · x_k · c_kbmod7 · t_k · x_k+1
Exact mathematical passage
c_k\bmod7
CUse in source · 6 passages
Search aliases: C
Use in source · Constructive_Repair.tex, line 1085
At the quotient level, L induces an injection ℚ^m/im D→ℚ^d. If Lv=0, the split identity gives v=DPv, proving that its class is zero. The image is im L. Hence the required residual obstruction span is isomorphic to the column space of C=LR. This quotient interpretation is an ordinary consequence of the displayed identities.
Exact mathematical passage
C=LR
c_0Use in source · 2 passages
Search aliases: c_0
Use in source · Constructive_Repair.tex, line 479
A weighting makes the distinction sharper. Assigning positive costs c_0,c_1 gives optimum c_0+c_1 for this menu. A subspace containing e_0-e_1 does not charge those two entries separately unless its cost model explicitly does so.
Exact mathematical passage
c_0,c_1
c_1Use in source · 2 passages
Search aliases: c_1
Use in source · Constructive_Repair.tex, line 479
A weighting makes the distinction sharper. Assigning positive costs c_0,c_1 gives optimum c_0+c_1 for this menu. A subspace containing e_0-e_1 does not charge those two entries separately unless its cost model explicitly does so.
Exact mathematical passage
c_0,c_1
c_jUse in source · 2 passages
Search aliases: c_j
Use in source · Constructive_Repair.tex, line 1211
Fix rational matrices D∈ℚ^m× n, E∈ℚ^m× q, R∈ℚ^m× s. The columns e_j of E are the available new directions. The finite family A⊆ P({0,…,q-1}) contains exactly the admissible selections. It need not be downward closed. Nonnegative integer weights c_j define the cost c(S)=∑_j∈ Sc_j. These matrices, selections, and costs are fixed original input. A certificate cannot replace them with another problem.
Exact mathematical passage
c_j
c_kUse in source · 2 passages
Search aliases: c_k
Use in source · Constructive_Repair.tex, line 798
An exact seven-adic trace. For x^2=2 at p=7, start with x_1=3. At each step, let c_k=fracx_k^2-27^k, c_k+2x_kt_k≡0pmod7, x_k+1=x_k+7^kt_k. The following table records normalized choices for this example. Every displayed digit equation is an exact integer calculation.
Exact mathematical passage
c_k=\frac{x_k^2-2}{7^k},\qquad c_k+2x_kt_k\equiv0\pmod7,\qquad x_{k+1}=x_k+7^kt_k.
c_\astUse in source · 5 passages
Search aliases: c_∗ ast
Use in source · Constructive_Repair.tex, line 1453
Nonnegative additive costs are monotone under inclusion: A⊆ T Longrightarrow c(A)≤ c(T). Therefore, when an incumbent repair has cost c_∗, the finite check c_∗≤ c(A) excludes every strictly cheaper repair in I(A,B). It does not say the interval is infeasible. It only says that it cannot improve the incumbent. formalKomorebiRepair.RationalCertificates.additiveCost_mono
Exact mathematical passage
c_\ast
\codeUse in source · 1 passage
Search aliases: code
Use in source · Constructive_Repair.tex, line 1735
Verification and provenance. The evidence attached to the formal release. The v0.2.0 verification record reports successful compilation of ten proof modules, an axiom audit of all 49 named theorem declarations, and individual replay of those modules through Lean's kernel. The allowed transitive axiom set is {codepropext, codeClassical.choice, codeQuot.sound}. No additional assumption axiom, placeholder axiom, or native decision axiom is allowed in the accepted theorem library.
Exact mathematical passage
\{\code{propext},\ \code{Classical.choice},\ \code{Quot.sound}\}.
\cokerUse in source · 1 passage
Search aliases: coker operatorname
Use in source · Constructive_Repair.tex, line 182
What the quotient remembers. Write Q_D=coker D=V/im D, q_D:V⟶ Q_D. The class q_D(r) records the part of r that cannot be changed by the original correction map. Since q_D(Du)=0, all residuals that differ by an original correction have the same class.
Exact mathematical passage
Q_D=\coker D=V/\im D,\qquad q_D:V\longrightarrow Q_D.
\mathsf DUse in source · 3 passages
Search aliases: D mathsf
Use in source · Constructive_Repair.tex, line 375
[Rank difference in matrix coordinates] Let the columns of a matrix R be a finite residual family and let D represent D. Then dim O_D(r)=rank[ Dmid R]-rank D. Set M=im D+span{r_i}. The restriction q_Dvert_M has image O and kernel im D. Rank and nullity give dim M=dimim D+dim O. The columns of [ Dmid R] span M. sourcescopeThis coordinate corollary is an ordinary derivation included for the computational interpretation. The v0.2.0 Lean release proves the abstract attained dimension theorem, but do…
Exact mathematical passage
\mathsf D
\operatorname{decide}Use in source · 1 passage
Search aliases: decide operatorname
Use in source · Constructive_Repair.tex, line 628
For each finite subset S⊆ J, define the Boolean test check(S)=decide( ∀ i∈ I ∃ u∈ U ∃ a∈𝕜^S, Du+E_Sa=-r_i ). All quantified domains are finite. Decidable equality in V determines each candidate equation.
Exact mathematical passage
\label{eq:boolean-check} \operatorname{check}(S)=\operatorname{decide}\left( \forall i\in I\ \exists u\in U\ \exists a\in\kk^S,\quad Du+E_Sa=-r_i \right).
\operatorname{diag}Use in source · 2 passages
Search aliases: diag operatorname
Use in source · Constructive_Repair.tex, line 1138
0 · 0 · 1. Thus LD=0, DP=diag(1,0,0), and KL=diag(0,1,1). The residual coordinates are C=LR=1 · 2
Exact mathematical passage
DP=\operatorname{diag}(1,0,0)
\dimUse in source · 9 passages
Search aliases: dim
Use in source · Constructive_Repair.tex, line 142
[title=The central result] Let D:U→ V be linear over a field and let q:V→ V/im D, O=span{q(r_i):i∈ I}. If V is finite dimensional, the least added dimension that repairs every r_i is dim O. If an allowed subspace A≤ V satisfies O⊆ q(A), the minimum can be attained with all added directions in A. Selecting entries from a fixed menu is a different optimization problem.
Exact mathematical passage
\dim O
\dim_{\kk}Use in source · 1 passage
Search aliases: dim_kk dim_𝕜 dim kk dim Bbbk
Use in source · Constructive_Repair.tex, line 274
[Dimension lower bound] If E:W→ V repairs r and W is finite dimensional, then O=O_D(r) is finite dimensional and dim_𝕜O≤dim_𝕜W. By [source reference], O⊆im(q_DE). The image of a linear map from a finite dimensional space is finite dimensional and has dimension at most that of its domain. Hence dim O≤dimim(q_DE)≤dim W.qedhere formalrepair_dimension_lower_bound
Exact mathematical passage
\dim_{\kk}O\leq\dim_{\kk}W.
E'Use in source · 5 passages
Search aliases: E'
Use in source · Constructive_Repair.tex, line 996
[Dimension lower certificate] Assume [source reference]. If an arbitrary competing augmentation E'∈ℚ^m× w has coefficients satisfying DU'+E'W'=-R, then t≤ w. Multiplication by H and Q gives HE'W'Q=-I_t, hence (HE')(-W'Q)=I_t. Thus HE':ℚ^w→ℚ^t has a right inverse. It is surjective, and consequently t≤ w. formalRationalCertificates.dimension_certificate_right_inverse formalRationalCertificates.dimension_certificate_lower_bound
Exact mathematical passage
E'\in\Q^{m\times w}
e_0Use in source · 7 passages
Search aliases: e_0
Use in source · Constructive_Repair.tex, line 448
One obstruction, two selected entries. [The difference between the two minima] Over ℚ, let D(u)=(u,0,0), r=(0,1,0), and make only the following directions available: e_0=(0,1,1), e_1=(0,0,1). The quotient by im D is the plane of the second and third coordinates. There q_D(r)=(1,0), q_D(e_0)=(1,1), and q_D(e_1)=(0,1).
Exact mathematical passage
e_0=(0,1,1),\qquad e_1=(0,0,1).
e_1Use in source · 7 passages
Search aliases: e_1
Use in source · Constructive_Repair.tex, line 448
One obstruction, two selected entries. [The difference between the two minima] Over ℚ, let D(u)=(u,0,0), r=(0,1,0), and make only the following directions available: e_0=(0,1,1), e_1=(0,0,1). The quotient by im D is the plane of the second and third coordinates. There q_D(r)=(1,0), q_D(e_0)=(1,1), and q_D(e_1)=(0,1).
Exact mathematical passage
e_0=(0,1,1),\qquad e_1=(0,0,1).
e_2Use in source · 1 passage
Search aliases: e_2
Use in source · Constructive_Repair.tex, line 1351
A third candidate can make the cost distinction sharper. Add the direct direction e_0=(0,1,0) at cost five, and price e_1=(0,1,1) and e_2=(0,0,1) at one each. One menu entry can now repair the residual, but the cheapest repair selects two entries, {1,2}, at total cost two. Minimum free dimension, minimum menu cardinality, and minimum menu cost are three different quantities.
Exact mathematical passage
e_2=(0,0,1)
e_jUse in source · 9 passages
Search aliases: e_j
Use in source · Constructive_Repair.tex, line 392
Finite menus and conservation. A menu is an actual coefficient map. Return to a commutative ring 𝕜 and modules U,V. Let e:J→ V be a family of candidate directions and let S⊆ J be finite. A coefficient vector is a function a:S→𝕜. Define E_S:𝕜^S⟶ V, E_S(a)=∑_j∈ Sa_je_j. Finite addition and scalar multiplication show that E_S is linear. The coefficient domain is the selected set itself, so no unselected direction appears in the equation.
Exact mathematical passage
\label{eq:menu} E_S:\kk^S\longrightarrow V,\qquad E_S(a)=\sum_{j\in S}a_je_j.
FUse in source · 19 passages
Search aliases: F
Use in source · Constructive_Repair.tex, line 863
Nonlinear limits and native realizations. A linearized problem is a different equation. Suppose a nonlinear map F is differentiable at an approximation x_0. Its linearized correction equation is DF(x_0)u=-F(x_0). The cokernel criterion completely decides [source reference] once the derivative is fixed. It does not, by itself, decide whether there is x with F(x)=0. Higher order terms are absent from the linearized equation, and they may either create a solution or prevent the linear prediction fr…
Exact mathematical passage
F
\FUse in source · 1 passage
Search aliases: F 𝔽 mathbb
Use in source · Constructive_Repair.tex, line 696
A fully evaluated example over two elements. Take the data of [source reference] over 𝔽_2. Negation is now the identity. The equation is (u,a,a+b)=(0,1,0). Thus the full menu succeeds with u=0, a=b=1. The two singleton menus still fail.
Exact mathematical passage
\F_2
fUse in source · 1 passage
Search aliases: f
Use in source · Constructive_Repair.tex, line 350
[Attainment inside a legal subspace] If O⊆ q_D(A), there exists a linear map E:O→ V satisfying im E⊆ A, q_DE=ι_O, and repairing the entire family. If V is finite dimensional, its added dimension is optimal even among all unrestricted repairs. Consider the surjection f:A⟶ q_D(A), a⟼ q_D(a). Choose a linear section s_A:q_D(A)→ A. Let j:O↪ q_D(A) and ι_A:A↪ V be inclusions. Define E=ι_As_Aj. Its image is in A by construction. Moreover, q_Dι_As_Aj=j as a map into Q_D, which is precisely ι_O. By [sou…
Exact mathematical passage
f:A\longrightarrow q_D(A),\qquad a\longmapsto q_D(a).
\F_2Use in source · 1 passage
Search aliases: F_2 𝔽_2 F mathbb
Use in source · Constructive_Repair.tex, line 696
A fully evaluated example over two elements. Take the data of [source reference] over 𝔽_2. Negation is now the identity. The equation is (u,a,a+b)=(0,1,0). Thus the full menu succeeds with u=0, a=b=1. The two singleton menus still fail.
Exact mathematical passage
\F_2
F_aUse in source · 3 passages
Search aliases: F_a
Use in source · Constructive_Repair.tex, line 872
[A nonlinear root with a nonzero first order obstruction] For a∈ℝ∖{0}, define F_a(x)=x^2-a^2. At zero, F_a'(0)=0, and the correction equation 0· u=a^2 has no solution. Nevertheless, F_a(a)=0. Differentiation gives F_a'(x)=2x, so the derivative at zero is zero. Since a≠0, its square is nonzero, while 0· u=0 for every u. Finally, F_a(a)=a^2-a^2=0. formalNonlinear.nonlinear_root_despite_first_order_obstruction
Exact mathematical passage
F_a(x)=x^2-a^2
F_a'Use in source · 2 passages
Search aliases: F_a'
Use in source · Constructive_Repair.tex, line 873
[A nonlinear root with a nonzero first order obstruction] For a∈ℝ∖{0}, define F_a(x)=x^2-a^2. At zero, F_a'(0)=0, and the correction equation 0· u=a^2 has no solution. Nevertheless, F_a(a)=0. Differentiation gives F_a'(x)=2x, so the derivative at zero is zero. Since a≠0, its square is nonzero, while 0· u=0 for every u. Finally, F_a(a)=a^2-a^2=0. formalNonlinear.nonlinear_root_despite_first_order_obstruction
Exact mathematical passage
F_a'(0)=0,
\mathrm{false}Use in source · 1 passage
Search aliases: false mathrm
Use in source · Constructive_Repair.tex, line 643
Additional admissibility is a supplied function allowed: P(J)→{false,true}. The cost is any supplied function c: P(J)→ℕ. The formal theorem does not require c to be additive in the selected entries.
Exact mathematical passage
\operatorname{allowed}:\mathcal P(J)\to\{\mathrm{false},\mathrm{true}\}
GUse in source · 13 passages
Search aliases: G
Use in source · Constructive_Repair.tex, line 886
[A solvable linearization without a real root] Let G(x)=x^2+x+1. Then G'(0)=1, ∃ u∈ℝ (u=-1), so the linearized correction at zero is solvable. However, G has no real root. The derivative is 2x+1, which equals one at zero, and G(0)=1. Thus u=-1 solves the linearized equation. But G(x)=(x+frac12)^2+frac34>0 for every real x. formalNonlinear.linearized_solution_without_real_root
Exact mathematical passage
G(x)=x^2+x+1
G'Use in source · 1 passage
Search aliases: G'
Use in source · Constructive_Repair.tex, line 887
[A solvable linearization without a real root] Let G(x)=x^2+x+1. Then G'(0)=1, ∃ u∈ℝ (u=-1), so the linearized correction at zero is solvable. However, G has no real root. The derivative is 2x+1, which equals one at zero, and G(0)=1. Thus u=-1 solves the linearized equation. But G(x)=(x+frac12)^2+frac34>0 for every real x. formalNonlinear.linearized_solution_without_real_root
Exact mathematical passage
G'(0)=1,\qquad \exists u\in\R\ (u=-1),
\gcdUse in source · 1 passage
Search aliases: gcd
Use in source · Constructive_Repair.tex, line 781
The quadratic lifting theorem. [One higher precision] Let p,x,a∈ℤ and k∈ℕ with k≥1. Assume p^kmid x^2-a, gcd(2x,p)=1. Then there exists t∈ℤ such that p^k+1mid (x+p^kt)^2-a. Choose c∈ℤ with x^2-a=p^kc. Coprimality supplies B ezout data for 2x and p, so [source reference] gives t with pmid c+2xt. Since k≥1, one has pmid p^k. Apply [source reference] with m=p^k. formalArithmetic.quadratic_hensel_step
Exact mathematical passage
p^k\mid x^2-a,\qquad \gcd(2x,p)=1.
HUse in source · 17 passages
Search aliases: H
Use in source · Constructive_Repair.tex, line 986
Dimension certificates without a reported rank. Suppose an augmentation with t columns succeeds. Its optimality can be certified by two additional matrices H∈ℚ^t× m, Q∈ℚ^s× t with HD=0, HRQ=I_t. These identities make a lower bound on the required dimension explicit.
Exact mathematical passage
H\in\Q^{t\times m},\qquad Q\in\Q^{s\times t}
hUse in source · 9 passages
Search aliases: h
Use in source · Constructive_Repair.tex, line 314
[column sep=large,row sep=large] O arrow[r,"E"] arrow[dr,hook,"ι_O"'] · V arrow[d,"q_D"] · Q_D The triangle records exactly what is preserved: a required quotient class is lifted to a representative of that same class. The lift does not manufacture an unrelated object with a similar invariant.
Exact mathematical passage
\begin{tikzcd}[column sep=large,row sep=large] O \arrow[r,"E"] \arrow[dr,hook,"\iota_O"'] & V \arrow[d,"q_D"]\\ & Q_D \end{tikzcd}
I_dUse in source · 2 passages
Search aliases: I_d
Use in source · Constructive_Repair.tex, line 1021
Exact rank and menu cost. For A∈ℚ^a× b, a certificate of rank d consists of appropriately shaped rational matrices with A=FG, PAQ=I_d, where the inner dimension of FG is d.
Exact mathematical passage
\label{eq:rational-rank} A=FG,\qquad PAQ=I_d,
I_mUse in source · 1 passage
Search aliases: I_m
Use in source · Constructive_Repair.tex, line 1068
Constructive matrix attainment. A complete detector. Fix D∈ℚ^m× n and R∈ℚ^m× s. A split correction certificate consists of P∈ℚ^n× m, K∈ℚ^m× d, L∈ℚ^d× m with LD=0, DP+KL=I_m. The first identity makes L a detector that ignores original corrections. The second proves that no further information has been discarded: every target vector has the decomposition v=DPv+KLv. There is no assumption that LK=I_d, and redundant detector coordinates are permitted.
Exact mathematical passage
\label{eq:split-certified} LD=0,\qquad DP+KL=I_m.
I_tUse in source · 5 passages
Search aliases: I_t
Use in source · Constructive_Repair.tex, line 990
Dimension certificates without a reported rank. Suppose an augmentation with t columns succeeds. Its optimality can be certified by two additional matrices H∈ℚ^t× m, Q∈ℚ^s× t with HD=0, HRQ=I_t. These identities make a lower bound on the required dimension explicit.
Exact mathematical passage
\label{eq:rational-dimension} HD=0,\qquad HRQ=I_t.
\idUse in source · 2 passages
Search aliases: id operatorname
Use in source · Constructive_Repair.tex, line 291
An attaining construction. [A section of the quotient] There is a linear map s:Q_D→ V with q_Ds=id_Q_D. Choose a basis of the vector space Q_D. Since q_D is surjective, choose a representative in V of each basis vector. Extend this assignment linearly. Its composite with q_D fixes the basis and therefore fixes all of Q_D. formalexists_obstruction_section
Exact mathematical passage
q_Ds=\id_{Q_D}.
\id_{\Q}Use in source · 1 passage
Search aliases: id_Q id_ℚ id Q operatorname mathbb
Use in source · Constructive_Repair.tex, line 606
A transport that conceals failure. [Correct in the target, false in the source] Let D:ℚ→ℚ^2, D(u)=(u,0), D'=id_ℚ, a=id_ℚ, b(x,y)=x. Then bD=D'a. For r=(0,1) there is no u with (u,0)=(0,-1), so the source residual is not correctable. Its image b(r)=0 is correctable by D'.
Exact mathematical passage
D:\Q\to\Q^2,\quad D(u)=(u,0),\qquad D'=\id_{\Q},\quad a=\id_{\Q},\quad b(x,y)=x.
\id_{Q_D}Use in source · 1 passage
Search aliases: id_Q_D id operatorname
Use in source · Constructive_Repair.tex, line 291
An attaining construction. [A section of the quotient] There is a linear map s:Q_D→ V with q_Ds=id_Q_D. Choose a basis of the vector space Q_D. Since q_D is surjective, choose a representative in V of each basis vector. Extend this assignment linearly. Its composite with q_D fixes the basis and therefore fixes all of Q_D. formalexists_obstruction_section
Exact mathematical passage
q_Ds=\id_{Q_D}.
\imUse in source · 32 passages
Search aliases: im operatorname
Use in source · Constructive_Repair.tex, line 139
[title=The central result] Let D:U→ V be linear over a field and let q:V→ V/im D, O=span{q(r_i):i∈ I}. If V is finite dimensional, the least added dimension that repairs every r_i is dim O. If an allowed subspace A≤ V satisfies O⊆ q(A), the minimum can be attained with all added directions in A. Selecting entries from a fixed menu is a different optimization problem.
Exact mathematical passage
q:V\to V/\im D,\qquad O=\Span\{q(r_i):i\in I\}.
KUse in source · 12 passages
Search aliases: K
Use in source · Constructive_Repair.tex, line 1064
Constructive matrix attainment. A complete detector. Fix D∈ℚ^m× n and R∈ℚ^m× s. A split correction certificate consists of P∈ℚ^n× m, K∈ℚ^m× d, L∈ℚ^d× m with LD=0, DP+KL=I_m. The first identity makes L a detector that ignores original corrections. The second proves that no further information has been discarded: every target vector has the decomposition v=DPv+KLv. There is no assumption that LK=I_d, and redundant detector coordinates are permitted.
Exact mathematical passage
P\in\Q^{n\times m},\quad K\in\Q^{m\times d},\quad L\in\Q^{d\times m}
kUse in source · 19 passages
Search aliases: k
Use in source · Constructive_Repair.tex, line 314
[column sep=large,row sep=large] O arrow[r,"E"] arrow[dr,hook,"ι_O"'] · V arrow[d,"q_D"] · Q_D The triangle records exactly what is preserved: a required quotient class is lifted to a representative of that same class. The lift does not manufacture an unrelated object with a similar invariant.
Exact mathematical passage
\begin{tikzcd}[column sep=large,row sep=large] O \arrow[r,"E"] \arrow[dr,hook,"\iota_O"'] & V \arrow[d,"q_D"]\\ & Q_D \end{tikzcd}
\kerUse in source · 1 passage
Search aliases: ker
Use in source · Constructive_Repair.tex, line 567
This condition is equivalent to ker B∩ O=0. It does not require injectivity on all of Q_D when only a smaller family of obstruction classes matters.
Exact mathematical passage
\ker B\cap O=0
\kk^SUse in source · 3 passages
Search aliases: kk^S 𝕜^S kk Bbbk
Use in source · Constructive_Repair.tex, line 392
Finite menus and conservation. A menu is an actual coefficient map. Return to a commutative ring 𝕜 and modules U,V. Let e:J→ V be a family of candidate directions and let S⊆ J be finite. A coefficient vector is a function a:S→𝕜. Define E_S:𝕜^S⟶ V, E_S(a)=∑_j∈ Sa_je_j. Finite addition and scalar multiplication show that E_S is linear. The coefficient domain is the selected set itself, so no unselected direction appears in the equation.
Exact mathematical passage
\label{eq:menu} E_S:\kk^S\longrightarrow V,\qquad E_S(a)=\sum_{j\in S}a_je_j.
LUse in source · 48 passages
Search aliases: L
Use in source · Constructive_Repair.tex, line 200
The quotient also has a universal property. If L:V→ Z annihilates im D, it descends to a unique linear map overline L:Q_D→ Z with L=overline Lq_D. Thus every linear detector that ignores correctable directions factors through the same quotient. This is the classical cokernel construction used in Paper III~[source reference]. Canonicality is relative to D, not to an unspecified mathematical problem.
Exact mathematical passage
L:V\to Z
\mathcal LUse in source · 9 passages
Search aliases: L mathcal
Use in source · Constructive_Repair.tex, line 646
Enumerating menus and selecting an optimum. Enumerate J as a sorted list. Take every sublist and convert it to a finite set. The resulting list, denoted L_J, contains every subset of J.
Exact mathematical passage
\mathcal L_J
\mathcal L_JUse in source · 5 passages
Search aliases: L_J mathcal
Use in source · Constructive_Repair.tex, line 646
Enumerating menus and selecting an optimum. Enumerate J as a sorted list. Take every sublist and convert it to a finite set. The resulting list, denoted L_J, contains every subset of J.
Exact mathematical passage
\mathcal L_J
\LongleftrightarrowUse in source · 4 passages
Search aliases: Longleftrightarrow
Use in source · Constructive_Repair.tex, line 189
[Exact obstruction criterion] For every r∈ V, ∃ u∈ U (Du=-r) Longleftrightarrow q_D(r)=0. Applying q_D to Du=-r gives 0=-q_D(r), hence q_D(r)=0. Conversely, q_D(r)=0 means r∈im D. Choose v∈ U with Dv=r. Then D(-v)=-r. formalcorrectable_iff_obstruction_zero
Exact mathematical passage
\exists u\in U\ (Du=-r)\quad\Longleftrightarrow\quad q_D(r)=0.
MUse in source · 4 passages
Search aliases: M
Use in source · Constructive_Repair.tex, line 381
[Rank difference in matrix coordinates] Let the columns of a matrix R be a finite residual family and let D represent D. Then dim O_D(r)=rank[ Dmid R]-rank D. Set M=im D+span{r_i}. The restriction q_Dvert_M has image O and kernel im D. Rank and nullity give dim M=dimim D+dim O. The columns of [ Dmid R] span M. sourcescopeThis coordinate corollary is an ordinary derivation included for the computational interpretation. The v0.2.0 Lean release proves the abstract attained dimension theorem, but do…
Exact mathematical passage
M=\im D+\Span\{r_i\}
m^2Use in source · 2 passages
Search aliases: m^2
Use in source · Constructive_Repair.tex, line 766
[Quadratic correction identity] Let p,m,x,a,c,t∈ℤ satisfy x^2-a=mc, pmid c+2xt, pmid m. Then mpmid (x+mt)^2-a. Write c+2xt=pd and m=ps. Direct expansion gives (x+mt)^2-a · =(x^2-a)+2mxt+m^2t^2 · =m(c+2xt)+m^2t^2 · =mp(d+st^2).qedhere The last expression displays the required quotient explicitly. formalArithmetic.quadratic_digit_correction
Exact mathematical passage
(x+mt)^2-a &=(x^2-a)+2mxt+m^2t^2\\ &=m(c+2xt)+m^2t^2\\ &=mp(d+st^2).\qedhere
\midUse in source · 12 passages
Search aliases: mid
Use in source · Constructive_Repair.tex, line 376
[Rank difference in matrix coordinates] Let the columns of a matrix R be a finite residual family and let D represent D. Then dim O_D(r)=rank[ Dmid R]-rank D. Set M=im D+span{r_i}. The restriction q_Dvert_M has image O and kernel im D. Rank and nullity give dim M=dimim D+dim O. The columns of [ Dmid R] span M. sourcescopeThis coordinate corollary is an ordinary derivation included for the computational interpretation. The v0.2.0 Lean release proves the abstract attained dimension theorem, but do…
Exact mathematical passage
\dim O_D(r)=\rank[\mathsf D\mid\mathsf R]-\rank\mathsf D.
\minUse in source · 1 passage
Search aliases: min
Use in source · Constructive_Repair.tex, line 324
[The attained free minimum] If V is finite dimensional, the minimum possible dimension of a finite dimensional added space that repairs the family is min{dim W: E:W→ V repairs r}=dim O_D(r). Every admissible term on the left is at least dim O by [source reference]. Because V is finite dimensional, its quotient and the subspace O are finite dimensional. The map in [source reference] is a repair with domain O, so the bound is attained. formalfree_minimal_repair_rank
Exact mathematical passage
\label{eq:minimum} \min\bigl\{\dim W: E:W\to V\text{ repairs }r\bigr\}=\dim O_D(r).
\NUse in source · 5 passages
Search aliases: N ℕ mathbb
Use in source · Constructive_Repair.tex, line 643
Additional admissibility is a supplied function allowed: P(J)→{false,true}. The cost is any supplied function c: P(J)→ℕ. The formal theorem does not require c to be additive in the selected entries.
Exact mathematical passage
c:\mathcal P(J)\to\N
\nexistsUse in source · 1 passage
Search aliases: nexists
Use in source · Constructive_Repair.tex, line 1479
If admissibility is specified by a list A, a terminal check establishes nexists T∈ A: A⊆ T⊆ B. It examines the original list, not the powerset of J. For the all-subsets rule this terminal certificate is unavailable. formalKomorebiRepair.RationalCertificates.intervalExcluded_sound
Exact mathematical passage
\nexists T\in\mathcal A:\quad A\subseteq T\subseteq B.
\notUse in source · 1 passage
Search aliases: not
Use in source · Constructive_Repair.tex, line 362
[Subspace impossibility] If Onot⊆ q_D(A), no added map E:W→ V with image contained in A repairs the family. Such a map satisfies im(q_DE)⊆ q_D(A). If it repaired the family, [source reference] would imply O⊆im(q_DE)⊆ q_D(A), contrary to the hypothesis. formaladmissible_subspace_no_go
Exact mathematical passage
O\not\subseteq q_D(A)
O_SUse in source · 6 passages
Search aliases: O_S
Use in source · Constructive_Repair.tex, line 398
Write O_S=span_𝕜{q_D(e_j):j∈ S}.
Exact mathematical passage
O_S=\Span_{\kk}\{q_D(e_j):j\in S\}.
O_TUse in source · 2 passages
Search aliases: O_T
Use in source · Constructive_Repair.tex, line 432
[Monotonicity of feasibility] If S⊆ T, then O_S⊆ O_T. Every family repairable with S is therefore repairable with T. Each generator defining O_S is also a generator defining O_T. Apply [source reference]. Equivalently, extend each coefficient vector by zero on T∖ S. formalrepairable_menu_mono
Exact mathematical passage
O_S\subseteq O_T
\overline LUse in source · 2 passages
Search aliases: overline L overline
Use in source · Constructive_Repair.tex, line 200
The quotient also has a universal property. If L:V→ Z annihilates im D, it descends to a unique linear map overline L:Q_D→ Z with L=overline Lq_D. Thus every linear detector that ignores correctable directions factors through the same quotient. This is the classical cokernel construction used in Paper III~[source reference]. Canonicality is relative to D, not to an unspecified mathematical problem.
Exact mathematical passage
\overline L:Q_D\to Z
PUse in source · 15 passages
Search aliases: P
Use in source · Constructive_Repair.tex, line 1021
Exact rank and menu cost. For A∈ℚ^a× b, a certificate of rank d consists of appropriately shaped rational matrices with A=FG, PAQ=I_d, where the inner dimension of FG is d.
Exact mathematical passage
\label{eq:rational-rank} A=FG,\qquad PAQ=I_d,
\mathcal PUse in source · 3 passages
Search aliases: P mathcal
Use in source · Constructive_Repair.tex, line 643
Additional admissibility is a supplied function allowed: P(J)→{false,true}. The cost is any supplied function c: P(J)→ℕ. The formal theorem does not require c to be additive in the selected entries.
Exact mathematical passage
\operatorname{allowed}:\mathcal P(J)\to\{\mathrm{false},\mathrm{true}\}
p^kUse in source · 5 passages
Search aliases: p^k
Use in source · Constructive_Repair.tex, line 781
The quadratic lifting theorem. [One higher precision] Let p,x,a∈ℤ and k∈ℕ with k≥1. Assume p^kmid x^2-a, gcd(2x,p)=1. Then there exists t∈ℤ such that p^k+1mid (x+p^kt)^2-a. Choose c∈ℤ with x^2-a=p^kc. Coprimality supplies B ezout data for 2x and p, so [source reference] gives t with pmid c+2xt. Since k≥1, one has pmid p^k. Apply [source reference] with m=p^k. formalArithmetic.quadratic_hensel_step
Exact mathematical passage
p^k\mid x^2-a,\qquad \gcd(2x,p)=1.
p^{k+1}Use in source · 1 passage
Search aliases: p^k+1
Use in source · Constructive_Repair.tex, line 785
The quadratic lifting theorem. [One higher precision] Let p,x,a∈ℤ and k∈ℕ with k≥1. Assume p^kmid x^2-a, gcd(2x,p)=1. Then there exists t∈ℤ such that p^k+1mid (x+p^kt)^2-a. Choose c∈ℤ with x^2-a=p^kc. Coprimality supplies B ezout data for 2x and p, so [source reference] gives t with pmid c+2xt. Since k≥1, one has pmid p^k. Apply [source reference] with m=p^k. formalArithmetic.quadratic_hensel_step
Exact mathematical passage
\label{eq:hensel} p^{k+1}\mid (x+p^kt)^2-a.
\pmodUse in source · 2 passages
Search aliases: pmod
Use in source · Constructive_Repair.tex, line 798
An exact seven-adic trace. For x^2=2 at p=7, start with x_1=3. At each step, let c_k=fracx_k^2-27^k, c_k+2x_kt_k≡0pmod7, x_k+1=x_k+7^kt_k. The following table records normalized choices for this example. Every displayed digit equation is an exact integer calculation.
Exact mathematical passage
c_k=\frac{x_k^2-2}{7^k},\qquad c_k+2x_kt_k\equiv0\pmod7,\qquad x_{k+1}=x_k+7^kt_k.
\Q^2Use in source · 5 passages
Search aliases: Q^2 ℚ^2 Q mathbb
Use in source · Constructive_Repair.tex, line 203
[A visible residual] Let D:ℚ→ℚ^2 be D(u)=(u,0) and let r=(2,3). The quotient is identified with the second coordinate. The correction u=-2 removes the first coordinate but leaves (0,3). The functional L(x,y)=y satisfies LD=0 and L(r)=3, so no original correction eliminates r.
Exact mathematical passage
D:\Q\to\Q^2
\Q^3Use in source · 1 passage
Search aliases: Q^3 ℚ^3 Q mathbb
Use in source · Constructive_Repair.tex, line 1536
Let b_1,b_2,b_3 be the standard basis of ℚ^3. Take D(u)=ub_1 and residual r=b_2+b_3. There are 24 candidate entries: a_0=b_2, a_1=b_3, a_j=b_1 (2≤ j<24). Their costs are two, three, and ten for each remaining entry. All subsets are admissible.
Exact mathematical passage
\Q^3
\Q^{a\times b}Use in source · 1 passage
Search aliases: Q^a× b ℚ^a× b Q times mathbb times
Use in source · Constructive_Repair.tex, line 1020
Exact rank and menu cost. For A∈ℚ^a× b, a certificate of rank d consists of appropriately shaped rational matrices with A=FG, PAQ=I_d, where the inner dimension of FG is d.
Exact mathematical passage
A\in\Q^{a\times b}
\Q^dUse in source · 1 passage
Search aliases: Q^d ℚ^d Q mathbb
Use in source · Constructive_Repair.tex, line 1085
At the quotient level, L induces an injection ℚ^m/im D→ℚ^d. If Lv=0, the split identity gives v=DPv, proving that its class is zero. The image is im L. Hence the required residual obstruction span is isomorphic to the column space of C=LR. This quotient interpretation is an ordinary consequence of the displayed identities.
Exact mathematical passage
\Q^m/\im D\to\Q^d
\Q^{d\times m}Use in source · 1 passage
Search aliases: Q^d× m ℚ^d× m Q times mathbb times
Use in source · Constructive_Repair.tex, line 1064
Constructive matrix attainment. A complete detector. Fix D∈ℚ^m× n and R∈ℚ^m× s. A split correction certificate consists of P∈ℚ^n× m, K∈ℚ^m× d, L∈ℚ^d× m with LD=0, DP+KL=I_m. The first identity makes L a detector that ignores original corrections. The second proves that no further information has been discarded: every target vector has the decomposition v=DPv+KLv. There is no assumption that LK=I_d, and redundant detector coordinates are permitted.
Exact mathematical passage
P\in\Q^{n\times m},\quad K\in\Q^{m\times d},\quad L\in\Q^{d\times m}
\Q^{d\times t}Use in source · 1 passage
Search aliases: Q^d× t ℚ^d× t Q times mathbb times
Use in source · Constructive_Repair.tex, line 1089
The attaining construction. Suppose the detected residual matrix C=LR has certificate data F∈ℚ^d× t, G∈ℚ^t× s, J∈ℚ^t× d, Q∈ℚ^s× t satisfying LR=FG, JLRQ=I_t. The new augmentation and its correction coefficients are not unspecified witnesses. They are E=KF, U=-PR, W=-G.
Exact mathematical passage
F\in\Q^{d\times t},\quad G\in\Q^{t\times s},\quad J\in\Q^{t\times d},\quad Q\in\Q^{s\times t}
\Q^mUse in source · 4 passages
Search aliases: Q^m ℚ^m Q mathbb
Use in source · Constructive_Repair.tex, line 980
For a fixed rational menu, either the correction matrices exist or a separating row exists, but not both. Exclusivity follows from the preceding theorem. If no correction matrices exist, some residual r_i lies outside the column space of [D widetilde E_S]. Choose a basis for that space, adjoin r_i, and extend to a basis of ℚ^m. The functional taking value one on r_i and zero on all other chosen basis vectors is a rational separating row. sourcescopeThis completeness argument is an ordinary proof…
Exact mathematical passage
\Q^m
\Q^{m\times d}Use in source · 1 passage
Search aliases: Q^m× d ℚ^m× d Q times mathbb times
Use in source · Constructive_Repair.tex, line 1064
Constructive matrix attainment. A complete detector. Fix D∈ℚ^m× n and R∈ℚ^m× s. A split correction certificate consists of P∈ℚ^n× m, K∈ℚ^m× d, L∈ℚ^d× m with LD=0, DP+KL=I_m. The first identity makes L a detector that ignores original corrections. The second proves that no further information has been discarded: every target vector has the decomposition v=DPv+KLv. There is no assumption that LK=I_d, and redundant detector coordinates are permitted.
Exact mathematical passage
P\in\Q^{n\times m},\quad K\in\Q^{m\times d},\quad L\in\Q^{d\times m}
\Q^{m\times n}Use in source · 3 passages
Search aliases: Q^m× n ℚ^m× n Q times mathbb times
Use in source · Constructive_Repair.tex, line 937
Fix matrices D∈ℚ^m× n, R∈ℚ^m× s, E∈ℚ^m× q. The residuals are the columns of R. For a selected menu S, let widetilde E_S retain the original candidate indexing and replace unselected columns by zero. The supplied coefficient matrices have shapes U∈ℚ^n× s and W∈ℚ^q× s. Their correction equation is DU+widetilde E_SW=-R. Keeping the original indexing avoids any ambiguity about a permutation of candidate columns. Coefficients on a zeroed column have no effect. The admissibility predicate and cost fun…
Exact mathematical passage
D\in\Q^{m\times n},\qquad R\in\Q^{m\times s},\qquad E\in\Q^{m\times q}.
\Q^{m\times q}Use in source · 2 passages
Search aliases: Q^m× q ℚ^m× q Q times mathbb times
Use in source · Constructive_Repair.tex, line 937
Fix matrices D∈ℚ^m× n, R∈ℚ^m× s, E∈ℚ^m× q. The residuals are the columns of R. For a selected menu S, let widetilde E_S retain the original candidate indexing and replace unselected columns by zero. The supplied coefficient matrices have shapes U∈ℚ^n× s and W∈ℚ^q× s. Their correction equation is DU+widetilde E_SW=-R. Keeping the original indexing avoids any ambiguity about a permutation of candidate columns. Coefficients on a zeroed column have no effect. The admissibility predicate and cost fun…
Exact mathematical passage
D\in\Q^{m\times n},\qquad R\in\Q^{m\times s},\qquad E\in\Q^{m\times q}.
\Q^{m\times s}Use in source · 3 passages
Search aliases: Q^m× s ℚ^m× s Q times mathbb times
Use in source · Constructive_Repair.tex, line 937
Fix matrices D∈ℚ^m× n, R∈ℚ^m× s, E∈ℚ^m× q. The residuals are the columns of R. For a selected menu S, let widetilde E_S retain the original candidate indexing and replace unselected columns by zero. The supplied coefficient matrices have shapes U∈ℚ^n× s and W∈ℚ^q× s. Their correction equation is DU+widetilde E_SW=-R. Keeping the original indexing avoids any ambiguity about a permutation of candidate columns. Coefficients on a zeroed column have no effect. The admissibility predicate and cost fun…
Exact mathematical passage
D\in\Q^{m\times n},\qquad R\in\Q^{m\times s},\qquad E\in\Q^{m\times q}.
\Q^{m\times w}Use in source · 1 passage
Search aliases: Q^m× w ℚ^m× w Q times mathbb times
Use in source · Constructive_Repair.tex, line 996
[Dimension lower certificate] Assume [source reference]. If an arbitrary competing augmentation E'∈ℚ^m× w has coefficients satisfying DU'+E'W'=-R, then t≤ w. Multiplication by H and Q gives HE'W'Q=-I_t, hence (HE')(-W'Q)=I_t. Thus HE':ℚ^w→ℚ^t has a right inverse. It is surjective, and consequently t≤ w. formalRationalCertificates.dimension_certificate_right_inverse formalRationalCertificates.dimension_certificate_lower_bound
Exact mathematical passage
E'\in\Q^{m\times w}
\Q^{n\times m}Use in source · 1 passage
Search aliases: Q^n× m ℚ^n× m Q times mathbb times
Use in source · Constructive_Repair.tex, line 1064
Constructive matrix attainment. A complete detector. Fix D∈ℚ^m× n and R∈ℚ^m× s. A split correction certificate consists of P∈ℚ^n× m, K∈ℚ^m× d, L∈ℚ^d× m with LD=0, DP+KL=I_m. The first identity makes L a detector that ignores original corrections. The second proves that no further information has been discarded: every target vector has the decomposition v=DPv+KLv. There is no assumption that LK=I_d, and redundant detector coordinates are permitted.
Exact mathematical passage
P\in\Q^{n\times m},\quad K\in\Q^{m\times d},\quad L\in\Q^{d\times m}
\Q^{n\times s}Use in source · 1 passage
Search aliases: Q^n× s ℚ^n× s Q times mathbb times
Use in source · Constructive_Repair.tex, line 940
Fix matrices D∈ℚ^m× n, R∈ℚ^m× s, E∈ℚ^m× q. The residuals are the columns of R. For a selected menu S, let widetilde E_S retain the original candidate indexing and replace unselected columns by zero. The supplied coefficient matrices have shapes U∈ℚ^n× s and W∈ℚ^q× s. Their correction equation is DU+widetilde E_SW=-R. Keeping the original indexing avoids any ambiguity about a permutation of candidate columns. Coefficients on a zeroed column have no effect. The admissibility predicate and cost fun…
Exact mathematical passage
U\in\Q^{n\times s}
\Q^{q\times s}Use in source · 2 passages
Search aliases: Q^q× s ℚ^q× s Q times mathbb times
Use in source · Constructive_Repair.tex, line 940
Fix matrices D∈ℚ^m× n, R∈ℚ^m× s, E∈ℚ^m× q. The residuals are the columns of R. For a selected menu S, let widetilde E_S retain the original candidate indexing and replace unselected columns by zero. The supplied coefficient matrices have shapes U∈ℚ^n× s and W∈ℚ^q× s. Their correction equation is DU+widetilde E_SW=-R. Keeping the original indexing avoids any ambiguity about a permutation of candidate columns. Coefficients on a zeroed column have no effect. The admissibility predicate and cost fun…
Exact mathematical passage
W\in\Q^{q\times s}
\Q^{s\times t}Use in source · 2 passages
Search aliases: Q^s× t ℚ^s× t Q times mathbb times
Use in source · Constructive_Repair.tex, line 986
Dimension certificates without a reported rank. Suppose an augmentation with t columns succeeds. Its optimality can be certified by two additional matrices H∈ℚ^t× m, Q∈ℚ^s× t with HD=0, HRQ=I_t. These identities make a lower bound on the required dimension explicit.
Exact mathematical passage
H\in\Q^{t\times m},\qquad Q\in\Q^{s\times t}
\Q^tUse in source · 3 passages
Search aliases: Q^t ℚ^t Q mathbb
Use in source · Constructive_Repair.tex, line 1003
[Dimension lower certificate] Assume [source reference]. If an arbitrary competing augmentation E'∈ℚ^m× w has coefficients satisfying DU'+E'W'=-R, then t≤ w. Multiplication by H and Q gives HE'W'Q=-I_t, hence (HE')(-W'Q)=I_t. Thus HE':ℚ^w→ℚ^t has a right inverse. It is surjective, and consequently t≤ w. formalRationalCertificates.dimension_certificate_right_inverse formalRationalCertificates.dimension_certificate_lower_bound
Exact mathematical passage
HE':\Q^w\to\Q^t
\Q^{t\times d}Use in source · 1 passage
Search aliases: Q^t× d ℚ^t× d Q times mathbb times
Use in source · Constructive_Repair.tex, line 1089
The attaining construction. Suppose the detected residual matrix C=LR has certificate data F∈ℚ^d× t, G∈ℚ^t× s, J∈ℚ^t× d, Q∈ℚ^s× t satisfying LR=FG, JLRQ=I_t. The new augmentation and its correction coefficients are not unspecified witnesses. They are E=KF, U=-PR, W=-G.
Exact mathematical passage
F\in\Q^{d\times t},\quad G\in\Q^{t\times s},\quad J\in\Q^{t\times d},\quad Q\in\Q^{s\times t}
\Q^{t\times m}Use in source · 1 passage
Search aliases: Q^t× m ℚ^t× m Q times mathbb times
Use in source · Constructive_Repair.tex, line 986
Dimension certificates without a reported rank. Suppose an augmentation with t columns succeeds. Its optimality can be certified by two additional matrices H∈ℚ^t× m, Q∈ℚ^s× t with HD=0, HRQ=I_t. These identities make a lower bound on the required dimension explicit.
Exact mathematical passage
H\in\Q^{t\times m},\qquad Q\in\Q^{s\times t}
\Q^{t\times s}Use in source · 1 passage
Search aliases: Q^t× s ℚ^t× s Q times mathbb times
Use in source · Constructive_Repair.tex, line 1089
The attaining construction. Suppose the detected residual matrix C=LR has certificate data F∈ℚ^d× t, G∈ℚ^t× s, J∈ℚ^t× d, Q∈ℚ^s× t satisfying LR=FG, JLRQ=I_t. The new augmentation and its correction coefficients are not unspecified witnesses. They are E=KF, U=-PR, W=-G.
Exact mathematical passage
F\in\Q^{d\times t},\quad G\in\Q^{t\times s},\quad J\in\Q^{t\times d},\quad Q\in\Q^{s\times t}
\Q^wUse in source · 1 passage
Search aliases: Q^w ℚ^w Q mathbb
Use in source · Constructive_Repair.tex, line 1003
[Dimension lower certificate] Assume [source reference]. If an arbitrary competing augmentation E'∈ℚ^m× w has coefficients satisfying DU'+E'W'=-R, then t≤ w. Multiplication by H and Q gives HE'W'Q=-I_t, hence (HE')(-W'Q)=I_t. Thus HE':ℚ^w→ℚ^t has a right inverse. It is surjective, and consequently t≤ w. formalRationalCertificates.dimension_certificate_right_inverse formalRationalCertificates.dimension_certificate_lower_bound
Exact mathematical passage
HE':\Q^w\to\Q^t
Q_{D'}Use in source · 3 passages
Search aliases: Q_D'
Use in source · Constructive_Repair.tex, line 541
It follows that there is a well defined linear map B:Q_D⟶ Q_D', B(q_D(v))=q_D'(b(v)). Indeed, changing v by an element of im D changes b(v) by an element of im D'. This is the quotient map constructed in the formal source, not an assumed function on unidentified obstruction spaces.
Exact mathematical passage
B:Q_D\longrightarrow Q_{D'},\qquad B(q_D(v))=q_{D'}(b(v)).
\qedhereUse in source · 3 passages
Search aliases: qedhere
Use in source · Constructive_Repair.tex, line 280
[Dimension lower bound] If E:W→ V repairs r and W is finite dimensional, then O=O_D(r) is finite dimensional and dim_𝕜O≤dim_𝕜W. By [source reference], O⊆im(q_DE). The image of a linear map from a finite dimensional space is finite dimensional and has dimension at most that of its domain. Hence dim O≤dimim(q_DE)≤dim W.qedhere formalrepair_dimension_lower_bound
Exact mathematical passage
\dim O\leq\dim\im(q_DE)\leq\dim W.\qedhere
\RUse in source · 2 passages
Search aliases: R ℝ mathbb
Use in source · Constructive_Repair.tex, line 872
[A nonlinear root with a nonzero first order obstruction] For a∈ℝ∖{0}, define F_a(x)=x^2-a^2. At zero, F_a'(0)=0, and the correction equation 0· u=a^2 has no solution. Nevertheless, F_a(a)=0. Differentiation gives F_a'(x)=2x, so the derivative at zero is zero. Since a≠0, its square is nonzero, while 0· u=0 for every u. Finally, F_a(a)=a^2-a^2=0. formalNonlinear.nonlinear_root_despite_first_order_obstruction
Exact mathematical passage
a\in\R\setminus\{0\}
\mathsf RUse in source · 3 passages
Search aliases: R mathsf
Use in source · Constructive_Repair.tex, line 375
[Rank difference in matrix coordinates] Let the columns of a matrix R be a finite residual family and let D represent D. Then dim O_D(r)=rank[ Dmid R]-rank D. Set M=im D+span{r_i}. The restriction q_Dvert_M has image O and kernel im D. Rank and nullity give dim M=dimim D+dim O. The columns of [ Dmid R] span M. sourcescopeThis coordinate corollary is an ordinary derivation included for the computational interpretation. The v0.2.0 Lean release proves the abstract attained dimension theorem, but do…
Exact mathematical passage
\mathsf R
\rankUse in source · 5 passages
Search aliases: rank operatorname
Use in source · Constructive_Repair.tex, line 376
[Rank difference in matrix coordinates] Let the columns of a matrix R be a finite residual family and let D represent D. Then dim O_D(r)=rank[ Dmid R]-rank D. Set M=im D+span{r_i}. The restriction q_Dvert_M has image O and kernel im D. Rank and nullity give dim M=dimim D+dim O. The columns of [ Dmid R] span M. sourcescopeThis coordinate corollary is an ordinary derivation included for the computational interpretation. The v0.2.0 Lean release proves the abstract attained dimension theorem, but do…
Exact mathematical passage
\dim O_D(r)=\rank[\mathsf D\mid\mathsf R]-\rank\mathsf D.
s_AUse in source · 3 passages
Search aliases: s_A
Use in source · Constructive_Repair.tex, line 353
abelthm:legal If O⊆ q_D(A), there exists a linear map E:O→ V satisfying im E⊆ A, q_DE=ι_O, and repairing the entire family. If V is finite dimensional, its added dimension is optimal even among all unrestricted repairs. Consider the surjection f:A⟶ q_D(A), a⟼ q_D(a). Choose a linear section s_A:q_D(A)→ A. Let j:O↪ q_D(A) and ι_A:A↪ V be inclusions. Define E=ι_As_Aj. Its image is in A by construction. Moreover, q_Dι_As_Aj=j as a map into Q_D, which is precisely ι_O. By [source reference], E repai…
Exact mathematical passage
s_A:q_D(A)\to A
\sqcupUse in source · 1 passage
Search aliases: sqcup
Use in source · Constructive_Repair.tex, line 1433
[Exact branch partition] If j∈ B∖ A, then I(A,B)= I(A,B∖{j}) sqcup I(A∪{j},B). Every T∈ I(A,B) either excludes j or includes j. In the first case it belongs to the left interval, and in the second it belongs to the right interval. Conversely, each child interval is contained in the parent. Their membership conditions on j are incompatible, so the union is disjoint.
Exact mathematical passage
\mathcal I(A,B)= \mathcal I(A,B\setminus\{j\})\;\sqcup\; \mathcal I(A\cup\{j\},B).
\mathsf TUse in source · 2 passages
Search aliases: T mathsf
Use in source · Constructive_Repair.tex, line 1166
The fractional case uses D=(2/3,4/3)^ T and R=(1/2,5/6)^ T. It exercises nonintegral splitting and correction coefficients while retaining exact arithmetic. Empty and rank-deficient cases are included in the same exported corpus. Every case has its own original input file, certificate file, and formal optimality statement.
Exact mathematical passage
D=(2/3,4/3)^{\mathsf T}
tUse in source · 39 passages
Search aliases: t
Use in source · Constructive_Repair.tex, line 725
What the algorithm does not promise. The reference solver is deliberately finite and exhaustive. With t=|J|, there are 2^t candidate subsets. For a subset of size s, each residual has at most |U| |𝕜|^s candidate coefficient and correction assignments to examine. Summing this upper bound over all subsets gives |I| |U|∑_s=0^tbinom ts|𝕜|^s =|I| |U|(1+|𝕜|)^t possible equation tests before accounting for short circuiting and inadmissible subsets. This is an elementary enumeration bound, not a formal …
Exact mathematical passage
t=|J|
t^2Use in source · 2 passages
Search aliases: t^2
Use in source · Constructive_Repair.tex, line 766
[Quadratic correction identity] Let p,m,x,a,c,t∈ℤ satisfy x^2-a=mc, pmid c+2xt, pmid m. Then mpmid (x+mt)^2-a. Write c+2xt=pd and m=ps. Direct expansion gives (x+mt)^2-a · =(x^2-a)+2mxt+m^2t^2 · =m(c+2xt)+m^2t^2 · =mp(d+st^2).qedhere The last expression displays the required quotient explicitly. formalArithmetic.quadratic_digit_correction
Exact mathematical passage
(x+mt)^2-a &=(x^2-a)+2mxt+m^2t^2\\ &=m(c+2xt)+m^2t^2\\ &=mp(d+st^2).\qedhere
t_kUse in source · 2 passages
Search aliases: t_k
Use in source · Constructive_Repair.tex, line 798
An exact seven-adic trace. For x^2=2 at p=7, start with x_1=3. At each step, let c_k=fracx_k^2-27^k, c_k+2x_kt_k≡0pmod7, x_k+1=x_k+7^kt_k. The following table records normalized choices for this example. Every displayed digit equation is an exact integer calculation.
Exact mathematical passage
c_k=\frac{x_k^2-2}{7^k},\qquad c_k+2x_kt_k\equiv0\pmod7,\qquad x_{k+1}=x_k+7^kt_k.
u_iUse in source · 3 passages
Search aliases: u_i
Use in source · Constructive_Repair.tex, line 420
[Exact finite menu feasibility] The selected menu S repairs the family exactly when O_D(r)⊆ O_S. Equivalently, ∀ i∈ I ∃ u_i∈ U ∃ a_i∈𝕜^S, Du_i+∑_j∈ Sa_ije_j=-r_i. Apply [source reference] to the actual map E_S and use [source reference]. Its reverse direction supplies the original correction witnesses and the selected coefficients, rather than only an abstract statement about dimensions. formalfinite_menu_repair_iff_span
Exact mathematical passage
\forall i\in I\ \exists u_i\in U\ \exists a_i\in\kk^S, \qquad Du_i+\sum_{j\in S}a_{ij}e_j=-r_i.
vUse in source · 17 passages
Search aliases: v
Use in source · Constructive_Repair.tex, line 194
[Exact obstruction criterion] For every r∈ V, ∃ u∈ U (Du=-r) Longleftrightarrow q_D(r)=0. Applying q_D to Du=-r gives 0=-q_D(r), hence q_D(r)=0. Conversely, q_D(r)=0 means r∈im D. Choose v∈ U with Dv=r. Then D(-v)=-r. formalcorrectable_iff_obstruction_zero
Exact mathematical passage
v\in U
\vertUse in source · 4 passages
Search aliases: vert
Use in source · Constructive_Repair.tex, line 337
Directions restricted to a subspace. An application usually prohibits some corrections. A first useful constraint is a subspace A≤ V containing every permitted added direction. Its quotient image is q_D(A)=im(q_Dvert_A:A→ Q_D).
Exact mathematical passage
q_D(A)=\im\bigl(q_D\vert_A:A\to Q_D\bigr).
\vert_AUse in source · 1 passage
Search aliases: vert_A vert
Use in source · Constructive_Repair.tex, line 337
Directions restricted to a subspace. An application usually prohibits some corrections. A first useful constraint is a subspace A≤ V containing every permitted added direction. Its quotient image is q_D(A)=im(q_Dvert_A:A→ Q_D).
Exact mathematical passage
q_D(A)=\im\bigl(q_D\vert_A:A\to Q_D\bigr).
\vert_MUse in source · 1 passage
Search aliases: vert_M vert
Use in source · Constructive_Repair.tex, line 381
[Rank difference in matrix coordinates] Let the columns of a matrix R be a finite residual family and let D represent D. Then dim O_D(r)=rank[ Dmid R]-rank D. Set M=im D+span{r_i}. The restriction q_Dvert_M has image O and kernel im D. Rank and nullity give dim M=dimim D+dim O. The columns of [ Dmid R] span M. sourcescopeThis coordinate corollary is an ordinary derivation included for the computational interpretation. The v0.2.0 Lean release proves the abstract attained dimension theorem, but do…
Exact mathematical passage
q_D\vert_M
\vert_OUse in source · 2 passages
Search aliases: vert_O vert
Use in source · Constructive_Repair.tex, line 570
[Equivalent injectivity criterion] The map B is faithful on O if and only if its restriction Bvert_O:O→ Q_D' is injective. If B is faithful and Bx=By for x,y∈ O, then x-y∈ O and B(x-y)=0. Faithfulness gives x=y. Conversely, if Bvert_O is injective and Bz=0=B0 for z∈ O, injectivity gives z=0. formalfaithfulOn_iff_injective
Exact mathematical passage
B\vert_O:O\to Q_{D'}
W'Use in source · 3 passages
Search aliases: W'
Use in source · Constructive_Repair.tex, line 996
[Dimension lower certificate] Assume [source reference]. If an arbitrary competing augmentation E'∈ℚ^m× w has coefficients satisfying DU'+E'W'=-R, then t≤ w. Multiplication by H and Q gives HE'W'Q=-I_t, hence (HE')(-W'Q)=I_t. Thus HE':ℚ^w→ℚ^t has a right inverse. It is surjective, and consequently t≤ w. formalRationalCertificates.dimension_certificate_right_inverse formalRationalCertificates.dimension_certificate_lower_bound
Exact mathematical passage
DU'+E'W'=-R
w'Use in source · 4 passages
Search aliases: w'
Use in source · Constructive_Repair.tex, line 220
Conversely, choose w with q_D(Ew)=q_D(r). Then q_D(r-Ew)=0, so there is v∈ U with Dv=r-Ew. Taking u=-v and w'=-w gives Du+Ew'=-(r-Ew)-Ew=-r. The witnesses solve the equation in V, not just in its quotient. formalrepairable_iff_obstruction_mem_range
Exact mathematical passage
w'=-w
w_iUse in source · 1 passage
Search aliases: w_i
Use in source · Constructive_Repair.tex, line 1575
The mathematical statements here use ∃ u,w with the same sign convention as the source. Families quantify ∀ i ∃ u_i,w_i. They do not assume one shared correction vector. The algebraic base is a commutative ring. The dimension and section results specialize to a field, and finiteness is stated when numerical dimensions or terminating enumeration are used.
Exact mathematical passage
\forall i\,\exists u_i,w_i
w_jUse in source · 1 passage
Search aliases: w_j
Use in source · Constructive_Repair.tex, line 1418
Let J={0,…,q-1} be the original candidate index set. The matrices D,E,R and the original correction equation remain fixed: DU+widetilde E_S W=-R. Here widetilde E_S zeros unselected columns of E while retaining its original indexing. Costs are nonnegative integers attached to those same columns: c(S)=∑_j∈ Sw_j, w_j∈ℕ. The admissibility rule either permits every subset or supplies a fixed finite table of permitted subsets. An empty table permits none. It is different from the all-subsets rule.
Exact mathematical passage
c(S)=\sum_{j\in S}w_j,\qquad w_j\in\N.
w_{ji}Use in source · 1 passage
Search aliases: w_ji
Use in source · Constructive_Repair.tex, line 950
[Successful certificate] If an admissible S and rational matrices U,W satisfy [source reference], they repair every original residual. Take the ith column of the displayed identity. It is the original equation Du_i+∑_j∈ Sw_jie_j=-r_i. formalRationalCertificates.checkRepair_sound
Exact mathematical passage
Du_i+\sum_{j\in S}w_{ji}e_j=-r_i
\wedgeUse in source · 1 passage
Search aliases: wedge
Use in source · Constructive_Repair.tex, line 667
The repair optimizer is bestRepairMenu =bestByCheck( S↦allowed(S)wedgecheck(S), c, L_J).
Exact mathematical passage
\operatorname{bestRepairMenu} =\operatorname{bestByCheck}\bigl( S\mapsto\operatorname{allowed}(S)\wedge\operatorname{check}(S),\ c,\ \mathcal L_J\bigr).
\widetilde E_TUse in source · 2 passages
Search aliases: widetilde E_T widetilde
Use in source · Constructive_Repair.tex, line 1258
[Downward validity of a separator] If (B,Y) is a separating block and T⊆ B, then Y also separates T. In particular, T cannot satisfy [source reference]. For a selected column j∈ T, one also has j∈ B, so (YE)_0j=0 by the block identity. Every unselected column is zero after masking. Thus Ywidetilde E_T=0. The other two equations in [source reference] are unchanged.
Exact mathematical passage
Y\widetilde E_T=0
XUse in source · 3 passages
Search aliases: X
Use in source · Constructive_Repair.tex, line 1075
[Exact detection] Under [source reference], (∃ X, DX=-R) Longleftrightarrow LR=0. When LR=0, the explicit witness is X=-PR. A correction gives 0=LDX=-LR. Conversely, LR=0 gives R=(DP+KL)R=DPR, so D(-PR)=-R. formalRationalCertificates.split_correctable_iff
Exact mathematical passage
(\exists X,\ DX=-R)\quad\Longleftrightarrow\quad LR=0.
xUse in source · 47 passages
Search aliases: x
Use in source · Constructive_Repair.tex, line 203
[A visible residual] Let D:ℚ→ℚ^2 be D(u)=(u,0) and let r=(2,3). The quotient is identified with the second coordinate. The correction u=-2 removes the first coordinate but leaves (0,3). The functional L(x,y)=y satisfies LD=0 and L(r)=3, so no original correction eliminates r.
Exact mathematical passage
L(x,y)=y
x^2Use in source · 10 passages
Search aliases: x^2
Use in source · Constructive_Repair.tex, line 756
[Quadratic correction identity] Let p,m,x,a,c,t∈ℤ satisfy x^2-a=mc, pmid c+2xt, pmid m. Then mpmid (x+mt)^2-a. Write c+2xt=pd and m=ps. Direct expansion gives (x+mt)^2-a · =(x^2-a)+2mxt+m^2t^2
Exact mathematical passage
x^2-a=mc,\qquad p\mid c+2xt,\qquad p\mid m.
x_0Use in source · 2 passages
Search aliases: x_0
Use in source · Constructive_Repair.tex, line 863
Nonlinear limits and native realizations. A linearized problem is a different equation. Suppose a nonlinear map F is differentiable at an approximation x_0. Its linearized correction equation is DF(x_0)u=-F(x_0). The cokernel criterion completely decides [source reference] once the derivative is fixed. It does not, by itself, decide whether there is x with F(x)=0. Higher order terms are absent from the linearized equation, and they may either create a solution or prevent the linear prediction fr…
Exact mathematical passage
x_0
x_1Use in source · 1 passage
Search aliases: x_1
Use in source · Constructive_Repair.tex, line 797
An exact seven-adic trace. For x^2=2 at p=7, start with x_1=3. At each step, let c_k=fracx_k^2-27^k, c_k+2x_kt_k≡0pmod7, x_k+1=x_k+7^kt_k. The following table records normalized choices for this example. Every displayed digit equation is an exact integer calculation.
Exact mathematical passage
x_1=3
x_kUse in source · 3 passages
Search aliases: x_k
Use in source · Constructive_Repair.tex, line 798
An exact seven-adic trace. For x^2=2 at p=7, start with x_1=3. At each step, let c_k=fracx_k^2-27^k, c_k+2x_kt_k≡0pmod7, x_k+1=x_k+7^kt_k. The following table records normalized choices for this example. Every displayed digit equation is an exact integer calculation.
Exact mathematical passage
c_k=\frac{x_k^2-2}{7^k},\qquad c_k+2x_kt_k\equiv0\pmod7,\qquad x_{k+1}=x_k+7^kt_k.
x_{k+1}Use in source · 2 passages
Search aliases: x_k+1
Use in source · Constructive_Repair.tex, line 798
An exact seven-adic trace. For x^2=2 at p=7, start with x_1=3. At each step, let c_k=fracx_k^2-27^k, c_k+2x_kt_k≡0pmod7, x_k+1=x_k+7^kt_k. The following table records normalized choices for this example. Every displayed digit equation is an exact integer calculation.
Exact mathematical passage
c_k=\frac{x_k^2-2}{7^k},\qquad c_k+2x_kt_k\equiv0\pmod7,\qquad x_{k+1}=x_k+7^kt_k.
x_k^2Use in source · 2 passages
Search aliases: x_k^2
Use in source · Constructive_Repair.tex, line 798
An exact seven-adic trace. For x^2=2 at p=7, start with x_1=3. At each step, let c_k=fracx_k^2-27^k, c_k+2x_kt_k≡0pmod7, x_k+1=x_k+7^kt_k. The following table records normalized choices for this example. Every displayed digit equation is an exact integer calculation.
Exact mathematical passage
c_k=\frac{x_k^2-2}{7^k},\qquad c_k+2x_kt_k\equiv0\pmod7,\qquad x_{k+1}=x_k+7^kt_k.
yUse in source · 12 passages
Search aliases: y
Use in source · Constructive_Repair.tex, line 203
[A visible residual] Let D:ℚ→ℚ^2 be D(u)=(u,0) and let r=(2,3). The quotient is identified with the second coordinate. The correction u=-2 removes the first coordinate but leaves (0,3). The functional L(x,y)=y satisfies LD=0 and L(r)=3, so no original correction eliminates r.
Exact mathematical passage
L(x,y)=y
Y_0Use in source · 1 passage
Search aliases: Y_0
Use in source · Constructive_Repair.tex, line 1331
0=-R. Two separating blocks suffice: B_0={0}, Y_0=(0,1,-1), B_1={1}, Y_1=(0,1,0). Both satisfy Y_iD=0, annihilate their masked candidate matrices, and give Y_iR=1.
Exact mathematical passage
B_0=\{0\},\quad Y_0=(0,1,-1),\qquad B_1=\{1\},\quad Y_1=(0,1,0).
Y_1Use in source · 1 passage
Search aliases: Y_1
Use in source · Constructive_Repair.tex, line 1331
0=-R. Two separating blocks suffice: B_0={0}, Y_0=(0,1,-1), B_1={1}, Y_1=(0,1,0). Both satisfy Y_iD=0, annihilate their masked candidate matrices, and give Y_iR=1.
Exact mathematical passage
B_0=\{0\},\quad Y_0=(0,1,-1),\qquad B_1=\{1\},\quad Y_1=(0,1,0).
Y_iUse in source · 2 passages
Search aliases: Y_i
Use in source · Constructive_Repair.tex, line 1335
0=-R. Two separating blocks suffice: B_0={0}, Y_0=(0,1,-1), B_1={1}, Y_1=(0,1,0). Both satisfy Y_iD=0, annihilate their masked candidate matrices, and give Y_iR=1.
Exact mathematical passage
Y_iD=0
ZUse in source · 5 passages
Search aliases: Z
Use in source · Constructive_Repair.tex, line 200
The quotient also has a universal property. If L:V→ Z annihilates im D, it descends to a unique linear map overline L:Q_D→ Z with L=overline Lq_D. Thus every linear detector that ignores correctable directions factors through the same quotient. This is the classical cokernel construction used in Paper III~[source reference]. Canonicality is relative to D, not to an unspecified mathematical problem.
Exact mathematical passage
L:V\to Z
\ZUse in source · 16 passages
Search aliases: Z ℤ mathbb
Use in source · Constructive_Repair.tex, line 385
The field hypothesis in the section argument is substantive. Over ℤ, take D:ℤ→ℤ to be multiplication by two. The quotient map q:ℤ→ℤ/2ℤ has no ℤ-linear section. A section would send the nonzero class to an integer n with 2n=0, forcing n=0 and contradicting q(n)=1. This elementary example explains why the module feasibility theorem does not automatically imply a splitting theorem over arbitrary rings.
Exact mathematical passage
\Z
|Use in source · 3 passages
Search aliases: |
Use in source · Constructive_Repair.tex, line 725
What the algorithm does not promise. The reference solver is deliberately finite and exhaustive. With t=|J|, there are 2^t candidate subsets. For a subset of size s, each residual has at most |U| |𝕜|^s candidate coefficient and correction assignments to examine. Summing this upper bound over all subsets gives |I| |U|∑_s=0^tbinom ts|𝕜|^s =|I| |U|(1+|𝕜|)^t possible equation tests before accounting for short circuiting and inadmissible subsets. This is an elementary enumeration bound, not a formal …
Exact mathematical passage
t=|J|
|^sUse in source · 2 passages
Search aliases: |^s
Use in source · Constructive_Repair.tex, line 725
What the algorithm does not promise. The reference solver is deliberately finite and exhaustive. With t=|J|, there are 2^t candidate subsets. For a subset of size s, each residual has at most |U| |𝕜|^s candidate coefficient and correction assignments to examine. Summing this upper bound over all subsets gives |I| |U|∑_s=0^tbinom ts|𝕜|^s =|I| |U|(1+|𝕜|)^t possible equation tests before accounting for short circuiting and inadmissible subsets. This is an elementary enumeration bound, not a formal …
Exact mathematical passage
|U|\,|\kk|^s
\cdotUse in source · 5 passages
Search aliases: · cdot
Use in source · Constructive_Repair.tex, line 827
For example, 10^2-2=98=7^2·2, and the next digit satisfies 2+2·10·2=42. Hence 108=10+7^2·2, 108^2-2=7^3·34. The new digit corrects the residual quotient at precisely the next required modulus.
Exact mathematical passage
10^2-2=98=7^2\cdot2,
\iotaUse in source · 10 passages
Search aliases: ι iota
Use in source · Constructive_Repair.tex, line 303
[Attainment on the obstruction span] Let ι_O:O↪ Q_D be inclusion. There exists a linear map E:O→ V such that q_DE=ι_O and E repairs the family. Choose the section s from [source reference] and set E=sι_O. Then q_DE=q_Dsι_O=ι_O. Every z∈ O is therefore in im(q_DE). Family feasibility follows from [source reference]. formalexists_attaining_repair
Exact mathematical passage
\iota_O:O\hookrightarrow Q_D
\iota_AUse in source · 3 passages
Search aliases: ι_A iota
Use in source · Constructive_Repair.tex, line 353
linear map E:O→ V satisfying im E⊆ A, q_DE=ι_O, and repairing the entire family. If V is finite dimensional, its added dimension is optimal even among all unrestricted repairs. Consider the surjection f:A⟶ q_D(A), a⟼ q_D(a). Choose a linear section s_A:q_D(A)→ A. Let j:O↪ q_D(A) and ι_A:A↪ V be inclusions. Define E=ι_As_Aj. Its image is in A by construction. Moreover, q_Dι_As_Aj=j as a map into Q_D, which is precisely ι_O. By [source reference], E repairs the family. The lower bound of [source r…
Exact mathematical passage
\iota_A:A\hookrightarrow V
\iota_OUse in source · 7 passages
Search aliases: ι_O iota
Use in source · Constructive_Repair.tex, line 303
[Attainment on the obstruction span] Let ι_O:O↪ Q_D be inclusion. There exists a linear map E:O→ V such that q_DE=ι_O and E repairs the family. Choose the section s from [source reference] and set E=sι_O. Then q_DE=q_Dsι_O=ι_O. Every z∈ O is therefore in im(q_DE). Family feasibility follows from [source reference]. formalexists_attaining_repair
Exact mathematical passage
\iota_O:O\hookrightarrow Q_D
\mapstoUse in source · 1 passage
Search aliases: ↦ mapsto
Use in source · Constructive_Repair.tex, line 667
The repair optimizer is bestRepairMenu =bestByCheck( S↦allowed(S)wedgecheck(S), c, L_J).
Exact mathematical passage
\operatorname{bestRepairMenu} =\operatorname{bestByCheck}\bigl( S\mapsto\operatorname{allowed}(S)\wedge\operatorname{check}(S),\ c,\ \mathcal L_J\bigr).
\hookrightarrowUse in source · 3 passages
Search aliases: ↪ hookrightarrow
Use in source · Constructive_Repair.tex, line 303
[Attainment on the obstruction span] Let ι_O:O↪ Q_D be inclusion. There exists a linear map E:O→ V such that q_DE=ι_O and E repairs the family. Choose the section s from [source reference] and set E=sι_O. Then q_DE=q_Dsι_O=ι_O. Every z∈ O is therefore in im(q_DE). Family feasibility follows from [source reference]. formalexists_attaining_repair
Exact mathematical passage
\iota_O:O\hookrightarrow Q_D
\existsUse in source · 8 passages
Search aliases: ∃ exists
Use in source · Constructive_Repair.tex, line 189
[Exact obstruction criterion] For every r∈ V, ∃ u∈ U (Du=-r) Longleftrightarrow q_D(r)=0. Applying q_D to Du=-r gives 0=-q_D(r), hence q_D(r)=0. Conversely, q_D(r)=0 means r∈im D. Choose v∈ U with Dv=r. Then D(-v)=-r. formalcorrectable_iff_obstruction_zero
Exact mathematical passage
\exists u\in U\ (Du=-r)\quad\Longleftrightarrow\quad q_D(r)=0.
\varnothingUse in source · 6 passages
Search aliases: ∅ varnothing
Use in source · Constructive_Repair.tex, line 469
∅ · 0 · No
Exact mathematical passage
\varnothing
\notinUse in source · 1 passage
Search aliases: ∉ notin
Use in source · Constructive_Repair.tex, line 1241
[Column-mask identity] For every row Y and column j, (Ywidetilde E_S)_0j= (YE)_0j, · j∈ S, 0, · j∉ S. The mask either retains the entire jth column or replaces it by zero. Expanding the finite matrix product gives the two cases. formalKomorebiRepair.RationalCertificates.mul_masked_entry
Exact mathematical passage
(Y\widetilde E_S)_{0j}= \begin{cases} (YE)_{0j},&j\in S,\\ 0,&j\notin S. \end{cases}
\sumUse in source · 8 passages
Search aliases: ∑ sum
Use in source · Constructive_Repair.tex, line 392
Finite menus and conservation. A menu is an actual coefficient map. Return to a commutative ring 𝕜 and modules U,V. Let e:J→ V be a family of candidate directions and let S⊆ J be finite. A coefficient vector is a function a:S→𝕜. Define E_S:𝕜^S⟶ V, E_S(a)=∑_j∈ Sa_je_j. Finite addition and scalar multiplication show that E_S is linear. The coefficient domain is the selected set itself, so no unselected direction appears in the equation.
Exact mathematical passage
\label{eq:menu} E_S:\kk^S\longrightarrow V,\qquad E_S(a)=\sum_{j\in S}a_je_j.
\sum_{j\in S}Use in source · 7 passages
Search aliases: ∑_j∈ S sum in
Use in source · Constructive_Repair.tex, line 392
Finite menus and conservation. A menu is an actual coefficient map. Return to a commutative ring 𝕜 and modules U,V. Let e:J→ V be a family of candidate directions and let S⊆ J be finite. A coefficient vector is a function a:S→𝕜. Define E_S:𝕜^S⟶ V, E_S(a)=∑_j∈ Sa_je_j. Finite addition and scalar multiplication show that E_S is linear. The coefficient domain is the selected set itself, so no unselected direction appears in the equation.
Exact mathematical passage
\label{eq:menu} E_S:\kk^S\longrightarrow V,\qquad E_S(a)=\sum_{j\in S}a_je_j.
\sum_{s=0}^tUse in source · 1 passage
Search aliases: ∑_s=0^t sum
Use in source · Constructive_Repair.tex, line 726
What the algorithm does not promise. The reference solver is deliberately finite and exhaustive. With t=|J|, there are 2^t candidate subsets. For a subset of size s, each residual has at most |U| |𝕜|^s candidate coefficient and correction assignments to examine. Summing this upper bound over all subsets gives |I| |U|∑_s=0^tbinom ts|𝕜|^s =|I| |U|(1+|𝕜|)^t possible equation tests before accounting for short circuiting and inadmissible subsets. This is an elementary enumeration bound, not a formal …
Exact mathematical passage
|I|\,|U|\sum_{s=0}^t\binom ts|\kk|^s =|I|\,|U|(1+|\kk|)^t
\astUse in source · 5 passages
Search aliases: ∗ ast
Use in source · Constructive_Repair.tex, line 1453
Nonnegative additive costs are monotone under inclusion: A⊆ T Longrightarrow c(A)≤ c(T). Therefore, when an incumbent repair has cost c_∗, the finite check c_∗≤ c(A) excludes every strictly cheaper repair in I(A,B). It does not say the interval is infeasible. It only says that it cannot improve the incumbent. formalKomorebiRepair.RationalCertificates.additiveCost_mono
Exact mathematical passage
c_\ast
\capUse in source · 1 passage
Search aliases: ∩ cap
Use in source · Constructive_Repair.tex, line 567
This condition is equivalent to ker B∩ O=0. It does not require injectivity on all of Q_D when only a smaller family of obstruction classes matters.
Exact mathematical passage
\ker B\cap O=0
\cupUse in source · 1 passage
Search aliases: ∪ cup
Use in source · Constructive_Repair.tex, line 1433
[Exact branch partition] If j∈ B∖ A, then I(A,B)= I(A,B∖{j}) sqcup I(A∪{j},B). Every T∈ I(A,B) either excludes j or includes j. In the first case it belongs to the left interval, and in the second it belongs to the right interval. Conversely, each child interval is contained in the parent. Their membership conditions on j are incompatible, so the union is disjoint.
Exact mathematical passage
\mathcal I(A,B)= \mathcal I(A,B\setminus\{j\})\;\sqcup\; \mathcal I(A\cup\{j\},B).
\congUse in source · 1 passage
Search aliases: ≅ cong
Use in source · Constructive_Repair.tex, line 1015
[Availability of lower certificates] Let O be the span of the residual classes in ℚ^m/im D, and let t=dim O. Then matrices H,Q satisfying [source reference] exist. Choose coordinates O≅ℚ^t, extend that map to the whole quotient, and compose with the quotient map to obtain H. Then HD=0. The columns of HR span ℚ^t, so HR has a linear right inverse Q. sourcescopeThe availability argument is an ordinary finite-dimensional proof. The concrete producer in the next chapter finds and exports such data. …
Exact mathematical passage
O\cong\Q^t
\equivUse in source · 2 passages
Search aliases: ≡ equiv
Use in source · Constructive_Repair.tex, line 798
An exact seven-adic trace. For x^2=2 at p=7, start with x_1=3. At each step, let c_k=fracx_k^2-27^k, c_k+2x_kt_k≡0pmod7, x_k+1=x_k+7^kt_k. The following table records normalized choices for this example. Every displayed digit equation is an exact integer calculation.
Exact mathematical passage
c_k=\frac{x_k^2-2}{7^k},\qquad c_k+2x_kt_k\equiv0\pmod7,\qquad x_{k+1}=x_k+7^kt_k.
\geqUse in source · 2 passages
Search aliases: ≥ geq
Use in source · Constructive_Repair.tex, line 780
The quadratic lifting theorem. [One higher precision] Let p,x,a∈ℤ and k∈ℕ with k≥1. Assume p^kmid x^2-a, gcd(2x,p)=1. Then there exists t∈ℤ such that p^k+1mid (x+p^kt)^2-a. Choose c∈ℤ with x^2-a=p^kc. Coprimality supplies B ezout data for 2x and p, so [source reference] gives t with pmid c+2xt. Since k≥1, one has pmid p^k. Apply [source reference] with m=p^k. formalArithmetic.quadratic_hensel_step
Exact mathematical passage
k\geq1
\longrightarrowUse in source · 5 passages
Search aliases: ⟶ longrightarrow
Use in source · Constructive_Repair.tex, line 159
Let 𝕜 be a commutative ring. All modules are unital 𝕜-modules and all maps in this chapter are 𝕜-linear. Fix D:U⟶ V, and let r:I→ V be a family of residuals. The index set I need not be finite for the algebraic statements. When finite enumeration is used later, finiteness will be imposed explicitly.
Exact mathematical passage
D:U\longrightarrow V,
\longmapstoUse in source · 1 passage
Search aliases: ⟼ longmapsto
Use in source · Constructive_Repair.tex, line 350
[Attainment inside a legal subspace] If O⊆ q_D(A), there exists a linear map E:O→ V satisfying im E⊆ A, q_DE=ι_O, and repairing the entire family. If V is finite dimensional, its added dimension is optimal even among all unrestricted repairs. Consider the surjection f:A⟶ q_D(A), a⟼ q_D(a). Choose a linear section s_A:q_D(A)→ A. Let j:O↪ q_D(A) and ι_A:A↪ V be inclusions. Define E=ι_As_Aj. Its image is in A by construction. Moreover, q_Dι_As_Aj=j as a map into Q_D, which is precisely ι_O. By [sou…
Exact mathematical passage
f:A\longrightarrow q_D(A),\qquad a\longmapsto q_D(a).
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
- packages/constructive-repair/README.md · 0 mathematical passages
- packages/constructive-repair/docs/LICENSING_STATUS.md · 0 mathematical passages
- packages/constructive-repair/docs/PUBLIC_API.md · 0 mathematical passages
- packages/constructive-repair/monograph/Constructive_Repair.tex · 763 mathematical passages
- packages/constructive-repair/python_baseline/README.md · 0 mathematical passages
PDF reading editions (1)
The text index does not extract PDF glyphs. Check the reading edition for notation in figures, tables, and PDF-only material.