Notation by work
Proof Path Theory
All notation · Glossary · Source coverage
389 symbol spellings in 1042 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 389 entries are available below.
=Notation table · 197 passages
Search aliases: =
Notation table · Read passage · Proof_Path_Theory.tex, line 2427
Q(a)=(q_i(a))_i · The joint task representation, least in retained distinctions for its task family.
Exact mathematical passage
Q(a)=(q_i(a))_i
ANotation table · 66 passages
Search aliases: A
Notation table · Read passage · Proof_Path_Theory.tex, line 2418
A, L, T_0 · Required premises, admissible leaves, and requested targets, with A⊆ L.
Exact mathematical passage
A
aNotation table · 52 passages
Search aliases: a
Notation table · Read passage · Proof_Path_Theory.tex, line 2427
Q(a)=(q_i(a))_i · The joint task representation, least in retained distinctions for its task family.
Exact mathematical passage
Q(a)=(q_i(a))_i
\AncNotation table · 4 passages
Search aliases: Anc operatorname
Notation table · Read passage · Proof_Path_Theory.tex, line 2421
Anc_L(T_0) · Backward ancestry expanded only outside the admissible leaves.
Exact mathematical passage
\Anc_L(T_0)
\Anc_LNotation table · 4 passages
Search aliases: Anc_L Anc operatorname
Notation table · Read passage · Proof_Path_Theory.tex, line 2421
Anc_L(T_0) · Backward ancestry expanded only outside the admissible leaves.
Exact mathematical passage
\Anc_L(T_0)
CNotation table · 55 passages
Search aliases: C
Notation table · Read passage · Proof_Path_Theory.tex, line 2428
mathscr A, C, q · A class of possible archives, an encoding scheme, and a task on that class.
Exact mathematical passage
C
\mathrm{cert}Notation table · 6 passages
Search aliases: cert mathrm
Notation table · Read passage · Proof_Path_Theory.tex, line 2420
D_cert(K,H) · The least certified closure in the selected record.
Exact mathematical passage
D_{\mathrm{cert}}(K,H)
\operatorname{cl}Notation table · 25 passages
Search aliases: cl operatorname
Notation table · Read passage · Proof_Path_Theory.tex, line 2424
cl_F(S) · The least declared rule model containing the positive observations S and all admitted leaves.
Exact mathematical passage
\operatorname{cl}_F(S)
\operatorname{cl}_FNotation table · 20 passages
Search aliases: cl_F operatorname
Notation table · Read passage · Proof_Path_Theory.tex, line 2424
cl_F(S) · The least declared rule model containing the positive observations S and all admitted leaves.
Exact mathematical passage
\operatorname{cl}_F(S)
DNotation table · 27 passages
Search aliases: D
Notation table · Read passage · Proof_Path_Theory.tex, line 2420
D_cert(K,H) · The least certified closure in the selected record.
Exact mathematical passage
D_{\mathrm{cert}}(K,H)
D_{\mathrm{cert}}Notation table · 3 passages
Search aliases: D_cert mathrm
Notation table · Read passage · Proof_Path_Theory.tex, line 2420
D_cert(K,H) · The least certified closure in the selected record.
Exact mathematical passage
D_{\mathrm{cert}}(K,H)
ENotation table · 19 passages
Search aliases: E
Notation table · Read passage · Proof_Path_Theory.tex, line 2430
D:E→ R, p:E→ S · A linear defect and a protected observable. The repair condition is Dy=0, p(y)=p(x).
Exact mathematical passage
D:E\to R
\mathrm{eff}Notation table · 7 passages
Search aliases: eff mathrm
Notation table · Read passage · Proof_Path_Theory.tex, line 2433
n_eff · A real, variance-equivalent review count in the specified covariance model.
Exact mathematical passage
n_{\mathrm{eff}}
\operatorname{Ext}Notation table · 7 passages
Search aliases: Ext operatorname
Notation table · Read passage · Proof_Path_Theory.tex, line 2425
Ext_F(S,N) · Rule models containing S and avoiding the negative observations N.
Exact mathematical passage
\operatorname{Ext}_F(S,N)
\operatorname{Ext}_FNotation table · 7 passages
Search aliases: Ext_F operatorname
Notation table · Read passage · Proof_Path_Theory.tex, line 2425
Ext_F(S,N) · Rule models containing S and avoiding the negative observations N.
Exact mathematical passage
\operatorname{Ext}_F(S,N)
FNotation table · 81 passages
Search aliases: F
Notation table · Read passage · Proof_Path_Theory.tex, line 2422
M_F(U) · Local models on patch U satisfying all certified rules supported entirely in U.
Exact mathematical passage
\mathcal M_F(U)
F_{\mathcal U}Notation table · 12 passages
Search aliases: F_ U mathcal
Notation table · Read passage · Proof_Path_Theory.tex, line 2426
F_ U · The same field with only rules whose entire supports appear in a covering patch.
Exact mathematical passage
F_{\mathcal U}
HNotation table · 47 passages
Search aliases: H
Notation table · Read passage · Proof_Path_Theory.tex, line 2419
(K,H) · Selected nodes and certified justification records. Only usable rules contribute to derivability.
Exact mathematical passage
(K,H)
iNotation table · 59 passages
Search aliases: i
Notation table · Read passage · Proof_Path_Theory.tex, line 2427
Q(a)=(q_i(a))_i · The joint task representation, least in retained distinctions for its task family.
Exact mathematical passage
Q(a)=(q_i(a))_i
\JcalNotation table · 6 passages
Search aliases: Jcal J mathcal
Notation table · Read passage · Proof_Path_Theory.tex, line 2417
P, V, J · A declared proof field, its nodes, and its justifications.
Exact mathematical passage
\Jcal
KNotation table · 64 passages
Search aliases: K
Notation table · Read passage · Proof_Path_Theory.tex, line 2419
(K,H) · Selected nodes and certified justification records. Only usable rules contribute to derivability.
Exact mathematical passage
(K,H)
\kerNotation table · 8 passages
Search aliases: ker
Notation table · Read passage · Proof_Path_Theory.tex, line 2431
H=ker D∩ker p · The ambiguity space of a nonempty protected fiber. This H is not a set of justifications.
Exact mathematical passage
H=\ker D\cap\ker p
LNotation table · 54 passages
Search aliases: L
Notation table · Read passage · Proof_Path_Theory.tex, line 2418
A, L, T_0 · Required premises, admissible leaves, and requested targets, with A⊆ L.
Exact mathematical passage
L
MNotation table · 31 passages
Search aliases: M
Notation table · Read passage · Proof_Path_Theory.tex, line 2432
U_M(S) · Weighted target reach from the mandatory starts and a selected supplement, in a fixed directed bridge graph.
Exact mathematical passage
U_M(S)
\mathcal MNotation table · 8 passages
Search aliases: M mathcal
Notation table · Read passage · Proof_Path_Theory.tex, line 2422
M_F(U) · Local models on patch U satisfying all certified rules supported entirely in U.
Exact mathematical passage
\mathcal M_F(U)
\mathcal M_FNotation table · 8 passages
Search aliases: M_F mathcal
Notation table · Read passage · Proof_Path_Theory.tex, line 2422
M_F(U) · Local models on patch U satisfying all certified rules supported entirely in U.
Exact mathematical passage
\mathcal M_F(U)
\mathscrNotation table · 20 passages
Search aliases: mathscr
Notation table · Read passage · Proof_Path_Theory.tex, line 2428
mathscr A, C, q · A class of possible archives, an encoding scheme, and a task on that class.
Exact mathematical passage
\mathscr A
NNotation table · 31 passages
Search aliases: N
Notation table · Read passage · Proof_Path_Theory.tex, line 2425
Ext_F(S,N) · Rule models containing S and avoiding the negative observations N.
Exact mathematical passage
\operatorname{Ext}_F(S,N)
nNotation table · 37 passages
Search aliases: n
Notation table · Read passage · Proof_Path_Theory.tex, line 2433
n_eff · A real, variance-equivalent review count in the specified covariance model.
Exact mathematical passage
n_{\mathrm{eff}}
n_{\mathrm{eff}}Notation table · 7 passages
Search aliases: n_eff mathrm
Notation table · Read passage · Proof_Path_Theory.tex, line 2433
n_eff · A real, variance-equivalent review count in the specified covariance model.
Exact mathematical passage
n_{\mathrm{eff}}
PNotation table · 17 passages
Search aliases: P
Notation table · Read passage · Proof_Path_Theory.tex, line 2429
P_K(S)=S∩ K · Pure retention of records selected by a fixed mask.
Exact mathematical passage
P_K(S)=S\cap K
pNotation table · 18 passages
Search aliases: p
Notation table · Read passage · Proof_Path_Theory.tex, line 2430
D:E→ R, p:E→ S · A linear defect and a protected observable. The repair condition is Dy=0, p(y)=p(x).
Exact mathematical passage
p:E\to S
P_KNotation table · 5 passages
Search aliases: P_K
Notation table · Read passage · Proof_Path_Theory.tex, line 2429
P_K(S)=S∩ K · Pure retention of records selected by a fixed mask.
Exact mathematical passage
P_K(S)=S\cap K
\PcalNotation table · 29 passages
Search aliases: Pcal P mathcal
Notation table · Read passage · Proof_Path_Theory.tex, line 2417
P, V, J · A declared proof field, its nodes, and its justifications.
Exact mathematical passage
\Pcal
QNotation table · 29 passages
Search aliases: Q
Notation table · Read passage · Proof_Path_Theory.tex, line 2427
Q(a)=(q_i(a))_i · The joint task representation, least in retained distinctions for its task family.
Exact mathematical passage
Q(a)=(q_i(a))_i
qNotation table · 47 passages
Search aliases: q
Notation table · Read passage · Proof_Path_Theory.tex, line 2427
Q(a)=(q_i(a))_i · The joint task representation, least in retained distinctions for its task family.
Exact mathematical passage
Q(a)=(q_i(a))_i
q_iNotation table · 5 passages
Search aliases: q_i
Notation table · Read passage · Proof_Path_Theory.tex, line 2427
Q(a)=(q_i(a))_i · The joint task representation, least in retained distinctions for its task family.
Exact mathematical passage
Q(a)=(q_i(a))_i
RNotation table · 40 passages
Search aliases: R
Notation table · Read passage · Proof_Path_Theory.tex, line 2430
D:E→ R, p:E→ S · A linear defect and a protected observable. The repair condition is Dy=0, p(y)=p(x).
Exact mathematical passage
D:E\to R
SNotation table · 98 passages
Search aliases: S
Notation table · Read passage · Proof_Path_Theory.tex, line 2424
cl_F(S) · The least declared rule model containing the positive observations S and all admitted leaves.
Exact mathematical passage
\operatorname{cl}_F(S)
TNotation table · 29 passages
Search aliases: T
Notation table · Read passage · Proof_Path_Theory.tex, line 2418
A, L, T_0 · Required premises, admissible leaves, and requested targets, with A⊆ L.
Exact mathematical passage
T_0
T_0Notation table · 11 passages
Search aliases: T_0
Notation table · Read passage · Proof_Path_Theory.tex, line 2418
A, L, T_0 · Required premises, admissible leaves, and requested targets, with A⊆ L.
Exact mathematical passage
T_0
UNotation table · 55 passages
Search aliases: U
Notation table · Read passage · Proof_Path_Theory.tex, line 2422
M_F(U) · Local models on patch U satisfying all certified rules supported entirely in U.
Exact mathematical passage
\mathcal M_F(U)
\mathcal UNotation table · 13 passages
Search aliases: U mathcal
Notation table · Read passage · Proof_Path_Theory.tex, line 2426
F_ U · The same field with only rules whose entire supports appear in a covering patch.
Exact mathematical passage
F_{\mathcal U}
U_MNotation table · 9 passages
Search aliases: U_M
Notation table · Read passage · Proof_Path_Theory.tex, line 2432
U_M(S) · Weighted target reach from the mandatory starts and a selected supplement, in a fixed directed bridge graph.
Exact mathematical passage
U_M(S)
VNotation table · 45 passages
Search aliases: V
Notation table · Read passage · Proof_Path_Theory.tex, line 2417
P, V, J · A declared proof field, its nodes, and its justifications.
Exact mathematical passage
V
xNotation table · 51 passages
Search aliases: x
Notation table · Read passage · Proof_Path_Theory.tex, line 2430
D:E→ R, p:E→ S · A linear defect and a protected observable. The repair condition is Dy=0, p(y)=p(x).
Exact mathematical passage
p(y)=p(x)
yNotation table · 41 passages
Search aliases: y
Notation table · Read passage · Proof_Path_Theory.tex, line 2430
D:E→ R, p:E→ S · A linear defect and a protected observable. The repair condition is Dy=0, p(y)=p(x).
Exact mathematical passage
Dy=0
\GammaNotation table · 6 passages
Search aliases: Γ Gamma
Notation table · Read passage · Proof_Path_Theory.tex, line 2423
Γ( M_F) · Coherent families of those local models under restriction.
Exact mathematical passage
\Gamma(\mathcal M_F)
\toNotation table · 53 passages
Search aliases: → to
Notation table · Read passage · Proof_Path_Theory.tex, line 2430
D:E→ R, p:E→ S · A linear defect and a protected observable. The repair condition is Dy=0, p(y)=p(x).
Exact mathematical passage
D:E\to R
\capNotation table · 23 passages
Search aliases: ∩ cap
Notation table · Read passage · Proof_Path_Theory.tex, line 2429
P_K(S)=S∩ K · Pure retention of records selected by a fixed mask.
Exact mathematical passage
P_K(S)=S\cap K
\subseteqNotation table · 63 passages
Search aliases: ⊆ subseteq
Notation table · Read passage · Proof_Path_Theory.tex, line 2418
A, L, T_0 · Required premises, admissible leaves, and requested targets, with A⊆ L.
Exact mathematical passage
A\subseteq L
*Definition passage · 11 passages
Search aliases: *
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 582
[Coherent views of a proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are addi…
Exact mathematical passage
e^*:F_w\to F_v
+Definition passage · 33 passages
Search aliases: +
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1110
A trace σ=(j_1,…,j_k) is a list of rule addresses. Replay begins with the list K_0=Lmathbin+ +S. It rejects an unknown rule address or a step whose premises are not all known. Otherwise it adds the conclusion. Strict replay additionally requires the conclusion to be new. Causal replay permits a conclusion already known. Lists are compared by membership when they represent sets.
Exact mathematical passage
K_0=L\mathbin{+\!+}S
\mathbf1Definition passage · 9 passages
Search aliases: 1 mathbf
Definition passage: Future reach utility · Read passage · Proof_Path_Theory.tex, line 1634
[Future reach utility] The weighted future reach of S is U(S)=∑_f∈ Fw_f 1{f∈Reach_ B(S)}.
Exact mathematical passage
U(S)=\sum_{f\in F}w_f\, \mathbf 1\{f\in\Reach_{\Bcal}(S)\}.
A_jDefinition passage · 13 passages
Search aliases: A_j
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1108
[Finite indexed problem and trace] An indexed problem P specifies a finite address space V_n={0,…,n-1}, admitted leaves L, a list of certified rules, positive observations S, and forbidden nodes N. A rule at address j has a finite premise list A_j and conclusion b_j. Two identical rows may have different rule addresses. Every listed node must belong to V_n. Node lists are individually duplicate free, but L, S, and N need not be disjoint.
Exact mathematical passage
A_j
\operatorname{Aff}Definition passage · 4 passages
Search aliases: Aff operatorname
Definition passage: Syntactic affected set · Read passage · Proof_Path_Theory.tex, line 1792
[Syntactic affected set] For a changed node set X⊆ V, define Aff(X)=X∪Desc(X), where descendants are computed in the declared dependency graph.
Exact mathematical passage
\operatorname{Aff}(X)=X\cup\Desc(X),
BDefinition passage · 30 passages
Search aliases: B
Definition passage: Latent bridge graph · Read passage · Proof_Path_Theory.tex, line 1623
[Latent bridge graph] A latent bridge graph is a finite directed graph B=(W,E_B) whose nodes include retained proof objects, omitted proof objects, and anticipated future targets. An edge x→ y means that x has been declared a possible transfer route toward y. The edge may be certified, conjectural, or exploratory, but its status must be recorded.
Exact mathematical passage
\Bcal=(W,E_B)
bDefinition passage · 64 passages
Search aliases: b
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1108
[Finite indexed problem and trace] An indexed problem P specifies a finite address space V_n={0,…,n-1}, admitted leaves L, a list of certified rules, positive observations S, and forbidden nodes N. A rule at address j has a finite premise list A_j and conclusion b_j. Two identical rows may have different rule addresses. Every listed node must belong to V_n. Node lists are individually duplicate free, but L, S, and N need not be disjoint.
Exact mathematical passage
b_j
b_jDefinition passage · 1 passage
Search aliases: b_j
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1108
[Finite indexed problem and trace] An indexed problem P specifies a finite address space V_n={0,…,n-1}, admitted leaves L, a list of certified rules, positive observations S, and forbidden nodes N. A rule at address j has a finite premise list A_j and conclusion b_j. Two identical rows may have different rule addresses. Every listed node must belong to V_n. Node lists are individually duplicate free, but L, S, and N need not be disjoint.
Exact mathematical passage
b_j
\BcalDefinition passage · 4 passages
Search aliases: Bcal B mathcal
Definition passage: Latent bridge graph · Read passage · Proof_Path_Theory.tex, line 1623
[Latent bridge graph] A latent bridge graph is a finite directed graph B=(W,E_B) whose nodes include retained proof objects, omitted proof objects, and anticipated future targets. An edge x→ y means that x has been declared a possible transfer route toward y. The edge may be certified, conjectural, or exploratory, but its status must be recorded.
Exact mathematical passage
\Bcal=(W,E_B)
\mathbf cDefinition passage · 2 passages
Search aliases: c mathbf
Definition passage: Typed proof field · Read passage · Proof_Path_Theory.tex, line 306
[Typed proof field] A finite typed proof field is a tuple P=(V, J,A,T,τ, E, v, c), where: item V is a finite set of claim nodes. item J is a finite set of justifications. item Each j∈ J has a finite premise set prem(j)⊆ V and one conclusion con(j)∈ V. item A⊆ V is the set of required premises of the declared judgment. item T⊆ V is the nonempty target set. item τ assigns node and justification types. item E is a typed evidence ledger. item v assigns nonnegative value coordinates to nodes. item c …
Exact mathematical passage
\Pcal=(V,\Jcal,A,T,\tau,\Ecal,\mathbf v,\mathbf c),
cDefinition passage · 50 passages
Search aliases: c
Definition passage: Future task model · Read passage · Proof_Path_Theory.tex, line 1521
[Future task model] Let T be a finite task set with probabilities p_t≥0 satisfying ∑_t p_t=1. Let R_t⊆ V be the node set required by task t, and let c(v)≥0 be the recovery cost of node v when it is absent.
Exact mathematical passage
c(v)\ge0
c_dDefinition passage · 5 passages
Search aliases: c_d
Definition passage: Goal-relative depth objective · Read passage · Proof_Path_Theory.tex, line 2065
[Goal-relative depth objective] For goal g with weights α_g,β_g≥0, define J_g(d)=α_g r_d+β_g c_d. An optimal expansion depth is any minimizer of J_g.
Exact mathematical passage
J_g(d)=\alpha_g r_d+\beta_g c_d.
\CcalDefinition passage · 2 passages
Search aliases: Ccal C mathcal
Definition passage: Certificate · Read passage · Proof_Path_Theory.tex, line 414
[Certificate] A certificate for a nonempty requested target set T_0⊆ V is a pair C=(K,H), K⊆ V, H⊆ J^cert, such that A∪ T_0⊆ K and T_0⊆ D_cert(K,H). Order certificates componentwise: (K,H)≤(K^prime,H^prime) means K⊆ K^prime and H⊆ H^prime. A least certificate is contained in every certificate for the same request. Minimizing only the node set, only the justification set, or a numerical cost is a different objective.
Exact mathematical passage
\Ccal=(K,H), \qquad K\subseteq V, \qquad H\subseteq\Jcal^{\mathrm{cert}},
\mathsf{Cert}Definition passage · 5 passages
Search aliases: Cert mathsf
Definition passage: Certified proof category · Read passage · Proof_Path_Theory.tex, line 529
[Certified proof category] Fix a directed graph of typed mathematical states and certified primitive transformations. Its path category Cert has these states as objects and finite composable paths as morphisms. The empty path is an identity, and composition is concatenation. One may further identify paths by a declared congruence compatible with concatenation. Associativity and the identity laws then hold by construction.
Exact mathematical passage
\mathsf{Cert}
\mathsf{Certificate}Definition passage · 1 passage
Search aliases: Certificate mathsf
Definition passage: Compositional certificate map · Read passage · Proof_Path_Theory.tex, line 556
[Compositional certificate map] A compositional certificate map is a functor C:Expanded⟶Certificate that sends expanded certified paths to checkable certificate paths and preserves identity and composition.
Exact mathematical passage
\Ccal:\mathsf{Expanded}\longrightarrow\mathsf{Certificate}
\operatorname{con}Definition passage · 4 passages
Search aliases: con operatorname
Definition passage: Typed proof field · Read passage · Proof_Path_Theory.tex, line 313
[Typed proof field] A finite typed proof field is a tuple P=(V, J,A,T,τ, E, v, c), where: item V is a finite set of claim nodes. item J is a finite set of justifications. item Each j∈ J has a finite premise set prem(j)⊆ V and one conclusion con(j)∈ V. item A⊆ V is the set of required premises of the declared judgment. item T⊆ V is the nonempty target set. item τ assigns node and justification types. item E is a typed evidence ledger. item v assigns nonnegative value coordinates to nodes. item c …
Exact mathematical passage
\operatorname{con}(j)\in V
dDefinition passage · 36 passages
Search aliases: d
Definition passage: Task-sufficient representation · Read passage · Proof_Path_Theory.tex, line 1265
[Task-sufficient representation] The scheme C:mathscr A→mathscr R is sufficient for q when there is a single decoder d_q:C(mathscr A)→ Y_q such that q( P)=d_q(C( P)) for every P∈mathscr A. It is Q-sufficient when this holds for every q∈ Q. The decoder may depend on the task and the scheme, but not on hidden knowledge of the particular archive being decoded.
Exact mathematical passage
d_q:C(\mathscr A)\to Y_q
d_qDefinition passage · 5 passages
Search aliases: d_q
Definition passage: Task-sufficient representation · Read passage · Proof_Path_Theory.tex, line 1265
[Task-sufficient representation] The scheme C:mathscr A→mathscr R is sufficient for q when there is a single decoder d_q:C(mathscr A)→ Y_q such that q( P)=d_q(C( P)) for every P∈mathscr A. It is Q-sufficient when this holds for every q∈ Q. The decoder may depend on the task and the scheme, but not on hidden knowledge of the particular archive being decoded.
Exact mathematical passage
d_q:C(\mathscr A)\to Y_q
\DebtDefinition passage · 2 passages
Search aliases: Debt operatorname
Definition passage: Expected compression debt · Read passage · Proof_Path_Theory.tex, line 1527
[Expected compression debt] The expected compression debt of retained set K is Debt(K) = ∑_t∈ Tp_t ∑_v∈ R_t∖ Kc(v).
Exact mathematical passage
\Debt(K) = \sum_{t\in\Tcal}p_t \sum_{v\in R_t\setminus K}c(v).
\DescDefinition passage · 1 passage
Search aliases: Desc operatorname
Definition passage: Syntactic affected set · Read passage · Proof_Path_Theory.tex, line 1792
[Syntactic affected set] For a changed node set X⊆ V, define Aff(X)=X∪Desc(X), where descendants are computed in the declared dependency graph.
Exact mathematical passage
\operatorname{Aff}(X)=X\cup\Desc(X),
eDefinition passage · 20 passages
Search aliases: e
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 582
[Coherent views of a proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are addi…
Exact mathematical passage
e:v\to w
e^*Definition passage · 3 passages
Search aliases: e^*
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 582
[Coherent views of a proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are addi…
Exact mathematical passage
e^*:F_w\to F_v
E_BDefinition passage · 1 passage
Search aliases: E_B
Definition passage: Latent bridge graph · Read passage · Proof_Path_Theory.tex, line 1623
[Latent bridge graph] A latent bridge graph is a finite directed graph B=(W,E_B) whose nodes include retained proof objects, omitted proof objects, and anticipated future targets. An edge x→ y means that x has been declared a possible transfer route toward y. The edge may be certified, conjectural, or exploratory, but its status must be recorded.
Exact mathematical passage
\Bcal=(W,E_B)
\EcalDefinition passage · 2 passages
Search aliases: Ecal E mathcal
Definition passage: Typed proof field · Read passage · Proof_Path_Theory.tex, line 306
[Typed proof field] A finite typed proof field is a tuple P=(V, J,A,T,τ, E, v, c), where: item V is a finite set of claim nodes. item J is a finite set of justifications. item Each j∈ J has a finite premise set prem(j)⊆ V and one conclusion con(j)∈ V. item A⊆ V is the set of required premises of the declared judgment. item T⊆ V is the nonempty target set. item τ assigns node and justification types. item E is a typed evidence ledger. item v assigns nonnegative value coordinates to nodes. item c …
Exact mathematical passage
\Pcal=(V,\Jcal,A,T,\tau,\Ecal,\mathbf v,\mathbf c),
\mathsf{Expanded}Definition passage · 1 passage
Search aliases: Expanded mathsf
Definition passage: Compositional certificate map · Read passage · Proof_Path_Theory.tex, line 556
[Compositional certificate map] A compositional certificate map is a functor C:Expanded⟶Certificate that sends expanded certified paths to checkable certificate paths and preserves identity and composition.
Exact mathematical passage
\Ccal:\mathsf{Expanded}\longrightarrow\mathsf{Certificate}
fDefinition passage · 29 passages
Search aliases: f
Definition passage: Future reach utility · Read passage · Proof_Path_Theory.tex, line 1634
[Future reach utility] The weighted future reach of S is U(S)=∑_f∈ Fw_f 1{f∈Reach_ B(S)}.
Exact mathematical passage
U(S)=\sum_{f\in F}w_f\, \mathbf 1\{f\in\Reach_{\Bcal}(S)\}.
F_vDefinition passage · 3 passages
Search aliases: F_v
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 582
[Coherent views of a proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are addi…
Exact mathematical passage
F_v
F_wDefinition passage · 1 passage
Search aliases: F_w
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 582
[Coherent views of a proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are addi…
Exact mathematical passage
e^*:F_w\to F_v
gDefinition passage · 11 passages
Search aliases: g
Definition passage: Proof compiler · Read passage · Proof_Path_Theory.tex, line 1594
[Proof compiler] Let g be a presentation goal and let P be a versioned proof field. A proof compiler is a map on the declared archive class Γ_g:mathscr A⟶ R_g that selects, orders, and renders the material required by g while preserving links to canonical claim and justification identifiers.
Exact mathematical passage
g
H^{\prime}Definition passage · 2 passages
Search aliases: H^prime prime
Definition passage: Certificate · Read passage · Proof_Path_Theory.tex, line 425
[Certificate] A certificate for a nonempty requested target set T_0⊆ V is a pair C=(K,H), K⊆ V, H⊆ J^cert, such that A∪ T_0⊆ K and T_0⊆ D_cert(K,H). Order certificates componentwise: (K,H)≤(K^prime,H^prime) means K⊆ K^prime and H⊆ H^prime. A least certificate is contained in every certificate for the same request. Minimizing only the node set, only the justification set, or a numerical cost is a different objective.
Exact mathematical passage
(K,H)\leq(K^{\prime},H^{\prime})
JDefinition passage · 6 passages
Search aliases: J
Definition passage: Goal-relative depth objective · Read passage · Proof_Path_Theory.tex, line 2065
[Goal-relative depth objective] For goal g with weights α_g,β_g≥0, define J_g(d)=α_g r_d+β_g c_d. An optimal expansion depth is any minimizer of J_g.
Exact mathematical passage
J_g(d)=\alpha_g r_d+\beta_g c_d.
jDefinition passage · 47 passages
Search aliases: j
Definition passage: Typed proof field · Read passage · Proof_Path_Theory.tex, line 313
[Typed proof field] A finite typed proof field is a tuple P=(V, J,A,T,τ, E, v, c), where: item V is a finite set of claim nodes. item J is a finite set of justifications. item Each j∈ J has a finite premise set prem(j)⊆ V and one conclusion con(j)∈ V. item A⊆ V is the set of required premises of the declared judgment. item T⊆ V is the nonempty target set. item τ assigns node and justification types. item E is a typed evidence ledger. item v assigns nonnegative value coordinates to nodes. item c …
Exact mathematical passage
j\in\Jcal
j_1Definition passage · 1 passage
Search aliases: j_1
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1110
A trace σ=(j_1,…,j_k) is a list of rule addresses. Replay begins with the list K_0=Lmathbin+ +S. It rejects an unknown rule address or a step whose premises are not all known. Otherwise it adds the conclusion. Strict replay additionally requires the conclusion to be new. Causal replay permits a conclusion already known. Lists are compared by membership when they represent sets.
Exact mathematical passage
\sigma=(j_1,\ldots,j_k)
J_gDefinition passage · 3 passages
Search aliases: J_g
Definition passage: Goal-relative depth objective · Read passage · Proof_Path_Theory.tex, line 2065
[Goal-relative depth objective] For goal g with weights α_g,β_g≥0, define J_g(d)=α_g r_d+β_g c_d. An optimal expansion depth is any minimizer of J_g.
Exact mathematical passage
J_g(d)=\alpha_g r_d+\beta_g c_d.
j_kDefinition passage · 1 passage
Search aliases: j_k
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1110
A trace σ=(j_1,…,j_k) is a list of rule addresses. Replay begins with the list K_0=Lmathbin+ +S. It rejects an unknown rule address or a step whose premises are not all known. Otherwise it adds the conclusion. Strict replay additionally requires the conclusion to be new. Causal replay permits a conclusion already known. Lists are compared by membership when they represent sets.
Exact mathematical passage
\sigma=(j_1,\ldots,j_k)
\Jcal^{\mathrm{cert}}Definition passage · 1 passage
Search aliases: Jcal^cert J^cert Jcal mathrm mathcal mathrm
Definition passage: Certificate · Read passage · Proof_Path_Theory.tex, line 414
[Certificate] A certificate for a nonempty requested target set T_0⊆ V is a pair C=(K,H), K⊆ V, H⊆ J^cert, such that A∪ T_0⊆ K and T_0⊆ D_cert(K,H). Order certificates componentwise: (K,H)≤(K^prime,H^prime) means K⊆ K^prime and H⊆ H^prime. A least certificate is contained in every certificate for the same request. Minimizing only the node set, only the justification set, or a numerical cost is a different objective.
Exact mathematical passage
\Ccal=(K,H), \qquad K\subseteq V, \qquad H\subseteq\Jcal^{\mathrm{cert}},
kDefinition passage · 25 passages
Search aliases: k
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1110
A trace σ=(j_1,…,j_k) is a list of rule addresses. Replay begins with the list K_0=Lmathbin+ +S. It rejects an unknown rule address or a step whose premises are not all known. Otherwise it adds the conclusion. Strict replay additionally requires the conclusion to be new. Causal replay permits a conclusion already known. Lists are compared by membership when they represent sets.
Exact mathematical passage
\sigma=(j_1,\ldots,j_k)
K^{\prime}Definition passage · 2 passages
Search aliases: K^prime prime
Definition passage: Certificate · Read passage · Proof_Path_Theory.tex, line 425
[Certificate] A certificate for a nonempty requested target set T_0⊆ V is a pair C=(K,H), K⊆ V, H⊆ J^cert, such that A∪ T_0⊆ K and T_0⊆ D_cert(K,H). Order certificates componentwise: (K,H)≤(K^prime,H^prime) means K⊆ K^prime and H⊆ H^prime. A least certificate is contained in every certificate for the same request. Minimizing only the node set, only the justification set, or a numerical cost is a different objective.
Exact mathematical passage
(K,H)\leq(K^{\prime},H^{\prime})
K_0Definition passage · 2 passages
Search aliases: K_0
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1110
A trace σ=(j_1,…,j_k) is a list of rule addresses. Replay begins with the list K_0=Lmathbin+ +S. It rejects an unknown rule address or a step whose premises are not all known. Otherwise it adds the conclusion. Strict replay additionally requires the conclusion to be new. Causal replay permits a conclusion already known. Lists are compared by membership when they represent sets.
Exact mathematical passage
K_0=L\mathbin{+\!+}S
\LossDefinition passage · 2 passages
Search aliases: Loss operatorname
Definition passage: Additive loss vector · Read passage · Proof_Path_Theory.tex, line 1487
[Additive loss vector] For a retained node set K⊆ V, define Loss( P,K) = ∑_v∉ K v(v). Normalize a coordinate by its total only when that total is positive. If the total is zero, nonnegativity makes every contribution in that coordinate zero. The implementation records normalized loss zero there as a convention, rather than dividing by zero.
Exact mathematical passage
\Loss(\Pcal,K) = \sum_{v\notin K}\mathbf v(v).
\mathbinDefinition passage · 2 passages
Search aliases: mathbin
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1110
A trace σ=(j_1,…,j_k) is a list of rule addresses. Replay begins with the list K_0=Lmathbin+ +S. It rejects an unknown rule address or a step whose premises are not all known. Otherwise it adds the conclusion. Strict replay additionally requires the conclusion to be new. Causal replay permits a conclusion already known. Lists are compared by membership when they represent sets.
Exact mathematical passage
K_0=L\mathbin{+\!+}S
p_tDefinition passage · 3 passages
Search aliases: p_t
Definition passage: Future task model · Read passage · Proof_Path_Theory.tex, line 1521
[Future task model] Let T be a finite task set with probabilities p_t≥0 satisfying ∑_t p_t=1. Let R_t⊆ V be the node set required by task t, and let c(v)≥0 be the recovery cost of node v when it is absent.
Exact mathematical passage
p_t\ge0
\Pcal^{\mathrm{cert}}Definition passage · 1 passage
Search aliases: Pcal^cert P^cert Pcal mathrm mathcal mathrm
Definition passage: Certified subfield · Read passage · Proof_Path_Theory.tex, line 335
[Certified subfield] The certified subfield P^cert contains every node of P and only those justifications accepted by the declared certification policy. Evidence and scope are part of that policy. A certification flag records acceptance: it is not itself a proof that the rule is sound under an intended mathematical interpretation. That separate soundness contract is made explicit in Section~[source reference].
Exact mathematical passage
\Pcal^{\mathrm{cert}}
\Pcal_0Definition passage · 1 passage
Search aliases: Pcal_0 P_0 Pcal mathcal
Definition passage: Versioned proof object · Read passage · Proof_Path_Theory.tex, line 1767
[Versioned proof object] A versioned proof object is a sequence P_0⟶ P_1⟶⋯ whose nodes and justifications carry stable identifiers. Each transition records additions, removals, altered scopes, evidence changes, and a digest of its parent version.
Exact mathematical passage
\Pcal_0\longrightarrow\Pcal_1\longrightarrow\cdots
\Pcal_1Definition passage · 4 passages
Search aliases: Pcal_1 P_1 Pcal mathcal
Definition passage: Versioned proof object · Read passage · Proof_Path_Theory.tex, line 1767
[Versioned proof object] A versioned proof object is a sequence P_0⟶ P_1⟶⋯ whose nodes and justifications carry stable identifiers. Each transition records additions, removals, altered scopes, evidence changes, and a digest of its parent version.
Exact mathematical passage
\Pcal_0\longrightarrow\Pcal_1\longrightarrow\cdots
\Pcal_iDefinition passage · 3 passages
Search aliases: Pcal_i P_i Pcal mathcal
Definition passage: Append-only certified update · Read passage · Proof_Path_Theory.tex, line 1775
[Append-only certified update] An update P_i→ P_i+1 is append-only certified when every existing node, admissible-leaf status, evidence record, interpretation, and certified justification remains unchanged. The later field may add records and certified rules but may not withdraw an earlier admitted leaf or change the scope of an earlier inference.
Exact mathematical passage
\Pcal_i\to\Pcal_{i+1}
\Pcal_{i+1}Definition passage · 3 passages
Search aliases: Pcal_i+1 P_i+1 Pcal mathcal
Definition passage: Append-only certified update · Read passage · Proof_Path_Theory.tex, line 1775
[Append-only certified update] An update P_i→ P_i+1 is append-only certified when every existing node, admissible-leaf status, evidence record, interpretation, and certified justification remains unchanged. The later field may add records and certified rules but may not withdraw an earlier admitted leaf or change the scope of an earlier inference.
Exact mathematical passage
\Pcal_i\to\Pcal_{i+1}
\preceqDefinition passage · 5 passages
Search aliases: preceq
Definition passage: Recoverability preorder · Read passage · Proof_Path_Theory.tex, line 1292
[Recoverability preorder] For a fixed task family Q, write R_1preceq_ Q R_2 when every task in Q that factors through the representation scheme R_1 also factors through R_2. Both schemes have domain mathscr A, and each factorization uses one decoder valid on that whole domain.
Exact mathematical passage
R_1\preceq_{\Qcal} R_2
\preceq_{\Qcal}Definition passage · 5 passages
Search aliases: preceq_Qcal preceq_ Q preceq Qcal preceq mathcal
Definition passage: Recoverability preorder · Read passage · Proof_Path_Theory.tex, line 1292
[Recoverability preorder] For a fixed task family Q, write R_1preceq_ Q R_2 when every task in Q that factors through the representation scheme R_1 also factors through R_2. Both schemes have domain mathscr A, and each factorization uses one decoder valid on that whole domain.
Exact mathematical passage
R_1\preceq_{\Qcal} R_2
\operatorname{prem}Definition passage · 3 passages
Search aliases: prem operatorname
Definition passage: Typed proof field · Read passage · Proof_Path_Theory.tex, line 313
[Typed proof field] A finite typed proof field is a tuple P=(V, J,A,T,τ, E, v, c), where: item V is a finite set of claim nodes. item J is a finite set of justifications. item Each j∈ J has a finite premise set prem(j)⊆ V and one conclusion con(j)∈ V. item A⊆ V is the set of required premises of the declared judgment. item T⊆ V is the nonempty target set. item τ assigns node and justification types. item E is a typed evidence ledger. item v assigns nonnegative value coordinates to nodes. item c …
Exact mathematical passage
\operatorname{prem}(j)\subseteq V
\primeDefinition passage · 6 passages
Search aliases: prime
Definition passage: Certificate · Read passage · Proof_Path_Theory.tex, line 425
[Certificate] A certificate for a nonempty requested target set T_0⊆ V is a pair C=(K,H), K⊆ V, H⊆ J^cert, such that A∪ T_0⊆ K and T_0⊆ D_cert(K,H). Order certificates componentwise: (K,H)≤(K^prime,H^prime) means K⊆ K^prime and H⊆ H^prime. A least certificate is contained in every certificate for the same request. Minimizing only the node set, only the justification set, or a numerical cost is a different objective.
Exact mathematical passage
(K,H)\leq(K^{\prime},H^{\prime})
\QcalDefinition passage · 12 passages
Search aliases: Qcal Q mathcal
Definition passage: Task · Read passage · Proof_Path_Theory.tex, line 1260
[Task] A task is a map q:mathscr A→ Y_q to a declared answer set. A task family Q is a set of such maps. Examples include asking for the target certificate, a dependency list, a specified boundary example, or the claims affected by a recorded revision. A teaching or discovery objective becomes an exact task only after its required output or acceptance criterion has been specified.
Exact mathematical passage
\Qcal
rDefinition passage · 37 passages
Search aliases: r
Definition passage: Goal-relative depth objective · Read passage · Proof_Path_Theory.tex, line 2065
[Goal-relative depth objective] For goal g with weights α_g,β_g≥0, define J_g(d)=α_g r_d+β_g c_d. An optimal expansion depth is any minimizer of J_g.
Exact mathematical passage
J_g(d)=\alpha_g r_d+\beta_g c_d.
R_1Definition passage · 7 passages
Search aliases: R_1
Definition passage: Recoverability preorder · Read passage · Proof_Path_Theory.tex, line 1292
[Recoverability preorder] For a fixed task family Q, write R_1preceq_ Q R_2 when every task in Q that factors through the representation scheme R_1 also factors through R_2. Both schemes have domain mathscr A, and each factorization uses one decoder valid on that whole domain.
Exact mathematical passage
R_1\preceq_{\Qcal} R_2
R_2Definition passage · 7 passages
Search aliases: R_2
Definition passage: Recoverability preorder · Read passage · Proof_Path_Theory.tex, line 1292
[Recoverability preorder] For a fixed task family Q, write R_1preceq_ Q R_2 when every task in Q that factors through the representation scheme R_1 also factors through R_2. Both schemes have domain mathscr A, and each factorization uses one decoder valid on that whole domain.
Exact mathematical passage
R_1\preceq_{\Qcal} R_2
r_dDefinition passage · 5 passages
Search aliases: r_d
Definition passage: Goal-relative depth objective · Read passage · Proof_Path_Theory.tex, line 2065
[Goal-relative depth objective] For goal g with weights α_g,β_g≥0, define J_g(d)=α_g r_d+β_g c_d. An optimal expansion depth is any minimizer of J_g.
Exact mathematical passage
J_g(d)=\alpha_g r_d+\beta_g c_d.
R_gDefinition passage · 1 passage
Search aliases: R_g
Definition passage: Proof compiler · Read passage · Proof_Path_Theory.tex, line 1595
[Proof compiler] Let g be a presentation goal and let P be a versioned proof field. A proof compiler is a map on the declared archive class Γ_g:mathscr A⟶ R_g that selects, orders, and renders the material required by g while preserving links to canonical claim and justification identifiers.
Exact mathematical passage
\Gamma_g:\mathscr A\longrightarrow R_g
R_tDefinition passage · 4 passages
Search aliases: R_t
Definition passage: Future task model · Read passage · Proof_Path_Theory.tex, line 1521
[Future task model] Let T be a finite task set with probabilities p_t≥0 satisfying ∑_t p_t=1. Let R_t⊆ V be the node set required by task t, and let c(v)≥0 be the recovery cost of node v when it is absent.
Exact mathematical passage
R_t\subseteq V
\ReachDefinition passage · 2 passages
Search aliases: Reach operatorname
Definition passage: Future reach utility · Read passage · Proof_Path_Theory.tex, line 1634
[Future reach utility] The weighted future reach of S is U(S)=∑_f∈ Fw_f 1{f∈Reach_ B(S)}.
Exact mathematical passage
U(S)=\sum_{f\in F}w_f\, \mathbf 1\{f\in\Reach_{\Bcal}(S)\}.
\Reach_{\Bcal}Definition passage · 2 passages
Search aliases: Reach_Bcal Reach_ B Reach Bcal operatorname mathcal
Definition passage: Future reach utility · Read passage · Proof_Path_Theory.tex, line 1634
[Future reach utility] The weighted future reach of S is U(S)=∑_f∈ Fw_f 1{f∈Reach_ B(S)}.
Exact mathematical passage
U(S)=\sum_{f\in F}w_f\, \mathbf 1\{f\in\Reach_{\Bcal}(S)\}.
sDefinition passage · 28 passages
Search aliases: s
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 586
proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are additional explicit oblig…
Exact mathematical passage
s
tDefinition passage · 27 passages
Search aliases: t
Definition passage: Scoped branch assessment · Read passage · Proof_Path_Theory.tex, line 375
[Scoped branch assessment] Let P be a finite typed proof field with declared premises A and target t. An exploratory branch is a finite sequence of candidate justifications whose certification and outstanding obligations are explicitly recorded. Its assessment is one of the following, relative to stated premises and rules: [label=textup(roman*)] item Open: obligations remain unresolved. item Abandoned: exploration stopped without a certificate of impossibility. item Locally refuted: a checked co…
Exact mathematical passage
t
\TcalDefinition passage · 2 passages
Search aliases: Tcal T mathcal
Definition passage: Future task model · Read passage · Proof_Path_Theory.tex, line 1521
[Future task model] Let T be a finite task set with probabilities p_t≥0 satisfying ∑_t p_t=1. Let R_t⊆ V be the node set required by task t, and let c(v)≥0 be the recovery cost of node v when it is absent.
Exact mathematical passage
\Tcal
uDefinition passage · 11 passages
Search aliases: u
Definition passage: Typed proof field · Read passage · Proof_Path_Theory.tex, line 321
he set of required premises of the declared judgment. item T⊆ V is the nonempty target set. item τ assigns node and justification types. item E is a typed evidence ledger. item v assigns nonnegative value coordinates to nodes. item c assigns nonnegative storage, audit, recovery, and cognitive costs. The dependency graph contains an edge u→ v whenever u∈prem(j) and v=con(j) for some justification j. It is required to be acyclic.
Exact mathematical passage
u\to v
\mathbf vDefinition passage · 4 passages
Search aliases: v mathbf
Definition passage: Typed proof field · Read passage · Proof_Path_Theory.tex, line 306
[Typed proof field] A finite typed proof field is a tuple P=(V, J,A,T,τ, E, v, c), where: item V is a finite set of claim nodes. item J is a finite set of justifications. item Each j∈ J has a finite premise set prem(j)⊆ V and one conclusion con(j)∈ V. item A⊆ V is the set of required premises of the declared judgment. item T⊆ V is the nonempty target set. item τ assigns node and justification types. item E is a typed evidence ledger. item v assigns nonnegative value coordinates to nodes. item c …
Exact mathematical passage
\Pcal=(V,\Jcal,A,T,\tau,\Ecal,\mathbf v,\mathbf c),
vDefinition passage · 48 passages
Search aliases: v
Definition passage: Typed proof field · Read passage · Proof_Path_Theory.tex, line 321
he set of required premises of the declared judgment. item T⊆ V is the nonempty target set. item τ assigns node and justification types. item E is a typed evidence ledger. item v assigns nonnegative value coordinates to nodes. item c assigns nonnegative storage, audit, recovery, and cognitive costs. The dependency graph contains an edge u→ v whenever u∈prem(j) and v=con(j) for some justification j. It is required to be acyclic.
Exact mathematical passage
u\to v
V_nDefinition passage · 3 passages
Search aliases: V_n
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1108
[Finite indexed problem and trace] An indexed problem P specifies a finite address space V_n={0,…,n-1}, admitted leaves L, a list of certified rules, positive observations S, and forbidden nodes N. A rule at address j has a finite premise list A_j and conclusion b_j. Two identical rows may have different rule addresses. Every listed node must belong to V_n. Node lists are individually duplicate free, but L, S, and N need not be disjoint.
Exact mathematical passage
V_n=\{0,\ldots,n-1\}
WDefinition passage · 13 passages
Search aliases: W
Definition passage: Latent bridge graph · Read passage · Proof_Path_Theory.tex, line 1623
[Latent bridge graph] A latent bridge graph is a finite directed graph B=(W,E_B) whose nodes include retained proof objects, omitted proof objects, and anticipated future targets. An edge x→ y means that x has been declared a possible transfer route toward y. The edge may be certified, conjectural, or exploratory, but its status must be recorded.
Exact mathematical passage
\Bcal=(W,E_B)
wDefinition passage · 24 passages
Search aliases: w
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 582
[Coherent views of a proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are addi…
Exact mathematical passage
e:v\to w
w_fDefinition passage · 4 passages
Search aliases: w_f
Definition passage: Future reach utility · Read passage · Proof_Path_Theory.tex, line 1634
[Future reach utility] The weighted future reach of S is U(S)=∑_f∈ Fw_f 1{f∈Reach_ B(S)}.
Exact mathematical passage
U(S)=\sum_{f\in F}w_f\, \mathbf 1\{f\in\Reach_{\Bcal}(S)\}.
XDefinition passage · 47 passages
Search aliases: X
Definition passage: Syntactic affected set · Read passage · Proof_Path_Theory.tex, line 1791
[Syntactic affected set] For a changed node set X⊆ V, define Aff(X)=X∪Desc(X), where descendants are computed in the declared dependency graph.
Exact mathematical passage
X\subseteq V
x_vDefinition passage · 1 passage
Search aliases: x_v
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 583
[Coherent views of a proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are addi…
Exact mathematical passage
\Gamma(F)=\big\{(x_v)\in\prod_{v\in V}F_v : e^*(x_w)=x_v\text{ for every declared edge }e\big\}.
x_wDefinition passage · 1 passage
Search aliases: x_w
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 583
[Coherent views of a proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are addi…
Exact mathematical passage
\Gamma(F)=\big\{(x_v)\in\prod_{v\in V}F_v : e^*(x_w)=x_v\text{ for every declared edge }e\big\}.
YDefinition passage · 22 passages
Search aliases: Y
Definition passage: Task · Read passage · Proof_Path_Theory.tex, line 1260
[Task] A task is a map q:mathscr A→ Y_q to a declared answer set. A task family Q is a set of such maps. Examples include asking for the target certificate, a dependency list, a specified boundary example, or the claims affected by a recorded revision. A teaching or discovery objective becomes an exact task only after its required output or acceptance criterion has been specified.
Exact mathematical passage
q:\mathscr A\to Y_q
Y_qDefinition passage · 2 passages
Search aliases: Y_q
Definition passage: Task · Read passage · Proof_Path_Theory.tex, line 1260
[Task] A task is a map q:mathscr A→ Y_q to a declared answer set. A task family Q is a set of such maps. Examples include asking for the target certificate, a dependency list, a specified boundary example, or the claims affected by a recorded revision. A teaching or discovery objective becomes an exact task only after its required output or acceptance criterion has been specified.
Exact mathematical passage
q:\mathscr A\to Y_q
\alphaDefinition passage · 6 passages
Search aliases: α alpha
Definition passage: Goal-relative depth objective · Read passage · Proof_Path_Theory.tex, line 2064
[Goal-relative depth objective] For goal g with weights α_g,β_g≥0, define J_g(d)=α_g r_d+β_g c_d. An optimal expansion depth is any minimizer of J_g.
Exact mathematical passage
\alpha_g,\beta_g\ge0
\alpha_gDefinition passage · 4 passages
Search aliases: α_g alpha
Definition passage: Goal-relative depth objective · Read passage · Proof_Path_Theory.tex, line 2064
[Goal-relative depth objective] For goal g with weights α_g,β_g≥0, define J_g(d)=α_g r_d+β_g c_d. An optimal expansion depth is any minimizer of J_g.
Exact mathematical passage
\alpha_g,\beta_g\ge0
\betaDefinition passage · 6 passages
Search aliases: β beta
Definition passage: Goal-relative depth objective · Read passage · Proof_Path_Theory.tex, line 2064
[Goal-relative depth objective] For goal g with weights α_g,β_g≥0, define J_g(d)=α_g r_d+β_g c_d. An optimal expansion depth is any minimizer of J_g.
Exact mathematical passage
\alpha_g,\beta_g\ge0
\beta_gDefinition passage · 4 passages
Search aliases: β_g beta
Definition passage: Goal-relative depth objective · Read passage · Proof_Path_Theory.tex, line 2064
[Goal-relative depth objective] For goal g with weights α_g,β_g≥0, define J_g(d)=α_g r_d+β_g c_d. An optimal expansion depth is any minimizer of J_g.
Exact mathematical passage
\alpha_g,\beta_g\ge0
\Gamma_gDefinition passage · 1 passage
Search aliases: Γ_g Gamma
Definition passage: Proof compiler · Read passage · Proof_Path_Theory.tex, line 1595
[Proof compiler] Let g be a presentation goal and let P be a versioned proof field. A proof compiler is a map on the declared archive class Γ_g:mathscr A⟶ R_g that selects, orders, and renders the material required by g while preserving links to canonical claim and justification identifiers.
Exact mathematical passage
\Gamma_g:\mathscr A\longrightarrow R_g
\sigmaDefinition passage · 15 passages
Search aliases: σ sigma
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1110
A trace σ=(j_1,…,j_k) is a list of rule addresses. Replay begins with the list K_0=Lmathbin+ +S. It rejects an unknown rule address or a step whose premises are not all known. Otherwise it adds the conclusion. Strict replay additionally requires the conclusion to be new. Causal replay permits a conclusion already known. Lists are compared by membership when they represent sets.
Exact mathematical passage
\sigma=(j_1,\ldots,j_k)
\tauDefinition passage · 6 passages
Search aliases: τ tau
Definition passage: Typed proof field · Read passage · Proof_Path_Theory.tex, line 306
[Typed proof field] A finite typed proof field is a tuple P=(V, J,A,T,τ, E, v, c), where: item V is a finite set of claim nodes. item J is a finite set of justifications. item Each j∈ J has a finite premise set prem(j)⊆ V and one conclusion con(j)∈ V. item A⊆ V is the set of required premises of the declared judgment. item T⊆ V is the nonempty target set. item τ assigns node and justification types. item E is a typed evidence ledger. item v assigns nonnegative value coordinates to nodes. item c …
Exact mathematical passage
\Pcal=(V,\Jcal,A,T,\tau,\Ecal,\mathbf v,\mathbf c),
\ldotsDefinition passage · 5 passages
Search aliases: … ldots
Definition passage: Finite indexed problem and trace · Read passage · Proof_Path_Theory.tex, line 1108
[Finite indexed problem and trace] An indexed problem P specifies a finite address space V_n={0,…,n-1}, admitted leaves L, a list of certified rules, positive observations S, and forbidden nodes N. A rule at address j has a finite premise list A_j and conclusion b_j. Two identical rows may have different rule addresses. Every listed node must belong to V_n. Node lists are individually duplicate free, but L, S, and N need not be disjoint.
Exact mathematical passage
V_n=\{0,\ldots,n-1\}
\inDefinition passage · 45 passages
Search aliases: ∈ in
Definition passage: Typed proof field · Read passage · Proof_Path_Theory.tex, line 313
[Typed proof field] A finite typed proof field is a tuple P=(V, J,A,T,τ, E, v, c), where: item V is a finite set of claim nodes. item J is a finite set of justifications. item Each j∈ J has a finite premise set prem(j)⊆ V and one conclusion con(j)∈ V. item A⊆ V is the set of required premises of the declared judgment. item T⊆ V is the nonempty target set. item τ assigns node and justification types. item E is a typed evidence ledger. item v assigns nonnegative value coordinates to nodes. item c …
Exact mathematical passage
j\in\Jcal
\notinDefinition passage · 5 passages
Search aliases: ∉ notin
Definition passage: Additive loss vector · Read passage · Proof_Path_Theory.tex, line 1487
[Additive loss vector] For a retained node set K⊆ V, define Loss( P,K) = ∑_v∉ K v(v). Normalize a coordinate by its total only when that total is positive. If the total is zero, nonnegativity makes every contribution in that coordinate zero. The implementation records normalized loss zero there as a convention, rather than dividing by zero.
Exact mathematical passage
\Loss(\Pcal,K) = \sum_{v\notin K}\mathbf v(v).
\prodDefinition passage · 1 passage
Search aliases: ∏ prod
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 583
[Coherent views of a proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are addi…
Exact mathematical passage
\Gamma(F)=\big\{(x_v)\in\prod_{v\in V}F_v : e^*(x_w)=x_v\text{ for every declared edge }e\big\}.
\prod_{v\in V}Definition passage · 1 passage
Search aliases: ∏_v∈ V prod in
Definition passage: Coherent views of a proof field · Read passage · Proof_Path_Theory.tex, line 583
[Coherent views of a proof field] Choose a finite collection of views V, fibers F_v of local proof states or annotations, and for each declared directed edge e:v→ w a restriction map e^*:F_w→ F_v. The strict realization set is Γ(F)={(x_v)∈∏_v∈ VF_v : e^*(x_w)=x_v for every declared edge e}. The extension fiber of prescribed information s on U⊆ V consists of those global coherent families whose restrictions equal s. If the edges form a category, the usual functorial composition equations are addi…
Exact mathematical passage
\Gamma(F)=\big\{(x_v)\in\prod_{v\in V}F_v : e^*(x_w)=x_v\text{ for every declared edge }e\big\}.
\sumDefinition passage · 7 passages
Search aliases: ∑ sum
Definition passage: Additive loss vector · Read passage · Proof_Path_Theory.tex, line 1487
[Additive loss vector] For a retained node set K⊆ V, define Loss( P,K) = ∑_v∉ K v(v). Normalize a coordinate by its total only when that total is positive. If the total is zero, nonnegativity makes every contribution in that coordinate zero. The implementation records normalized loss zero there as a convention, rather than dividing by zero.
Exact mathematical passage
\Loss(\Pcal,K) = \sum_{v\notin K}\mathbf v(v).
\sum_{f\in F}Definition passage · 1 passage
Search aliases: ∑_f∈ F sum in
Definition passage: Future reach utility · Read passage · Proof_Path_Theory.tex, line 1634
[Future reach utility] The weighted future reach of S is U(S)=∑_f∈ Fw_f 1{f∈Reach_ B(S)}.
Exact mathematical passage
U(S)=\sum_{f\in F}w_f\, \mathbf 1\{f\in\Reach_{\Bcal}(S)\}.
\sum_tDefinition passage · 1 passage
Search aliases: ∑_t sum
Definition passage: Future task model · Read passage · Proof_Path_Theory.tex, line 1521
[Future task model] Let T be a finite task set with probabilities p_t≥0 satisfying ∑_t p_t=1. Let R_t⊆ V be the node set required by task t, and let c(v)≥0 be the recovery cost of node v when it is absent.
Exact mathematical passage
\sum_t p_t=1
\sum_{t\in\Tcal}Definition passage · 1 passage
Search aliases: ∑_t∈Tcal ∑_t∈ T sum in Tcal sum in mathcal
Definition passage: Expected compression debt · Read passage · Proof_Path_Theory.tex, line 1527
[Expected compression debt] The expected compression debt of retained set K is Debt(K) = ∑_t∈ Tp_t ∑_v∈ R_t∖ Kc(v).
Exact mathematical passage
\Debt(K) = \sum_{t\in\Tcal}p_t \sum_{v\in R_t\setminus K}c(v).
\sum_{v\in R_t\setminus K}Definition passage · 1 passage
Search aliases: ∑_v∈ R_t∖ K sum in setminus
Definition passage: Expected compression debt · Read passage · Proof_Path_Theory.tex, line 1527
[Expected compression debt] The expected compression debt of retained set K is Debt(K) = ∑_t∈ Tp_t ∑_v∈ R_t∖ Kc(v).
Exact mathematical passage
\Debt(K) = \sum_{t\in\Tcal}p_t \sum_{v\in R_t\setminus K}c(v).
\sum_{v\notin K}Definition passage · 1 passage
Search aliases: ∑_v∉ K sum notin
Definition passage: Additive loss vector · Read passage · Proof_Path_Theory.tex, line 1487
[Additive loss vector] For a retained node set K⊆ V, define Loss( P,K) = ∑_v∉ K v(v). Normalize a coordinate by its total only when that total is positive. If the total is zero, nonnegativity makes every contribution in that coordinate zero. The implementation records normalized loss zero there as a convention, rather than dividing by zero.
Exact mathematical passage
\Loss(\Pcal,K) = \sum_{v\notin K}\mathbf v(v).
\setminusDefinition passage · 7 passages
Search aliases: ∖ setminus
Definition passage: Expected compression debt · Read passage · Proof_Path_Theory.tex, line 1527
[Expected compression debt] The expected compression debt of retained set K is Debt(K) = ∑_t∈ Tp_t ∑_v∈ R_t∖ Kc(v).
Exact mathematical passage
\Debt(K) = \sum_{t\in\Tcal}p_t \sum_{v\in R_t\setminus K}c(v).
\cupDefinition passage · 17 passages
Search aliases: ∪ cup
Definition passage: Certificate · Read passage · Proof_Path_Theory.tex, line 420
[Certificate] A certificate for a nonempty requested target set T_0⊆ V is a pair C=(K,H), K⊆ V, H⊆ J^cert, such that A∪ T_0⊆ K and T_0⊆ D_cert(K,H). Order certificates componentwise: (K,H)≤(K^prime,H^prime) means K⊆ K^prime and H⊆ H^prime. A least certificate is contained in every certificate for the same request. Minimizing only the node set, only the justification set, or a numerical cost is a different objective.
Exact mathematical passage
A\cup T_0\subseteq K \qquad\text{and}\qquad T_0\subseteq D_{\mathrm{cert}}(K,H).
\leqDefinition passage · 4 passages
Search aliases: ≤ leq
Definition passage: Certificate · Read passage · Proof_Path_Theory.tex, line 425
[Certificate] A certificate for a nonempty requested target set T_0⊆ V is a pair C=(K,H), K⊆ V, H⊆ J^cert, such that A∪ T_0⊆ K and T_0⊆ D_cert(K,H). Order certificates componentwise: (K,H)≤(K^prime,H^prime) means K⊆ K^prime and H⊆ H^prime. A least certificate is contained in every certificate for the same request. Minimizing only the node set, only the justification set, or a numerical cost is a different objective.
Exact mathematical passage
(K,H)\leq(K^{\prime},H^{\prime})
\geDefinition passage · 7 passages
Search aliases: ≥ ge
Definition passage: Future task model · Read passage · Proof_Path_Theory.tex, line 1521
[Future task model] Let T be a finite task set with probabilities p_t≥0 satisfying ∑_t p_t=1. Let R_t⊆ V be the node set required by task t, and let c(v)≥0 be the recovery cost of node v when it is absent.
Exact mathematical passage
p_t\ge0
\cdotsDefinition passage · 4 passages
Search aliases: ⋯ cdots
Definition passage: Versioned proof object · Read passage · Proof_Path_Theory.tex, line 1767
[Versioned proof object] A versioned proof object is a sequence P_0⟶ P_1⟶⋯ whose nodes and justifications carry stable identifiers. Each transition records additions, removals, altered scopes, evidence changes, and a digest of its parent version.
Exact mathematical passage
\Pcal_0\longrightarrow\Pcal_1\longrightarrow\cdots
\longrightarrowDefinition passage · 7 passages
Search aliases: ⟶ longrightarrow
Definition passage: Compositional certificate map · Read passage · Proof_Path_Theory.tex, line 556
[Compositional certificate map] A compositional certificate map is a functor C:Expanded⟶Certificate that sends expanded certified paths to checkable certificate paths and preserves identity and composition.
Exact mathematical passage
\Ccal:\mathsf{Expanded}\longrightarrow\mathsf{Certificate}
\mathrm{core}Introduction passage · 6 passages
Search aliases: core mathrm
Introduction passage · Read passage · Proof_Path_Theory.tex, line 439
Let Anc_L(T_0) denote the premise nodes reached by this backward expansion, stopping at L. Let H_core contain exactly the justifications selected at expanded nodes outside L.
Exact mathematical passage
H_{\mathrm{core}}
H_{\mathrm{core}}Introduction passage · 4 passages
Search aliases: H_core mathrm
Introduction passage · Read passage · Proof_Path_Theory.tex, line 439
Let Anc_L(T_0) denote the premise nodes reached by this backward expansion, stopping at L. Let H_core contain exactly the justifications selected at expanded nodes outside L.
Exact mathematical passage
H_{\mathrm{core}}
\operatorname{im}Introduction passage · 3 passages
Search aliases: im operatorname
Introduction passage · Read passage · Proof_Path_Theory.tex, line 1393
The collision obstruction of Theorem~[source reference] has a converse. It gives a complete test for exact task recovery at the level of sets. Write imC=C(mathscr A) for the attained output set. A decoder is required on this set and nowhere else.
Exact mathematical passage
\operatorname{im}C=C(\mathscr A)
\mathbf1^\topUse in source · 6 passages
Search aliases: 1^top mathbf top
Use in source · Read passage · Proof_Path_Theory.tex, line 1916
For a general positive definite covariance matrix Σ, consider unbiased linear aggregates w^top X with 1^top w=1.
Exact mathematical passage
\mathbf 1^\top w=1
\mathcal AUse in source · 7 passages
Search aliases: A mathcal
Use in source · Read passage · Proof_Path_Theory.tex, line 858
Let T:E→ R and Q:E→ W be linear, and fix a known point x_0. Put A={y:Ty=Tx_0}, H=ker T, Q_H=Q|_H. Translation h↦ x_0+h identifies H with A. The observation image is the translate Qx_0+Q(H), and the fiber above the attained value Qx_0 is a translate of ker Q_H.
Exact mathematical passage
\mathcal A=\{y:Ty=Tx_0\},\quad H=\ker T,\quad Q_H=Q|_H.
a'Use in source · 2 passages
Search aliases: a'
Use in source · Read passage · Proof_Path_Theory.tex, line 1384
ly injective encodings] Let C:A→ B. Every predicate q:A→Prop factors through C if and only if C is injective. If C is injective, define the decoder of q at b by the predicate ∃ a (C(a)=b and q(a)). At b=C(a_0), injectivity makes this equivalent to q(a_0). Conversely, if C(a)=C(a'), use the predicate q(z)≡(z=a). Its decoded values at the equal encodings must agree, giving a'=a. This is the general collision criterion specialized to all predicates.
Exact mathematical passage
C(a)=C(a')
A^F_jUse in source · 1 passage
Search aliases: A^F_j
Use in source · Read passage · Proof_Path_Theory.tex, line 1059
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G, j certified in F · Longrightarrow h(j) certified in G, A^G_h(j) · ⊆ f(A^F_j), c^G_h(j) · =f(c^F_j). The premise inclusion points in the direction needed for executing the translated step. The mapped target rule may need fewer premises, but it must not introduce a new premise unsupported …
Exact mathematical passage
\begin{aligned} f(L_F)&\subseteq L_G,\\ j\text{ certified in }F&\Longrightarrow h(j)\text{ certified in }G,\\ A^G_{h(j)}&\subseteq f(A^F_j),\\ c^G_{h(j)}&=f(c^F_j). \end{aligned}
A^G_{h(j)}Use in source · 1 passage
Search aliases: A^G_h(j)
Use in source · Read passage · Proof_Path_Theory.tex, line 1059
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G, j certified in F · Longrightarrow h(j) certified in G, A^G_h(j) · ⊆ f(A^F_j), c^G_h(j) · =f(c^F_j). The premise inclusion points in the direction needed for executing the translated step. The mapped target rule may need fewer premises, but it must not introduce a new premise unsupported …
Exact mathematical passage
\begin{aligned} f(L_F)&\subseteq L_G,\\ j\text{ certified in }F&\Longrightarrow h(j)\text{ certified in }G,\\ A^G_{h(j)}&\subseteq f(A^F_j),\\ c^G_{h(j)}&=f(c^F_j). \end{aligned}
A^\primeUse in source · 1 passage
Search aliases: A^prime prime
Use in source · Read passage · Proof_Path_Theory.tex, line 1673
[htbp] centering includegraphics[width=linewidth]fig_07_bridge_dominators.pdf captionA declared bridge graph. The boundary theorem C dominates future targets A^prime and B^prime but not C^prime, which has a bypass from E. These arrows describe future reach in the supplied model, not proof certification. Deleting a bridge vertex is different from merely retaining a different source set.
Exact mathematical passage
A^\prime
a_0Use in source · 2 passages
Search aliases: a_0
Use in source · Read passage · Proof_Path_Theory.tex, line 1384
[All predicates distinguish exactly injective encodings] Let C:A→ B. Every predicate q:A→Prop factors through C if and only if C is injective. If C is injective, define the decoder of q at b by the predicate ∃ a (C(a)=b and q(a)). At b=C(a_0), injectivity makes this equivalent to q(a_0). Conversely, if C(a)=C(a'), use the predicate q(z)≡(z=a). Its decoded values at the equal encodings must agree, giving a'=a. This is the general collision criterion specialized to all predicates.
Exact mathematical passage
b=C(a_0)
a_tUse in source · 3 passages
Search aliases: a_t
Use in source · Read passage · Proof_Path_Theory.tex, line 1998
Let a_t≥0 be candidate arrivals during audit cycle t, let s_t≥0 be service capacity, and let B_t≥0 be the unresolved backlog. Suppose arrivals in a cycle are available to that cycle's service. The basic deterministic queue is B_t+1=max{0,B_t+a_t-s_t}.
Exact mathematical passage
a_t\geq0
\mathrm{archive}Use in source · 1 passage
Search aliases: archive mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
\mathrm{audit}Use in source · 2 passages
Search aliases: audit mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 2026
A simple audit priority score is P(x) = fracp_err(x) c_consequence(x) (1+r_dependency(x)) c_audit(x). Here p_err(x)∈[0,1], the consequence and dependency factors are nonnegative, and c_audit(x)>0. Zero-cost checks can be handled separately. This is a declared priority heuristic, not a probability of truth or a proved optimal scheduling rule.
Exact mathematical passage
P(x) = \frac{p_{\mathrm{err}}(x)\,c_{\mathrm{consequence}}(x) \bigl(1+r_{\mathrm{dependency}}(x)\bigr)} {c_{\mathrm{audit}}(x)}.
b^2Use in source · 3 passages
Search aliases: b^2
Use in source · Read passage · Proof_Path_Theory.tex, line 1947
[Bias is not covariance] Covariance-aware weighting does not remove a common bias that is absent from the covariance model. If every reviewer shares bias b, the mean squared error contains the irreducible term b^2.
Exact mathematical passage
b^2
B^\primeUse in source · 1 passage
Search aliases: B^prime prime
Use in source · Read passage · Proof_Path_Theory.tex, line 1673
[htbp] centering includegraphics[width=linewidth]fig_07_bridge_dominators.pdf captionA declared bridge graph. The boundary theorem C dominates future targets A^prime and B^prime but not C^prime, which has a bypass from E. These arrows describe future reach in the supplied model, not proof certification. Deleting a bridge vertex is different from merely retaining a different source set.
Exact mathematical passage
B^\prime
B_0Use in source · 1 passage
Search aliases: B_0
Use in source · Read passage · Proof_Path_Theory.tex, line 2015
Before the truncation at zero, each cycle adds λ-μ. When this quantity is negative, the backlog decreases by a fixed amount until it reaches zero. When it is zero, the backlog is unchanged. When it is positive, the truncation is never active after a nonnegative start, and the backlog is B_0+t(λ-μ).
Exact mathematical passage
B_0+t(\lambda-\mu)
B_tUse in source · 2 passages
Search aliases: B_t
Use in source · Read passage · Proof_Path_Theory.tex, line 1998
Let a_t≥0 be candidate arrivals during audit cycle t, let s_t≥0 be service capacity, and let B_t≥0 be the unresolved backlog. Suppose arrivals in a cycle are available to that cycle's service. The basic deterministic queue is B_t+1=max{0,B_t+a_t-s_t}.
Exact mathematical passage
B_t\geq0
B_{t+1}Use in source · 1 passage
Search aliases: B_t+1
Use in source · Read passage · Proof_Path_Theory.tex, line 1999
Let a_t≥0 be candidate arrivals during audit cycle t, let s_t≥0 be service capacity, and let B_t≥0 be the unresolved backlog. Suppose arrivals in a cycle are available to that cycle's service. The basic deterministic queue is B_t+1=max{0,B_t+a_t-s_t}.
Exact mathematical passage
B_{t+1}=\max\{0,B_t+a_t-s_t\}.
\bar XUse in source · 2 passages
Search aliases: bar X bar
Use in source · Read passage · Proof_Path_Theory.tex, line 1875
Let X_i=θ+ε_i be numerical estimates of a fixed quantity θ. Assume Eε_i=0, Var(ε_i)=σ^2>0, and common pairwise correlation ρ. For n>1, assume -1/(n-1)<ρ≤1, so the mean has positive variance. These variables model estimates, not proof truth values. The mean has variance Var(bar X) = σ^2(frac1-ρn+ρ).
Exact mathematical passage
\operatorname{Var}(\bar X) = \sigma^2\left(\frac{1-\rho}{n}+\rho\right).
c^F_jUse in source · 1 passage
Search aliases: c^F_j
Use in source · Read passage · Proof_Path_Theory.tex, line 1059
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G, j certified in F · Longrightarrow h(j) certified in G, A^G_h(j) · ⊆ f(A^F_j), c^G_h(j) · =f(c^F_j). The premise inclusion points in the direction needed for executing the translated step. The mapped target rule may need fewer premises, but it must not introduce a new premise unsupported …
Exact mathematical passage
\begin{aligned} f(L_F)&\subseteq L_G,\\ j\text{ certified in }F&\Longrightarrow h(j)\text{ certified in }G,\\ A^G_{h(j)}&\subseteq f(A^F_j),\\ c^G_{h(j)}&=f(c^F_j). \end{aligned}
c^G_{h(j)}Use in source · 1 passage
Search aliases: c^G_h(j)
Use in source · Read passage · Proof_Path_Theory.tex, line 1059
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G, j certified in F · Longrightarrow h(j) certified in G, A^G_h(j) · ⊆ f(A^F_j), c^G_h(j) · =f(c^F_j). The premise inclusion points in the direction needed for executing the translated step. The mapped target rule may need fewer premises, but it must not introduce a new premise unsupported …
Exact mathematical passage
\begin{aligned} f(L_F)&\subseteq L_G,\\ j\text{ certified in }F&\Longrightarrow h(j)\text{ certified in }G,\\ A^G_{h(j)}&\subseteq f(A^F_j),\\ c^G_{h(j)}&=f(c^F_j). \end{aligned}
C^\primeUse in source · 1 passage
Search aliases: C^prime prime
Use in source · Read passage · Proof_Path_Theory.tex, line 1673
[htbp] centering includegraphics[width=linewidth]fig_07_bridge_dominators.pdf captionA declared bridge graph. The boundary theorem C dominates future targets A^prime and B^prime but not C^prime, which has a bypass from E. These arrows describe future reach in the supplied model, not proof certification. Deleting a bridge vertex is different from merely retaining a different source set.
Exact mathematical passage
C^\prime
C_0Use in source · 5 passages
Search aliases: C_0
Use in source · Read passage · Proof_Path_Theory.tex, line 1363
[htbp] centering includegraphics[width=linewidth]fig_05_recoverability_preorder.pdf captionA concrete retention diamond for the four archives (C_0,x,y) with x,y∈{0,1}. Arrows discard coordinates. The two middle schemes are incomparable for the task family {q_x,q_y}. This is not a universal ranking of teaching, discovery, and formal presentations.
Exact mathematical passage
(C_0,x,y)
c_{\mathrm{audit}}Use in source · 2 passages
Search aliases: c_audit mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 2026
A simple audit priority score is P(x) = fracp_err(x) c_consequence(x) (1+r_dependency(x)) c_audit(x). Here p_err(x)∈[0,1], the consequence and dependency factors are nonnegative, and c_audit(x)>0. Zero-cost checks can be handled separately. This is a declared priority heuristic, not a probability of truth or a proved optimal scheduling rule.
Exact mathematical passage
P(x) = \frac{p_{\mathrm{err}}(x)\,c_{\mathrm{consequence}}(x) \bigl(1+r_{\mathrm{dependency}}(x)\bigr)} {c_{\mathrm{audit}}(x)}.
c_{\mathrm{consequence}}Use in source · 1 passage
Search aliases: c_consequence mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 2026
A simple audit priority score is P(x) = fracp_err(x) c_consequence(x) (1+r_dependency(x)) c_audit(x). Here p_err(x)∈[0,1], the consequence and dependency factors are nonnegative, and c_audit(x)>0. Zero-cost checks can be handled separately. This is a declared priority heuristic, not a probability of truth or a proved optimal scheduling rule.
Exact mathematical passage
P(x) = \frac{p_{\mathrm{err}}(x)\,c_{\mathrm{consequence}}(x) \bigl(1+r_{\mathrm{dependency}}(x)\bigr)} {c_{\mathrm{audit}}(x)}.
c_{d-1}Use in source · 2 passages
Search aliases: c_d-1
Use in source · Read passage · Proof_Path_Theory.tex, line 2085
A practical stopping rule selects the first depth satisfying r_d≤ε or fracr_d-1-r_dc_d-c_d-1<τ. The first condition uses a declared tolerance. The second applies only at d≥1 with c_d>c_d-1 and compares the most recent reduction with its extra cost. Zero-cost refinements require separate handling. These stopping rules do not generally minimize J_g over all remaining depths.
Exact mathematical passage
r_d\le\varepsilon\qquad\text{or}\qquad \frac{r_{d-1}-r_d}{c_d-c_{d-1}}<\tau.
c_{d_1}Use in source · 2 passages
Search aliases: c_d_1
Use in source · Read passage · Proof_Path_Theory.tex, line 2077
Take a proof object with exactly two available depths d_1<d_2, with r_d_2<r_d_1 and c_d_2>c_d_1. Direct subtraction shows that d_2 is preferred exactly when α_g(r_d_1-r_d_2)>β_g(c_d_2-c_d_1). The goal (α_g,β_g)=(1,0) strictly prefers d_2, whereas (0,1) strictly prefers d_1. Since these are the only available depths, each preference is a global optimum. If both weights vanish, every depth is optimal. No division by a possibly zero weight is needed.
Exact mathematical passage
c_{d_2}>c_{d_1}
c_{d_2}Use in source · 2 passages
Search aliases: c_d_2
Use in source · Read passage · Proof_Path_Theory.tex, line 2077
Take a proof object with exactly two available depths d_1<d_2, with r_d_2<r_d_1 and c_d_2>c_d_1. Direct subtraction shows that d_2 is preferred exactly when α_g(r_d_1-r_d_2)>β_g(c_d_2-c_d_1). The goal (α_g,β_g)=(1,0) strictly prefers d_2, whereas (0,1) strictly prefers d_1. Since these are the only available depths, each preference is a global optimum. If both weights vanish, every depth is optimal. No division by a possibly zero weight is needed.
Exact mathematical passage
c_{d_2}>c_{d_1}
C_iUse in source · 4 passages
Search aliases: C_i
Use in source · Read passage · Proof_Path_Theory.tex, line 1577
[Portfolio robustness] For representation schemes C_i:mathscr A→ R_i, retain the tagged portfolio C( P)=(C_i( P))_i. Every task recoverable from any one C_i is recoverable from C.
Exact mathematical passage
C_i:\mathscr A\to R_i
c_jUse in source · 8 passages
Search aliases: c_j
Use in source · Read passage · Proof_Path_Theory.tex, line 669
Fix a node set V, a set L⊆ V of admissible leaves, and a set J of justifications. A justification j has a premise set A_j, a conclusion c_j, and a certification predicate. Define its support by S_j=A_j∪{c_j}. A set X⊆ V is a model of the declared field when L⊆ X and, for every certified j, A_j⊆ X Longrightarrow c_j∈ X. Each justification is one implication with conjunctive premises. Alternative justifications remain separate implications. Uncertified attempts and failed-route annotations do not …
Exact mathematical passage
c_j
\mathsf{Cert}_1Use in source · 2 passages
Search aliases: Cert_1 mathsf
Use in source · Read passage · Proof_Path_Theory.tex, line 536
[Functorial transport] Let F:Cert_1→Cert_2 be a functor. If Axrightarrowf_1S_1xrightarrowf_2⋯xrightarrowf_rB is a certified path in Cert_1, then F(A)xrightarrowF(f_1)F(S_1)xrightarrowF(f_2)⋯xrightarrowF(f_r)F(B) is a certified path in Cert_2.
Exact mathematical passage
F:\mathsf{Cert}_1\to\mathsf{Cert}_2
\mathsf{Cert}_2Use in source · 2 passages
Search aliases: Cert_2 mathsf
Use in source · Read passage · Proof_Path_Theory.tex, line 536
[Functorial transport] Let F:Cert_1→Cert_2 be a functor. If Axrightarrowf_1S_1xrightarrowf_2⋯xrightarrowf_rB is a certified path in Cert_1, then F(A)xrightarrowF(f_1)F(S_1)xrightarrowF(f_2)⋯xrightarrowF(f_r)F(B) is a certified path in Cert_2.
Exact mathematical passage
F:\mathsf{Cert}_1\to\mathsf{Cert}_2
\operatorname{cl}_{F_{\mathcal U}}Use in source · 5 passages
Search aliases: cl_F_ U operatorname mathcal
Use in source · Read passage · Proof_Path_Theory.tex, line 1007
Let U=(U_i)_i cover every node. Define F_ U to have the same nodes and leaves as F but only those certified rules whose entire support lies in some U_i. The distinction between the two fields is explicit. We call the cover semantically sufficient for the declared rules when ∀ j certified in F, c_j∈cl_F_ U(A_j). tagSC The word semantic here refers to the Boolean rule-model semantics of Section~[source reference], not to an automatic interpretation of node labels as arbitrary mathematical truths.
Exact mathematical passage
\forall j\text{ certified in }F,\qquad c_j\in\operatorname{cl}_{F_{\mathcal U}}(A_j). \tag{SC}\label{eq:semantic-cover}
\operatorname{cl}_GUse in source · 2 passages
Search aliases: cl_G operatorname
Use in source · Read passage · Proof_Path_Theory.tex, line 1087
Positive seeds can be added before transport. The same rule transport sends F[S] to G[f(S)], and hence f(cl_F(S)) ⊆cl_G(f(S)). A forbidden source consequence n∈ N∩cl_F(S) maps to the explicit forbidden consequence f(n)∈ f(N)∩cl_G(f(S)). The formal development checks this witness map, not only the existence statement obtained by contraposition.
Exact mathematical passage
f\bigl(\operatorname{cl}_F(S)\bigr) \subseteq\operatorname{cl}_G(f(S)).
\mathrm{consequence}Use in source · 1 passage
Search aliases: consequence mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 2026
A simple audit priority score is P(x) = fracp_err(x) c_consequence(x) (1+r_dependency(x)) c_audit(x). Here p_err(x)∈[0,1], the consequence and dependency factors are nonnegative, and c_audit(x)>0. Zero-cost checks can be handled separately. This is a declared priority heuristic, not a probability of truth or a proved optimal scheduling rule.
Exact mathematical passage
P(x) = \frac{p_{\mathrm{err}}(x)\,c_{\mathrm{consequence}}(x) \bigl(1+r_{\mathrm{dependency}}(x)\bigr)} {c_{\mathrm{audit}}(x)}.
\operatorname{Cov}Use in source · 1 passage
Search aliases: Cov operatorname
Use in source · Read passage · Proof_Path_Theory.tex, line 1965
[MSE with a shared interpretive offset] Suppose reviewers report J_i=θ+b+ε_i, where θ is the target quantity, b is a fixed shared offset, Eε_i=0, Var(ε_i)=σ^2, and Cov(ε_i,ε_j)=ρσ^2 for i≠ j. For admissible ρ, the mean squared error of the reviewer average is E(overline J_n-θ)^2=b^2+σ^2(ρ+frac1-ρn). For fixed ρ≥0, it approaches b^2+ρσ^2 as n→∞. The estimation error is overline J_n-θ=b+overlineε_n. Its mean is b, and its variance is σ^2((1-ρ)/n+ρ) by summing all diagonal and off-diagonal covarian…
Exact mathematical passage
\operatorname{Cov}(\varepsilon_i,\varepsilon_j)=\rho\sigma^2
d_1Use in source · 5 passages
Search aliases: d_1
Use in source · Read passage · Proof_Path_Theory.tex, line 2077
Take a proof object with exactly two available depths d_1<d_2, with r_d_2<r_d_1 and c_d_2>c_d_1. Direct subtraction shows that d_2 is preferred exactly when α_g(r_d_1-r_d_2)>β_g(c_d_2-c_d_1). The goal (α_g,β_g)=(1,0) strictly prefers d_2, whereas (0,1) strictly prefers d_1. Since these are the only available depths, each preference is a global optimum. If both weights vanish, every depth is optimal. No division by a possibly zero weight is needed.
Exact mathematical passage
d_1<d_2
d_2Use in source · 6 passages
Search aliases: d_2
Use in source · Read passage · Proof_Path_Theory.tex, line 2077
Take a proof object with exactly two available depths d_1<d_2, with r_d_2<r_d_1 and c_d_2>c_d_1. Direct subtraction shows that d_2 is preferred exactly when α_g(r_d_1-r_d_2)>β_g(c_d_2-c_d_1). The goal (α_g,β_g)=(1,0) strictly prefers d_2, whereas (0,1) strictly prefers d_1. Since these are the only available depths, each preference is a global optimum. If both weights vanish, every depth is optimal. No division by a possibly zero weight is needed.
Exact mathematical passage
d_1<d_2
d_CUse in source · 2 passages
Search aliases: d_C
Use in source · Read passage · Proof_Path_Theory.tex, line 1225
[Lossless encoding at the typed syntax boundary] Let e_P,d_P and e_C,d_C be the stated Lean encoders and partial decoders for problem and certificate records. For every typed problem P and certificate C, d_P(e_P(P))=some(P), d_C(e_C(C))=some(C). Consequently both encoders are injective on their typed domains. These identities do not require the encoded record to pass the separate validity checks. The natural-number and Boolean constructors decode to their original values. Induction on a list pro…
Exact mathematical passage
e_C,d_C
d_iUse in source · 2 passages
Search aliases: d_i
Use in source · Read passage · Proof_Path_Theory.tex, line 1581
If q=d_i∘ C_i, compose d_i with the ith coordinate projection from the portfolio. This gives a decoder of q from C. Retaining the coordinate labels is part of the construction. An untagged union that loses source identities need not permit the same recovery.
Exact mathematical passage
q=d_i\circ C_i
d_PUse in source · 2 passages
Search aliases: d_P
Use in source · Read passage · Proof_Path_Theory.tex, line 1225
[Lossless encoding at the typed syntax boundary] Let e_P,d_P and e_C,d_C be the stated Lean encoders and partial decoders for problem and certificate records. For every typed problem P and certificate C, d_P(e_P(P))=some(P), d_C(e_C(C))=some(C). Consequently both encoders are injective on their typed domains. These identities do not require the encoded record to pass the separate validity checks. The natural-number and Boolean constructors decode to their original values. Induction on a list pro…
Exact mathematical passage
e_P,d_P
\mathrm{dependency}Use in source · 1 passage
Search aliases: dependency mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 2026
A simple audit priority score is P(x) = fracp_err(x) c_consequence(x) (1+r_dependency(x)) c_audit(x). Here p_err(x)∈[0,1], the consequence and dependency factors are nonnegative, and c_audit(x)>0. Zero-cost checks can be handled separately. This is a declared priority heuristic, not a probability of truth or a proved optimal scheduling rule.
Exact mathematical passage
P(x) = \frac{p_{\mathrm{err}}(x)\,c_{\mathrm{consequence}}(x) \bigl(1+r_{\mathrm{dependency}}(x)\bigr)} {c_{\mathrm{audit}}(x)}.
\operatorname{Der}Use in source · 7 passages
Search aliases: Der operatorname
Use in source · Read passage · Proof_Path_Theory.tex, line 679
Let Der_F be the inductively generated set obtained from the leaves by certified rules. For a finite field, repeated forward closure computes this set. It is not necessary to enumerate all valuations to perform that computation.
Exact mathematical passage
\operatorname{Der}_F
\operatorname{Der}_FUse in source · 6 passages
Search aliases: Der_F operatorname
Use in source · Read passage · Proof_Path_Theory.tex, line 679
Let Der_F be the inductively generated set obtained from the leaves by certified rules. For a finite field, repeated forward closure computes this set. It is not necessary to enumerate all valuations to perform that computation.
Exact mathematical passage
\operatorname{Der}_F
\operatorname{Der}_{F[S]}Use in source · 1 passage
Search aliases: Der_F[S] operatorname
Use in source · Read passage · Proof_Path_Theory.tex, line 931
Fix the field F, including its admitted leaves and certified rules. For a positive observation set S⊆ V, let cl_F(S)=Der_F[S], where F[S] is obtained by admitting L∪ S as leaves and changing nothing else. For a negative observation set N⊆ V, define Ext_F(S,N)= {X⊆ V:X is an F-model, S⊆ X, X∩ N=∅}. Positive and negative observations are both part of the preservation contract. Dropping the negative observations can turn an impossible request into a different, feasible problem.
Exact mathematical passage
\operatorname{cl}_F(S)=\operatorname{Der}_{F[S]},
\dimUse in source · 7 passages
Search aliases: dim
Use in source · Read passage · Proof_Path_Theory.tex, line 628
| K_P(x)|=2^n-rank(M). item A row vector λ exists with λ M=0 and λ b=1. It is a directly checkable certificate that K_P(x)=∅. If My_0=b, any other solution differs from y_0 by an element of ker M=H, and every such difference gives another solution. Rank nullity gives dim H=n-rank(M). If b is not in the column space of M, linear algebra supplies a linear functional that vanishes on that column space and takes value 1 on b. Expressing it as a row vector gives λ. Conversely such a witness contradic…
Exact mathematical passage
\dim H=n-\operatorname{rank}(M)
\dim_KUse in source · 2 passages
Search aliases: dim_K dim
Use in source · Read passage · Proof_Path_Theory.tex, line 868
[Exact observation counts] Suppose K is a finite field of cardinality q and E is a finite-dimensional K-vector space. Set k=dim_K H and r=dim_K Q(H). Then | A|=q^k, |Q( A)|=q^r, |{y∈ A:Qy=Qx_0}|=q^k-r. In particular the exact count identity is | A|= |{y∈ A:Qy=Qx_0}| q^r. Every attained observation fiber has the same size. For the uniform distribution on A, the observation removes exactly rlog_2q bits of uncertainty. The two translation equivalences reduce the counts to finite vector spaces. Such…
Exact mathematical passage
k=\dim_K H
\mathrm{discovery}Use in source · 1 passage
Search aliases: discovery mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
\mathbb EUse in source · 3 passages
Search aliases: E mathbb
Use in source · Read passage · Proof_Path_Theory.tex, line 1874
Let X_i=θ+ε_i be numerical estimates of a fixed quantity θ. Assume Eε_i=0, Var(ε_i)=σ^2>0, and common pairwise correlation ρ. For n>1, assume -1/(n-1)<ρ≤1, so the mean has positive variance. These variables model estimates, not proof truth values. The mean has variance Var(bar X) = σ^2(frac1-ρn+ρ).
Exact mathematical passage
\mathbb E\varepsilon_i=0
e^{-1}Use in source · 1 passage
Search aliases: e^-1
Use in source · Read passage · Proof_Path_Theory.tex, line 1740
ginal contribution of the at most k elements of O_k beyond S_i is at least G^*-G_i. Hence at least one candidate has marginal gain at least (G^*-G_i)/k. Greedy chooses a candidate with at least that gain, so G^*-G_i+1 ≤ (1-frac1k)(G^*-G_i). Iterating from G_0=0 gives G^*-G_k ≤ (1-frac1k)^kG^*. Rearranging gives the first bound. The inequality (1-1/k)^k≤ e^-1 gives the second.
Exact mathematical passage
(1-1/k)^k\le e^{-1}
e_1Use in source · 1 passage
Search aliases: e_1
Use in source · Read passage · Proof_Path_Theory.tex, line 503
, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificate for t must derive every e_j. Deriving e_j requires at least one se…
Exact mathematical passage
\{e_1,\ldots,e_m\}\Longrightarrow t.
e_CUse in source · 2 passages
Search aliases: e_C
Use in source · Read passage · Proof_Path_Theory.tex, line 1225
[Lossless encoding at the typed syntax boundary] Let e_P,d_P and e_C,d_C be the stated Lean encoders and partial decoders for problem and certificate records. For every typed problem P and certificate C, d_P(e_P(P))=some(P), d_C(e_C(C))=some(C). Consequently both encoders are injective on their typed domains. These identities do not require the encoded record to pass the separate validity checks. The natural-number and Boolean constructors decode to their original values. Induction on a list pro…
Exact mathematical passage
e_C,d_C
e_jUse in source · 4 passages
Search aliases: e_j
Use in source · Read passage · Proof_Path_Theory.tex, line 498
For NP-hardness, reduce Set Cover. Let U={u_1,…,u_m} be the universe, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificat…
Exact mathematical passage
e_j
e_mUse in source · 1 passage
Search aliases: e_m
Use in source · Read passage · Proof_Path_Theory.tex, line 503
, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificate for t must derive every e_j. Deriving e_j requires at least one se…
Exact mathematical passage
\{e_1,\ldots,e_m\}\Longrightarrow t.
e_PUse in source · 2 passages
Search aliases: e_P
Use in source · Read passage · Proof_Path_Theory.tex, line 1225
[Lossless encoding at the typed syntax boundary] Let e_P,d_P and e_C,d_C be the stated Lean encoders and partial decoders for problem and certificate records. For every typed problem P and certificate C, d_P(e_P(P))=some(P), d_C(e_C(C))=some(C). Consequently both encoders are injective on their typed domains. These identities do not require the encoded record to pass the separate validity checks. The natural-number and Boolean constructors decode to their original values. Induction on a list pro…
Exact mathematical passage
e_P,d_P
\mathrm{err}Use in source · 2 passages
Search aliases: err mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 2026
A simple audit priority score is P(x) = fracp_err(x) c_consequence(x) (1+r_dependency(x)) c_audit(x). Here p_err(x)∈[0,1], the consequence and dependency factors are nonnegative, and c_audit(x)>0. Zero-cost checks can be handled separately. This is a declared priority heuristic, not a probability of truth or a proved optimal scheduling rule.
Exact mathematical passage
P(x) = \frac{p_{\mathrm{err}}(x)\,c_{\mathrm{consequence}}(x) \bigl(1+r_{\mathrm{dependency}}(x)\bigr)} {c_{\mathrm{audit}}(x)}.
\operatorname{Ext}_GUse in source · 1 passage
Search aliases: Ext_G operatorname
Use in source · Read passage · Proof_Path_Theory.tex, line 1072
[Compositional rule transport] Rule transports admit identities and associative composition. A transport (f,h):F→ G sends every derivation of v in F to a derivation of f(v) in G. Every G-model pulls back along f to an F-model. In particular, Y∈Ext_G(f(S),f(N)) Longrightarrow f^-1(Y)∈Ext_F(S,N). An obstruction in the source extension problem therefore implies an obstruction in the target extension problem with the mapped observations. Identity maps meet each displayed condition. For two composabl…
Exact mathematical passage
Y\in\operatorname{Ext}_G(f(S),f(N)) \Longrightarrow f^{-1}(Y)\in\operatorname{Ext}_F(S,N).
\mathbb FUse in source · 7 passages
Search aliases: F mathbb
Use in source · Read passage · Proof_Path_Theory.tex, line 608
A second connection is quantitative. Work over F_2 with E= F_2^n. Let A:E→ F_2^m impose coherence, P:E→ F_2^p retain prescribed information, and x∈ E be a raw candidate. Define K_P(x)={y∈ E:Ay=0, Py=Px}, M=A
Exact mathematical passage
\mathbb F_2
f^{-1}Use in source · 2 passages
Search aliases: f^-1
Use in source · Read passage · Proof_Path_Theory.tex, line 1072
[Compositional rule transport] Rule transports admit identities and associative composition. A transport (f,h):F→ G sends every derivation of v in F to a derivation of f(v) in G. Every G-model pulls back along f to an F-model. In particular, Y∈Ext_G(f(S),f(N)) Longrightarrow f^-1(Y)∈Ext_F(S,N). An obstruction in the source extension problem therefore implies an obstruction in the target extension problem with the mapped observations. Identity maps meet each displayed condition. For two composabl…
Exact mathematical passage
Y\in\operatorname{Ext}_G(f(S),f(N)) \Longrightarrow f^{-1}(Y)\in\operatorname{Ext}_F(S,N).
f_1Use in source · 2 passages
Search aliases: f_1
Use in source · Read passage · Proof_Path_Theory.tex, line 537
[Functorial transport] Let F:Cert_1→Cert_2 be a functor. If Axrightarrowf_1S_1xrightarrowf_2⋯xrightarrowf_rB is a certified path in Cert_1, then F(A)xrightarrowF(f_1)F(S_1)xrightarrowF(f_2)⋯xrightarrowF(f_r)F(B) is a certified path in Cert_2.
Exact mathematical passage
A\xrightarrow{f_1}S_1\xrightarrow{f_2}\cdots\xrightarrow{f_r}B
\mathbb F_2Use in source · 2 passages
Search aliases: F_2 mathbb
Use in source · Read passage · Proof_Path_Theory.tex, line 608
A second connection is quantitative. Work over F_2 with E= F_2^n. Let A:E→ F_2^m impose coherence, P:E→ F_2^p retain prescribed information, and x∈ E be a raw candidate. Define K_P(x)={y∈ E:Ay=0, Py=Px}, M=A
Exact mathematical passage
\mathbb F_2
f_2Use in source · 2 passages
Search aliases: f_2
Use in source · Read passage · Proof_Path_Theory.tex, line 537
[Functorial transport] Let F:Cert_1→Cert_2 be a functor. If Axrightarrowf_1S_1xrightarrowf_2⋯xrightarrowf_rB is a certified path in Cert_1, then F(A)xrightarrowF(f_1)F(S_1)xrightarrowF(f_2)⋯xrightarrowF(f_r)F(B) is a certified path in Cert_2.
Exact mathematical passage
A\xrightarrow{f_1}S_1\xrightarrow{f_2}\cdots\xrightarrow{f_r}B
\mathbb F_2^3Use in source · 1 passage
Search aliases: F_2^3 mathbb
Use in source · Read passage · Proof_Path_Theory.tex, line 655
[One informative question] Let y=(a,b,c)∈ F_2^3 with a+b+c=0 and protected value a=0. The realization fiber is {(0,0,0),(0,1,1)}. It has one bit of ambiguity. Observing b resolves that bit exactly. Observing a supplies no new information, despite being a perfectly valid measurement. This difference is measured by the rank of the observation restricted to H, rather than by the output width of the observation.
Exact mathematical passage
y=(a,b,c)\in\mathbb F_2^3
\mathbb F_2^mUse in source · 1 passage
Search aliases: F_2^m mathbb
Use in source · Read passage · Proof_Path_Theory.tex, line 608
A second connection is quantitative. Work over F_2 with E= F_2^n. Let A:E→ F_2^m impose coherence, P:E→ F_2^p retain prescribed information, and x∈ E be a raw candidate. Define K_P(x)={y∈ E:Ay=0, Py=Px}, M=A
Exact mathematical passage
A:E\to\mathbb F_2^m
\mathbb F_2^nUse in source · 1 passage
Search aliases: F_2^n mathbb
Use in source · Read passage · Proof_Path_Theory.tex, line 608
A second connection is quantitative. Work over F_2 with E= F_2^n. Let A:E→ F_2^m impose coherence, P:E→ F_2^p retain prescribed information, and x∈ E be a raw candidate. Define K_P(x)={y∈ E:Ay=0, Py=Px}, M=A
Exact mathematical passage
E=\mathbb F_2^n
\mathbb F_2^pUse in source · 1 passage
Search aliases: F_2^p mathbb
Use in source · Read passage · Proof_Path_Theory.tex, line 608
A second connection is quantitative. Work over F_2 with E= F_2^n. Let A:E→ F_2^m impose coherence, P:E→ F_2^p retain prescribed information, and x∈ E be a raw candidate. Define K_P(x)={y∈ E:Ay=0, Py=Px}, M=A
Exact mathematical passage
P:E\to\mathbb F_2^p
\mathbb F_2^qUse in source · 1 passage
Search aliases: F_2^q mathbb
Use in source · Read passage · Proof_Path_Theory.tex, line 635
Suppose the realization fiber is nonempty and a new linear observation Q:E→ F_2^q becomes available. The right question is not how many bits appear in the output of Q but how many remaining degrees of freedom in the fiber it distinguishes.
Exact mathematical passage
Q:E\to\mathbb F_2^q
f_rUse in source · 2 passages
Search aliases: f_r
Use in source · Read passage · Proof_Path_Theory.tex, line 537
[Functorial transport] Let F:Cert_1→Cert_2 be a functor. If Axrightarrowf_1S_1xrightarrowf_2⋯xrightarrowf_rB is a certified path in Cert_1, then F(A)xrightarrowF(f_1)F(S_1)xrightarrowF(f_2)⋯xrightarrowF(f_r)F(B) is a certified path in Cert_2.
Exact mathematical passage
A\xrightarrow{f_1}S_1\xrightarrow{f_2}\cdots\xrightarrow{f_r}B
\mathrm{feasible}Use in source · 1 passage
Search aliases: feasible mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1195
erdict The complete result format contains a Boolean feasibility flag, a reported closure, a strict closure trace, and an optional forbidden-node witness. Both branches require the complete-closure check. A positive result additionally requires no obstruction witness and no forbidden node in the closure. A negative result requires an accepted obstruction witness. For every accepted result C, C.K=cl_F(S), (C.feasible=true) Longleftrightarrow Ext_F(S,N)≠∅. The complete-closure check proves the fir…
Exact mathematical passage
C.K=\operatorname{cl}_F(S),\qquad \bigl(C.\mathrm{feasible}=\mathrm{true}\bigr) \Longleftrightarrow \operatorname{Ext}_F(S,N)\ne\varnothing.
\mathrm{formal}Use in source · 1 passage
Search aliases: formal mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
GUse in source · 18 passages
Search aliases: G
Use in source · Read passage · Proof_Path_Theory.tex, line 1058
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G,
Exact mathematical passage
G
G^*Use in source · 5 passages
Search aliases: G^*
Use in source · Read passage · Proof_Path_Theory.tex, line 1728
Write G_i=U_M(S_i)-U_M(∅) and G^*=U_M(O_k)-U_M(∅). By monotonicity and submodularity, the total marginal contribution of the at most k elements of O_k beyond S_i is at least G^*-G_i. Hence at least one candidate has marginal gain at least (G^*-G_i)/k. Greedy chooses a candidate with at least that gain, so G^*-G_i+1 ≤ (1-frac1k)(G^*-G_i). Iterating from G_0=0 gives G^*-G_k ≤ (1-frac1k)^kG^*. Rearranging gives the first bound. The inequality (1-1/k)^k≤ e^-1 gives the second.
Exact mathematical passage
G^*=U_M(O_k)-U_M(\varnothing)
G_0Use in source · 1 passage
Search aliases: G_0
Use in source · Read passage · Proof_Path_Theory.tex, line 1734
_M(S_i)-U_M(∅) and G^*=U_M(O_k)-U_M(∅). By monotonicity and submodularity, the total marginal contribution of the at most k elements of O_k beyond S_i is at least G^*-G_i. Hence at least one candidate has marginal gain at least (G^*-G_i)/k. Greedy chooses a candidate with at least that gain, so G^*-G_i+1 ≤ (1-frac1k)(G^*-G_i). Iterating from G_0=0 gives G^*-G_k ≤ (1-frac1k)^kG^*. Rearranging gives the first bound. The inequality (1-1/k)^k≤ e^-1 gives the second.
Exact mathematical passage
G_0=0
G_iUse in source · 4 passages
Search aliases: G_i
Use in source · Read passage · Proof_Path_Theory.tex, line 1728
Write G_i=U_M(S_i)-U_M(∅) and G^*=U_M(O_k)-U_M(∅). By monotonicity and submodularity, the total marginal contribution of the at most k elements of O_k beyond S_i is at least G^*-G_i. Hence at least one candidate has marginal gain at least (G^*-G_i)/k. Greedy chooses a candidate with at least that gain, so G^*-G_i+1 ≤ (1-frac1k)(G^*-G_i). Iterating from G_0=0 gives G^*-G_k ≤ (1-frac1k)^kG^*. Rearranging gives the first bound. The inequality (1-1/k)^k≤ e^-1 gives the second.
Exact mathematical passage
G_i=U_M(S_i)-U_M(\varnothing)
G_{i+1}Use in source · 1 passage
Search aliases: G_i+1
Use in source · Read passage · Proof_Path_Theory.tex, line 1729
Write G_i=U_M(S_i)-U_M(∅) and G^*=U_M(O_k)-U_M(∅). By monotonicity and submodularity, the total marginal contribution of the at most k elements of O_k beyond S_i is at least G^*-G_i. Hence at least one candidate has marginal gain at least (G^*-G_i)/k. Greedy chooses a candidate with at least that gain, so G^*-G_i+1 ≤ (1-frac1k)(G^*-G_i). Iterating from G_0=0 gives G^*-G_k ≤ (1-frac1k)^kG^*. Rearranging gives the first bound. The inequality (1-1/k)^k≤ e^-1 gives the second.
Exact mathematical passage
G^*-G_{i+1} \le \left(1-\frac1k\right)(G^*-G_i).
G_kUse in source · 1 passage
Search aliases: G_k
Use in source · Read passage · Proof_Path_Theory.tex, line 1735
rnothing) and G^*=U_M(O_k)-U_M(∅). By monotonicity and submodularity, the total marginal contribution of the at most k elements of O_k beyond S_i is at least G^*-G_i. Hence at least one candidate has marginal gain at least (G^*-G_i)/k. Greedy chooses a candidate with at least that gain, so G^*-G_i+1 ≤ (1-frac1k)(G^*-G_i). Iterating from G_0=0 gives G^*-G_k ≤ (1-frac1k)^kG^*. Rearranging gives the first bound. The inequality (1-1/k)^k≤ e^-1 gives the second.
Exact mathematical passage
G^*-G_k \le \left(1-\frac1k\right)^kG^*.
hUse in source · 19 passages
Search aliases: h
Use in source · Read passage · Proof_Path_Theory.tex, line 819
[A linear certificate alternative] The protected problem is infeasible if and only if there is a linear functional λ:R→ K satisfying λ(Dh)=0 whenever p(h)=0, λ(Dx)=1. For a finite matrix M and right side b, the corresponding alternative is nexists y (My=b) Longleftrightarrow ∃ℓ (ℓ M=0 and ℓ b=1). If Dx∉ B, linear separation of a vector from a subspace gives a functional vanishing on B and nonzero at Dx. One construction extends a basis of B by Dx and then to a basis of R. Assign value zero to th…
Exact mathematical passage
\lambda(Dh)=0\quad\text{whenever }p(h)=0, \qquad \lambda(Dx)=1.
IUse in source · 3 passages
Search aliases: I
Use in source · Read passage · Proof_Path_Theory.tex, line 758
Let (U_i)_i∈ I cover the nodes. A family X_i∈ M_F(U_i) is matching when X_i∩ U_j=X_j∩ U_i for every i,j. This equality includes agreement about false values, not merely common true values.
Exact mathematical passage
(U_i)_{i\in I}
\mathrm{id}Use in source · 1 passage
Search aliases: id mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 714
[The proof-field view laws] The restriction maps satisfy ρ_U,U=id, ρ_U,Wρ_W,Z=ρ_U,Z (U⊆ W⊆ Z). Consequently U↦ M_F(U) is a contravariant set-valued view system on the inclusion order of patches. Both laws are the corresponding intersection identities. For the second, (X∩ W)∩ U=X∩ U because U⊆ W. The values outside a patch are absent, or equivalently normalized to false in the Lean representation. There are no additional hidden coordinates.
Exact mathematical passage
\rho_{U,U}=\mathrm{id},\qquad \rho_{U,W}\rho_{W,Z}=\rho_{U,Z}\quad(U\subseteq W\subseteq Z).
J_FUse in source · 1 passage
Search aliases: J_F
Use in source · Read passage · Proof_Path_Theory.tex, line 1058
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G,
Exact mathematical passage
h:J_F\to J_G
J_GUse in source · 1 passage
Search aliases: J_G
Use in source · Read passage · Proof_Path_Theory.tex, line 1058
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G,
Exact mathematical passage
h:J_F\to J_G
J_iUse in source · 1 passage
Search aliases: J_i
Use in source · Read passage · Proof_Path_Theory.tex, line 1965
[MSE with a shared interpretive offset] Suppose reviewers report J_i=θ+b+ε_i, where θ is the target quantity, b is a fixed shared offset, Eε_i=0, Var(ε_i)=σ^2, and Cov(ε_i,ε_j)=ρσ^2 for i≠ j. For admissible ρ, the mean squared error of the reviewer average is E(overline J_n-θ)^2=b^2+σ^2(ρ+frac1-ρn). For fixed ρ≥0, it approaches b^2+ρσ^2 as n→∞. The estimation error is overline J_n-θ=b+overlineε_n. Its mean is b, and its variance is σ^2((1-ρ)/n+ρ) by summing all diagonal and off-diagonal covarian…
Exact mathematical passage
J_i=\theta+b+\varepsilon_i
\mathrm{journal}Use in source · 1 passage
Search aliases: journal mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
\mathfrak KUse in source · 3 passages
Search aliases: K mathfrak
Use in source · Read passage · Proof_Path_Theory.tex, line 609
A second connection is quantitative. Work over F_2 with E= F_2^n. Let A:E→ F_2^m impose coherence, P:E→ F_2^p retain prescribed information, and x∈ E be a raw candidate. Define K_P(x)={y∈ E:Ay=0, Py=Px}, M=A P, b=0 Px. This is a finite linear realization fiber. The equation My=b does not by itself produce a solution. Compatibility of the prescribed information must first be established.
Exact mathematical passage
\mathfrak K_P(x)=\{y\in E:Ay=0,\ Py=Px\},\qquad M=\begin{bmatrix}A\\P\end{bmatrix},\quad b=\begin{bmatrix}0\\Px\end{bmatrix}.
K'Use in source · 2 passages
Search aliases: K'
Use in source · Read passage · Proof_Path_Theory.tex, line 1117
[Replay preserves derivability and composes] Suppose every member of K belongs to cl_F(S). If either replay mode accepts a trace starting from K and returns K', then K⊆ K'⊆cl_F(S). For a fixed replay mode, replaying σmathbin+ +τ is the same as replaying σ and then replaying τ from the returned state. Failure at either stage propagates to the concatenated execution. Induct on the trace. The empty trace returns the initial state. For a nonempty trace, a successful first step identifies a certified…
Exact mathematical passage
K'
K_1Use in source · 4 passages
Search aliases: K_1
Use in source · Read passage · Proof_Path_Theory.tex, line 1537
[Debt is monotone under retention] If K_1⊆ K_2, then Debt(K_2)≤Debt(K_1).
Exact mathematical passage
K_1\subseteq K_2
K_2Use in source · 3 passages
Search aliases: K_2
Use in source · Read passage · Proof_Path_Theory.tex, line 1537
[Debt is monotone under retention] If K_1⊆ K_2, then Debt(K_2)≤Debt(K_1).
Exact mathematical passage
K_1\subseteq K_2
K_{\mathrm{core}}Use in source · 3 passages
Search aliases: K_core mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 445
[Unique verification core] Let P be a finite acyclic AND-DAG relative to T_0. Put K_core=A∪ T_0∪Anc_L(T_0). Then (K_core,H_core) is a certificate and is the least certificate under componentwise inclusion. In particular it is the unique inclusion-minimal certificate pair for this recorded inference problem.
Exact mathematical passage
K_{\mathrm{core}}=A\cup T_0\cup\Anc_L(T_0).
\mathfrak K_PUse in source · 3 passages
Search aliases: K_P mathfrak
Use in source · Read passage · Proof_Path_Theory.tex, line 609
A second connection is quantitative. Work over F_2 with E= F_2^n. Let A:E→ F_2^m impose coherence, P:E→ F_2^p retain prescribed information, and x∈ E be a raw candidate. Define K_P(x)={y∈ E:Ay=0, Py=Px}, M=A P, b=0 Px. This is a finite linear realization fiber. The equation My=b does not by itself produce a solution. Compatibility of the prescribed information must first be established.
Exact mathematical passage
\mathfrak K_P(x)=\{y\in E:Ay=0,\ Py=Px\},\qquad M=\begin{bmatrix}A\\P\end{bmatrix},\quad b=\begin{bmatrix}0\\Px\end{bmatrix}.
K_rUse in source · 1 passage
Search aliases: K_r
Use in source · Read passage · Proof_Path_Theory.tex, line 1550
[Irreversible compression accumulates debt] For a descending sequence of retained sets K_0⊇ K_1⊇⋯⊇ K_r, the expected debt is nondecreasing.
Exact mathematical passage
K_0\supseteq K_1\supseteq\cdots\supseteq K_r,
lUse in source · 1 passage
Search aliases: l
Use in source · Read passage · Proof_Path_Theory.tex, line 2395
The final thesis is therefore: 0.88linewidth A proof should be published as a certificate and maintained as a versioned proof field. The certificate preserves deductive validity. The larger field preserves the dependencies, alternatives, examples, failures, provenance, and bridges from which later mathematics may grow.
Exact mathematical passage
\boxed{\begin{minipage}{0.88\linewidth} A proof should be published as a certificate and maintained as a versioned proof field. The certificate preserves deductive validity. The larger field preserves the dependencies, alternatives, examples, failures, provenance, and bridges from which later mathematics may grow. \end{minipage}}
L_1Use in source · 6 passages
Search aliases: L_1
Use in source · Read passage · Proof_Path_Theory.tex, line 469
[htbp] centering includegraphics[width=linewidth]fig_02_and_dag_core.pdf captionThe canonical pathand_dag.json example. The AND gate requires both A and D for L_1. Its least certificate contains five nodes and four certified rules. The gold branch is certified but unnecessary for B. The dashed route to F is uncertified and cannot enter the certificate.
Exact mathematical passage
L_1
L_2Use in source · 3 passages
Search aliases: L_2
Use in source · Read passage · Proof_Path_Theory.tex, line 1810
[htbp] centering includegraphics[width=linewidth]fig_09_version_invalidation.pdf captionChanging L_1 marks L_1, L_2, and B for syntactic review. The lower branch has no forward dependency path from L_1. Membership in the review set is not a claim that a theorem has become false.
Exact mathematical passage
L_2
L_FUse in source · 1 passage
Search aliases: L_F
Use in source · Read passage · Proof_Path_Theory.tex, line 1059
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G, j certified in F · Longrightarrow h(j) certified in G, A^G_h(j) · ⊆ f(A^F_j), c^G_h(j) · =f(c^F_j). The premise inclusion points in the direction needed for executing the translated step. The mapped target rule may need fewer premises, but it must not introduce a new premise unsupported …
Exact mathematical passage
\begin{aligned} f(L_F)&\subseteq L_G,\\ j\text{ certified in }F&\Longrightarrow h(j)\text{ certified in }G,\\ A^G_{h(j)}&\subseteq f(A^F_j),\\ c^G_{h(j)}&=f(c^F_j). \end{aligned}
L_GUse in source · 1 passage
Search aliases: L_G
Use in source · Read passage · Proof_Path_Theory.tex, line 1059
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G, j certified in F · Longrightarrow h(j) certified in G, A^G_h(j) · ⊆ f(A^F_j), c^G_h(j) · =f(c^F_j). The premise inclusion points in the direction needed for executing the translated step. The mapped target rule may need fewer premises, but it must not introduce a new premise unsupported …
Exact mathematical passage
\begin{aligned} f(L_F)&\subseteq L_G,\\ j\text{ certified in }F&\Longrightarrow h(j)\text{ certified in }G,\\ A^G_{h(j)}&\subseteq f(A^F_j),\\ c^G_{h(j)}&=f(c^F_j). \end{aligned}
L_{\mathrm{short}}Use in source · 1 passage
Search aliases: L_short mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 2114
The field examples/alternative_proofs.json contains a short route and a richer explanatory route. The short route has storage cost 1, while the richer route has storage cost 3 and larger meaning and discovery values. Exact certificate search chooses A⟶ L_short⟶ B when the objective is storage cost alone. A teaching compiler may rationally choose the other route because it uses a different objective.
Exact mathematical passage
A\longrightarrow L_{\mathrm{short}}\longrightarrow B
\linewidthUse in source · 1 passage
Search aliases: linewidth
Use in source · Read passage · Proof_Path_Theory.tex, line 2395
The final thesis is therefore: 0.88linewidth A proof should be published as a certificate and maintained as a versioned proof field. The certificate preserves deductive validity. The larger field preserves the dependencies, alternatives, examples, failures, provenance, and bridges from which later mathematics may grow.
Exact mathematical passage
\boxed{\begin{minipage}{0.88\linewidth} A proof should be published as a certificate and maintained as a versioned proof field. The certificate preserves deductive validity. The larger field preserves the dependencies, alternatives, examples, failures, provenance, and bridges from which later mathematics may grow. \end{minipage}}
\logUse in source · 3 passages
Search aliases: log
Use in source · Read passage · Proof_Path_Theory.tex, line 650
s. The image Q(H) is a vector subspace of dimension r=rank(Q|_H), so the observed values form the affine set Qy_0+Q(H) of size 2^r. Every such value has a preimage that is a coset of H∩ker Q, whose dimension is dim H-r by rank nullity. Equal fiber cardinalities make the induced output distribution uniform on 2^r values. Its entropy is log_2(2^r)=r, and each conditional fiber has cardinality 2^dim H-r.
Exact mathematical passage
\log_2(2^r)=r
\log_2Use in source · 3 passages
Search aliases: log_2 log
Use in source · Read passage · Proof_Path_Theory.tex, line 650
s. The image Q(H) is a vector subspace of dimension r=rank(Q|_H), so the observed values form the affine set Qy_0+Q(H) of size 2^r. Every such value has a preimage that is a coset of H∩ker Q, whose dimension is dim H-r by rank nullity. Equal fiber cardinalities make the induced output distribution uniform on 2^r values. Its entropy is log_2(2^r)=r, and each conditional fiber has cardinality 2^dim H-r.
Exact mathematical passage
\log_2(2^r)=r
\LongleftrightarrowUse in source · 5 passages
Search aliases: Longleftrightarrow
Use in source · Read passage · Proof_Path_Theory.tex, line 687
[Soundness and relative completeness] For every node v, v∈Der_F Longleftrightarrow v∈ X for every model X of the declared field. If v is not derivable, Der_F itself is a model omitting v. Every model contains the leaves. Induction on a derivation shows that it contains the conclusion of every certified application whose premises have already been derived. Thus every model contains Der_F. Conversely, the inductive constructors show that Der_F contains the leaves and is closed under every certifie…
Exact mathematical passage
v\in\operatorname{Der}_F \quad\Longleftrightarrow\quad \text{$v\in X$ for every model $X$ of the declared field}.
\LongrightarrowUse in source · 6 passages
Search aliases: Longrightarrow
Use in source · Read passage · Proof_Path_Theory.tex, line 499
For NP-hardness, reduce Set Cover. Let U={u_1,…,u_m} be the universe, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificat…
Exact mathematical passage
\{s_i\}\Longrightarrow e_j.
mUse in source · 8 passages
Search aliases: m
Use in source · Read passage · Proof_Path_Theory.tex, line 498
For NP-hardness, reduce Set Cover. Let U={u_1,…,u_m} be the universe, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificat…
Exact mathematical passage
U=\{u_1,\ldots,u_m\}
\maxUse in source · 1 passage
Search aliases: max
Use in source · Read passage · Proof_Path_Theory.tex, line 1999
Let a_t≥0 be candidate arrivals during audit cycle t, let s_t≥0 be service capacity, and let B_t≥0 be the unresolved backlog. Suppose arrivals in a cycle are available to that cycle's service. The basic deterministic queue is B_t+1=max{0,B_t+a_t-s_t}.
Exact mathematical passage
B_{t+1}=\max\{0,B_t+a_t-s_t\}.
\operatorname{Models}Use in source · 1 passage
Search aliases: Models operatorname
Use in source · Read passage · Proof_Path_Theory.tex, line 730
The strict Komorebi realization is now an actual set of coherent local models, Γ( M_F)= {(X_U)_U:ρ_U,W(X_W)=X_U whenever U⊆ W}. There is an explicit bijection Models(F)≃Γ( M_F), X⟼(X∩ U)_U. Its inverse evaluates a coherent family at the full patch V. Coherence shows that every other component is precisely the restriction of that value. The Lean declaration pathProofPath.Field.modelEquivSections constructs this equivalence, using pathViewDiagram and the actual local restriction maps.
Exact mathematical passage
\operatorname{Models}(F)\simeq\Gamma(\mathcal M_F), \qquad X\longmapsto(X\cap U)_U.
N'Use in source · 2 passages
Search aliases: N'
Use in source · Read passage · Proof_Path_Theory.tex, line 982
[Staged closure and persistent obstructions] For positive sets S,T, cl_F(cl_F(S)∪ T) =cl_F(S∪ T). If S⊆ S' and N⊆ N', then Ext_F(S',N')⊆Ext_F(S,N). Consequently an infeasible request stays infeasible under those additions, while the field and the meaning of its rules remain fixed. Closure is extensive, monotone, and idempotent because it is the least model containing its seed. The model cl_F(S∪ T) contains cl_F(S) and T, giving one inclusion in the first equation. Extensivity gives S∪ T⊆cl_F(S)∪…
Exact mathematical passage
N\subseteq N'
N^{-1}Use in source · 1 passage
Search aliases: N^-1
Use in source · Read passage · Proof_Path_Theory.tex, line 1979
luations of reviewer i under two labels. In a finite set of N reviewers, assign exactly n_1 to the first label and n_0=N-n_1 to the second, uniformly over assignments with those sizes, where n_0,n_1>0. Assume each observed response equals the potential response under its assigned label and does not depend on other assignments. Then the difference of the two sample means is unbiased for N^-1∑_i(Y_i(1)-Y_i(0)). Indeed, each reviewer has inclusion probability n_1/N in the first mean and n_0/N in th…
Exact mathematical passage
N^{-1}\sum_i(Y_i(1)-Y_i(0))
n_0Use in source · 3 passages
Search aliases: n_0
Use in source · Read passage · Proof_Path_Theory.tex, line 1979
A claim about identity effects needs a design that can distinguish them from other differences. Hold the mathematical content fixed and let Y_i(1) and Y_i(0) be the fixed potential evaluations of reviewer i under two labels. In a finite set of N reviewers, assign exactly n_1 to the first label and n_0=N-n_1 to the second, uniformly over assignments with those sizes, where n_0,n_1>0. Assume each observed response equals the potential response under its assigned label and does not depend on other …
Exact mathematical passage
n_0=N-n_1
n_1Use in source · 4 passages
Search aliases: n_1
Use in source · Read passage · Proof_Path_Theory.tex, line 1979
A claim about identity effects needs a design that can distinguish them from other differences. Hold the mathematical content fixed and let Y_i(1) and Y_i(0) be the fixed potential evaluations of reviewer i under two labels. In a finite set of N reviewers, assign exactly n_1 to the first label and n_0=N-n_1 to the second, uniformly over assignments with those sizes, where n_0,n_1>0. Assume each observed response equals the potential response under its assigned label and does not depend on other …
Exact mathematical passage
n_1
\nexistsUse in source · 1 passage
Search aliases: nexists
Use in source · Read passage · Proof_Path_Theory.tex, line 824
[A linear certificate alternative] The protected problem is infeasible if and only if there is a linear functional λ:R→ K satisfying λ(Dh)=0 whenever p(h)=0, λ(Dx)=1. For a finite matrix M and right side b, the corresponding alternative is nexists y (My=b) Longleftrightarrow ∃ℓ (ℓ M=0 and ℓ b=1). If Dx∉ B, linear separation of a vector from a subspace gives a functional vanishing on B and nonzero at Dx. One construction extends a basis of B by Dx and then to a basis of R. Assign value zero to th…
Exact mathematical passage
\nexists y\ (My=b) \quad\Longleftrightarrow\quad \exists\ell\ (\ell M=0\ \text{and}\ \ell b=1).
OUse in source · 4 passages
Search aliases: O
Use in source · Read passage · Proof_Path_Theory.tex, line 1717
[Greedy cardinality guarantee] Let k be an integer with 1≤ k≤|C|. Starting from the empty supplement, let S_k result from repeatedly adding an unselected candidate with largest marginal future reach. Let O_k be an optimal supplement of size at most k. Then U_M(S_k)-U_M(∅) ≥ (1-(1-frac1k)^k) (U_M(O_k)-U_M(∅)), and therefore the greedy gain is at least (1-1/e) times the optimal gain.
Exact mathematical passage
O_k
oUse in source · 1 passage
Search aliases: o
Use in source · Read passage · Proof_Path_Theory.tex, line 2395
The final thesis is therefore: 0.88linewidth A proof should be published as a certificate and maintained as a versioned proof field. The certificate preserves deductive validity. The larger field preserves the dependencies, alternatives, examples, failures, provenance, and bridges from which later mathematics may grow.
Exact mathematical passage
\boxed{\begin{minipage}{0.88\linewidth} A proof should be published as a certificate and maintained as a versioned proof field. The certificate preserves deductive validity. The larger field preserves the dependencies, alternatives, examples, failures, provenance, and bridges from which later mathematics may grow. \end{minipage}}
O_kUse in source · 4 passages
Search aliases: O_k
Use in source · Read passage · Proof_Path_Theory.tex, line 1717
[Greedy cardinality guarantee] Let k be an integer with 1≤ k≤|C|. Starting from the empty supplement, let S_k result from repeatedly adding an unselected candidate with largest marginal future reach. Let O_k be an optimal supplement of size at most k. Then U_M(S_k)-U_M(∅) ≥ (1-(1-frac1k)^k) (U_M(O_k)-U_M(∅)), and therefore the greedy gain is at least (1-1/e) times the optimal gain.
Exact mathematical passage
O_k
\overline JUse in source · 2 passages
Search aliases: overline J overline
Use in source · Read passage · Proof_Path_Theory.tex, line 1966
shared interpretive offset] Suppose reviewers report J_i=θ+b+ε_i, where θ is the target quantity, b is a fixed shared offset, Eε_i=0, Var(ε_i)=σ^2, and Cov(ε_i,ε_j)=ρσ^2 for i≠ j. For admissible ρ, the mean squared error of the reviewer average is E(overline J_n-θ)^2=b^2+σ^2(ρ+frac1-ρn). For fixed ρ≥0, it approaches b^2+ρσ^2 as n→∞. The estimation error is overline J_n-θ=b+overlineε_n. Its mean is b, and its variance is σ^2((1-ρ)/n+ρ) by summing all diagonal and off-diagonal covariance entries. …
Exact mathematical passage
\boxed{\mathbb E(\overline J_n-\theta)^2=b^2+\sigma^2\left(\rho+\frac{1-\rho}{n}\right).}
\overline J_nUse in source · 2 passages
Search aliases: overline J_n overline
Use in source · Read passage · Proof_Path_Theory.tex, line 1966
shared interpretive offset] Suppose reviewers report J_i=θ+b+ε_i, where θ is the target quantity, b is a fixed shared offset, Eε_i=0, Var(ε_i)=σ^2, and Cov(ε_i,ε_j)=ρσ^2 for i≠ j. For admissible ρ, the mean squared error of the reviewer average is E(overline J_n-θ)^2=b^2+σ^2(ρ+frac1-ρn). For fixed ρ≥0, it approaches b^2+ρσ^2 as n→∞. The estimation error is overline J_n-θ=b+overlineε_n. Its mean is b, and its variance is σ^2((1-ρ)/n+ρ) by summing all diagonal and off-diagonal covariance entries. …
Exact mathematical passage
\boxed{\mathbb E(\overline J_n-\theta)^2=b^2+\sigma^2\left(\rho+\frac{1-\rho}{n}\right).}
\overline\varepsilonUse in source · 1 passage
Search aliases: overlineε overline varepsilon
Use in source · Read passage · Proof_Path_Theory.tex, line 1972
psilon_i)=σ^2, and Cov(ε_i,ε_j)=ρσ^2 for i≠ j. For admissible ρ, the mean squared error of the reviewer average is E(overline J_n-θ)^2=b^2+σ^2(ρ+frac1-ρn). For fixed ρ≥0, it approaches b^2+ρσ^2 as n→∞. The estimation error is overline J_n-θ=b+overlineε_n. Its mean is b, and its variance is σ^2((1-ρ)/n+ρ) by summing all diagonal and off-diagonal covariance entries. Mean squared error is variance plus squared bias. Taking the limit completes the proof.
Exact mathematical passage
\overline J_n-\theta=b+\overline\varepsilon_n
\overline\varepsilon_nUse in source · 1 passage
Search aliases: overlineε_n overline varepsilon
Use in source · Read passage · Proof_Path_Theory.tex, line 1972
psilon_i)=σ^2, and Cov(ε_i,ε_j)=ρσ^2 for i≠ j. For admissible ρ, the mean squared error of the reviewer average is E(overline J_n-θ)^2=b^2+σ^2(ρ+frac1-ρn). For fixed ρ≥0, it approaches b^2+ρσ^2 as n→∞. The estimation error is overline J_n-θ=b+overlineε_n. Its mean is b, and its variance is σ^2((1-ρ)/n+ρ) by summing all diagonal and off-diagonal covariance entries. Mean squared error is variance plus squared bias. Taking the limit completes the proof.
Exact mathematical passage
\overline J_n-\theta=b+\overline\varepsilon_n
p_{\mathrm{err}}Use in source · 2 passages
Search aliases: p_err mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 2026
A simple audit priority score is P(x) = fracp_err(x) c_consequence(x) (1+r_dependency(x)) c_audit(x). Here p_err(x)∈[0,1], the consequence and dependency factors are nonnegative, and c_audit(x)>0. Zero-cost checks can be handled separately. This is a declared priority heuristic, not a probability of truth or a proved optimal scheduling rule.
Exact mathematical passage
P(x) = \frac{p_{\mathrm{err}}(x)\,c_{\mathrm{consequence}}(x) \bigl(1+r_{\mathrm{dependency}}(x)\bigr)} {c_{\mathrm{audit}}(x)}.
P_{K\cap L}Use in source · 1 passage
Search aliases: P_K∩ L cap
Use in source · Read passage · Proof_Path_Theory.tex, line 1335
[Retention projection algebra] For masks K,L⊆ V, P_K∘ P_L=P_K∩ L=P_L∘ P_K. Consequently every retention projection is idempotent, and the masks form a Boolean lattice with meet K∩ L and join K∪ L.
Exact mathematical passage
P_K\circ P_L=P_{K\cap L}=P_L\circ P_K.
P_LUse in source · 3 passages
Search aliases: P_L
Use in source · Read passage · Proof_Path_Theory.tex, line 1335
[Retention projection algebra] For masks K,L⊆ V, P_K∘ P_L=P_K∩ L=P_L∘ P_K. Consequently every retention projection is idempotent, and the masks form a Boolean lattice with meet K∩ L and join K∪ L.
Exact mathematical passage
P_K\circ P_L=P_{K\cap L}=P_L\circ P_K.
\Pcal_{0y}Use in source · 1 passage
Search aliases: Pcal_0y P_0y Pcal mathcal
Use in source · Read passage · Proof_Path_Theory.tex, line 1373
Let the archives be P_xy=(C_0,x,y) for (x,y)∈{0,1}^2, where C_0 is a fixed certificate retained by every allowed mask. Let q_x( P_xy)=x and q_y( P_xy)=y. Retaining x is sufficient for q_x. Any mask omitting x identifies P_0y with P_1y, so it is not sufficient for that task. Thus the least mask for {q_x} retains exactly C_0 and x. The same argument gives the least mask C_0 and y for {q_y}. Their joint task family requires both records. These masks are also the unique minima for unit cost per reta…
Exact mathematical passage
\Pcal_{0y}
\Pcal_{1y}Use in source · 1 passage
Search aliases: Pcal_1y P_1y Pcal mathcal
Use in source · Read passage · Proof_Path_Theory.tex, line 1373
Let the archives be P_xy=(C_0,x,y) for (x,y)∈{0,1}^2, where C_0 is a fixed certificate retained by every allowed mask. Let q_x( P_xy)=x and q_y( P_xy)=y. Retaining x is sufficient for q_x. Any mask omitting x identifies P_0y with P_1y, so it is not sufficient for that task. Thus the least mask for {q_x} retains exactly C_0 and x. The same argument gives the least mask C_0 and y for {q_y}. Their joint task family requires both records. These masks are also the unique minima for unit cost per reta…
Exact mathematical passage
\Pcal_{1y}
\Pcal_2Use in source · 3 passages
Search aliases: Pcal_2 P_2 Pcal mathcal
Use in source · Read passage · Proof_Path_Theory.tex, line 1276
[Task information loss criterion] Let C be a compression map and let q be a task. If there exist proof fields P_1 and P_2 such that C( P_1)=C( P_2) but q( P_1)≠ q( P_2), then the compressed representation is not sufficient for q.
Exact mathematical passage
\Pcal_2
\Pcal_{xy}Use in source · 3 passages
Search aliases: Pcal_xy P_xy Pcal mathcal
Use in source · Read passage · Proof_Path_Theory.tex, line 1373
Let the archives be P_xy=(C_0,x,y) for (x,y)∈{0,1}^2, where C_0 is a fixed certificate retained by every allowed mask. Let q_x( P_xy)=x and q_y( P_xy)=y. Retaining x is sufficient for q_x. Any mask omitting x identifies P_0y with P_1y, so it is not sufficient for that task. Thus the least mask for {q_x} retains exactly C_0 and x. The same argument gives the least mask C_0 and y for {q_y}. Their joint task family requires both records. These masks are also the unique minima for unit cost per reta…
Exact mathematical passage
\Pcal_{xy}=(C_0,x,y)
\mathrm{Prop}Use in source · 3 passages
Search aliases: Prop mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 700
For an intended interpretation μ:V→Prop, the transfer to mathematical truth has explicit hypotheses: every leaf must satisfy μ, and every certified rule must preserve μ from all its premises to its conclusion. Under those hypotheses, induction gives v∈Der_F⇒μ(v). Lean checks this statement as pathProofPath.Field.semantic_soundness. It does not infer those hypotheses from a JSON certification flag.
Exact mathematical passage
\mu:V\to\mathrm{Prop}
q^dUse in source · 1 passage
Search aliases: q^d
Use in source · Read passage · Proof_Path_Theory.tex, line 882
] In particular the exact count identity is | A|= |{y∈ A:Qy=Qx_0}| q^r. Every attained observation fiber has the same size. For the uniform distribution on A, the observation removes exactly rlog_2q bits of uncertainty. The two translation equivalences reduce the counts to finite vector spaces. Such a space of dimension d has q^d elements. Rank-nullity for Q_H gives dimker Q_H+r=k, proving the product identity and all the counts. An attained value can be treated by choosing a point attaining it …
Exact mathematical passage
q^d
q^kUse in source · 3 passages
Search aliases: q^k
Use in source · Read passage · Proof_Path_Theory.tex, line 869
[Exact observation counts] Suppose K is a finite field of cardinality q and E is a finite-dimensional K-vector space. Set k=dim_K H and r=dim_K Q(H). Then | A|=q^k, |Q( A)|=q^r, |{y∈ A:Qy=Qx_0}|=q^k-r. In particular the exact count identity is | A|= |{y∈ A:Qy=Qx_0}| q^r. Every attained observation fiber has the same size. For the uniform distribution on A, the observation removes exactly rlog_2q bits of uncertainty. The two translation equivalences reduce the counts to finite vector spaces. Such…
Exact mathematical passage
|\mathcal A|=q^k,\qquad |Q(\mathcal A)|=q^r,\qquad |\{y\in\mathcal A:Qy=Qx_0\}|=q^{k-r}.
q^{k-r}Use in source · 3 passages
Search aliases: q^k-r
Use in source · Read passage · Proof_Path_Theory.tex, line 869
[Exact observation counts] Suppose K is a finite field of cardinality q and E is a finite-dimensional K-vector space. Set k=dim_K H and r=dim_K Q(H). Then | A|=q^k, |Q( A)|=q^r, |{y∈ A:Qy=Qx_0}|=q^k-r. In particular the exact count identity is | A|= |{y∈ A:Qy=Qx_0}| q^r. Every attained observation fiber has the same size. For the uniform distribution on A, the observation removes exactly rlog_2q bits of uncertainty. The two translation equivalences reduce the counts to finite vector spaces. Such…
Exact mathematical passage
|\mathcal A|=q^k,\qquad |Q(\mathcal A)|=q^r,\qquad |\{y\in\mathcal A:Qy=Qx_0\}|=q^{k-r}.
q^rUse in source · 3 passages
Search aliases: q^r
Use in source · Read passage · Proof_Path_Theory.tex, line 869
[Exact observation counts] Suppose K is a finite field of cardinality q and E is a finite-dimensional K-vector space. Set k=dim_K H and r=dim_K Q(H). Then | A|=q^k, |Q( A)|=q^r, |{y∈ A:Qy=Qx_0}|=q^k-r. In particular the exact count identity is | A|= |{y∈ A:Qy=Qx_0}| q^r. Every attained observation fiber has the same size. For the uniform distribution on A, the observation removes exactly rlog_2q bits of uncertainty. The two translation equivalences reduce the counts to finite vector spaces. Such…
Exact mathematical passage
|\mathcal A|=q^k,\qquad |Q(\mathcal A)|=q^r,\qquad |\{y\in\mathcal A:Qy=Qx_0\}|=q^{k-r}.
Q_HUse in source · 4 passages
Search aliases: Q_H
Use in source · Read passage · Proof_Path_Theory.tex, line 858
Let T:E→ R and Q:E→ W be linear, and fix a known point x_0. Put A={y:Ty=Tx_0}, H=ker T, Q_H=Q|_H. Translation h↦ x_0+h identifies H with A. The observation image is the translate Qx_0+Q(H), and the fiber above the attained value Qx_0 is a translate of ker Q_H.
Exact mathematical passage
\mathcal A=\{y:Ty=Tx_0\},\quad H=\ker T,\quad Q_H=Q|_H.
q_xUse in source · 4 passages
Search aliases: q_x
Use in source · Read passage · Proof_Path_Theory.tex, line 1363
[htbp] centering includegraphics[width=linewidth]fig_05_recoverability_preorder.pdf captionA concrete retention diamond for the four archives (C_0,x,y) with x,y∈{0,1}. Arrows discard coordinates. The two middle schemes are incomparable for the task family {q_x,q_y}. This is not a universal ranking of teaching, discovery, and formal presentations.
Exact mathematical passage
\{q_x,q_y\}
q_yUse in source · 3 passages
Search aliases: q_y
Use in source · Read passage · Proof_Path_Theory.tex, line 1363
[htbp] centering includegraphics[width=linewidth]fig_05_recoverability_preorder.pdf captionA concrete retention diamond for the four archives (C_0,x,y) with x,y∈{0,1}. Arrows discard coordinates. The two middle schemes are incomparable for the task family {q_x,q_y}. This is not a universal ranking of teaching, discovery, and formal presentations.
Exact mathematical passage
\{q_x,q_y\}
\mathcal RUse in source · 3 passages
Search aliases: R mathcal
Use in source · Read passage · Proof_Path_Theory.tex, line 1397
[Attained factorization and unique decoding] For C:mathscr A→ R and q:mathscr A→ Y, the following are equivalent: · ∃ d:imC→ Y ∀ a∈mathscr A, q(a)=d(C(a)),
Exact mathematical passage
C:\mathscr A\to\mathcal R
r'Use in source · 3 passages
Search aliases: r'
Use in source · Read passage · Proof_Path_Theory.tex, line 1850
If s(r)=s(r'), applying the function h gives equal digests. If s(r)≠ s(r') but h(s(r))=h(s(r')), the two serialized strings form a hash collision by definition. Thus change detection at the record level requires both preservation of the audited distinction by s and exclusion of a collision for the resulting bytes. No injectivity of a fixed-length hash on arbitrary byte strings is asserted.
Exact mathematical passage
s(r)=s(r')
r_0Use in source · 1 passage
Search aliases: r_0
Use in source · Read passage · Proof_Path_Theory.tex, line 1179
Take V_4={0,1,2,3}, L={0}, S=∅, and the two rules r_0:0→1 and r_1:1→2. The least closure is {0,1,2}. Node 3 has no derivation from these inputs.
Exact mathematical passage
r_0:0\to1
r_1Use in source · 2 passages
Search aliases: r_1
Use in source · Read passage · Proof_Path_Theory.tex, line 1179
Take V_4={0,1,2,3}, L={0}, S=∅, and the two rules r_0:0→1 and r_1:1→2. The least closure is {0,1,2}. Node 3 has no derivation from these inputs.
Exact mathematical passage
r_1:1\to2
R_3Use in source · 2 passages
Search aliases: R_3
Use in source · Read passage · Proof_Path_Theory.tex, line 1304
Every representation supports every task it supports, so the relation is reflexive. If every task supported by R_1 is supported by R_2, and every task supported by R_2 is supported by R_3, then every task supported by R_1 is supported by R_3. Thus the relation is transitive.
Exact mathematical passage
R_3
R_{\mathrm{archive}}Use in source · 1 passage
Search aliases: R_archive mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
R_{\mathrm{cert}}Use in source · 1 passage
Search aliases: R_cert mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
R_dUse in source · 4 passages
Search aliases: R_d
Use in source · Read passage · Proof_Path_Theory.tex, line 2047
A refinement preserves the certified target on its declared scope. Preservation of other tasks requires a separate recovery condition. Let R_d:mathscr A→ R_d be the representation scheme at depth d. A sufficient condition is a map π_d:R_d+1(mathscr A)⟶ R_d(mathscr A) with R_d=π_d∘ R_d+1. If a task factors as q=d_q∘ R_d, then q=(d_q∘π_d)∘ R_d+1. Hence R_dpreceq_ QR_d+1. Repeated refinements satisfying this condition give the recoverability chain. For a restricted task family, preserving its suppo…
Exact mathematical passage
R_d:\mathscr A\to\mathcal R_d
\mathcal R_dUse in source · 1 passage
Search aliases: R_d mathcal
Use in source · Read passage · Proof_Path_Theory.tex, line 2047
A refinement preserves the certified target on its declared scope. Preservation of other tasks requires a separate recovery condition. Let R_d:mathscr A→ R_d be the representation scheme at depth d. A sufficient condition is a map π_d:R_d+1(mathscr A)⟶ R_d(mathscr A) with R_d=π_d∘ R_d+1. If a task factors as q=d_q∘ R_d, then q=(d_q∘π_d)∘ R_d+1. Hence R_dpreceq_ QR_d+1. Repeated refinements satisfying this condition give the recoverability chain. For a restricted task family, preserving its suppo…
Exact mathematical passage
R_d:\mathscr A\to\mathcal R_d
R_{d+1}Use in source · 3 passages
Search aliases: R_d+1
Use in source · Read passage · Proof_Path_Theory.tex, line 2048
A refinement preserves the certified target on its declared scope. Preservation of other tasks requires a separate recovery condition. Let R_d:mathscr A→ R_d be the representation scheme at depth d. A sufficient condition is a map π_d:R_d+1(mathscr A)⟶ R_d(mathscr A) with R_d=π_d∘ R_d+1. If a task factors as q=d_q∘ R_d, then q=(d_q∘π_d)∘ R_d+1. Hence R_dpreceq_ QR_d+1. Repeated refinements satisfying this condition give the recoverability chain. For a restricted task family, preserving its suppo…
Exact mathematical passage
\pi_d:R_{d+1}(\mathscr A)\longrightarrow R_d(\mathscr A) \qquad\text{with}\qquad R_d=\pi_d\circ R_{d+1}.
r_{d-1}Use in source · 1 passage
Search aliases: r_d-1
Use in source · Read passage · Proof_Path_Theory.tex, line 2085
A practical stopping rule selects the first depth satisfying r_d≤ε or fracr_d-1-r_dc_d-c_d-1<τ. The first condition uses a declared tolerance. The second applies only at d≥1 with c_d>c_d-1 and compares the most recent reduction with its extra cost. Zero-cost refinements require separate handling. These stopping rules do not generally minimize J_g over all remaining depths.
Exact mathematical passage
r_d\le\varepsilon\qquad\text{or}\qquad \frac{r_{d-1}-r_d}{c_d-c_{d-1}}<\tau.
r_{d_1}Use in source · 2 passages
Search aliases: r_d_1
Use in source · Read passage · Proof_Path_Theory.tex, line 2077
Take a proof object with exactly two available depths d_1<d_2, with r_d_2<r_d_1 and c_d_2>c_d_1. Direct subtraction shows that d_2 is preferred exactly when α_g(r_d_1-r_d_2)>β_g(c_d_2-c_d_1). The goal (α_g,β_g)=(1,0) strictly prefers d_2, whereas (0,1) strictly prefers d_1. Since these are the only available depths, each preference is a global optimum. If both weights vanish, every depth is optimal. No division by a possibly zero weight is needed.
Exact mathematical passage
r_{d_2}<r_{d_1}
r_{d_2}Use in source · 2 passages
Search aliases: r_d_2
Use in source · Read passage · Proof_Path_Theory.tex, line 2077
Take a proof object with exactly two available depths d_1<d_2, with r_d_2<r_d_1 and c_d_2>c_d_1. Direct subtraction shows that d_2 is preferred exactly when α_g(r_d_1-r_d_2)>β_g(c_d_2-c_d_1). The goal (α_g,β_g)=(1,0) strictly prefers d_2, whereas (0,1) strictly prefers d_1. Since these are the only available depths, each preference is a global optimum. If both weights vanish, every depth is optimal. No division by a possibly zero weight is needed.
Exact mathematical passage
r_{d_2}<r_{d_1}
r_{\mathrm{dependency}}Use in source · 1 passage
Search aliases: r_dependency mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 2026
A simple audit priority score is P(x) = fracp_err(x) c_consequence(x) (1+r_dependency(x)) c_audit(x). Here p_err(x)∈[0,1], the consequence and dependency factors are nonnegative, and c_audit(x)>0. Zero-cost checks can be handled separately. This is a declared priority heuristic, not a probability of truth or a proved optimal scheduling rule.
Exact mathematical passage
P(x) = \frac{p_{\mathrm{err}}(x)\,c_{\mathrm{consequence}}(x) \bigl(1+r_{\mathrm{dependency}}(x)\bigr)} {c_{\mathrm{audit}}(x)}.
R_{\mathrm{discovery}}Use in source · 1 passage
Search aliases: R_discovery mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
R_{\mathrm{formal}}Use in source · 1 passage
Search aliases: R_formal mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
R_iUse in source · 1 passage
Search aliases: R_i
Use in source · Read passage · Proof_Path_Theory.tex, line 1577
[Portfolio robustness] For representation schemes C_i:mathscr A→ R_i, retain the tagged portfolio C( P)=(C_i( P))_i. Every task recoverable from any one C_i is recoverable from C.
Exact mathematical passage
C_i:\mathscr A\to R_i
R_{\mathrm{journal}}Use in source · 1 passage
Search aliases: R_journal mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
R_MUse in source · 2 passages
Search aliases: R_M
Use in source · Read passage · Proof_Path_Theory.tex, line 1698
For each candidate x∈ C, let R_x⊆ F be the set of future targets reachable from M∪{x}. Let R_M be the targets already reachable from M. Reachability from a union of starting nodes is the union of their individual reach sets, so U_M(S)= ∑_f∈ R_M∪⋃_x∈ SR_xw_f. Adding a candidate cannot remove a reachable target, so U_M is monotone.
Exact mathematical passage
R_M
R_{\mathrm{teach}}Use in source · 1 passage
Search aliases: R_teach mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
R_xUse in source · 3 passages
Search aliases: R_x
Use in source · Read passage · Proof_Path_Theory.tex, line 1698
For each candidate x∈ C, let R_x⊆ F be the set of future targets reachable from M∪{x}. Let R_M be the targets already reachable from M. Reachability from a union of starting nodes is the union of their individual reach sets, so U_M(S)= ∑_f∈ R_M∪⋃_x∈ SR_xw_f. Adding a candidate cannot remove a reachable target, so U_M is monotone.
Exact mathematical passage
R_x\subseteq F
\operatorname{rank}Use in source · 6 passages
Search aliases: rank operatorname
Use in source · Read passage · Proof_Path_Theory.tex, line 621
[Finite realization alternative and ambiguity] Exactly one of the following holds: [label=textup(roman*)] item My=b has a solution y_0. Its complete solution set is y_0+H, where H=ker A∩ker P, and | K_P(x)|=2^n-rank(M). item A row vector λ exists with λ M=0 and λ b=1. It is a directly checkable certificate that K_P(x)=∅. If My_0=b, any other solution differs from y_0 by an element of ker M=H, and every such difference gives another solution. Rank nullity gives dim H=n-rank(M). If b is not in the…
Exact mathematical passage
|\mathfrak K_P(x)|=2^{n-\operatorname{rank}(M)}.
\RcalUse in source · 1 passage
Search aliases: Rcal R mathcal
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
S'Use in source · 2 passages
Search aliases: S'
Use in source · Read passage · Proof_Path_Theory.tex, line 982
[Staged closure and persistent obstructions] For positive sets S,T, cl_F(cl_F(S)∪ T) =cl_F(S∪ T). If S⊆ S' and N⊆ N', then Ext_F(S',N')⊆Ext_F(S,N). Consequently an infeasible request stays infeasible under those additions, while the field and the meaning of its rules remain fixed. Closure is extensive, monotone, and idempotent because it is the least model containing its seed. The model cl_F(S∪ T) contains cl_F(S) and T, giving one inclusion in the first equation. Extensivity gives S∪ T⊆cl_F(S)∪…
Exact mathematical passage
S\subseteq S'
S_1Use in source · 5 passages
Search aliases: S_1
Use in source · Read passage · Proof_Path_Theory.tex, line 498
For NP-hardness, reduce Set Cover. Let U={u_1,…,u_m} be the universe, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificat…
Exact mathematical passage
S_1,\ldots,S_n\subseteq U
S_3Use in source · 2 passages
Search aliases: S_3
Use in source · Read passage · Proof_Path_Theory.tex, line 512
[htbp] centering includegraphics[width=linewidth]fig_04_certificate_complexity.pdf captionThe Set Cover example as a membership matrix. Filled marks belong to the selected rows S_1 and S_3; open marks show unselected memberships. Every obligation is covered. The target requires all four obligations through one AND rule. The exact minimum is two, although the minimizing pair need not be unique.
Exact mathematical passage
S_3
S_iUse in source · 5 passages
Search aliases: S_i
Use in source · Read passage · Proof_Path_Theory.tex, line 498
For NP-hardness, reduce Set Cover. Let U={u_1,…,u_m} be the universe, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificat…
Exact mathematical passage
S_i
s_iUse in source · 6 passages
Search aliases: s_i
Use in source · Read passage · Proof_Path_Theory.tex, line 498
For NP-hardness, reduce Set Cover. Let U={u_1,…,u_m} be the universe, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificat…
Exact mathematical passage
s_i
S_jUse in source · 2 passages
Search aliases: S_j
Use in source · Read passage · Proof_Path_Theory.tex, line 670
Fix a node set V, a set L⊆ V of admissible leaves, and a set J of justifications. A justification j has a premise set A_j, a conclusion c_j, and a certification predicate. Define its support by S_j=A_j∪{c_j}. A set X⊆ V is a model of the declared field when L⊆ X and, for every certified j, A_j⊆ X Longrightarrow c_j∈ X. Each justification is one implication with conjunctive premises. Alternative justifications remain separate implications. Uncertified attempts and failed-route annotations do not …
Exact mathematical passage
S_j=A_j\cup\{c_j\}.
S_kUse in source · 2 passages
Search aliases: S_k
Use in source · Read passage · Proof_Path_Theory.tex, line 1717
[Greedy cardinality guarantee] Let k be an integer with 1≤ k≤|C|. Starting from the empty supplement, let S_k result from repeatedly adding an unselected candidate with largest marginal future reach. Let O_k be an optimal supplement of size at most k. Then U_M(S_k)-U_M(∅) ≥ (1-(1-frac1k)^k) (U_M(O_k)-U_M(∅)), and therefore the greedy gain is at least (1-1/e) times the optimal gain.
Exact mathematical passage
S_k
S_nUse in source · 1 passage
Search aliases: S_n
Use in source · Read passage · Proof_Path_Theory.tex, line 498
For NP-hardness, reduce Set Cover. Let U={u_1,…,u_m} be the universe, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificat…
Exact mathematical passage
S_1,\ldots,S_n\subseteq U
s_tUse in source · 3 passages
Search aliases: s_t
Use in source · Read passage · Proof_Path_Theory.tex, line 1998
Let a_t≥0 be candidate arrivals during audit cycle t, let s_t≥0 be service capacity, and let B_t≥0 be the unresolved backlog. Suppose arrivals in a cycle are available to that cycle's service. The basic deterministic queue is B_t+1=max{0,B_t+a_t-s_t}.
Exact mathematical passage
s_t\geq0
\mathrm{short}Use in source · 1 passage
Search aliases: short mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 2114
The field examples/alternative_proofs.json contains a short route and a richer explanatory route. The short route has storage cost 1, while the richer route has storage cost 3 and larger meaning and discovery values. Exact certificate search chooses A⟶ L_short⟶ B when the objective is storage cost alone. A teaching compiler may rationally choose the other route because it uses a different objective.
Exact mathematical passage
A\longrightarrow L_{\mathrm{short}}\longrightarrow B
\operatorname{some}Use in source · 1 passage
Search aliases: some operatorname
Use in source · Read passage · Proof_Path_Theory.tex, line 1226
[Lossless encoding at the typed syntax boundary] Let e_P,d_P and e_C,d_C be the stated Lean encoders and partial decoders for problem and certificate records. For every typed problem P and certificate C, d_P(e_P(P))=some(P), d_C(e_C(C))=some(C). Consequently both encoders are injective on their typed domains. These identities do not require the encoded record to pass the separate validity checks. The natural-number and Boolean constructors decode to their original values. Induction on a list pro…
Exact mathematical passage
d_P(e_P(P))=\operatorname{some}(P),\qquad d_C(e_C(C))=\operatorname{some}(C).
\mathrm{teach}Use in source · 1 passage
Search aliases: teach mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1563
The same theorem can support several legitimate representations: R(B)= {R_cert,R_journal,R_teach, R_formal,R_discovery,R_archive}. The certificate is optimized for checking. The journal form balances rigor and readable length. The teaching form expands conceptual bottlenecks. The formal form exposes primitive dependencies. The discovery form retains alternatives and failed routes. The archive preserves reconstruction information.
Exact mathematical passage
\Rcal(B)= \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}}, R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
\topUse in source · 8 passages
Search aliases: top
Use in source · Read passage · Proof_Path_Theory.tex, line 1916
For a general positive definite covariance matrix Σ, consider unbiased linear aggregates w^top X with 1^top w=1.
Exact mathematical passage
w^\top X
\mathrm{true}Use in source · 1 passage
Search aliases: true mathrm
Use in source · Read passage · Proof_Path_Theory.tex, line 1195
erdict The complete result format contains a Boolean feasibility flag, a reported closure, a strict closure trace, and an optional forbidden-node witness. Both branches require the complete-closure check. A positive result additionally requires no obstruction witness and no forbidden node in the closure. A negative result requires an accepted obstruction witness. For every accepted result C, C.K=cl_F(S), (C.feasible=true) Longleftrightarrow Ext_F(S,N)≠∅. The complete-closure check proves the fir…
Exact mathematical passage
C.K=\operatorname{cl}_F(S),\qquad \bigl(C.\mathrm{feasible}=\mathrm{true}\bigr) \Longleftrightarrow \operatorname{Ext}_F(S,N)\ne\varnothing.
U_0Use in source · 3 passages
Search aliases: U_0
Use in source · Read passage · Proof_Path_Theory.tex, line 783
[Pairwise dependencies do not suffice] Take nodes a,b,c, no admissible leaves (L=∅), and one certified rule {a,b}⟶ c. Use patches U_0={a,c} and U_1={b,c}. The local valuations X_0={a} and X_1={b} agree on their overlap: both assign false to c. Both are local models, since neither patch contains the full rule support. They cover every node and both pairwise premise-to-conclusion dependencies. Nevertheless, a global model realizing them would contain a,b and omit c, contradicting the rule. Thus re…
Exact mathematical passage
U_0=\{a,c\}
U_1Use in source · 3 passages
Search aliases: U_1
Use in source · Read passage · Proof_Path_Theory.tex, line 783
[Pairwise dependencies do not suffice] Take nodes a,b,c, no admissible leaves (L=∅), and one certified rule {a,b}⟶ c. Use patches U_0={a,c} and U_1={b,c}. The local valuations X_0={a} and X_1={b} agree on their overlap: both assign false to c. Both are local models, since neither patch contains the full rule support. They cover every node and both pairwise premise-to-conclusion dependencies. Nevertheless, a global model realizing them would contain a,b and omit c, contradicting the rule. Thus re…
Exact mathematical passage
U_1=\{b,c\}
u_1Use in source · 1 passage
Search aliases: u_1
Use in source · Read passage · Proof_Path_Theory.tex, line 498
For NP-hardness, reduce Set Cover. Let U={u_1,…,u_m} be the universe, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificat…
Exact mathematical passage
U=\{u_1,\ldots,u_m\}
U_{\Bcal\setminus\{v\}}Use in source · 1 passage
Search aliases: U_Bcal∖{v} U_ B∖{v} Bcal setminus mathcal setminus
Use in source · Read passage · Proof_Path_Theory.tex, line 1663
[Weighted criticality] For v∉ S, the utility lost by deleting v is the total weight of initially reachable future targets dominated by v: U(S)-U_ B∖{v}(S) =∑_substackf∈ F∩Reach_ B(S) v dominates fw_f. Deleted target vertices are counted as unreachable.
Exact mathematical passage
U(S)-U_{\Bcal\setminus\{v\}}(S) =\sum_{\substack{f\in F\cap\Reach_{\Bcal}(S)\\v\text{ dominates }f}}w_f.
U_iUse in source · 12 passages
Search aliases: U_i
Use in source · Read passage · Proof_Path_Theory.tex, line 593
[Finite arrow-cover gluing] Suppose patches U_i⊆ V cover every view and every declared edge has both endpoints in some U_i. Let s_i be coherent assignments on U_i that agree on all overlaps. There is a unique global coherent assignment s∈Γ(F) restricting to every s_i. For each view v, choose any patch containing it and define s(v) to be the value supplied by that patch. Agreement on overlaps makes this independent of the choice. For a declared edge e:v→ w, choose a patch containing both endpoint…
Exact mathematical passage
U_i\subseteq V
U_jUse in source · 1 passage
Search aliases: U_j
Use in source · Read passage · Proof_Path_Theory.tex, line 759
Let (U_i)_i∈ I cover the nodes. A family X_i∈ M_F(U_i) is matching when X_i∩ U_j=X_j∩ U_i for every i,j. This equality includes agreement about false values, not merely common true values.
Exact mathematical passage
X_i\cap U_j=X_j\cap U_i\qquad\text{for every }i,j.
u_jUse in source · 3 passages
Search aliases: u_j
Use in source · Read passage · Proof_Path_Theory.tex, line 498
For NP-hardness, reduce Set Cover. Let U={u_1,…,u_m} be the universe, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificat…
Exact mathematical passage
u_j
u_mUse in source · 1 passage
Search aliases: u_m
Use in source · Read passage · Proof_Path_Theory.tex, line 498
For NP-hardness, reduce Set Cover. Let U={u_1,…,u_m} be the universe, let S_1,…,S_n⊆ U be the available sets, and let k be the cover budget. Construct one optional admissible leaf node s_i for each set S_i, with unit cost. Construct one zero-cost obligation node e_j for each element u_j. Whenever u_j∈ S_i, add a certified justification {s_i}Longrightarrow e_j. Add a zero-cost target node t with the certified justification {e_1,…,e_m}Longrightarrow t. The dependency graph is acyclic. A certificat…
Exact mathematical passage
U=\{u_1,\ldots,u_m\}
V_4Use in source · 1 passage
Search aliases: V_4
Use in source · Read passage · Proof_Path_Theory.tex, line 1179
Take V_4={0,1,2,3}, L={0}, S=∅, and the two rules r_0:0→1 and r_1:1→2. The least closure is {0,1,2}. Node 3 has no derivation from these inputs.
Exact mathematical passage
V_4=\{0,1,2,3\}
V_FUse in source · 1 passage
Search aliases: V_F
Use in source · Read passage · Proof_Path_Theory.tex, line 1058
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G,
Exact mathematical passage
f:V_F\to V_G
V_GUse in source · 1 passage
Search aliases: V_G
Use in source · Read passage · Proof_Path_Theory.tex, line 1058
A change of proof-field representation needs more than a map of node names. Let F and G be declared fields. A rule transport consists of a node map f:V_F→ V_G and a rule map h:J_F→ J_G satisfying f(L_F) · ⊆ L_G,
Exact mathematical passage
f:V_F\to V_G
\operatorname{Var}Use in source · 4 passages
Search aliases: Var operatorname
Use in source · Read passage · Proof_Path_Theory.tex, line 1874
Let X_i=θ+ε_i be numerical estimates of a fixed quantity θ. Assume Eε_i=0, Var(ε_i)=σ^2>0, and common pairwise correlation ρ. For n>1, assume -1/(n-1)<ρ≤1, so the mean has positive variance. These variables model estimates, not proof truth values. The mean has variance Var(bar X) = σ^2(frac1-ρn+ρ).
Exact mathematical passage
\operatorname{Var}(\varepsilon_i)=\sigma^2>0
\vdashUse in source · 2 passages
Search aliases: vdash
Use in source · Read passage · Proof_Path_Theory.tex, line 235
also remove mathematical information that is not needed for the present theorem. An example may explain why a definition was chosen. A failed route may isolate the exact boundary of a method. An alternative proof may carry a bridge to another field. A computation may reveal a stronger statement than the one originally sought. None of these objects is automatically part of the final implication Avdash B. They may still be part of the mathematical event that produced it.
Exact mathematical passage
A\vdash B.
w^*Use in source · 1 passage
Search aliases: w^*
Use in source · Read passage · Proof_Path_Theory.tex, line 1921
[Minimum-variance covariance-aware weights] The unique minimum-variance unbiased linear aggregate has weights w^* = fracΣ^-1 1 1^topΣ^-1 1. Its variance is frac1 1^topΣ^-1 1.
Exact mathematical passage
w^* = \frac{\Sigma^{-1}\mathbf 1} {\mathbf 1^\top\Sigma^{-1}\mathbf 1}.
w^\topUse in source · 3 passages
Search aliases: w^top top
Use in source · Read passage · Proof_Path_Theory.tex, line 1916
For a general positive definite covariance matrix Σ, consider unbiased linear aggregates w^top X with 1^top w=1.
Exact mathematical passage
w^\top X
X_0Use in source · 2 passages
Search aliases: X_0
Use in source · Read passage · Proof_Path_Theory.tex, line 783
[Pairwise dependencies do not suffice] Take nodes a,b,c, no admissible leaves (L=∅), and one certified rule {a,b}⟶ c. Use patches U_0={a,c} and U_1={b,c}. The local valuations X_0={a} and X_1={b} agree on their overlap: both assign false to c. Both are local models, since neither patch contains the full rule support. They cover every node and both pairwise premise-to-conclusion dependencies. Nevertheless, a global model realizing them would contain a,b and omit c, contradicting the rule. Thus re…
Exact mathematical passage
X_0=\{a\}
x_0Use in source · 7 passages
Search aliases: x_0
Use in source · Read passage · Proof_Path_Theory.tex, line 857
Let T:E→ R and Q:E→ W be linear, and fix a known point x_0. Put A={y:Ty=Tx_0}, H=ker T, Q_H=Q|_H. Translation h↦ x_0+h identifies H with A. The observation image is the translate Qx_0+Q(H), and the fiber above the attained value Qx_0 is a translate of ker Q_H.
Exact mathematical passage
x_0
X_1Use in source · 2 passages
Search aliases: X_1
Use in source · Read passage · Proof_Path_Theory.tex, line 783
[Pairwise dependencies do not suffice] Take nodes a,b,c, no admissible leaves (L=∅), and one certified rule {a,b}⟶ c. Use patches U_0={a,c} and U_1={b,c}. The local valuations X_0={a} and X_1={b} agree on their overlap: both assign false to c. Both are local models, since neither patch contains the full rule support. They cover every node and both pairwise premise-to-conclusion dependencies. Nevertheless, a global model realizing them would contain a,b and omit c, contradicting the rule. Thus re…
Exact mathematical passage
X_1=\{b\}
X_iUse in source · 7 passages
Search aliases: X_i
Use in source · Read passage · Proof_Path_Theory.tex, line 758
Let (U_i)_i∈ I cover the nodes. A family X_i∈ M_F(U_i) is matching when X_i∩ U_j=X_j∩ U_i for every i,j. This equality includes agreement about false values, not merely common true values.
Exact mathematical passage
X_i\in\mathcal M_F(U_i)
X_jUse in source · 1 passage
Search aliases: X_j
Use in source · Read passage · Proof_Path_Theory.tex, line 759
Let (U_i)_i∈ I cover the nodes. A family X_i∈ M_F(U_i) is matching when X_i∩ U_j=X_j∩ U_i for every i,j. This equality includes agreement about false values, not merely common true values.
Exact mathematical passage
X_i\cap U_j=X_j\cap U_i\qquad\text{for every }i,j.
X_UUse in source · 2 passages
Search aliases: X_U
Use in source · Read passage · Proof_Path_Theory.tex, line 704
For a patch U⊆ V, let M_F(U) consist of subsets X_U⊆ U which contain L∩ U and obey every certified rule whose entire support lies in U. If U⊆ W, define ρ_U,W: M_F(W)⟶ M_F(U), ρ_U,W(X_W)=X_W∩ U. This map is well defined. A rule supported in U is also supported in W, and its conclusion remains in U. The restriction therefore preserves both the local leaves and the local implication conditions.
Exact mathematical passage
X_U\subseteq U
X_WUse in source · 2 passages
Search aliases: X_W
Use in source · Read passage · Proof_Path_Theory.tex, line 705
For a patch U⊆ V, let M_F(U) consist of subsets X_U⊆ U which contain L∩ U and obey every certified rule whose entire support lies in U. If U⊆ W, define ρ_U,W: M_F(W)⟶ M_F(U), ρ_U,W(X_W)=X_W∩ U. This map is well defined. A rule supported in U is also supported in W, and its conclusion remains in U. The restriction therefore preserves both the local leaves and the local implication conditions.
Exact mathematical passage
\rho_{U,W}:\mathcal M_F(W)\longrightarrow\mathcal M_F(U), \qquad \rho_{U,W}(X_W)=X_W\cap U.
\xrightarrowUse in source · 2 passages
Search aliases: xrightarrow
Use in source · Read passage · Proof_Path_Theory.tex, line 537
[Functorial transport] Let F:Cert_1→Cert_2 be a functor. If Axrightarrowf_1S_1xrightarrowf_2⋯xrightarrowf_rB is a certified path in Cert_1, then F(A)xrightarrowF(f_1)F(S_1)xrightarrowF(f_2)⋯xrightarrowF(f_r)F(B) is a certified path in Cert_2.
Exact mathematical passage
A\xrightarrow{f_1}S_1\xrightarrow{f_2}\cdots\xrightarrow{f_r}B
y_0Use in source · 8 passages
Search aliases: y_0
Use in source · Read passage · Proof_Path_Theory.tex, line 620
[Finite realization alternative and ambiguity] Exactly one of the following holds: [label=textup(roman*)] item My=b has a solution y_0. Its complete solution set is y_0+H, where H=ker A∩ker P, and | K_P(x)|=2^n-rank(M). item A row vector λ exists with λ M=0 and λ b=1. It is a directly checkable certificate that K_P(x)=∅. If My_0=b, any other solution differs from y_0 by an element of ker M=H, and every such difference gives another solution. Rank nullity gives dim H=n-rank(M). If b is not in the…
Exact mathematical passage
y_0
Y_iUse in source · 4 passages
Search aliases: Y_i
Use in source · Read passage · Proof_Path_Theory.tex, line 1423
Suppose tasks q_i:mathscr A→ Y_i are indexed by i∈ I. Their joint representation is Q(a)=(q_i(a))_i∈ I. It records every distinction asked for by the task family and makes no demand to recover the entire source archive.
Exact mathematical passage
q_i:\mathscr A\to Y_i
ZUse in source · 1 passage
Search aliases: Z
Use in source · Read passage · Proof_Path_Theory.tex, line 714
[The proof-field view laws] The restriction maps satisfy ρ_U,U=id, ρ_U,Wρ_W,Z=ρ_U,Z (U⊆ W⊆ Z). Consequently U↦ M_F(U) is a contravariant set-valued view system on the inclusion order of patches. Both laws are the corresponding intersection identities. For the second, (X∩ W)∩ U=X∩ U because U⊆ W. The values outside a patch are absent, or equivalently normalized to false in the Lean representation. There are no additional hidden coordinates.
Exact mathematical passage
\rho_{U,U}=\mathrm{id},\qquad \rho_{U,W}\rho_{W,Z}=\rho_{U,Z}\quad(U\subseteq W\subseteq Z).
zUse in source · 1 passage
Search aliases: z
Use in source · Read passage · Proof_Path_Theory.tex, line 1384
es:7:11 Let C:A→ B. Every predicate q:A→Prop factors through C if and only if C is injective. If C is injective, define the decoder of q at b by the predicate ∃ a (C(a)=b and q(a)). At b=C(a_0), injectivity makes this equivalent to q(a_0). Conversely, if C(a)=C(a'), use the predicate q(z)≡(z=a). Its decoded values at the equal encodings must agree, giving a'=a. This is the general collision criterion specialized to all predicates.
Exact mathematical passage
q(z)\equiv(z=a)
|Use in source · 14 passages
Search aliases: |
Use in source · Read passage · Proof_Path_Theory.tex, line 461
[Linear extraction] With indexed certified adjacency and constant-time membership bookkeeping, the core can be extracted in time linear in |A| plus the number of visited nodes, selected justifications, and premise incidences.
Exact mathematical passage
|A|
|_HUse in source · 5 passages
Search aliases: |_H
Use in source · Read passage · Proof_Path_Theory.tex, line 640
[Exact observation gain] Give the nonempty finite affine fiber y_0+H the uniform distribution. Then the Shannon entropy of the observed value Qy is H(Qy)=rank(Q|_H) bits. For every observation value that actually occurs, the corresponding conditional fiber contains 2^dim H-rank(Q|_H) realizations. Thus the uncertainty reduction is exactly rank(Q|_H) bits. The image Q(H) is a vector subspace of dimension r=rank(Q|_H), so the observed values form the affine set Qy_0+Q(H) of size 2^r. Every such va…
Exact mathematical passage
H(Qy)=\operatorname{rank}(Q|_H)\quad\text{bits}.
\varepsilonUse in source · 8 passages
Search aliases: ε varepsilon
Use in source · Read passage · Proof_Path_Theory.tex, line 1874
Let X_i=θ+ε_i be numerical estimates of a fixed quantity θ. Assume Eε_i=0, Var(ε_i)=σ^2>0, and common pairwise correlation ρ. For n>1, assume -1/(n-1)<ρ≤1, so the mean has positive variance. These variables model estimates, not proof truth values. The mean has variance Var(bar X) = σ^2(frac1-ρn+ρ).
Exact mathematical passage
X_i=\theta+\varepsilon_i
\varepsilon_iUse in source · 7 passages
Search aliases: ε_i varepsilon
Use in source · Read passage · Proof_Path_Theory.tex, line 1874
Let X_i=θ+ε_i be numerical estimates of a fixed quantity θ. Assume Eε_i=0, Var(ε_i)=σ^2>0, and common pairwise correlation ρ. For n>1, assume -1/(n-1)<ρ≤1, so the mean has positive variance. These variables model estimates, not proof truth values. The mean has variance Var(bar X) = σ^2(frac1-ρn+ρ).
Exact mathematical passage
X_i=\theta+\varepsilon_i
\varepsilon_jUse in source · 1 passage
Search aliases: ε_j varepsilon
Use in source · Read passage · Proof_Path_Theory.tex, line 1965
[MSE with a shared interpretive offset] Suppose reviewers report J_i=θ+b+ε_i, where θ is the target quantity, b is a fixed shared offset, Eε_i=0, Var(ε_i)=σ^2, and Cov(ε_i,ε_j)=ρσ^2 for i≠ j. For admissible ρ, the mean squared error of the reviewer average is E(overline J_n-θ)^2=b^2+σ^2(ρ+frac1-ρn). For fixed ρ≥0, it approaches b^2+ρσ^2 as n→∞. The estimation error is overline J_n-θ=b+overlineε_n. Its mean is b, and its variance is σ^2((1-ρ)/n+ρ) by summing all diagonal and off-diagonal covarian…
Exact mathematical passage
\operatorname{Cov}(\varepsilon_i,\varepsilon_j)=\rho\sigma^2
\thetaUse in source · 6 passages
Search aliases: θ theta
Use in source · Read passage · Proof_Path_Theory.tex, line 1874
Let X_i=θ+ε_i be numerical estimates of a fixed quantity θ. Assume Eε_i=0, Var(ε_i)=σ^2>0, and common pairwise correlation ρ. For n>1, assume -1/(n-1)<ρ≤1, so the mean has positive variance. These variables model estimates, not proof truth values. The mean has variance Var(bar X) = σ^2(frac1-ρn+ρ).
Exact mathematical passage
X_i=\theta+\varepsilon_i
\lambdaUse in source · 18 passages
Search aliases: λ lambda
Use in source · Read passage · Proof_Path_Theory.tex, line 624
[Finite realization alternative and ambiguity] Exactly one of the following holds: [label=textup(roman*)] item My=b has a solution y_0. Its complete solution set is y_0+H, where H=ker A∩ker P, and | K_P(x)|=2^n-rank(M). item A row vector λ exists with λ M=0 and λ b=1. It is a directly checkable certificate that K_P(x)=∅. If My_0=b, any other solution differs from y_0 by an element of ker M=H, and every such difference gives another solution. Rank nullity gives dim H=n-rank(M). If b is not in the…
Exact mathematical passage
\lambda
\muUse in source · 14 passages
Search aliases: μ mu
Use in source · Read passage · Proof_Path_Theory.tex, line 700
For an intended interpretation μ:V→Prop, the transfer to mathematical truth has explicit hypotheses: every leaf must satisfy μ, and every certified rule must preserve μ from all its premises to its conclusion. Under those hypotheses, induction gives v∈Der_F⇒μ(v). Lean checks this statement as pathProofPath.Field.semantic_soundness. It does not infer those hypotheses from a JSON certification flag.
Exact mathematical passage
\mu:V\to\mathrm{Prop}
\piUse in source · 4 passages
Search aliases: π pi
Use in source · Read passage · Proof_Path_Theory.tex, line 1438
For the second assertion, write R=π∘ C and q=d∘ R on their attained sets. Then q=(d∘π)∘ C. The identity decoder proves reflexivity, and composition of two recovery maps proves transitivity. All maps are applied only to outputs in their declared domains.
Exact mathematical passage
R=\pi\circ C
\pi_dUse in source · 2 passages
Search aliases: π_d pi
Use in source · Read passage · Proof_Path_Theory.tex, line 2048
A refinement preserves the certified target on its declared scope. Preservation of other tasks requires a separate recovery condition. Let R_d:mathscr A→ R_d be the representation scheme at depth d. A sufficient condition is a map π_d:R_d+1(mathscr A)⟶ R_d(mathscr A) with R_d=π_d∘ R_d+1. If a task factors as q=d_q∘ R_d, then q=(d_q∘π_d)∘ R_d+1. Hence R_dpreceq_ QR_d+1. Repeated refinements satisfying this condition give the recoverability chain. For a restricted task family, preserving its suppo…
Exact mathematical passage
\pi_d:R_{d+1}(\mathscr A)\longrightarrow R_d(\mathscr A) \qquad\text{with}\qquad R_d=\pi_d\circ R_{d+1}.
\rhoUse in source · 20 passages
Search aliases: ρ rho
Use in source · Read passage · Proof_Path_Theory.tex, line 705
For a patch U⊆ V, let M_F(U) consist of subsets X_U⊆ U which contain L∩ U and obey every certified rule whose entire support lies in U. If U⊆ W, define ρ_U,W: M_F(W)⟶ M_F(U), ρ_U,W(X_W)=X_W∩ U. This map is well defined. A rule supported in U is also supported in W, and its conclusion remains in U. The restriction therefore preserves both the local leaves and the local implication conditions.
Exact mathematical passage
\rho_{U,W}:\mathcal M_F(W)\longrightarrow\mathcal M_F(U), \qquad \rho_{U,W}(X_W)=X_W\cap U.
\rho_{U,U}Use in source · 1 passage
Search aliases: ρ_U,U rho
Use in source · Read passage · Proof_Path_Theory.tex, line 714
[The proof-field view laws] The restriction maps satisfy ρ_U,U=id, ρ_U,Wρ_W,Z=ρ_U,Z (U⊆ W⊆ Z). Consequently U↦ M_F(U) is a contravariant set-valued view system on the inclusion order of patches. Both laws are the corresponding intersection identities. For the second, (X∩ W)∩ U=X∩ U because U⊆ W. The values outside a patch are absent, or equivalently normalized to false in the Lean representation. There are no additional hidden coordinates.
Exact mathematical passage
\rho_{U,U}=\mathrm{id},\qquad \rho_{U,W}\rho_{W,Z}=\rho_{U,Z}\quad(U\subseteq W\subseteq Z).
\rho_{U,W}Use in source · 4 passages
Search aliases: ρ_U,W rho
Use in source · Read passage · Proof_Path_Theory.tex, line 705
For a patch U⊆ V, let M_F(U) consist of subsets X_U⊆ U which contain L∩ U and obey every certified rule whose entire support lies in U. If U⊆ W, define ρ_U,W: M_F(W)⟶ M_F(U), ρ_U,W(X_W)=X_W∩ U. This map is well defined. A rule supported in U is also supported in W, and its conclusion remains in U. The restriction therefore preserves both the local leaves and the local implication conditions.
Exact mathematical passage
\rho_{U,W}:\mathcal M_F(W)\longrightarrow\mathcal M_F(U), \qquad \rho_{U,W}(X_W)=X_W\cap U.
\rho_{U,Z}Use in source · 1 passage
Search aliases: ρ_U,Z rho
Use in source · Read passage · Proof_Path_Theory.tex, line 714
[The proof-field view laws] The restriction maps satisfy ρ_U,U=id, ρ_U,Wρ_W,Z=ρ_U,Z (U⊆ W⊆ Z). Consequently U↦ M_F(U) is a contravariant set-valued view system on the inclusion order of patches. Both laws are the corresponding intersection identities. For the second, (X∩ W)∩ U=X∩ U because U⊆ W. The values outside a patch are absent, or equivalently normalized to false in the Lean representation. There are no additional hidden coordinates.
Exact mathematical passage
\rho_{U,U}=\mathrm{id},\qquad \rho_{U,W}\rho_{W,Z}=\rho_{U,Z}\quad(U\subseteq W\subseteq Z).
\rho_{W,Z}Use in source · 1 passage
Search aliases: ρ_W,Z rho
Use in source · Read passage · Proof_Path_Theory.tex, line 714
[The proof-field view laws] The restriction maps satisfy ρ_U,U=id, ρ_U,Wρ_W,Z=ρ_U,Z (U⊆ W⊆ Z). Consequently U↦ M_F(U) is a contravariant set-valued view system on the inclusion order of patches. Both laws are the corresponding intersection identities. For the second, (X∩ W)∩ U=X∩ U because U⊆ W. The values outside a patch are absent, or equivalently normalized to false in the Lean representation. There are no additional hidden coordinates.
Exact mathematical passage
\rho_{U,U}=\mathrm{id},\qquad \rho_{U,W}\rho_{W,Z}=\rho_{U,Z}\quad(U\subseteq W\subseteq Z).
\SigmaUse in source · 8 passages
Search aliases: Σ Sigma
Use in source · Read passage · Proof_Path_Theory.tex, line 1916
For a general positive definite covariance matrix Σ, consider unbiased linear aggregates w^top X with 1^top w=1.
Exact mathematical passage
\Sigma
\Sigma^{-1}Use in source · 4 passages
Search aliases: Σ^-1 Sigma
Use in source · Read passage · Proof_Path_Theory.tex, line 1921
[Minimum-variance covariance-aware weights] The unique minimum-variance unbiased linear aggregate has weights w^* = fracΣ^-1 1 1^topΣ^-1 1. Its variance is frac1 1^topΣ^-1 1.
Exact mathematical passage
w^* = \frac{\Sigma^{-1}\mathbf 1} {\mathbf 1^\top\Sigma^{-1}\mathbf 1}.
\sigma^2Use in source · 11 passages
Search aliases: σ^2 sigma
Use in source · Read passage · Proof_Path_Theory.tex, line 1874
Let X_i=θ+ε_i be numerical estimates of a fixed quantity θ. Assume Eε_i=0, Var(ε_i)=σ^2>0, and common pairwise correlation ρ. For n>1, assume -1/(n-1)<ρ≤1, so the mean has positive variance. These variables model estimates, not proof truth values. The mean has variance Var(bar X) = σ^2(frac1-ρn+ρ).
Exact mathematical passage
\operatorname{Var}(\varepsilon_i)=\sigma^2>0
\ellUse in source · 6 passages
Search aliases: ℓ ell
Use in source · Read passage · Proof_Path_Theory.tex, line 824
[A linear certificate alternative] The protected problem is infeasible if and only if there is a linear functional λ:R→ K satisfying λ(Dh)=0 whenever p(h)=0, λ(Dx)=1. For a finite matrix M and right side b, the corresponding alternative is nexists y (My=b) Longleftrightarrow ∃ℓ (ℓ M=0 and ℓ b=1). If Dx∉ B, linear separation of a vector from a subspace gives a functional vanishing on B and nonzero at Dx. One construction extends a basis of B by Dx and then to a basis of R. Assign value zero to th…
Exact mathematical passage
\nexists y\ (My=b) \quad\Longleftrightarrow\quad \exists\ell\ (\ell M=0\ \text{and}\ \ell b=1).
\mapstoUse in source · 2 passages
Search aliases: ↦ mapsto
Use in source · Read passage · Proof_Path_Theory.tex, line 718
[The proof-field view laws] The restriction maps satisfy ρ_U,U=id, ρ_U,Wρ_W,Z=ρ_U,Z (U⊆ W⊆ Z). Consequently U↦ M_F(U) is a contravariant set-valued view system on the inclusion order of patches. Both laws are the corresponding intersection identities. For the second, (X∩ W)∩ U=X∩ U because U⊆ W. The values outside a patch are absent, or equivalently normalized to false in the Lean representation. There are no additional hidden coordinates.
Exact mathematical passage
U\mapsto\mathcal M_F(U)
\RightarrowUse in source · 1 passage
Search aliases: ⇒ Rightarrow
Use in source · Read passage · Proof_Path_Theory.tex, line 700
For an intended interpretation μ:V→Prop, the transfer to mathematical truth has explicit hypotheses: every leaf must satisfy μ, and every certified rule must preserve μ from all its premises to its conclusion. Under those hypotheses, induction gives v∈Der_F⇒μ(v). Lean checks this statement as pathProofPath.Field.semantic_soundness. It does not infer those hypotheses from a JSON certification flag.
Exact mathematical passage
v\in\operatorname{Der}_F\Rightarrow\mu(v)
\forallUse in source · 3 passages
Search aliases: ∀ forall
Use in source · Read passage · Proof_Path_Theory.tex, line 768
[Whole-support gluing] Suppose every certified justification has its whole support in some patch: ∀ j certified, ∃ i S_j⊆ U_i. Then every matching family (X_i) has a unique global field model X satisfying X∩ U_i=X_i for all i. Set X=⋃_iX_i. Matching and node coverage imply X∩ U_i=X_i. A leaf belongs to some patch and hence to its local model, so L⊆ X. Consider a certified rule whose premises belong to X. Choose a patch containing its entire support. Matching implies that every premise is true in…
Exact mathematical passage
\forall j\text{ certified},\quad\exists i\quad S_j\subseteq U_i.
\existsUse in source · 4 passages
Search aliases: ∃ exists
Use in source · Read passage · Proof_Path_Theory.tex, line 768
[Whole-support gluing] Suppose every certified justification has its whole support in some patch: ∀ j certified, ∃ i S_j⊆ U_i. Then every matching family (X_i) has a unique global field model X satisfying X∩ U_i=X_i for all i. Set X=⋃_iX_i. Matching and node coverage imply X∩ U_i=X_i. A leaf belongs to some patch and hence to its local model, so L⊆ X. Consider a certified rule whose premises belong to X. Choose a patch containing its entire support. Matching implies that every premise is true in…
Exact mathematical passage
\forall j\text{ certified},\quad\exists i\quad S_j\subseteq U_i.
\varnothingUse in source · 17 passages
Search aliases: ∅ varnothing
Use in source · Read passage · Proof_Path_Theory.tex, line 624
ernative and ambiguity] Exactly one of the following holds: [label=textup(roman*)] item My=b has a solution y_0. Its complete solution set is y_0+H, where H=ker A∩ker P, and | K_P(x)|=2^n-rank(M). item A row vector λ exists with λ M=0 and λ b=1. It is a directly checkable certificate that K_P(x)=∅. If My_0=b, any other solution differs from y_0 by an element of ker M=H, and every such difference gives another solution. Rank nullity gives dim H=n-rank(M). If b is not in the column space of M, lin…
Exact mathematical passage
\mathfrak K_P(x)=\varnothing
\sum_{f\in R_M\cup\bigcup_{x\in S}R_x}Use in source · 1 passage
Search aliases: ∑_f∈ R_M∪⋃_x∈ SR_x sum in cup bigcup in
Use in source · Read passage · Proof_Path_Theory.tex, line 1699
For each candidate x∈ C, let R_x⊆ F be the set of future targets reachable from M∪{x}. Let R_M be the targets already reachable from M. Reachability from a union of starting nodes is the union of their individual reach sets, so U_M(S)= ∑_f∈ R_M∪⋃_x∈ SR_xw_f. Adding a candidate cannot remove a reachable target, so U_M is monotone.
Exact mathematical passage
U_M(S)= \sum_{f\in R_M\cup\bigcup_{x\in S}R_x}w_f.
\sum_iUse in source · 1 passage
Search aliases: ∑_i sum
Use in source · Read passage · Proof_Path_Theory.tex, line 1979
luations of reviewer i under two labels. In a finite set of N reviewers, assign exactly n_1 to the first label and n_0=N-n_1 to the second, uniformly over assignments with those sizes, where n_0,n_1>0. Assume each observed response equals the potential response under its assigned label and does not depend on other assignments. Then the difference of the two sample means is unbiased for N^-1∑_i(Y_i(1)-Y_i(0)). Indeed, each reviewer has inclusion probability n_1/N in the first mean and n_0/N in th…
Exact mathematical passage
N^{-1}\sum_i(Y_i(1)-Y_i(0))
\sum_{\substack{f\in F\cap\Reach_{\Bcal}(S)\\v\text{ dominates }f}}Use in source · 1 passage
Search aliases: ∑_substackf∈ F∩Reach_Bcal(S) v dominates f ∑_substackf∈ F∩Reach_ B(S) v dominates f sum substack in cap Reach Bcal v text sum substack in cap operatorname mathcal v text
Use in source · Read passage · Proof_Path_Theory.tex, line 1663
[Weighted criticality] For v∉ S, the utility lost by deleting v is the total weight of initially reachable future targets dominated by v: U(S)-U_ B∖{v}(S) =∑_substackf∈ F∩Reach_ B(S) v dominates fw_f. Deleted target vertices are counted as unreachable.
Exact mathematical passage
U(S)-U_{\Bcal\setminus\{v\}}(S) =\sum_{\substack{f\in F\cap\Reach_{\Bcal}(S)\\v\text{ dominates }f}}w_f.
\circUse in source · 9 passages
Search aliases: ∘ circ
Use in source · Read passage · Proof_Path_Theory.tex, line 1335
[Retention projection algebra] For masks K,L⊆ V, P_K∘ P_L=P_K∩ L=P_L∘ P_K. Consequently every retention projection is idempotent, and the masks form a Boolean lattice with meet K∩ L and join K∪ L.
Exact mathematical passage
P_K\circ P_L=P_{K\cap L}=P_L\circ P_K.
\inftyUse in source · 2 passages
Search aliases: ∞ infty
Use in source · Read passage · Proof_Path_Theory.tex, line 1907
For n=1, the effective count is one. At the excluded boundary ρ=-1/(n-1), the mean has zero variance and there is no finite variance-equivalent count. For fixed 0<ρ≤1, n_eff→1/ρ as n→∞. Negative correlations can give n_eff>n, but a fixed negative correlation is not admissible for arbitrarily large n.
Exact mathematical passage
n\to\infty
\simUse in source · 2 passages
Search aliases: ∼ sim
Use in source · Read passage · Proof_Path_Theory.tex, line 1307
Define R_1∼_ QR_2 when both R_1preceq_ QR_2 and R_2preceq_ QR_1.
Exact mathematical passage
R_1\sim_{\Qcal}R_2
\sim_{\Qcal}Use in source · 2 passages
Search aliases: ∼_Qcal ∼_ Q sim Qcal sim mathcal
Use in source · Read passage · Proof_Path_Theory.tex, line 1307
Define R_1∼_ QR_2 when both R_1preceq_ QR_2 and R_2preceq_ QR_1.
Exact mathematical passage
R_1\sim_{\Qcal}R_2
\simeqUse in source · 1 passage
Search aliases: ≃ simeq
Use in source · Read passage · Proof_Path_Theory.tex, line 730
The strict Komorebi realization is now an actual set of coherent local models, Γ( M_F)= {(X_U)_U:ρ_U,W(X_W)=X_U whenever U⊆ W}. There is an explicit bijection Models(F)≃Γ( M_F), X⟼(X∩ U)_U. Its inverse evaluates a coherent family at the full patch V. Coherence shows that every other component is precisely the restriction of that value. The Lean declaration pathProofPath.Field.modelEquivSections constructs this equivalence, using pathViewDiagram and the actual local restriction maps.
Exact mathematical passage
\operatorname{Models}(F)\simeq\Gamma(\mathcal M_F), \qquad X\longmapsto(X\cap U)_U.
\approxUse in source · 1 passage
Search aliases: ≈ approx
Use in source · Read passage · Proof_Path_Theory.tex, line 2130
For one hundred equicorrelated reviewers with ρ=0.1, n_eff = frac1001+99(0.1) ≈ 9.17. The audit example begins with backlog 10. Arrivals 4 and capacity 5 clear the queue. Equal rates hold the backlog at 10. Arrivals 6 and capacity 5 increase it by one per cycle.
Exact mathematical passage
n_{\mathrm{eff}} = \frac{100}{1+99(0.1)} \approx 9.17.
\neUse in source · 5 passages
Search aliases: ≠ ne
Use in source · Read passage · Proof_Path_Theory.tex, line 241
Proof Path Theory studies this larger object without changing the standard of proof. Its central separation is certificate of validity ≠ expanded discovery field. The certificate answers whether the conclusion follows. The discovery field records how the conclusion became reachable, what alternatives were considered, what was lost during compression, and which omitted structures may matter later.
Exact mathematical passage
\boxed{ \text{certificate of validity} \quad\ne\quad \text{expanded discovery field}. }
\equivUse in source · 3 passages
Search aliases: ≡ equiv
Use in source · Read passage · Proof_Path_Theory.tex, line 1384
es:7:11 Let C:A→ B. Every predicate q:A→Prop factors through C if and only if C is injective. If C is injective, define the decoder of q at b by the predicate ∃ a (C(a)=b and q(a)). At b=C(a_0), injectivity makes this equivalent to q(a_0). Conversely, if C(a)=C(a'), use the predicate q(z)≡(z=a). Its decoded values at the equal encodings must agree, giving a'=a. This is the general collision criterion specialized to all predicates.
Exact mathematical passage
q(z)\equiv(z=a)
\leUse in source · 5 passages
Search aliases: ≤ le
Use in source · Read passage · Proof_Path_Theory.tex, line 1538
[Debt is monotone under retention] If K_1⊆ K_2, then Debt(K_2)≤Debt(K_1).
Exact mathematical passage
\Debt(K_2)\le\Debt(K_1).
\geqUse in source · 6 passages
Search aliases: ≥ geq
Use in source · Read passage · Proof_Path_Theory.tex, line 1998
Let a_t≥0 be candidate arrivals during audit cycle t, let s_t≥0 be service capacity, and let B_t≥0 be the unresolved backlog. Suppose arrivals in a cycle are available to that cycle's service. The basic deterministic queue is B_t+1=max{0,B_t+a_t-s_t}.
Exact mathematical passage
a_t\geq0
\supseteqUse in source · 1 passage
Search aliases: ⊇ supseteq
Use in source · Read passage · Proof_Path_Theory.tex, line 1550
[Irreversible compression accumulates debt] For a descending sequence of retained sets K_0⊇ K_1⊇⋯⊇ K_r, the expected debt is nondecreasing.
Exact mathematical passage
K_0\supseteq K_1\supseteq\cdots\supseteq K_r,
\bigcupUse in source · 2 passages
Search aliases: ⋃ bigcup
Use in source · Read passage · Proof_Path_Theory.tex, line 774
[Whole-support gluing] Suppose every certified justification has its whole support in some patch: ∀ j certified, ∃ i S_j⊆ U_i. Then every matching family (X_i) has a unique global field model X satisfying X∩ U_i=X_i for all i. Set X=⋃_iX_i. Matching and node coverage imply X∩ U_i=X_i. A leaf belongs to some patch and hence to its local model, so L⊆ X. Consider a certified rule whose premises belong to X. Choose a patch containing its entire support. Matching implies that every premise is true in…
Exact mathematical passage
X=\bigcup_iX_i
\bigcup_iUse in source · 1 passage
Search aliases: ⋃_i bigcup
Use in source · Read passage · Proof_Path_Theory.tex, line 774
[Whole-support gluing] Suppose every certified justification has its whole support in some patch: ∀ j certified, ∃ i S_j⊆ U_i. Then every matching family (X_i) has a unique global field model X satisfying X∩ U_i=X_i for all i. Set X=⋃_iX_i. Matching and node coverage imply X∩ U_i=X_i. A leaf belongs to some patch and hence to its local model, so L⊆ X. Consider a certified rule whose premises belong to X. Choose a patch containing its entire support. Matching implies that every premise is true in…
Exact mathematical passage
X=\bigcup_iX_i
\bigcup_{x\in S}Use in source · 1 passage
Search aliases: ⋃_x∈ S bigcup in
Use in source · Read passage · Proof_Path_Theory.tex, line 1699
For each candidate x∈ C, let R_x⊆ F be the set of future targets reachable from M∪{x}. Let R_M be the targets already reachable from M. Reachability from a union of starting nodes is the union of their individual reach sets, so U_M(S)= ∑_f∈ R_M∪⋃_x∈ SR_xw_f. Adding a candidate cannot remove a reachable target, so U_M is monotone.
Exact mathematical passage
U_M(S)= \sum_{f\in R_M\cup\bigcup_{x\in S}R_x}w_f.
\langleUse in source · 1 passage
Search aliases: ⟨ langle
Use in source · Read passage · Proof_Path_Theory.tex, line 903
0 · 1 · 0. Its two rows are identical. On H=⟨011⟩ it has rank one, so | A|=2, |Q( A)|=2, and every attained observation fiber has size one. These are count identities before they are interpreted probabilistically.
Exact mathematical passage
H=\langle011\rangle
\rangleUse in source · 1 passage
Search aliases: ⟩ rangle
Use in source · Read passage · Proof_Path_Theory.tex, line 903
0 · 1 · 0. Its two rows are identical. On H=⟨011⟩ it has rank one, so | A|=2, |Q( A)|=2, and every attained observation fiber has size one. These are count identities before they are interpreted probabilistically.
Exact mathematical passage
H=\langle011\rangle
\longmapstoUse in source · 1 passage
Search aliases: ⟼ longmapsto
Use in source · Read passage · Proof_Path_Theory.tex, line 730
The strict Komorebi realization is now an actual set of coherent local models, Γ( M_F)= {(X_U)_U:ρ_U,W(X_W)=X_U whenever U⊆ W}. There is an explicit bijection Models(F)≃Γ( M_F), X⟼(X∩ U)_U. Its inverse evaluates a coherent family at the full patch V. Coherence shows that every other component is precisely the restriction of that value. The Lean declaration pathProofPath.Field.modelEquivSections constructs this equivalence, using pathViewDiagram and the actual local restriction maps.
Exact mathematical passage
\operatorname{Models}(F)\simeq\Gamma(\mathcal M_F), \qquad X\longmapsto(X\cap U)_U.
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
- monographs/proof-path-theory/README.md · 0 mathematical passages
- monographs/proof-path-theory/STATUS.md · 0 mathematical passages
- monographs/proof-path-theory/docs/LEAN_GUIDE.md · 0 mathematical passages
- monographs/proof-path-theory/docs/Proof_Path_Theory.tex · 1042 mathematical passages
- monographs/proof-path-theory/evidence/README.md · 0 mathematical passages
PDF reading editions (2)
The text index does not extract PDF glyphs. Check the reading edition for notation in figures, tables, and PDF-only material.