Proof Path Theory

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \documentclass[11pt,oneside]{article}
2 \usepackage[a4paper,inner=23mm,outer=22mm,top=24mm,bottom=24mm,headsep=7mm,footskip=12mm]{geometry}
3 \usepackage[T1]{fontenc}
4 \usepackage[utf8]{inputenc}
5 \usepackage{amsmath,amssymb,amsthm,mathtools}
6 \usepackage{newtxtext,newtxmath}
7 \usepackage[scaled=0.92]{sourcesanspro}
8 \usepackage[nopatch=footnote]{microtype}
9 \usepackage{booktabs,longtable,array,enumitem,tabularx}
10 \newcolumntype{L}[1]{>{\raggedright\arraybackslash}p{#1}}
11 \usepackage{graphicx,float,caption}
12 \usepackage{xcolor,tikz,titlesec,fancyhdr,listings,setspace,needspace,placeins}
13 \usepackage[most]{tcolorbox}
14 \usepackage{etoolbox}
15 \usepackage{upquote}
16 \usepackage{xurl}
17 \usepackage{hyperref}
18 \definecolor{KomorebiTeal}{HTML}{285A50}
19 \definecolor{KomorebiInk}{HTML}{1E3430}
20 \definecolor{KomorebiMuted}{HTML}{65706D}
21 \definecolor{KomorebiPaper}{HTML}{F5F2E9}
22 \definecolor{KomorebiPale}{HTML}{EAF0ED}
23 \definecolor{KomorebiGold}{HTML}{B57F2A}
24 \definecolor{KomorebiGoldPale}{HTML}{EFE2BE}
25 \definecolor{KomorebiBlue}{HTML}{4C6A92}
26 \definecolor{KomorebiBluePale}{HTML}{E4EBF4}
27 \definecolor{KomorebiRose}{HTML}{D98673}
28 \definecolor{KomorebiRosePale}{HTML}{F3E2DD}
29 \definecolor{KomorebiLine}{HTML}{7A867F}
30 \hypersetup{colorlinks=true,linkcolor=KomorebiTeal,citecolor=KomorebiTeal,urlcolor=KomorebiTeal,
31  pdftitle={Proof Path Theory: Certificates, Compression, Discovery Fields, and Mathematical Memory},
32  pdfauthor={Komorebi P.},pdfsubject={Monograph edition 1.8.0},
33  pdfkeywords={proof fields, realization, compression, certificates, mathematical memory}}
34 \graphicspath{{figures/}}
35 \setstretch{1.055}
36 \setlength{\parindent}{0pt}
37 \setlength{\parskip}{5.4pt plus 0.5pt}
38 \setlength{\emergencystretch}{2em}
39 \setlength{\headheight}{14pt}
40 \setcounter{secnumdepth}{2}
41 \setcounter{tocdepth}{1}
42 \setlist[itemize]{leftmargin=1.45em,itemsep=2pt,topsep=4pt}
43 \setlist[enumerate]{leftmargin=1.8em,itemsep=2pt,topsep=4pt}
44 \captionsetup{font={small,sf},labelfont={bf,color=KomorebiTeal},labelsep=period,skip=8pt,justification=raggedright,singlelinecheck=false}
45 \renewcommand{\figurename}{Figure}
46 \setlength{\textfloatsep}{15pt plus 2pt minus 2pt}
47 \setlength{\intextsep}{14pt plus 2pt minus 2pt}
48 \renewcommand{\topfraction}{0.9}
49 \renewcommand{\bottomfraction}{0.85}
50 \renewcommand{\textfraction}{0.08}
51 \renewcommand{\floatpagefraction}{0.72}
52 \pagestyle{fancy}
53 \fancyhf{}
54 \fancyhead[L]{\sffamily\fontsize{8}{10}\selectfont\color{KomorebiMuted}PROOF PATH THEORY}
55 \fancyhead[R]{\sffamily\fontsize{8}{10}\selectfont\color{KomorebiMuted}\nouppercase{\leftmark}}
56 \fancyfoot[L]{\sffamily\fontsize{7.7}{9}\selectfont\color{KomorebiTeal}OPERATION KOMOREBI}
57 \fancyfoot[R]{\sffamily\small\color{KomorebiInk}\thepage}
58 \renewcommand{\headrulewidth}{0pt}
59 \renewcommand{\footrulewidth}{0pt}
60 \renewcommand{\sectionmark}[1]{}
61 \titleformat{\section}{\Large\sffamily\bfseries\color{KomorebiTeal}}{\thesection}{0.65em}{}
62 \titlespacing*{\section}{0pt}{19pt plus 3pt}{8pt}
63 \titleformat{\subsection}{\large\sffamily\bfseries\color{KomorebiInk}}{\thesubsection}{0.65em}{}
64 \titlespacing*{\subsection}{0pt}{13pt plus 2pt}{5pt}
65 \newtheoremstyle{komorebiplain}{7pt}{7pt}{\itshape}{}{\bfseries\color{KomorebiInk}}{.}{0.6em}{}
66 \newtheoremstyle{komorebidefinition}{7pt}{7pt}{}{}{\bfseries\color{KomorebiInk}}{.}{0.6em}{}
67 \newtheoremstyle{komorebiremark}{6pt}{6pt}{}{}{\itshape\color{KomorebiInk}}{.}{0.6em}{}
68 \theoremstyle{komorebiplain}
69 \newtheorem{theorem}{Theorem}[section]
70 \newtheorem{proposition}[theorem]{Proposition}
71 \newtheorem{lemma}[theorem]{Lemma}
72 \newtheorem{corollary}[theorem]{Corollary}
73 \theoremstyle{komorebidefinition}
74 \newtheorem{definition}[theorem]{Definition}
75 \newtheorem{example}[theorem]{Example}
76 \newtheorem{problem}[theorem]{Problem}
77 \theoremstyle{komorebiremark}
78 \newtheorem{remark}[theorem]{Remark}
79 \newtheorem{warning}[theorem]{Warning}
80 % Deliberately restrained formal typography: statements, not repeated boxes.
81 \BeforeBeginEnvironment{theorem}{\Needspace{5\baselineskip}}
82 \BeforeBeginEnvironment{proposition}{\Needspace{4\baselineskip}}
83 \BeforeBeginEnvironment{lemma}{\Needspace{4\baselineskip}}
84 \BeforeBeginEnvironment{corollary}{\Needspace{4\baselineskip}}
85 \BeforeBeginEnvironment{definition}{\Needspace{4\baselineskip}}
86 \BeforeBeginEnvironment{example}{\Needspace{4\baselineskip}}
87 \tcolorboxenvironment{theorem}{blanker,breakable,left=8pt,
88   borderline west={1.25pt}{0pt}{KomorebiTeal},before skip=10pt,after skip=10pt}
89 \tcolorboxenvironment{example}{blanker,breakable,left=8pt,
90   borderline west={1.0pt}{0pt}{KomorebiGold},before skip=9pt,after skip=9pt}
91 \newcommand{\calloutbox}[2]{\par\medskip
92  {\sffamily\small\bfseries\color{KomorebiTeal}#1\par}
93  \smallskip #2\par\medskip}
94 \newcommand{\Pcal}{\mathcal P}
95 \newcommand{\Jcal}{\mathcal J}
96 \newcommand{\Qcal}{\mathcal Q}
97 \newcommand{\Rcal}{\mathcal R}
98 \newcommand{\Ecal}{\mathcal E}
99 \newcommand{\Vcal}{\mathcal V}
100 \newcommand{\Ccal}{\mathcal C}
101 \newcommand{\Bcal}{\mathcal B}
102 \newcommand{\Tcal}{\mathcal T}
103 \newcommand{\Fcal}{\mathcal F}
104 \newcommand{\Anc}{\operatorname{Anc}}
105 \newcommand{\AncL}{\operatorname{Anc}_L}
106 \newcommand{\Desc}{\operatorname{Desc}}
107 \newcommand{\Reach}{\operatorname{Reach}}
108 \newcommand{\Cost}{\operatorname{Cost}}
109 \newcommand{\Loss}{\operatorname{Loss}}
110 \newcommand{\Debt}{\operatorname{Debt}}
111 \newcommand{\argmin}{\operatorname*{arg\,min}}
112 \newcommand{\argmax}{\operatorname*{arg\,max}}
113 \lstset{language=Python,basicstyle=\ttfamily\fontsize{9.5}{11.4}\selectfont,breaklines=true,
114  frame=single,rulecolor=\color{KomorebiPale},backgroundcolor=\color{KomorebiPale!35},
115  framerule=0.4pt,xleftmargin=5pt,xrightmargin=5pt,framexleftmargin=4pt,framexrightmargin=4pt,
116  showstringspaces=false,columns=fullflexible,keepspaces=true,upquote=true,aboveskip=9pt,belowskip=9pt}
117 \newcommand{\openingfigure}[3]{%
118 \begin{figure}[H]\centering
119 \includegraphics[width=\linewidth]{#1}
120 \caption{#2}\label{#3}
121 \end{figure}}
122 \newcommand{\monographpart}[3]{%
123  \FloatBarrier\clearpage\refstepcounter{part}\markboth{#2}{#2}%
124  \addcontentsline{toc}{part}{\protect\numberline{\thepart}#1}%
125  {\sffamily\fontsize{10}{12}\selectfont\bfseries\color{KomorebiTeal}PART \thepart\par}
126  \vspace{8pt}
127  {\raggedright\hyphenpenalty=10000\exhyphenpenalty=10000\sffamily\fontsize{29}{32}\selectfont\bfseries\color{KomorebiInk}#1\par}
128  \vspace{10pt}
129  {\large\color{KomorebiMuted}#3\par}
130  \vspace{10pt}
131  {\color{KomorebiTeal}\rule{24mm}{1pt}\par}
132  \vspace{9pt}
133  \ifcase\value{part}\relax
134  \or
135   \openingfigure{fig_14_ambient_field.pdf}{A declared proof field retains three different statuses. The solid route certifies the target. The upper branch has an unresolved obligation. The lower branch has a scoped refutation. Neither the open branch nor the refuted step invalidates the certified route.}{fig:ambient}
136   \vspace{4pt}{\sffamily\bfseries\color{KomorebiTeal}The governing distinction}\par
137   A proof field preserves more than a proof needs. Its failed and unresolved records remain available to inquiry without acquiring the force of certified deductions.
138  \or
139   \openingfigure{fig_17_binary_cube.pdf}{Eight vertices encode the states of $\mathbb F_2^3$. Four satisfy $a+b+c=0$. Protecting $a=0$ leaves the two green vertices $000$ and $011$. The cube edges show single-coordinate changes, not continuous solution lines or proof steps.}{fig:binary-cube}
140   \vspace{3pt}{\sffamily\bfseries\color{KomorebiTeal}The governing distinction}\par
141   Existence asks whether the fiber is empty. Ambiguity asks what remains inside it. An informative observation distinguishes points of that fiber rather than merely producing more output coordinates.
142  \or
143   \openingfigure{fig_20_compression_collision.pdf}{Two archives have the same certificate $C_0$ but different side records. Compression forgets that record. A single decoder receiving $C_0$ cannot return both answers to the side-record query. This is the collision criterion in its smallest finite form.}{fig:compression-collision}
144   \vspace{3pt}{\sffamily\bfseries\color{KomorebiTeal}The governing distinction}\par
145   A valid certificate can be sufficient for checking the present theorem and insufficient for a later question. The lost distinction, not the length of the file, determines the failure.
146  \or
147   \openingfigure{fig_21_review_error_floor.pdf}{Three declared review models separate independent noise, a common offset, and a common offset with correlated errors. The marginal variance is one. The offset is $b=0.3$ when present and the correlation is $\rho=0.1$ when present. Both axes are logarithmic. These are model consequences, not observed reviewer data.}{fig:review-floor}
148   \vspace{3pt}{\sffamily\bfseries\color{KomorebiTeal}The governing distinction}\par
149   Aggregation can reduce independent error without removing a shared offset. Review evidence, provenance, and certificate validity must therefore remain distinguishable.
150  \or
151   \openingfigure{fig_13_repository_workflow.pdf}{The actual publication workflow separates declared records, software checks, certificate reports, formal interfaces, and delivered artifacts. Certification flags describe the finite input model. They do not prove arbitrary statements attached to node labels.}{fig:workflow}
152  \fi
153  \clearpage}
154 \newcommand{\studyhead}[2]{%
155  \FloatBarrier\clearpage
156  {\sffamily\small\bfseries\color{KomorebiTeal}VISUAL STUDY\quad #1\par}
157  \vspace{7pt}{\sffamily\fontsize{23}{27}\selectfont\bfseries\color{KomorebiInk}#2\par}\vspace{8pt}}
158 \begin{document}
159 \begin{titlepage}
160 \thispagestyle{empty}
161 \begin{tikzpicture}[remember picture,overlay]
162  \fill[KomorebiPaper] (current page.south west) rectangle (current page.north east);
163  \fill[KomorebiTeal] (current page.south west) rectangle ([xshift=3mm]current page.north west);
164 \end{tikzpicture}
165 \vspace*{1mm}
166 {\sffamily\bfseries\fontsize{9.4}{12}\selectfont\color{KomorebiTeal}OPERATION KOMOREBI\par}
167 \vspace{5pt}
168 {\sffamily\fontsize{8.3}{11}\selectfont\color{KomorebiMuted}REALIZATION CALCULUS\enspace /\enspace MATHEMATICAL REASONING\par}
169 \vspace{22mm}
170 {\sffamily\bfseries\fontsize{42}{45}\selectfont\color{KomorebiInk}Proof Path\\Theory\par}
171 \vspace{11pt}
172 {\fontsize{16}{21}\selectfont\color{KomorebiInk}Certificates, compression, discovery fields,\\and mathematical memory\par}
173 \vspace{11pt}
174 {\color{KomorebiGold}\rule{36mm}{1.1pt}\par}
175 \vspace{8mm}
176 \includegraphics[width=\linewidth]{cover_field.pdf}
177 \vspace{4pt}
178 {\sffamily\fontsize{9}{12}\selectfont\color{KomorebiMuted}The proof is a certified core. The field retains the surrounding mathematics.\par}
179 \vfill
180 {\sffamily\bfseries\fontsize{11}{14}\selectfont\color{KomorebiInk}Komorebi P.\par}
181 \vspace{6pt}
182 {\sffamily\fontsize{9}{12}\selectfont\color{KomorebiMuted}Monograph edition 1.8.0\quad /\quad 19 October 2026\par}
183 \vspace*{3mm}
184 \end{titlepage}
185 \pagenumbering{roman}
186 \markboth{Monograph}{Monograph}
187 \section*{Preface}
188 \addcontentsline{toc}{section}{Preface}
189 A proof establishes an implication. The work surrounding that proof may answer other questions: why a definition was chosen, which hypothesis prevented an argument from failing, or how a change of representation opened a route that had not previously been visible. Publishing a certificate and preserving this larger mathematical record are related tasks, but they are not the same task.
190 
191 Proof Path Theory studies that distinction through explicit finite objects. A proof field contains typed claims, justifications, evidence, and targets. Each justification requires all of its listed premises, while alternative justifications supply different routes to a conclusion. A certified derivation lies inside this field without converting its conjectures, examples, and unsuccessful attempts into additional proof steps.
192 
193 The theory has two complementary directions. One selects or compresses a record while asking what remains recoverable. The other assembles local descriptions into coherent realizations. The first leads to certificate complexity, task sufficiency, information loss, and retention. The second gives a precise connection with Komorebi Space through local rule models, restriction maps, and gluing. A separate linear model yields positive realization certificates, negative obstruction witnesses, and exact observation counts.
194 
195 Failed approaches remain part of the ambient record for a reason. They may isolate a missing hypothesis or reveal a limitation of one method. Their value does not turn a failed search into a proof of impossibility. A refutation must identify the assertion it refutes, the assumptions under which it applies, and the witness that establishes the failure. That scope is as important as the witness itself.
196 
197 The later chapters examine how an archive changes and how its claims are evaluated. Their review and queue models are deliberately conditional. A covariance formula describes a specified dependence model, not an empirical diagnosis of a community. A record of social reception does not determine whether a proof is valid. Keeping those distinctions explicit allows the theory to study the transmission of mathematics without replacing mathematical standards with social judgments.
198 
199 The mathematical ingredients come from proof theory, graph theory, category theory, linear algebra, information theory, and optimization. Their role here is to form one account of certified reasoning and the surrounding information that later inquiry may need. Familiar ingredients are not concealed, and a new notation is not presented as evidence of new mathematical truth.
200 
201 This monograph preserves written proofs, finite examples, and the connection to the accompanying implementation. Its formal concordance identifies the selected Lean interfaces. The aim is a record that a reader can inspect at several levels: the statement, its argument, the hypotheses that make it valid, and the computational evidence supplied for its implementation.
202 
203 \clearpage
204 \section*{Reading map}
205 \addcontentsline{toc}{section}{Reading map}
206 The five parts follow one mathematical record from discovery to certification, realization, compression, review, and reuse. The visual studies work through actual finite examples rather than replacing the proofs.
207 
208 \begin{figure}[H]\centering
209 \includegraphics[width=\linewidth]{fig_00_theory_map.pdf}
210 \caption{Five questions organize the monograph. The order is a reading route, not a claim that one kind of evidence replaces another.}
211 \label{fig:theory-map}
212 \end{figure}
213 
214 \begin{minipage}[t]{0.47\linewidth}
215 {\sffamily\bfseries\color{KomorebiTeal}A short technical route}\par\smallskip
216 Begin with Sections~\ref{sec:old3}, \ref{sec:old4}, \ref{sec:old24}, and \ref{sec:old7}. For collective interpretation, read Sections~\ref{sec:old17} and \ref{sec:old25} together.
217 \end{minipage}\hfill
218 \begin{minipage}[t]{0.47\linewidth}
219 {\sffamily\bfseries\color{KomorebiTeal}Evidence in this edition}\par\smallskip
220 The 41 prior result groups are retained. Six new groups specify trace checking and typed exchange. Eighteen Lean modules were freshly built, replayed with Lean's kernel, and axiom audited. Exact finite checks remain separate from the formal proofs.
221 \end{minipage}
222 
223 \clearpage
224 \tableofcontents
225 \clearpage
226 \pagenumbering{arabic}
227 \monographpart{Proof fields and certificates}{Fields and certificates}{A completed proof occupies only part of its surrounding field. Keep the successful deduction, but do not confuse its unused alternatives with either errors in that deduction or proofs of impossibility.}
228 
229 \section{Introduction}
230 \label{sec:old1}
231 
232 A published proof often presents an argument after its exploratory work has been compressed. Definitions have stabilized, unsuccessful approaches have been set aside, and a long calculation may now appear as a lemma. The change of representation that first made the argument visible can disappear into a single sentence. Such compression is often useful: it leaves a certificate that is easier to check and reuse.
233 
234 Compression can 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
235 \[
236 A\vdash B.
237 \]
238 They may still be part of the mathematical event that produced it.
239 
240 Proof Path Theory studies this larger object without changing the standard of proof. Its central separation is
241 \[
242 \boxed{
243 \text{certificate of validity}
244 \quad\ne\quad
245 \text{expanded discovery field}.
246 }
247 \]
248 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.
249 
250 The construction begins with a typed field of claims, justifications, evidence, and targets. Its certified rules determine which targets are derivable. A certificate selects enough of those records to support a declared conclusion, while the ambient field can retain unresolved or refuted alternatives.
251 
252 A second layer asks what survives when the field is compressed. The answer depends on the questions that a representation must support. An archive intended for future discovery may preserve examples and failed approaches that a verification certificate can omit. A bridge graph makes one such retention problem precise.
253 
254 The final layer concerns the continuing life of the archive. Revisions change the set of claims that need review. Shared errors affect the information supplied by multiple reviewers. Audit capacity limits how quickly new candidates can be checked. These models are connected by their declared proof objects, without treating social judgments as substitutes for deduction.
255 
256 
257 
258 \begin{figure}[htbp]
259 \centering
260 \includegraphics[width=\linewidth]{fig_01_architecture.pdf}
261 \caption{Three different questions about the same declared archive. A certificate records derivability, local models record rule compatibility, and a task representation records recoverable information. None of these questions subsumes the others without additional hypotheses.}
262 \label{fig:architecture}
263 \end{figure}
264 
265 Komorebi Space enters when local descriptions of a proof field must agree. The construction of local rule models supplies actual restriction maps, not merely a visual analogy between two graphs. A gluing theorem identifies a sufficient condition for assembling those models, and a counterexample explains why pairwise dependency checks can miss a conjunctive rule. In a separate linear setting, the size of a realization fiber measures exactly what a new observation distinguishes.
266 
267 The implemented proof fields are finite and acyclic. Some structural statements, including rule soundness and the linear separation alternative, are given in greater generality where their hypotheses allow it. Extensions to infinite search, probabilistic inference, and higher categorical proof objects require their own assumptions. Background on formal proof systems may be found in \cite{buss,troelstra}.
268 
269 
270 \section{Claim types and logical boundaries}
271 \label{sec:old2}
272 
273 A useful theory of proof paths must not turn every recorded object into a proof step. A notebook may contain a theorem, a conjecture, a failed analogy, a numerical experiment, and a historical interpretation on the same page. Their coexistence does not give them the same logical status.
274 
275 \begin{definition}[Evidence kind]
276 \label{res:2:1}
277 An evidence kind is a declared type attached to a record supporting a claim or justification. The core finite vocabulary used here is
278 \[
279 \begin{aligned}
280 &\text{formal proof},\quad \text{assumption},\quad \text{exact computation},\\
281 &\text{numerical evidence},\quad \text{conjecture},\quad \text{external result},\\
282 &\text{counterexample},\quad \text{interpretation}.
283 \end{aligned}
284 \]
285 An evidence record also states its source, scope, and whether it certifies the justification to which it is attached.
286 \end{definition}
287 
288 The word ``certifies'' is deliberately separate from the evidence label. An exact computation may certify a finite identity while providing only numerical evidence for a general statement. An external result may certify a step only on the domain covered by its hypotheses. The scope field is therefore part of the mathematical object.
289 
290 \begin{warning}[Evidence types are not one ranking]
291 \label{res:2:2}
292 The evidence kinds do not form a universal total order. A formal proof of a weak statement and an exact computation of a stronger finite instance cannot be compared by one scalar without specifying the task. The ledger retains type and scope instead of replacing them with a single confidence number.
293 \end{warning}
294 
295 This separation will be used throughout. Candidate edges may remain in the discovery field, but only certified edges enter a proof certificate.
296 
297 
298 \section{Typed proof fields}
299 \label{sec:old3}
300 
301 The first formal object is a directed hypergraph. A justification may require several premises at once, and a claim may admit several alternative justifications.
302 
303 \begin{definition}[Typed proof field]
304 \label{res:3:1}
305 A finite typed proof field is a tuple
306 \[
307 \Pcal=(V,\Jcal,A,T,\tau,\Ecal,\mathbf v,\mathbf c),
308 \]
309 where:
310 \begin{itemize}
311 \item $V$ is a finite set of claim nodes.
312 \item $\Jcal$ is a finite set of justifications.
313 \item Each $j\in\Jcal$ has a finite premise set $\operatorname{prem}(j)\subseteq V$ and one conclusion $\operatorname{con}(j)\in V$.
314 \item $A\subseteq V$ is the set of required premises of the declared judgment.
315 \item $T\subseteq V$ is the nonempty target set.
316 \item $\tau$ assigns node and justification types.
317 \item $\Ecal$ is a typed evidence ledger.
318 \item $\mathbf v$ assigns nonnegative value coordinates to nodes.
319 \item $\mathbf c$ assigns nonnegative storage, audit, recovery, and cognitive costs.
320 \end{itemize}
321 The dependency graph contains an edge $u\to v$ whenever $u\in\operatorname{prem}(j)$ and $v=\operatorname{con}(j)$ for some justification $j$. It is required to be acyclic.
322 \end{definition}
323 
324 A single justification is conjunctive in its premise set. All listed premises must be available. Multiple justifications with the same conclusion are alternatives. This gives the familiar AND/OR structure of proof search without forcing it into an ordinary graph.
325 
326 \begin{definition}[Admissible leaf]
327 \label{res:3:2}
328 A node is an admissible leaf when it is a required premise, a declared axiom, or an explicitly admitted external result. Write $L$ for this set, so $A\subseteq L$. A certified justification with no premises can also derive a node, but it remains a justification and need not make that node a member of $L$. The distinction matters when extracting the smallest certificate.
329 \end{definition}
330 
331 Required premises are not necessarily the entire assumption context. Admitted axioms and external results remain visible in the supporting ledger. The notation $A\vdash B$ is relative to that declared background and does not erase those dependencies. A comparison between certificates must retain the assumptions under which each certificate is valid.
332 
333 \begin{definition}[Certified subfield]
334 \label{res:3:3}
335 The certified subfield $\Pcal^{\mathrm{cert}}$ contains every node of $\Pcal$ 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~\ref{sec:old24}.
336 \end{definition}
337 
338 \begin{definition}[Derivability]
339 \label{res:3:4}
340 Let $K\subseteq V$ be a selected node set and let $H\subseteq\Jcal$ be a selected justification set. The derivable set $D(K,H)$ is the least subset of $K$ satisfying:
341 \begin{enumerate}[label=\textup{(\roman*)}]
342 \item every selected admissible leaf belongs to $D(K,H)$.
343 \item if $j\in H$, $\operatorname{prem}(j)\subseteq D(K,H)$, and $\operatorname{con}(j)\in K$, then $\operatorname{con}(j)\in D(K,H)$.
344 \end{enumerate}
345 When only certified justifications are allowed, write $D_{\mathrm{cert}}(K,H)$.
346 \end{definition}
347 
348 \begin{proposition}[Finite derivability]
349 \label{res:3:5}
350 For a finite acyclic proof field, $D(K,H)$ is uniquely determined and can be computed in one topological pass through the dependency graph.
351 \end{proposition}
352 
353 \begin{proof}
354 Acyclicity gives a topological ordering of the nodes. Begin with the selected admissible leaves. At each later node, test whether one selected incoming justification has all of its premises already derived. Add the node exactly when such a justification exists. No later step can change the status of an earlier node because all dependencies point forward. The resulting set satisfies the closure rules. Any set satisfying the rules must contain every node added by this pass, so the result is the least such set and is unique.
355 \end{proof}
356 
357 \begin{figure}[htbp]
358 \centering
359 \includegraphics[width=\linewidth]{fig_03_alternative_hypergraph.pdf}
360 \caption{Two certified routes in \protect\path{alternative_proofs.json}. Their stored node costs are one and three. A storage objective selects the short route, while a task requiring explanatory information can prefer the richer route. Alternative derivations are OR choices, not extra conjunctive premises.}
361 \label{fig:andor}
362 \end{figure}
363 
364 
365 \section{The ambient proof field and the meaning of failure}
366 \label{sec:old22}
367 \label{sec:ambient}
368 
369 A finished proof is rarely the only route the researcher could have explored. An archive often contains sketches that were never completed, arguments that failed because of a specific hypothesis, conjectured bridges that remain untested, and genuinely refuted local constructions. It is tempting to call this whole archive a proof, but doing so would erase the distinction between a certified result and a record of exploration. The \emph{ambient proof field} provides a more precise language: it is the declared field of reachable or recorded mathematical states and typed candidate transitions in which certified proof paths form a distinguished subfield.
370 
371 The finite hypergraph model permits \path{failed_route}, \path{boundary_case}, and \path{counterexample} nodes. Their presence is useful, but none is a logically justified global nonexistence claim by itself. A failed search is not necessarily a proof of impossibility. A counterexample to one proposed lemma is not necessarily a counterexample to the goal. An exact obstruction must have a declared scope and a checkable witness.
372 
373 \begin{definition}[Scoped branch assessment]
374 \label{res:22:1}
375 Let $\Pcal$ 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:
376 \begin{enumerate}[label=\textup{(\roman*)}]
377 \item \emph{Open}: obligations remain unresolved.
378 \item \emph{Abandoned}: exploration stopped without a certificate of impossibility.
379 \item \emph{Locally refuted}: a checked counterexample or obstruction excludes a stated intermediate step under specified hypotheses.
380 \item \emph{Certified}: the selected justifications meet the declared proof certificate conditions.
381 \end{enumerate}
382 An assessment is a record of the branch, not a truth value assigned to every possible proof of $t$.
383 \end{definition}
384 
385 \begin{proposition}[Local failure does not imply global failure]
386 \label{res:22:2}
387 A finite proof field may contain a locally refuted branch to target $t$ while also containing a certified derivation of $t$ from its declared premises.
388 \end{proposition}
389 \begin{proof}
390 Take a premise $A$ and two alternative candidate derivations of $t$. Let the first use a proposed intermediate lemma $L$ that has a checked counterexample, so the corresponding justification is not certified. Let the second use a distinct certified justification from $A$ to $t$. The certified closure reaches $t$ by the second route. The failed first route remains a valid record of unsuccessful exploration, but cannot negate the existence of the second certificate. The same example can be represented by the alternative justification hypergraph developed earlier.
391 \end{proof}
392 
393 
394 
395 The logical lesson is substantive for machine reasoning. A search timeout, budget exhaustion, invalid intermediate conjecture, or failure to find a proof all have different meanings. Only a certificate whose conclusion explicitly concerns nonexistence under a declared model and scope licenses a nonexistence claim. This is especially important when a failed branch is used to prune an automated search. Pruning the refuted step may be safe, while pruning its entire goal may discard a genuine proof.
396 
397 \begin{proposition}[Scoped refutation survives unchanged context]
398 \label{res:22:3}
399 Suppose a witness $w$ is verified by a sound checker to refute the predicate $L$ under assumptions $A$. In any later archive revision that retains the same interpretation of $L$, the same assumptions, and the checker's verification rules, $w$ remains a refutation of $L$. No conclusion follows about different predicates, altered assumptions, or alternative branches to a different goal.
400 \end{proposition}
401 \begin{proof}
402 The verification of $w$ depends only on the declared predicate, assumptions, and checking rules. An append-only collection of unrelated exploratory records does not alter those inputs. Therefore the same verification remains valid. When any of those inputs changes, the earlier check no longer certifies the revised claim without an explicit comparison theorem.
403 \end{proof}
404 
405 This is a qualified stability principle, not a general theorem that proof search is decidable. The append-only derivability result of Section~\ref{sec:versioned} concerns certified edges. The present proposition concerns the narrower persistence of a checked counterexample under a fixed interpretation. Both retain scope as part of the mathematical data.
406 
407 
408 \section{Certificates and verification closure}
409 \label{sec:old4}
410 
411 \begin{definition}[Certificate]
412 \label{res:4:1}
413 A certificate for a nonempty requested target set $T_0\subseteq V$ is a pair
414 \[
415 \Ccal=(K,H),
416 \qquad K\subseteq V,
417 \qquad H\subseteq\Jcal^{\mathrm{cert}},
418 \]
419 such that
420 \[
421 A\cup T_0\subseteq K
422 \qquad\text{and}\qquad
423 T_0\subseteq D_{\mathrm{cert}}(K,H).
424 \]
425 Order certificates componentwise: $(K,H)\leq(K^{\prime},H^{\prime})$ means $K\subseteq K^{\prime}$ and $H\subseteq 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.
426 \end{definition}
427 
428 The usual target request is a subset of $T$, but an intermediate node may be requested for local analysis. Only a justification whose premises have been derived and whose conclusion is selected can contribute to the derivation. A record may retain other, inactive justifications without using them as proof steps. Extra records cannot lower a nonnegative additive cost, although zero costs can allow several minimizing records.
429 
430 \subsection{The fixed AND-DAG case}
431 
432 The simplest case occurs when each relevant node that is not an admissible leaf has one certified incoming justification. Backward expansion stops at admissible leaves. A proof of a statement that has already been admitted as a leaf is not required to use that statement.
433 
434 \begin{definition}[AND-DAG]
435 \label{res:4:2}
436 Starting at $T_0$, expand backward only at nodes outside $L$. The field is an AND-DAG relative to $T_0$ when every node reached outside $L$ has exactly one certified incoming justification. Every premise of that justification is then expanded in the same manner. The process may terminate at an admissible leaf or at a certified justification with no premises.
437 \end{definition}
438 
439 Let $\Anc_L(T_0)$ denote the premise nodes reached by this backward expansion, stopping at $L$. Let $H_{\mathrm{core}}$ contain exactly the justifications selected at expanded nodes outside $L$.
440 
441 \begin{theorem}[Unique verification core]
442 \label{res:4:3}
443 \label{thm:and-core}
444 Let $\Pcal$ be a finite acyclic AND-DAG relative to $T_0$. Put
445 \[
446 K_{\mathrm{core}}=A\cup T_0\cup\Anc_L(T_0).
447 \]
448 Then $(K_{\mathrm{core}},H_{\mathrm{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.
449 \end{theorem}
450 
451 \begin{proof}
452 Backward expansion terminates because the dependency graph is finite and acyclic. Every terminal node is either an admissible leaf or the conclusion of the selected justification with no premises. A forward topological pass therefore derives every expanded node. The required premises in $A$ are admissible and are retained even if the target does not use them. Thus the constructed pair is a certificate.
453 
454 Now let $(K,H)$ be any certificate for the same request. It contains $A\cup T_0$. If a requested or required predecessor node is outside $L$, its derivation must use its unique certified incoming justification. That justification belongs to $H$, and every one of its premises belongs to $K$. Repeating the argument forces all of $\Anc_L(T_0)$ and $H_{\mathrm{core}}$. At nodes in $L$ the argument stops. Hence $K_{\mathrm{core}}\subseteq K$ and $H_{\mathrm{core}}\subseteq H$, which proves the least-pair assertion.
455 
456 Minimizing one coordinate alone does not make the whole record unique. One may add an irrelevant node without changing the least justification set, or retain an unused rule without changing the least node set. The componentwise statement avoids this ambiguity.
457 \end{proof}
458 
459 \begin{corollary}[Linear extraction]
460 \label{res:4:4}
461 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.
462 \end{corollary}
463 
464 This bound concerns the indexed graph algorithm. It is not a verified running-time bound for every scanning routine in the reference Python package.
465 
466 \begin{figure}[htbp]
467 \centering
468 \includegraphics[width=\linewidth]{fig_02_and_dag_core.pdf}
469 \caption{The canonical \protect\path{and_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.}
470 \label{fig:andcore}
471 \end{figure}
472 
473 \begin{remark}
474 \label{res:4:5}
475 The theorem identifies the minimum certificate for the recorded derivation. It does not claim that the derivation is globally shortest among all possible proofs of the theorem. A different proof field may have a smaller core.
476 \end{remark}
477 
478 
479 \section{Alternative derivations and certificate complexity}
480 \label{sec:old5}
481 
482 When a claim admits several certified justifications, certificate extraction is no longer a backward closure problem. A local choice may be reused by several later obligations, which couples decisions across the field.
483 
484 \begin{problem}[Minimum Certificate Decision]
485 \label{res:5:1}
486 Given a finite acyclic certified proof field, a target set, nonnegative integer node and justification costs, and a budget $B$, determine whether a certificate of total cost at most $B$ exists.
487 \end{problem}
488 
489 \begin{theorem}[Minimum certificate selection is NP-complete]
490 \label{res:5:2}
491 \label{thm:minimum-certificate}
492 Minimum Certificate Decision is NP-complete, even when every nonzero cost is a unit node cost and all justification costs are zero.
493 \end{theorem}
494 
495 \begin{proof}
496 The problem belongs to NP. A proposed node and justification set can be checked in polynomial time by verifying references, computing derivability in topological order, and summing costs.
497 
498 For NP-hardness, reduce Set Cover. Let $U=\{u_1,\ldots,u_m\}$ be the universe, let $S_1,\ldots,S_n\subseteq 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\in S_i$, add a certified justification
499 \[
500 \{s_i\}\Longrightarrow e_j.
501 \]
502 Add a zero-cost target node $t$ with the certified justification
503 \[
504 \{e_1,\ldots,e_m\}\Longrightarrow t.
505 \]
506 The dependency graph is acyclic. A certificate for $t$ must derive every $e_j$. Deriving $e_j$ requires at least one selected source node $s_i$ with $u_j\in S_i$. One selected $s_i$ may discharge several obligations, and its cost is paid once. Therefore a certificate of cost at most $k$ exists exactly when the original Set Cover instance has a cover of size at most $k$. The reduction is polynomial.
507 \end{proof}
508 
509 \begin{figure}[htbp]
510 \centering
511 \includegraphics[width=\linewidth]{fig_04_certificate_complexity.pdf}
512 \caption{The 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.}
513 \label{fig:setcover}
514 \end{figure}
515 
516 \begin{remark}[Algorithmic consequence]
517 \label{res:5:3}
518 Exhaustive certificate selection is useful for small fields or fields with few alternatives. The reference implementation uses branch and bound with an explicit search-state limit. Its result is optimal for the stored finite cost data when the search completes. It does not remove the exponential worst case. The decision theorem concerns integer costs, while the Python interface accepts finite floating-point costs and compares their exact stored binary values as rationals. Printed cost totals remain floating-point summaries. The input conversion does not recover an intended real or decimal value that was never represented. See \cite{garey-johnson} for the background complexity language.
519 \end{remark}
520 
521 
522 \section{Certified paths as a category}
523 \label{sec:old6}
524 
525 The hypergraph model records local justifications. A complementary construction treats complete certified transformations as morphisms. It uses the usual category of paths \cite{maclane}.
526 
527 \begin{definition}[Certified proof category]
528 \label{res:6:1}
529 Fix a directed graph of typed mathematical states and certified primitive transformations. Its path category $\mathsf{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.
530 \end{definition}
531 
532 A state may be a proposition, a diagram, an exact finite computation, a coordinate representation, or a structured collection of claims. Candidate analogies may live in a larger discovery graph, but they do not enter $\mathsf{Cert}$ until their logical force and domain have been certified.
533 
534 \begin{proposition}[Functorial transport]
535 \label{res:6:2}
536 Let $F:\mathsf{Cert}_1\to\mathsf{Cert}_2$ be a functor. If
537 \[
538 A\xrightarrow{f_1}S_1\xrightarrow{f_2}\cdots\xrightarrow{f_r}B
539 \]
540 is a certified path in $\mathsf{Cert}_1$, then
541 \[
542 F(A)\xrightarrow{F(f_1)}F(S_1)\xrightarrow{F(f_2)}\cdots\xrightarrow{F(f_r)}F(B)
543 \]
544 is a certified path in $\mathsf{Cert}_2$.
545 \end{proposition}
546 
547 \begin{proof}
548 A functor maps objects to objects and morphisms to morphisms. It preserves identities and composition. The image of the composite path is therefore the composite of the image morphisms, which is certified in the target category.
549 \end{proof}
550 
551 The proposition transports certification inside the two declared categories. To interpret that transport as preservation of a mathematical judgment, the target category and functor must also have sound interpretations of their objects and rules. These requirements cannot be inferred merely from the word functor. Under that contract, different representations can preserve a judgment while exposing different features of its argument. The category language is standard \cite{maclane}.
552 
553 \begin{definition}[Compositional certificate map]
554 \label{res:6:3}
555 A compositional certificate map is a functor
556 \[
557 \Ccal:\mathsf{Expanded}\longrightarrow\mathsf{Certificate}
558 \]
559 that sends expanded certified paths to checkable certificate paths and preserves identity and composition.
560 \end{definition}
561 
562 \begin{proposition}[Local audit composes]
563 \label{res:6:4}
564 If every primitive morphism in a finite path has an auditable certificate and the certificate map is compositional, then the composite path is auditable from the primitive certificates and the declared composition rules.
565 \end{proposition}
566 
567 \begin{proof}
568 Proceed by induction on path length. The length-zero case is an identity. Assume the first $r$ morphisms have an auditable composite certificate and append one certified morphism. Functoriality identifies the new certificate with the composition of the earlier certificate and the primitive certificate of the appended morphism. The declared composition rule completes the audit.
569 \end{proof}
570 
571 
572 \monographpart{Coherent realization and information}{Coherent realization}{Compatibility, extension, obstruction, and ambiguity become concrete once the views and protected observations are specified. This part gives the actual bridge to Komorebi Space.}
573 
574 \section{Komorebi Space, realization fibers, and informative questions}
575 \label{sec:old23}
576 \label{sec:komorebi-bridge}
577 
578 Komorebi Space supplies a natural setting for studying the proof field's coherent realizations. Here the connection is \emph{relative} to an explicitly chosen system of views. Nothing in a finite proof hypergraph canonically supplies one universal category of all proofs, and a formal proof term is not automatically equivalent to an intended semantic object. The view system must be stated, together with its restrictions and the observations that are required to survive.
579 
580 \begin{definition}[Coherent views of a proof field]
581 \label{res:23:1}
582 Choose a finite collection of views $V$, fibers $F_v$ of local proof states or annotations, and for each declared directed edge $e:v\to w$ a restriction map $e^*:F_w\to F_v$. The \emph{strict realization set} is
583 \[
584 \Gamma(F)=\big\{(x_v)\in\prod_{v\in V}F_v : e^*(x_w)=x_v\text{ for every declared edge }e\big\}.
585 \]
586 The \emph{extension fiber} of prescribed information $s$ on $U\subseteq 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 obligations.
587 \end{definition}
588 
589 The finite implementation \path{ambient.py} realizes this edge-defined model exactly. The gluing condition should not be weakened to covering the objects alone: a compatibility equation is attached to an edge and must appear in at least one patch.
590 
591 \begin{theorem}[Finite arrow-cover gluing]
592 \label{res:23:2}
593 Suppose patches $U_i\subseteq 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\in\Gamma(F)$ restricting to every $s_i$.
594 \end{theorem}
595 \begin{proof}
596 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\to w$, choose a patch containing both endpoints. The local assignment on that patch obeys $e^*s(w)=s(v)$, so the global assignment is coherent. It is the only possible glue because every coordinate was prescribed by at least one patch.
597 \end{proof}
598 
599 \begin{example}[Object coverage cannot replace arrow coverage]
600 \label{res:23:3}
601 Let $V=\{v,w\}$ with an edge $v\to w$, both fibers $\{0,1\}$, and identity restriction. Singleton patches prescribe $s(v)=0$ and $s(w)=1$. These assignments cover all views and agree on their empty overlap. There is no global coherent assignment with those coordinates. The missing ingredient is the edge condition, not the availability of the two individual values.
602 \end{example}
603 
604 The theorem is a finite instance of the strict gluing construction in \emph{Komorebi Space} \cite{komorebi-space}. It does not claim a general stack theorem for nonabelian proof objects. Gluing up to isomorphism requires the identifications and their coherence witnesses, which are retained in the corresponding groupoid setting.
605 
606 \subsection{Exact finite realization and obstruction certificates}
607 
608 A second connection is quantitative. Work over $\mathbb F_2$ with $E=\mathbb F_2^n$. Let $A:E\to\mathbb F_2^m$ impose coherence, $P:E\to\mathbb F_2^p$ retain prescribed information, and $x\in E$ be a raw candidate. Define
609 \[
610 \mathfrak K_P(x)=\{y\in E:Ay=0,\ Py=Px\},\qquad
611 M=\begin{bmatrix}A\\P\end{bmatrix},\quad
612 b=\begin{bmatrix}0\\Px\end{bmatrix}.
613 \]
614 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.
615 
616 \begin{theorem}[Finite realization alternative and ambiguity]
617 \label{res:23:4}
618 Exactly one of the following holds:
619 \begin{enumerate}[label=\textup{(\roman*)}]
620 \item $My=b$ has a solution $y_0$. Its complete solution set is $y_0+H$, where $H=\ker A\cap\ker P$, and
621 \[
622 |\mathfrak K_P(x)|=2^{n-\operatorname{rank}(M)}.
623 \]
624 \item A row vector $\lambda$ exists with $\lambda M=0$ and $\lambda b=1$. It is a directly checkable certificate that $\mathfrak K_P(x)=\varnothing$.
625 \end{enumerate}
626 \end{theorem}
627 \begin{proof}
628 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-\operatorname{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 $\lambda$. Conversely such a witness contradicts any proposed equation $My=b$, since it would imply $0=\lambda My=\lambda b=1$. These cases are mutually exclusive and exhaustive over a field.
629 \end{proof}
630 
631 This negative certificate is a concrete instance of the protected obstruction principle from Komorebi Space. Its scope is exactly the finite linear system $My=b$. It is not a certificate that some broad mathematical conjecture is unprovable.
632 
633 \subsection{The information gained by a new observation}
634 
635 Suppose the realization fiber is nonempty and a new linear observation $Q:E\to\mathbb 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.
636 
637 \begin{theorem}[Exact observation gain]
638 \label{res:23:5}
639 Give the nonempty finite affine fiber $y_0+H$ the uniform distribution. Then the Shannon entropy of the observed value $Qy$ is
640 \[
641 H(Qy)=\operatorname{rank}(Q|_H)\quad\text{bits}.
642 \]
643 For every observation value that actually occurs, the corresponding conditional fiber contains
644 \[
645 2^{\dim H-\operatorname{rank}(Q|_H)}
646 \]
647 realizations. Thus the uncertainty reduction is exactly $\operatorname{rank}(Q|_H)$ bits.
648 \end{theorem}
649 \begin{proof}
650 The image $Q(H)$ is a vector subspace of dimension $r=\operatorname{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\cap\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}$.
651 \end{proof}
652 
653 \begin{example}[One informative question]
654 \label{res:23:6}
655 Let $y=(a,b,c)\in\mathbb 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.
656 \end{example}
657 
658 The module \path{realization.py} computes these quantities through exact binary row reduction, and returns an explicit linear witness when the protected realization is impossible. The program does not enumerate all solutions, although the tests compare its results with exhaustive enumeration on small cases. The entropy statement uses Shannon entropy \cite{cover-thomas} and assumes uniform sampling of the compatible realizations. It does not assert a universal prior over mathematical discoveries, or that the most informative observation is automatically the most valuable research question once costs and task priorities are included.
659 
660 
661 \section{A checked realization bridge for proof fields}
662 \label{sec:old24}
663 \label{sec:checked-bridge}
664 
665 The ambient interpretation can be made into a mathematical construction rather than left as an analogy. The important step is to specify what a local realization means. A node label may describe an arbitrary mathematical sentence, but a Boolean value attached to that node does not automatically evaluate that sentence. In this section it records membership in a set closed under the declared certified rules. This restricted interpretation has an exact soundness and completeness theorem. An interpretation in actual mathematical propositions is a separate contract.
666 
667 \subsection{The declared rule system and its models}
668 
669 Fix a node set $V$, a set $L\subseteq 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
670 \[
671 S_j=A_j\cup\{c_j\}.
672 \]
673 A set $X\subseteq V$ is a \emph{model of the declared field} when $L\subseteq X$ and, for every certified $j$,
674 \[
675 A_j\subseteq X\quad\Longrightarrow\quad c_j\in X.
676 \]
677 Each justification is one implication with conjunctive premises. Alternative justifications remain separate implications. Uncertified attempts and failed-route annotations do not contribute a deduction rule merely by appearing in the archive.
678 
679 Let $\operatorname{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.
680 
681 Every declared field of this positive-implication form has a model: the full set $V$. It contains every leaf and every rule conclusion. Nonexistence in the following extension problems therefore concerns prescribed local values or additional preservation requirements, not this unrestricted model space. This does not make every node derivable. Derivability is membership in the least model, not membership in some model.
682 
683 \begin{theorem}[Soundness and relative completeness]
684 \label{res:24:1}
685 \label{thm:relative-completeness}
686 For every node $v$,
687 \[
688 v\in\operatorname{Der}_F
689 \quad\Longleftrightarrow\quad
690 \text{$v\in X$ for every model $X$ of the declared field}.
691 \]
692 If $v$ is not derivable, $\operatorname{Der}_F$ itself is a model omitting $v$.
693 \end{theorem}
694 \begin{proof}
695 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 $\operatorname{Der}_F$. Conversely, the inductive constructors show that $\operatorname{Der}_F$ contains the leaves and is closed under every certified rule. It is therefore a model. Applying the universal condition to this particular model proves the reverse implication, and the same model gives the stated countermodel.
696 \end{proof}
697 
698 This is relative completeness for the declared rule system, not completeness of arbitrary mathematical proof search. A missing theorem may simply require a rule or a lemma absent from the field. A failed search can therefore produce a useful countermodel to a proposed finite inference architecture without disproving the mathematical target.
699 
700 For an intended interpretation $\mu:V\to\mathrm{Prop}$, the transfer to mathematical truth has explicit hypotheses: every leaf must satisfy $\mu$, and every certified rule must preserve $\mu$ from all its premises to its conclusion. Under those hypotheses, induction gives $v\in\operatorname{Der}_F\Rightarrow\mu(v)$. Lean checks this statement as \path{ProofPath.Field.semantic_soundness}. It does not infer those hypotheses from a JSON certification flag.
701 
702 \subsection{From patches to a contravariant view system}
703 
704 For a patch $U\subseteq V$, let $\mathcal M_F(U)$ consist of subsets $X_U\subseteq U$ which contain $L\cap U$ and obey every certified rule whose entire support lies in $U$. If $U\subseteq W$, define
705 \[
706 \rho_{U,W}:\mathcal M_F(W)\longrightarrow\mathcal M_F(U),
707 \qquad \rho_{U,W}(X_W)=X_W\cap U.
708 \]
709 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.
710 
711 \begin{proposition}[The proof-field view laws]
712 \label{res:24:2}
713 The restriction maps satisfy
714 \[
715 \rho_{U,U}=\mathrm{id},\qquad
716 \rho_{U,W}\rho_{W,Z}=\rho_{U,Z}\quad(U\subseteq W\subseteq Z).
717 \]
718 Consequently $U\mapsto\mathcal M_F(U)$ is a contravariant set-valued view system on the inclusion order of patches.
719 \end{proposition}
720 \begin{proof}
721 Both laws are the corresponding intersection identities. For the second, $(X\cap W)\cap U=X\cap U$ because $U\subseteq W$. The values outside a patch are absent, or equivalently normalized to false in the Lean representation. There are no additional hidden coordinates.
722 \end{proof}
723 
724 The strict Komorebi realization is now an actual set of coherent local models,
725 \[
726 \Gamma(\mathcal M_F)=
727 \left\{(X_U)_U:\rho_{U,W}(X_W)=X_U\text{ whenever }U\subseteq W\right\}.
728 \]
729 There is an explicit bijection
730 \[
731 \operatorname{Models}(F)\simeq\Gamma(\mathcal M_F),
732 \qquad X\longmapsto(X\cap U)_U.
733 \]
734 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 \path{ProofPath.Field.modelEquivSections} constructs this equivalence, using \path{ViewDiagram} and the actual local restriction maps.
735 
736 The full-patch equivalence identifies the ambient construction. It does not prove that arbitrary prescribed proper-patch data extend: the full patch already contains the global problem. Extension from smaller views is the distinct content of the following theorem.
737 
738 
739 \studyhead{01}{The bridge is a restriction map}
740 For one certified rule $\{a,b\}\to c$ and no admissible leaves ($L=\varnothing$), there are seven global Boolean rule models. Only $(1,1,0)$ violates the implication. On either two-node patch below, the complete support is absent, so all four local valuations are admissible.
741 
742 \begin{figure}[H]\centering
743 \includegraphics[width=\linewidth]{fig_16_restriction_bridge.pdf}
744 \caption{The local model sets and their actual restrictions. Each arrow is $\rho_{U,W}(X)=X\cap U$. The two ways of restricting a global model to $\{c\}$ agree. The diagram is counted directly from the finite rule model, with seven global models, four models on each two-node patch, and two overlap values.}
745 \label{fig:restriction-models}
746 \end{figure}
747 
748 {\sffamily\bfseries\color{KomorebiTeal}What the diagram establishes}\par\smallskip
749 It displays the contravariant view construction and the consistency of restriction. The full-patch equivalence identifies global rule models with their coherent families of restrictions.
750 
751 \medskip
752 {\sffamily\bfseries\color{KomorebiGold}What the diagram does not establish}\par\smallskip
753 A pair of matching proper-patch models need not be in the image of a global model. That extension question is controlled by the support of the rule, as the next study shows.
754 \clearpage
755 
756 \subsection{The correct coverage condition is a whole support}
757 
758 Let $(U_i)_{i\in I}$ cover the nodes. A family $X_i\in\mathcal M_F(U_i)$ is matching when
759 \[
760 X_i\cap U_j=X_j\cap U_i\qquad\text{for every }i,j.
761 \]
762 This equality includes agreement about false values, not merely common true values.
763 
764 \begin{theorem}[Whole-support gluing]
765 \label{res:24:3}
766 \label{thm:support-gluing}
767 Suppose every certified justification has its whole support in some patch:
768 \[
769 \forall j\text{ certified},\quad\exists i\quad S_j\subseteq U_i.
770 \]
771 Then every matching family $(X_i)$ has a unique global field model $X$ satisfying $X\cap U_i=X_i$ for all $i$.
772 \end{theorem}
773 \begin{proof}
774 Set $X=\bigcup_iX_i$. Matching and node coverage imply $X\cap U_i=X_i$. A leaf belongs to some patch and hence to its local model, so $L\subseteq 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 that patch's local model, whose rule condition forces the conclusion. Hence $X$ obeys all certified rules. Any other global model with the specified restrictions agrees with $X$ at every node because the patches cover the nodes. This proves uniqueness.
775 \end{proof}
776 
777 \begin{example}[Pairwise dependencies do not suffice]
778 \label{res:24:4}
779 Take nodes $a,b,c$, no admissible leaves ($L=\varnothing$), and one certified rule
780 \[
781 \{a,b\}\longrightarrow c.
782 \]
783 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 replacing a conjunctive hyperedge by unrelated pairwise checks can lose precisely the constraint that matters.
784 \end{example}
785 
786 The example is kernel checked in \path{ProofPath.Examples}. It does not contradict the earlier arrow-cover theorem. That theorem applies to a problem already specified by binary restriction equations. A conjunctive proof rule is a different constraint until a correct representation of its whole support has been supplied. The full support may be redundant in particular fields, so the theorem gives a sufficient cover condition rather than a necessary one for every individual diagram. Section~\ref{sec:semantic-cover} gives an exact entailment criterion for those redundancies.
787 
788 The Python class \path{ProofFieldViews} implements these definitions. It freezes the rule and leaf contents at construction, restricts local valuations by literal intersection, checks support coverage before gluing, and can form a finite intersection-closed diagram for \path{FiniteViewSystem}. Local enumeration has explicit size limits. Forward closure and declared-field countermodels do not require that enumeration.
789 
790 
791 \studyhead{02}{Agreement can hide a missing rule}
792 Keep the same rule and choose the local data $X_0=\{a\}$ on $U_0=\{a,c\}$ and $X_1=\{b\}$ on $U_1=\{b,c\}$. Both local models assign false to their shared coordinate $c$. They match exactly, yet their only assembled valuation violates the global rule.
793 
794 \begin{figure}[H]\centering
795 \includegraphics[width=\linewidth]{fig_15_whole_support.pdf}
796 \caption{The explicit counterexample to replacing whole-support coverage with pairwise dependency coverage. The local data force $(a,b,c)=(1,1,0)$, so both premises hold and the conclusion fails. Green nodes carry value one and open nodes carry value zero.}
797 \label{fig:whole-support-example}
798 \end{figure}
799 
800 {\sffamily\bfseries\color{KomorebiTeal}The successful gluing argument}\par\smallskip
801 A patch containing the entire support $\{a,b,c\}$ must enforce the conjunctive rule. If all local models match and every certified support occurs in a patch, their union obeys every rule. Node coverage then gives uniqueness. This is the content of Theorem~\ref{thm:support-gluing}, not an inference from pairwise agreement alone.
802 
803 \medskip
804 The cover condition is sufficient for all matching data. It need not be necessary for an individual field whose other rules already make a support constraint redundant.
805 \clearpage
806 
807 \subsection{Protected realization over a field}
808 
809 The exact binary model admits a general algebraic formulation. Let $K$ be a field, let $E,R,S$ be $K$-vector spaces, and let $D:E\to R$ and $p:E\to S$ be linear. The prescribed problem is to repair $x$ while retaining $p(x)$:
810 \[
811 Dy=0,\qquad p(y)=p(x).
812 \]
813 The admissible correction image is $B=D(\ker p)$. The elementary correction equivalence gives feasibility exactly when $Dx\in B$.
814 
815 \begin{theorem}[A linear certificate alternative]
816 \label{res:24:5}
817 \label{thm:linear-alternative}
818 The protected problem is infeasible if and only if there is a linear functional $\lambda:R\to K$ satisfying
819 \[
820 \lambda(Dh)=0\quad\text{whenever }p(h)=0,
821 \qquad \lambda(Dx)=1.
822 \]
823 For a finite matrix $M$ and right side $b$, the corresponding alternative is
824 \[
825 \nexists y\ (My=b)
826 \quad\Longleftrightarrow\quad
827 \exists\ell\ (\ell M=0\ \text{and}\ \ell b=1).
828 \]
829 \end{theorem}
830 \begin{proof}
831 If $Dx\notin 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 the basis of $B$ and value one to $Dx$, and extend linearly. Equivalently, normalize any separating functional by its nonzero value. Conversely, if $y$ were feasible, then $h=x-y$ would satisfy $p(h)=0$ and $Dh=Dx$, contradicting the displayed functional equations. For a matrix, take $B$ to be its column image. In finite coordinates the separating functional is a row vector, giving the stated alternative.
832 \end{proof}
833 
834 The general existence proof is classical. It does not claim an efficient procedure for arbitrary infinite spaces. In the implemented binary case, Gaussian elimination constructs a row witness, and the witness is checked against the original matrix and right side. A positive solution and a normalized negative witness cannot both verify.
835 
836 
837 \studyhead{03}{An obstruction is a checkable equation}
838 In the binary example from \path{data/bridge_examples.json}, compatibility demands $a+b=0$ while the protected observations require $a=0$ and $b=1$. The variable $c$ is unconstrained. Its freedom cannot remove the incompatible requirement on the first two coordinates.
839 
840 \begin{figure}[H]\centering
841 \includegraphics[width=\linewidth]{fig_19_obstruction_witness.pdf}
842 \caption{A normalized negative witness in $\mathbb F_2$. Adding the three rows gives zero on the left and one on the right. The witness is $\ell=(1,1,1)$, which satisfies $\ell M=0$ and $\ell b=1$ for the original stacked system.}
843 \label{fig:obstruction-witness}
844 \end{figure}
845 
846 The exact system and witness can be inspected without trusting a search procedure:
847 \[
848  M=\begin{pmatrix}1&1&0\\1&0&0\\0&1&0\end{pmatrix},\qquad
849  b=\begin{pmatrix}0\\0\\1\end{pmatrix},\qquad
850  \ell M=(0,0,0),\quad \ell b=1.
851 \]
852 If $My=b$ had a solution, multiplying by $\ell$ would give $0=1$. This is a certificate for the declared protected problem. A search that merely stops supplies no comparable implication.
853 \clearpage
854 
855 \subsection{Counting what remains after an observation}
856 
857 Let $T:E\to R$ and $Q:E\to W$ be linear, and fix a known point $x_0$. Put
858 \[
859 \mathcal A=\{y:Ty=Tx_0\},\quad H=\ker T,\quad
860 Q_H=Q|_H.
861 \]
862 Translation $h\mapsto x_0+h$ identifies $H$ with $\mathcal 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$.
863 
864 \begin{theorem}[Exact observation counts]
865 \label{res:24:6}
866 \label{thm:checked-counts}
867 Suppose $K$ is a finite field of cardinality $q$ and $E$ is a finite-dimensional $K$-vector space. Set
868 $k=\dim_K H$ and $r=\dim_K Q(H)$. Then
869 \[
870 |\mathcal A|=q^k,\qquad
871 |Q(\mathcal A)|=q^r,\qquad
872 |\{y\in\mathcal A:Qy=Qx_0\}|=q^{k-r}.
873 \]
874 In particular the exact count identity is
875 \[
876 |\mathcal A|=
877 |\{y\in\mathcal A:Qy=Qx_0\}|\,q^r.
878 \]
879 Every attained observation fiber has the same size. For the uniform distribution on $\mathcal A$, the observation removes exactly $r\log_2q$ bits of uncertainty.
880 \end{theorem}
881 \begin{proof}
882 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 $\dim\ker Q_H+r=k$, proving the product identity and all the counts. An attained value can be treated by choosing a point attaining it as the base point. Equal fiber sizes imply a uniform observation distribution and a uniform conditional distribution on each fiber. The entropy difference is therefore $\log_2(q^k)-\log_2(q^{k-r})=r\log_2q$.
883 \end{proof}
884 
885 Lean checks the translation equivalences, rank-nullity specialization, fiber cardinalities, and product identity in \path{ProofPath.Protected}, with the binary specialization in \path{ProofPath.Binary}. The logarithmic entropy interpretation is the written corollary above, not a newly compiled theorem about a Lean probability distribution. Uniformity is substantive. With a nonuniform prior, dimension alone does not determine Shannon information.
886 
887 For the protected problem, set $T=(D,p)$ and choose an actual feasible $y_0$, so $Ty_0=(0,px)$. This reduces its solution fiber to the theorem without changing the protected values. A concrete binary example has $a+b+c=0$ and $a=0$. Its two realizations are $(0,0,0)$ and $(0,1,1)$. Observing $b$ has rank one on the ambiguity space and determines the remaining coordinate. Repeating the same observation in two output rows does not double the information.
888 
889 
890 \studyhead{04}{Ask what an observation distinguishes}
891 Return to the two vertices $000$ and $011$ from the opening cube. The ambiguity space is the span of $011$. Reading the protected coordinate $a$ repeats known information. Reading $b$ separates the two points. Reading $b$ twice creates two output rows but no additional distinction.
892 
893 \begin{figure}[H]\centering
894 \includegraphics[width=\linewidth]{fig_18_observation_partitions.pdf}
895 \caption{Three observation maps on the same feasible binary fiber. The last column is the size of each attained conditional fiber. Gains of zero, one, and one bit follow from the rank of the map restricted to $H$, under the uniform distribution. The duplicated output is not twice as informative.}
896 \label{fig:observation-partitions}
897 \end{figure}
898 
899 For example, the repeated observation has matrix
900 \[
901  Q=\begin{pmatrix}0&1&0\\0&1&0\end{pmatrix}.
902 \]
903 Its two rows are identical. On $H=\langle011\rangle$ it has rank one, so $|\mathcal A|=2$, $|Q(\mathcal A)|=2$, and every attained observation fiber has size one. These are count identities before they are interpreted probabilistically.
904 
905 \medskip
906 The general finite-field formula in Theorem~\ref{thm:checked-counts} retains the same separation: $q^k$ initial possibilities, $q^r$ attained outcomes, and $q^{k-r}$ realizations per outcome.
907 \clearpage
908 
909 \subsection{Executable witnesses and a native declaration export}
910 
911 Four exact examples are regenerated from the Python implementation: a one-bit ambiguity, an incompatible protected assignment, a redundant observation, and a uniquely determined realization. The generator emits the original stacked matrices and right sides alongside the proposed solutions or row witnesses. It also emits Lean declarations which check those concrete equations and cardinalities by kernel reduction. A faulty generator cannot make a false displayed proposition pass merely by assigning a certification flag. The generator itself is not thereby verified for arbitrary inputs, and the correspondence between the supplied JSON input and its emitted Lean syntax remains an audited software boundary.
912 
913 A separate native exporter reads five already compiled Lean declarations, extracts their direct type and proof-constant dependencies, and records the transitive axiom sets. Dependencies outside the selected roots are explicit external leaves. This yields an actual proof-field JSON record rather than a hand-authored imitation of one. The exported field is then loaded through the public Python importer, and its declared closure is checked to contain its roots.
914 
915 The export has a deliberately narrow meaning. It is syntactic dependency data for selected declarations, not a reconstruction of the entire discovery process. It does not recover failed attempts, prove that every constant in a type was a historically essential idea, or formally verify the metaprogram that extracts the data. The mathematical proof-field bridge is checked independently of that metaprogram. Its semantic interpretation retains the explicit hypotheses in Theorem~\ref{thm:relative-completeness}.
916 
917 \subsection{Verification scope and reproducibility}
918 
919 The present release freshly builds eighteen production Lean modules in a new object directory. Each module is replayed through Lean's own kernel against the pinned imported environment. The nine dependency revisions and the compiler hash are checked before building. All explicit named source declarations receive an axiom audit against the declared whitelist. The thirteen preceding mathematical modules are unchanged. Five new modules add executable trace checking, finite witness completeness, a typed JSON codec, and checked exchange examples.
920 
921 Ten deliberately invalid files test false conclusions, missing support, placeholders, invalid decoders, merged observations, forged or incomplete closures, and a Boolean used as a node index. A further file introduces an explicit false axiom. Lean correctly accepts a consequence relative to that axiom, while the release's separate axiom policy rejects the dependency. A missing import, unavailable decision procedure, or timeout does not count as a mathematical rejection.
922 
923 The fresh record is in \path{evidence/formal_1.8.0/}. The older record remains separately identified. Kernel replay here is not an independent implementation of Lean and does not rebuild or replay the entire cached Mathlib library. Written proofs, general Lean statements, generated concrete examples, and Python tests remain different evidence categories. In particular, a sound mathematical algorithm does not make its Python implementation universally verified.
924 
925 \subsection{Protected extensions of the actual rule field}
926 \label{sec:protected-rule-extension}
927 
928 The linear model is not the only setting in which an obstruction can be returned explicitly. The original rule field has its own constructive extension problem. A partial Boolean description records which nodes must belong to a model and which must remain absent. These are observations about the declared model, not assertions that the sentences attached to the nodes are true or false in an intended mathematical universe.
929 
930 Fix the field $F$, including its admitted leaves and certified rules. For a positive observation set $S\subseteq V$, let
931 \[
932   \operatorname{cl}_F(S)=\operatorname{Der}_{F[S]},
933 \]
934 where $F[S]$ is obtained by admitting $L\cup S$ as leaves and changing nothing else. For a negative observation set $N\subseteq V$, define
935 \[
936  \operatorname{Ext}_F(S,N)=
937  \{X\subseteq V:X\text{ is an }F\text{-model},\ S\subseteq X,\ X\cap N=\varnothing\}.
938 \]
939 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.
940 
941 \begin{theorem}[Least protected extension and a complete obstruction]
942 \label{res:new:extension}
943 The extension fiber is nonempty exactly when
944 \[
945  \operatorname{cl}_F(S)\cap N=\varnothing.
946 \]
947 When this condition holds, $\operatorname{cl}_F(S)$ is its least member. More generally,
948 \[
949  X\in\operatorname{Ext}_F(S,N)
950  \quad\Longleftrightarrow\quad
951  X\text{ is an }F\text{-model and }
952  \operatorname{cl}_F(S)\subseteq X\subseteq V\setminus N.
953 \]
954 If no extension exists, some $n\in N$ has a derivation from $L\cup S$ using only the declared certified rules.
955 \end{theorem}
956 \begin{proof}
957 Induction on a derivation shows that every model containing $S$ contains $\operatorname{cl}_F(S)$. The inductive closure is itself a model and contains $S$. If it avoids $N$, it is therefore a permitted extension, and the preceding inclusion proves leastness. If it meets $N$, every model containing $S$ contains a forbidden node, so no extension is possible. The displayed classification follows from the same inclusions. A point of the nonempty intersection is exactly the conclusion of the stated forbidden-node derivation.
958 \end{proof}
959 
960 This describes an interval \emph{inside the family of rule models}, not an arbitrary interval of the power set. Closure under the rules remains essential. Nor is the fiber generally an affine space. For the rule $\{a,b\}\to c$, with no leaves, $S=\varnothing$ and $N=\{c\}$, the allowed models are precisely $\varnothing$, $\{a\}$, and $\{b\}$. There are three, not a power of two. The rank and entropy formulas for vector spaces cannot be imported into this model without additional structure.
961 
962 \begin{corollary}[Exact extension of a partial valuation]
963 \label{res:new:partial}
964 Let $S\subseteq U\subseteq V$. A global model whose true nodes on $U$ are exactly $S$ exists if and only if
965 \[
966  \operatorname{cl}_F(S)\cap U=S.
967 \]
968 \end{corollary}
969 \begin{proof}
970 Set $N=U\setminus S$. Closure always contains $S$, so avoiding $N$ is equivalent to the displayed equality. Apply Theorem~\ref{res:new:extension}.
971 \end{proof}
972 
973 In particular, the test works for partial data that already violate a local rule. It need not assume local consistency and then hide that failure in a precondition. A contradictory observation can be exposed as a specific forbidden consequence.
974 
975 \begin{proposition}[Staged closure and persistent obstructions]
976 \label{res:new:stages}
977 For positive sets $S,T$,
978 \[
979  \operatorname{cl}_F\bigl(\operatorname{cl}_F(S)\cup T\bigr)
980    =\operatorname{cl}_F(S\cup T).
981 \]
982 If $S\subseteq S'$ and $N\subseteq N'$, then
983 $\operatorname{Ext}_F(S',N')\subseteq\operatorname{Ext}_F(S,N)$.
984 Consequently an infeasible request stays infeasible under those additions, while the field and the meaning of its rules remain fixed.
985 \end{proposition}
986 \begin{proof}
987 Closure is extensive, monotone, and idempotent because it is the least model containing its seed. The model $\operatorname{cl}_F(S\cup T)$ contains $\operatorname{cl}_F(S)$ and $T$, giving one inclusion in the first equation. Extensivity gives $S\cup T\subseteq\operatorname{cl}_F(S)\cup T$, and monotonicity gives the other. A model satisfying the larger positive and negative prescriptions also satisfies the smaller ones. The last conclusion follows by inclusion of the extension fibers.
988 \end{proof}
989 
990 The module \path{ProofPath.Extension} checks these statements on the existing \path{Field} type. The Python module \path{extension.py} uses the same \path{ProofFieldViews} snapshot as the local-model construction. It computes closure by forward rule scans and records each newly derived node. At most $|V|$ successful insertions occur. If a forbidden node is reached, a causal subtrace is extracted. It need not be the shortest or cheapest refutation.
991 
992 The independent result checker replays that trace and checks that the recorded closure is closed under every rule. Derivability of every recorded node and closure of the recorded set together establish leastness. A negative witness only needs a valid derivation of one forbidden node. Its replay permits a previously derived node to have become an admitted observation, so the same witness can remain valid after positive data are strengthened. The checker does not call the producer, and a timeout is never returned as an obstruction.
993 
994 
995 \begin{figure}[htbp]\centering
996 \includegraphics[width=\linewidth]{fig_23_protected_closure.pdf}
997 \caption{Two protected requests for the same rule field. With only $a$ prescribed true and $c$ prescribed false, the least model is $\{a\}$. Adding $b$ to the positive data derives the forbidden node $c$. The obstruction is the certified rule application, not the act of abandoning a search.}
998 \label{fig:protected-closure}
999 \end{figure}
1000 
1001 \subsection{Semantic covers rather than only syntactic covers}
1002 \label{sec:semantic-cover}
1003 
1004 Whole-support coverage is easy to inspect and is sufficient for gluing. It can nevertheless be unnecessarily strong. Suppose $F$ contains $a\to b$, $b\to c$, and $a\to c$, with patches $\{a,b\}$ and $\{b,c\}$. The last support $\{a,c\}$ is absent from both patches. Yet the first two visible rules already imply the last rule. Requiring another patch would duplicate information rather than restore a missing constraint.
1005 
1006 Let $\mathcal U=(U_i)_i$ cover every node. Define $F_{\mathcal 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 \emph{semantically sufficient for the declared rules} when
1007 \[
1008  \forall j\text{ certified in }F,\qquad
1009  c_j\in\operatorname{cl}_{F_{\mathcal U}}(A_j).
1010  \tag{SC}\label{eq:semantic-cover}
1011 \]
1012 The word semantic here refers to the Boolean rule-model semantics of Section~\ref{sec:old24}, not to an automatic interpretation of node labels as arbitrary mathematical truths.
1013 
1014 \begin{theorem}[Exact criterion for universal gluing]
1015 \label{res:new:semantic-cover}
1016 Under node coverage, the following conditions are equivalent:
1017 \begin{enumerate}[label=(\roman*)]
1018 \item Every matching family of local $F$-models on the patches has a unique global $F$-model extending it.
1019 \item Every model of $F_{\mathcal U}$ is a model of $F$.
1020 \item Condition~\eqref{eq:semantic-cover} holds.
1021 \item For every positive seed $S$, $\operatorname{cl}_{F_{\mathcal U}}(S)=\operatorname{cl}_F(S)$.
1022 \end{enumerate}
1023 Whole-support coverage implies these conditions, but the converse need not hold.
1024 \end{theorem}
1025 \begin{proof}
1026 A matching family assembles uniquely to a subset $X\subseteq V$ because the patches cover all nodes and agree on their common coordinates. Its local rule conditions say exactly that $X$ is a model of $F_{\mathcal U}$. Conversely, a model of $F_{\mathcal U}$ restricts to an $F$-model on every patch: every original rule supported in that patch is among the retained rules. Those restrictions match. Thus (i) and (ii) are equivalent, and uniqueness follows from node coverage.
1027 
1028 Assume (ii) and fix a certified rule $j$. The set $\operatorname{cl}_{F_{\mathcal U}}(A_j)$ is a model of $F_{\mathcal U}$ containing all of $A_j$. By (ii) it obeys the original rule and contains $c_j$, proving (iii). Conversely, if $X$ is a model of $F_{\mathcal U}$ containing $A_j$, leastness gives $\operatorname{cl}_{F_{\mathcal U}}(A_j)\subseteq X$. Condition (iii) therefore forces $c_j\in X$. Every original rule is satisfied, which proves (ii).
1029 
1030 Under (ii) the two fields have exactly the same models, since every $F$-model already obeys the retained rules. Their least models containing any seed are equal, giving (iv). If (iv) holds, apply it to $A_j$. The conclusion $c_j$ lies in $\operatorname{cl}_F(A_j)$ by the original rule, so it lies in the retained closure as required by (iii). Finally, whole-support coverage retains every certified rule. The three-rule example above proves that this condition is not necessary.
1031 \end{proof}
1032 
1033 There is a constructive negative result as well. If (SC) fails for $j$, let
1034 \[
1035  X=\operatorname{cl}_{F_{\mathcal U}}(A_j).
1036 \]
1037 Then $A_j\subseteq X$ and $c_j\notin X$. The restrictions $X\cap U_i$ are matching local $F$-models, but their only assembled subset violates the original rule. They are a checkable obstruction to \emph{universal gluing for this cover}. They do not show that every matching family on the cover fails.
1038 
1039 The module \path{ProofPath.SemanticCover} proves the criterion, including its connection to the actual \path{Local}, \path{Matching}, and \path{gluedValue} constructions. It is not a replacement field chosen only to have a convenient name. The Python producer returns a derivation of each original conclusion from its premises using only visible rules, or the countermodel just described. The verifier replays the positive derivations or checks the negative valuation directly. A new \path{glue_semantic} operation requires the positive certificate. The older \path{glue} method retains its simpler whole-support contract.
1040 
1041 \studyhead{05}{A missing support can be redundant}
1042 The patches $U_0=\{a,b\}$ and $U_1=\{b,c\}$ do not contain the support of $a\to c$. Their visible rules $a\to b$ and $b\to c$ nevertheless provide a certified derivation of that implication. Compare this with the missing conjunctive support in Figure~\ref{fig:whole-support-example}: neither visible patch there provides a substitute for $\{a,b\}\to c$.
1043 
1044 \begin{figure}[H]\centering
1045 \includegraphics[width=\linewidth]{fig_22_semantic_cover.pdf}
1046 \caption{The exact semantic-cover check for a redundant rule. The two solid rules are visible in the displayed patches. The dashed original rule has no covered whole support, but its conclusion is derived by the solid path. Dashed here means omitted from the visible subsystem, not uncertified in the original field.}
1047 \label{fig:semantic-cover}
1048 \end{figure}
1049 
1050 \calloutbox{Preserve the constraint, not necessarily its original presentation}{The cover is sufficient because its visible rules impose the same models as the full field. The criterion checks every original rule, not just the target of one successful example.}
1051 
1052 For a finite field, one closure computation per original rule is enough to produce the positive certificates or expose a failed entailment. This avoids enumerating all local valuations or all matching families. The implementation uses repeated rule scans, so the release does not claim the indexed linear-time bound for its code. Its output certificates can be verified without trusting that search procedure.
1053 \clearpage
1054 
1055 \subsection{Typed transport of derivations and obstructions}
1056 \label{sec:rule-transports}
1057 
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\to V_G$ and a rule map $h:J_F\to J_G$ satisfying
1059 \[
1060 \begin{aligned}
1061  f(L_F)&\subseteq L_G,\\
1062  j\text{ certified in }F&\Longrightarrow h(j)\text{ certified in }G,\\
1063  A^G_{h(j)}&\subseteq f(A^F_j),\\
1064  c^G_{h(j)}&=f(c^F_j).
1065 \end{aligned}
1066 \]
1067 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 by the source step. This is a sufficient, deliberately concrete transport interface. A more general translation could map one rule to an entire derivation.
1068 
1069 \begin{theorem}[Compositional rule transport]
1070 \label{res:new:transport}
1071 Rule transports admit identities and associative composition. A transport $(f,h):F\to 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,
1072 \[
1073  Y\in\operatorname{Ext}_G(f(S),f(N))
1074    \Longrightarrow f^{-1}(Y)\in\operatorname{Ext}_F(S,N).
1075 \]
1076 An obstruction in the source extension problem therefore implies an obstruction in the target extension problem with the mapped observations.
1077 \end{theorem}
1078 \begin{proof}
1079 Identity maps meet each displayed condition. For two composable transports, compose the node and rule maps. Applying the second map to the first premise inclusion and then using the second inclusion proves the composite premise condition. The conclusion and leaf conditions also compose. Function composition gives the identity and associativity laws.
1080 
1081 Proceed by induction on a source derivation. A source leaf maps to a target leaf. For a rule step, every premise of the target rule is the image of a source premise, so the induction hypotheses supply all the required target premises. Certification and the conclusion equation then give the translated conclusion.
1082 
1083 If $Y$ is a target model, $f^{-1}(Y)$ contains all source leaves. When it contains every premise of a source rule, $Y$ contains every premise of the mapped rule and hence its conclusion. This proves the model pullback. Positive and negative observations pull back by their image definitions. If a target extension existed while the source problem were infeasible, its pullback would contradict that infeasibility.
1084 \end{proof}
1085 
1086 Positive seeds can be added before transport. The same rule transport sends $F[S]$ to $G[f(S)]$, and hence
1087 \[
1088  f\bigl(\operatorname{cl}_F(S)\bigr)
1089       \subseteq\operatorname{cl}_G(f(S)).
1090 \]
1091 A forbidden source consequence $n\in N\cap\operatorname{cl}_F(S)$ maps to the explicit forbidden consequence $f(n)\in f(N)\cap\operatorname{cl}_G(f(S))$. The formal development checks this witness map, not only the existence statement obtained by contraposition.
1092 
1093 \begin{example}[Why transport is not an equivalence]
1094 \label{res:new:collapse}
1095 Let the source have nodes $a,b$, no leaves, and no rules. The request $a$ true and $b$ false is feasible. Map both nodes to one target node $u$, again with no leaves or rules. This is a rule transport, but the image request requires $u$ both true and false and is infeasible. Thus source feasibility need not imply target feasibility, and target infeasibility need not imply source infeasibility.
1096 \end{example}
1097 
1098 \path{ProofPath.RuleTransport} checks these laws for actual derivations, and \path{ProofPath.ExtensionExamples} checks the collapse. The transported conclusion is true under an intended interpretation only if the target leaves and rules are sound. Renaming alone does not provide that contract.
1099 
1100 
1101 \subsection{Executable certificates for the declared closure}
1102 \label{sec:trace-checker}
1103 
1104 A mathematical characterization of closure is not yet a correctness theorem for the program that checks a certificate. The next construction closes that boundary for an explicit Lean checker. It uses the existing \path{Field} and seeded-closure definitions, rather than replacing their meaning by the output of an algorithm.
1105 
1106 \begin{definition}[Finite indexed problem and trace]
1107 \label{res:trace:problem}
1108 An indexed problem $P$ specifies a finite address space $V_n=\{0,\ldots,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.
1109 
1110 A trace $\sigma=(j_1,\ldots,j_k)$ is a list of rule addresses. Replay begins with the list $K_0=L\mathbin{+\!+}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.
1111 \end{definition}
1112 
1113 Only rows declared certified enter this indexed rule list. The finite checker does not infer certification from a claim's label, its position in a document, or an author's confidence. An adapter that selects these rows must preserve the intended field and its assumptions.
1114 
1115 \begin{theorem}[Replay preserves derivability and composes]
1116 \label{res:trace:replay}
1117 Suppose every member of $K$ belongs to $\operatorname{cl}_F(S)$. If either replay mode accepts a trace starting from $K$ and returns $K'$, then
1118 \[
1119  K\subseteq K'\subseteq\operatorname{cl}_F(S).
1120 \]
1121 For a fixed replay mode, replaying $\sigma\mathbin{+\!+}\tau$ is the same as replaying $\sigma$ and then replaying $\tau$ from the returned state. Failure at either stage propagates to the concatenated execution.
1122 \end{theorem}
1123 \begin{proof}
1124 Induct on the trace. The empty trace returns the initial state. For a nonempty trace, a successful first step identifies a certified rule whose premises are already derivable. Closure under that rule proves its conclusion derivable. Adding the conclusion preserves all previously known nodes, and the induction hypothesis applies to the remaining trace. The stricter novelty test can reject a step but cannot invalidate this argument for an accepted one. The composition identity follows by the same induction, with the lookup and enabling tests taking the same branch on both sides.
1125 \end{proof}
1126 
1127 The functions \path{replay}, \path{enabled}, and \path{lookup} are executable definitions. The formal theorems \path{replay_sound}, \path{replay_extensive}, and \path{replay_append} concern those definitions themselves. They are not specifications assumed of an otherwise unchecked replay routine.
1128 
1129 \begin{theorem}[Acceptance identifies the least seeded model]
1130 \label{res:trace:least}
1131 A complete-closure certificate consists of a strict trace $\sigma$ and a reported node list $K$. The checker accepts precisely when replay succeeds, its output has the same members as $K$, and $K$ contains the admitted leaves and satisfies every declared rule. Acceptance implies
1132 \[
1133  \boxed{K=\operatorname{cl}_F(S).}
1134 \]
1135 Here equality means equality of the represented sets, not equality of list order.
1136 \end{theorem}
1137 \begin{proof}
1138 Theorem~\ref{res:trace:replay} gives $K\subseteq\operatorname{cl}_F(S)$ because every initial node is an admitted leaf or a positive observation. Extensivity of replay ensures that $K$ contains $S$. The final closedness test makes $K$ an $F$-model, so leastness of seeded closure gives the reverse inclusion. Both tests are needed: replay provides derivability, while the model test provides saturation under rules not used in the trace.
1139 \end{proof}
1140 
1141 The connection to the prior theory is exact. In Lean, \path{closed_iff_model} identifies the Boolean rule check with the existing \path{Field.Model} predicate, and \path{checkClosure_exact} proves the displayed equality with \path{Field.closure}. For a valid indexed problem, \path{valid_closure_bounded} proves that every member of that closure has an address below $n$. Thus totalizing rule lookup in the abstract \path{Field} cannot introduce a conclusion at an unnamed address: only successful lookups are certified.
1142 
1143 Logical meaning remains a separate, explicit hypothesis. If an interpretation $\mu:V_n\to\mathrm{Prop}$ satisfies the admitted leaves and rules, and every observation in $S$ is true under $\mu$, then every member of an accepted closure is true under $\mu$. This follows by applying the prior model-soundness theorem to the derived nodes. Acceptance does not establish the truth of arbitrarily attached sentence labels.
1144 
1145 \subsection{Finite witnesses for forbidden consequences}
1146 \label{sec:trace-obstruction}
1147 
1148 \begin{definition}[Checked forbidden-node witness]
1149 \label{res:trace:witness}
1150 A witness is a pair $(v,\tau)$, consisting of a target address and a causal trace. Its checker accepts when replay from $L\cup S$ succeeds, the returned state contains $v$, and $v\in N$.
1151 \end{definition}
1152 
1153 \begin{theorem}[Sound and complete obstruction witnesses]
1154 \label{res:trace:complete}
1155 For the finite-premise indexed rule field,
1156 \[
1157  \boxed{
1158  \text{an accepted forbidden-node witness exists}
1159  \quad\Longleftrightarrow\quad
1160  \operatorname{Ext}_F(S,N)=\varnothing.
1161  }
1162 \]
1163 The statement does not require the dependency graph to be acyclic.
1164 \end{theorem}
1165 \begin{proof}
1166 An accepted witness derives a node in $N$. Every model containing $L\cup S$ contains that node, so no protected extension exists.
1167 
1168 Conversely, Theorem~\ref{res:new:extension} gives a forbidden node with an inductive derivation. Every such derivation has a finite causal trace. For an admitted leaf or observation, the empty trace suffices. For a rule application, obtain a trace for each of its finitely many premises by induction, concatenate those traces, and append the rule address. Previously derived nodes are never removed. A trace valid from one known set remains valid from a larger known set in causal mode, so the premise traces remain valid when concatenated. Repeated conclusions are allowed, including when an earlier premise trace already established one. The resulting trace derives the forbidden node and is accepted.
1169 \end{proof}
1170 
1171 This proof explains the two replay modes. A causal witness can be reused after stronger positive observations make one of its intermediate conclusions already known. Requiring novelty at that point would reject a sound explanation. A complete-closure trace instead records fresh insertions and uses a separate final saturation test. The two contracts should not be conflated.
1172 
1173 The Lean development proves trace weakening, strict-to-causal replay, finite premise-trace assembly, and \path{derivation_has_trace} before proving \path{witness_exists_iff_infeasible}. Witness existence is not a claim that a particular search procedure finds the shortest trace, nor is it a bound on the time taken by a Python producer.
1174 
1175 \clearpage
1176 \studyhead{06}{Why replay and closedness are both necessary}
1177 \label{study:trace}
1178 
1179 Take $V_4=\{0,1,2,3\}$, $L=\{0\}$, $S=\varnothing$, and the two rules $r_0:0\to1$ and $r_1:1\to2$. The least closure is $\{0,1,2\}$. Node $3$ has no derivation from these inputs.
1180 
1181 \begin{figure}[H]\centering
1182 \includegraphics[width=\linewidth]{fig_24_trace_contract.pdf}
1183 \caption{Replay and the final model test establish opposite inclusions. Together they identify the least closure. The two rejected records fail different obligations. Changing only the forbidden set changes the correct feasibility verdict without changing the closure.}
1184 \label{fig:trace-contract}
1185 \end{figure}
1186 
1187 The trace $[0]$ derives exactly $\{0,1\}$ but leaves $r_1$ enabled with its conclusion absent. It is a valid partial derivation, not a complete closure. Conversely, $\{0,1,2,3\}$ is closed under both rules, but replay cannot establish its unsupported node $3$. A model need not be the least model.
1188 
1189 With $N=\{3\}$, the exact closure gives a positive result. With $N=\{2\}$, the same closure supports a negative result with witness $(2,[0,1])$. The second problem is not a different interpretation of the same request: its protected observations have changed. A checker must receive the fixed request separately from the proposed answer.
1190 
1191 \clearpage
1192 \begin{corollary}[Meaning of a complete result certificate]
1193 \label{res:trace:verdict}
1194 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$,
1195 \[
1196  C.K=\operatorname{cl}_F(S),\qquad
1197  \bigl(C.\mathrm{feasible}=\mathrm{true}\bigr)
1198  \Longleftrightarrow
1199  \operatorname{Ext}_F(S,N)\ne\varnothing.
1200 \]
1201 \end{corollary}
1202 \begin{proof}
1203 The complete-closure check proves the first equality. In the positive branch, the closure is a model containing $S$ and avoiding $N$, hence is an extension. In the negative branch, the witness excludes every extension by Theorem~\ref{res:trace:complete}. Case analysis on the Boolean flag gives the equivalence.
1204 \end{proof}
1205 
1206 A bare negative witness has its own checker and does not need a saturated closure. The complete result format asks for both because it promises both an exact closure and a feasibility verdict. Failure of either check means that this certificate was not accepted. It is not itself a refutation of the protected problem.
1207 
1208 \subsection{Typed exchange and the boundary of serialization}
1209 \label{sec:trace-wire}
1210 
1211 A certificate is useful outside its producer only when the receiving system knows exactly which data it checked. The exchange format therefore uses versioned positional arrays, exact nonnegative integer tokens, literal Booleans, and explicit rule addresses. Problem and certificate are separate records. The node address book and the selected certified-rule order remain associated with the originating proof-field snapshot.
1212 
1213 At the JSON syntax-tree level, the problem has the shape
1214 \begin{lstlisting}[language={}]
1215 ["proof-path/problem/1", node_count, leaves, rules, positive, negative]
1216 \end{lstlisting}
1217 where each rule is \texttt{[premises, conclusion]}. The certificate has the shape
1218 \begin{lstlisting}[language={}]
1219 ["proof-path/certificate/1", feasible, closure, trace, obstruction]
1220 \end{lstlisting}
1221 where an obstruction is either \texttt{null} or \texttt{[target, trace]}. Array lengths and tags are exact. A Boolean is not an integer address, and the string \texttt{"false"} is not a Boolean verdict. Duplicate node entries are rejected by validity checks, while identical rule rows at different addresses remain distinguishable.
1222 
1223 \begin{theorem}[Lossless encoding at the typed syntax boundary]
1224 \label{res:trace:codec}
1225 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$,
1226 \[
1227  d_P(e_P(P))=\operatorname{some}(P),\qquad
1228  d_C(e_C(C))=\operatorname{some}(C).
1229 \]
1230 Consequently both encoders are injective on their typed domains. These identities do not require the encoded record to pass the separate validity checks.
1231 \end{theorem}
1232 \begin{proof}
1233 The natural-number and Boolean constructors decode to their original values. Induction on a list proves the corresponding array round trip. The rule, witness, and optional-witness decoders then recover their components. Unfolding the exact-length record encoders and decoders gives the two identities. If two encoded records are equal, applying the decoder gives equal \texttt{some} values, hence equal original records.
1234 \end{proof}
1235 
1236 \begin{theorem}[Accepted JSON records certify their decoded answer]
1237 \label{res:trace:json}
1238 Suppose the JSON checker accepts the separately supplied problem and certificate syntax trees. Then both decode to typed records $P,C$, both pass their index and shape checks, and the decoded certificate satisfies the closure equality and feasibility equivalence of Corollary~\ref{res:trace:verdict} for that decoded problem.
1239 \end{theorem}
1240 \begin{proof}
1241 The executable checker rejects any failed decoding or validity check. In the remaining branch it calls the same complete result checker used in Corollary~\ref{res:trace:verdict}. Its acceptance therefore supplies that corollary's hypothesis. The round-trip identities additionally show that checking encoded typed records agrees with checking those records directly.
1242 \end{proof}
1243 
1244 The general proof ends at Lean's \path{Json} syntax-tree interface. It does not prove the correctness of the standard text parser, printer, file system, Python interpreter, or name-to-index adapter. The command-line reader is executed on actual canonical bytes and compared with an independent finite model oracle. That conformance test complements the formal theorem without extending its quantified scope.
1245 
1246 Canonical standalone files use compact ASCII JSON with an optional final newline. Decimal or exponent spellings, alternative internal whitespace, extra fields, and duplicate object-key constructions are outside this exchange contract. The format uses no objects. Resource limits are explicit operational rejections, not evidence that a protected realization is impossible. The encoder's injectivity is a statement about retained data, not a collision-freedom claim for a later cryptographic hash.
1247 
1248 The package supplies actual named-field exports, a separate indexed Python checker, the Lean text adapter, and generated Lean fixtures for six concrete exchanges. Their role is to test the entire executed route as well as its proved core. The original named proof fields remain finite and acyclic. Cyclic examples belong to the lower-level indexed checker and show that its soundness theorem does not depend on topological sorting. An unseeded cycle supplies no finite derivation merely by referring to itself.
1249 
1250 
1251 \monographpart{Compression, representation, and memory}{Compression and memory}{Compression changes which questions can still be answered. A certificate may preserve every required deduction while erasing distinctions that later inquiry needs.}
1252 
1253 \section{Compression relative to a task family}
1254 \label{sec:old7}
1255 
1256 A representation is sufficient only relative to specified questions and a specified class of possible archives. Fix a set $\mathscr A$ of admissible proof archives. A representation scheme is a map $C:\mathscr A\to\mathscr R$. Its output for an archive $\Pcal$ is $C(\Pcal)$. Distinguishing the scheme from one output is essential: a decoder chosen only after seeing one fixed archive could simply store the answer.
1257 
1258 \begin{definition}[Task]
1259 \label{res:7:1}
1260 A task is a map $q:\mathscr A\to Y_q$ to a declared answer set. A task family $\Qcal$ 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.
1261 \end{definition}
1262 
1263 \begin{definition}[Task-sufficient representation]
1264 \label{res:7:2}
1265 The scheme $C:\mathscr A\to\mathscr R$ is sufficient for $q$ when there is a single decoder $d_q:C(\mathscr A)\to Y_q$ such that
1266 \[
1267 q(\Pcal)=d_q(C(\Pcal))\qquad\text{for every }\Pcal\in\mathscr A.
1268 \]
1269 It is $\Qcal$-sufficient when this holds for every $q\in\Qcal$. The decoder may depend on the task and the scheme, but not on hidden knowledge of the particular archive being decoded.
1270 \end{definition}
1271 
1272 The decoder is defined on attained representations, so no arbitrary answer is required for an encoding that never occurs. Exact reconstruction is one possible task, not a requirement for every purpose. The basic definition is set theoretic and does not assert that a decoder is computable, efficient, or available to a particular reader. Those are additional conditions on a practical compiler.
1273 
1274 \begin{theorem}[Task information loss criterion]
1275 \label{res:7:3}
1276 Let $C$ be a compression map and let $q$ be a task. If there exist proof fields $\Pcal_1$ and $\Pcal_2$ such that
1277 \[
1278 C(\Pcal_1)=C(\Pcal_2)
1279 \qquad\text{but}\qquad
1280 q(\Pcal_1)\ne q(\Pcal_2),
1281 \]
1282 then the compressed representation is not sufficient for $q$.
1283 \end{theorem}
1284 
1285 \begin{proof}
1286 Suppose a decoder $d_q$ existed. Applying it to the common compressed representation would have to produce both $q(\Pcal_1)$ and $q(\Pcal_2)$. Since these answers differ, no such decoder exists.
1287 \end{proof}
1288 
1289 \begin{definition}[Recoverability preorder]
1290 \label{res:7:4}
1291 For a fixed task family $\Qcal$, write
1292 \[
1293 R_1\preceq_{\Qcal} R_2
1294 \]
1295 when every task in $\Qcal$ 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.
1296 \end{definition}
1297 
1298 \begin{proposition}[Recoverability is a preorder]
1299 \label{res:7:5}
1300 The relation $\preceq_{\Qcal}$ is reflexive and transitive.
1301 \end{proposition}
1302 
1303 \begin{proof}
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.
1305 \end{proof}
1306 
1307 Define $R_1\sim_{\Qcal}R_2$ when both $R_1\preceq_{\Qcal}R_2$ and $R_2\preceq_{\Qcal}R_1$.
1308 
1309 \begin{corollary}[Quotient poset]
1310 \label{res:7:6}
1311 The recoverability preorder descends to a partial order on the equivalence classes under $\sim_{\Qcal}$.
1312 \end{corollary}
1313 
1314 \begin{proof}
1315 Reflexivity and transitivity pass to equivalence classes. Mutual recoverability has been quotiented out, so antisymmetry holds by construction.
1316 \end{proof}
1317 
1318 
1319 \subsection{Pure retention operators}
1320 
1321 The simplest compression removes nodes without rewriting the retained material. This baseline is useful because it separates information deletion from more complicated summarization or reinterpretation.
1322 
1323 \begin{definition}[Retention projection]
1324 \label{res:7:7}
1325 Fix a finite node universe $V$. For a mask $K\subseteq V$, define
1326 \[
1327 P_K(S)=S\cap K,
1328 \qquad S\subseteq V.
1329 \]
1330 \end{definition}
1331 
1332 \begin{theorem}[Retention projection algebra]
1333 \label{res:7:8}
1334 For masks $K,L\subseteq V$,
1335 \[
1336 P_K\circ P_L=P_{K\cap L}=P_L\circ P_K.
1337 \]
1338 Consequently every retention projection is idempotent, and the masks form a Boolean lattice with meet $K\cap L$ and join $K\cup L$.
1339 \end{theorem}
1340 
1341 \begin{proof}
1342 For every $S\subseteq V$,
1343 \[
1344 P_K(P_L(S))=(S\cap L)\cap K=S\cap(K\cap L).
1345 \]
1346 Intersection is associative and commutative, which gives the composition identity and commutativity. Taking $L=K$ gives idempotence. The power set of $V$ with intersection, union, complement, bottom $\varnothing$, and top $V$ is a Boolean lattice.
1347 \end{proof}
1348 
1349 \begin{corollary}[Task monotonicity under retention]
1350 \label{res:7:9}
1351 If $K\subseteq L$, every task whose required nodes and metadata are retained by $P_K$ is also supported by $P_L$.
1352 \end{corollary}
1353 
1354 \begin{proof}
1355 Every item retained by $K$ is retained by $L$. Hence every task requirement contained in $K$ is contained in $L$.
1356 \end{proof}
1357 
1358 Pure retention operators commute. Noncommutativity in real proof workflows therefore requires an additional operation such as state-dependent summarization, renaming, quotienting, or reinterpretation. This distinction prevents simple deletion from being credited with structure it does not possess.
1359 
1360 \begin{figure}[htbp]
1361 \centering
1362 \includegraphics[width=\linewidth]{fig_05_recoverability_preorder.pdf}
1363 \caption{A concrete retention diamond for the four archives $(C_0,x,y)$ with $x,y\in\{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.}
1364 \label{fig:preorder}
1365 \end{figure}
1366 
1367 \begin{theorem}[Task-family dependence of minimal compression]
1368 \label{res:7:10}
1369 There is a family of archives with a fixed mandatory certificate and two independently variable side records for which different task families have different least sufficient retention masks.
1370 \end{theorem}
1371 
1372 \begin{proof}
1373 Let the archives be $\Pcal_{xy}=(C_0,x,y)$ for $(x,y)\in\{0,1\}^2$, where $C_0$ is a fixed certificate retained by every allowed mask. Let $q_x(\Pcal_{xy})=x$ and $q_y(\Pcal_{xy})=y$. Retaining $x$ is sufficient for $q_x$. Any mask omitting $x$ identifies $\Pcal_{0y}$ with $\Pcal_{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 retained side record.
1374 \end{proof}
1375 
1376 The example concerns pure retention. A general encoding may recode the records rather than delete them. Sufficiency for all archive queries requires an injective encoding, not literal preservation of the original file. The following theorem makes that distinction precise.
1377 
1378 \begin{theorem}[All predicates distinguish exactly injective encodings]
1379 \label{res:7:11}
1380 \label{thm:injective-compression}
1381 Let $C:A\to B$. Every predicate $q:A\to\mathrm{Prop}$ factors through $C$ if and only if $C$ is injective.
1382 \end{theorem}
1383 \begin{proof}
1384 If $C$ is injective, define the decoder of $q$ at $b$ by the predicate $\exists a\ (C(a)=b\ \text{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)\equiv(z=a)$. Its decoded values at the equal encodings must agree, giving $a'=a$. This is the general collision criterion specialized to all predicates.
1385 \end{proof}
1386 
1387 The formal result \path{ProofPath.all_predicates_sufficient_iff_injective} records the distinction between information loss and lossless recoding. It makes no assertion about how cheaply a decoder can be computed.
1388 
1389 
1390 \subsection{A complete factorization test on attained representations}
1391 \label{sec:attained-recovery}
1392 
1393 The collision obstruction of Theorem~\ref{res:7:3} has a converse. It gives a complete test for exact task recovery at the level of sets. Write $\operatorname{im}C=C(\mathscr A)$ for the attained output set. A decoder is required on this set and nowhere else.
1394 
1395 \begin{theorem}[Attained factorization and unique decoding]
1396 \label{res:new:factorization}
1397 For $C:\mathscr A\to\mathcal R$ and $q:\mathscr A\to Y$, the following are equivalent:
1398 \[
1399 \begin{aligned}
1400  &\exists d:\operatorname{im}C\to Y\quad
1401        \forall a\in\mathscr A,\quad q(a)=d(C(a)),\\
1402  &\forall a,b\in\mathscr A,\quad C(a)=C(b)\Longrightarrow q(a)=q(b).
1403 \end{aligned}
1404 \]
1405 When a decoder exists it is unique on $\operatorname{im}C$. Otherwise there are two archives with the same encoding and different task answers.
1406 \end{theorem}
1407 \begin{proof}
1408 A decoder applied to equal encodings gives equal answers. Conversely, for an attained value $r$, choose $a$ with $C(a)=r$ and define $d(r)=q(a)$. Constancy on each fiber makes the value independent of the choice. At $r=C(a)$ it gives the required answer. Any other decoder must give that same answer at every attained value, proving uniqueness. Negating fiber constancy supplies the pair in the last statement. The construction is set theoretic and uses classical choice in the Lean implementation. It does not provide an efficient decoder for arbitrary infinite archive classes.
1409 \end{proof}
1410 
1411 \begin{example}[The empty-domain boundary]
1412 \label{res:new:empty-decoder}
1413 Take $\mathscr A=\varnothing$, $\mathcal R=\{*\}$, and $Y=\varnothing$. There is one encoding and one task on the empty archive class. The attained set is empty, so its empty decoder exists. There is no total decoder $\{*\}\to\varnothing$. Thus attained decoding and decoding on the entire output type are not equivalent without an additional hypothesis.
1414 \end{example}
1415 
1416 The earlier formal definition \path{ProofPath.Sufficient} asks for a total decoder. It is retained for compatibility and was not false, but it was stronger than the manuscript's stated domain convention. The new namespace \path{ProofPath.Recovery} matches the manuscript exactly. It proves that total decoding implies attained decoding, and that the two are equivalent whenever the answer type is nonempty. In the latter case choose one default answer for unattained outputs. The empty-domain example is also kernel checked.
1417 
1418 The finite Python interface \path{factor_task} takes an explicitly declared table of archive encodings and a task table on the identical domain. It returns either a decoder table or two archive identifiers witnessing a collision. Its verifier checks the proposed result directly, including the empty domain, missing outputs, extra unattained entries, and contradictory records. The table strings are exact identifiers and answers, not a semantic equality procedure for arbitrary mathematical expressions. The existing retention-based \path{task_sufficient} function remains a different, narrower task model.
1419 
1420 \subsection{The least information for a family of tasks}
1421 \label{sec:joint-recovery}
1422 
1423 Suppose tasks $q_i:\mathscr A\to Y_i$ are indexed by $i\in I$. Their joint representation is
1424 \[
1425  Q(a)=(q_i(a))_{i\in I}.
1426 \]
1427 It records every distinction asked for by the task family and makes no demand to recover the entire source archive.
1428 
1429 \begin{theorem}[Joint task representation and compositional recovery]
1430 \label{res:new:joint}
1431 An encoding $C$ is sufficient for every $q_i$ if and only if it is sufficient for $Q$. In particular every sufficient encoding recovers the joint representation on attained values, while $Q$ itself recovers each task by projection.
1432 
1433 If a representation $R$ is recoverable from $C$, then every task recoverable from $R$ is recoverable from $C$. Recovery of representations is reflexive and transitive.
1434 \end{theorem}
1435 \begin{proof}
1436 If $Q$ factors through $C$, each coordinate factors by projection. Conversely, equal values of $C$ give equal values of every $q_i$. Function extensionality gives equal joint vectors, and Theorem~\ref{res:new:factorization} supplies the joint decoder. This argument allows a different answer type for each task and also covers an empty task family.
1437 
1438 For the second assertion, write $R=\pi\circ C$ and $q=d\circ R$ on their attained sets. Then $q=(d\circ\pi)\circ 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.
1439 \end{proof}
1440 
1441 The word least concerns retained distinctions, not bytes, running time, or the cognitive cost of reading an archive. Two archives are identified by $Q$ precisely when every declared task gives the same answer on them. Any sufficient representation may retain more, but it cannot identify archives that $Q$ distinguishes. For a finite archive family, the reference implementation labels these joint-answer classes and checks that every task is constant within a class. Costs remain a separate optimization problem.
1442 
1443 This result also completes the formal justification of the recovery condition in Section~\ref{sec:old19}. A refinement that reconstructs only the final theorem need not preserve the joint tasks of audit and discovery. A refinement with a checked recovery map for the preceding representation does preserve them. The distinction is between a longer proof and a genuinely more informative archive, not between short and long documents in general.
1444 
1445 
1446 \section{Endpoint, audit, and discovery equivalence}
1447 \label{sec:old8}
1448 
1449 The phrase ``the same proof'' can refer to several distinct equivalence relations.
1450 
1451 \begin{definition}[Endpoint equivalence]
1452 \label{res:8:1}
1453 Fix a background theory, an interpretation of claim labels, and an admissible inference policy. Within that context, two representations are endpoint equivalent when they certify the same judgment from the same complete assumption context and requested targets. Required premises and any additional admitted assumptions are accounted for in that context. A comparison across different contexts requires an explicitly specified transport of assumptions and judgments, not merely identical displayed labels.
1454 \end{definition}
1455 
1456 \begin{definition}[Audit equivalence]
1457 \label{res:8:2}
1458 Two representations are audit equivalent when they preserve equivalent dependency, evidence, provenance, and scope information for checking the declared targets.
1459 \end{definition}
1460 
1461 \begin{definition}[Discovery equivalence]
1462 \label{res:8:3}
1463 Two representations are discovery equivalent relative to a declared bridge model when they preserve the same examples, alternatives, boundary cases, candidate routes, and future reach, up to the chosen graph equivalence.
1464 \end{definition}
1465 
1466 When audit and discovery task families are required to include the endpoint tasks, either equivalence implies endpoint equivalence. Audit and discovery equivalence need not imply one another: a representation may preserve provenance without alternatives, or alternatives without provenance. Their joint task family is stronger than either. Any further hierarchy requires an explicit inclusion of task families. Two perfectly valid certificates can therefore expose different mathematical neighborhoods without differing in validity.
1467 
1468 \begin{remark}
1469 \label{res:8:4}
1470 These equivalences are task-relative. Discovery equivalence requires a declared bridge model. It is not an assertion that every future use of a proof can be predicted.
1471 \end{remark}
1472 
1473 
1474 \section{Vector-valued loss}
1475 \label{sec:old9}
1476 
1477 Let a node $v$ carry finite nonnegative numerical coordinates
1478 \[
1479 \mathbf v(v)=
1480 \bigl(V(v),D(v),M(v),F(v),A(v)\bigr),
1481 \]
1482 representing declared verification, discovery, meaning, future bridge, and auditability weights. Summation requires an additive numerical model. The weights may be supplied or estimated, but an ordinal ranking alone does not justify adding them. Changing a numerical scale can change the resulting loss and retention problem.
1483 
1484 \begin{definition}[Additive loss vector]
1485 \label{res:9:1}
1486 For a retained node set $K\subseteq V$, define
1487 \[
1488 \Loss(\Pcal,K)
1489 =
1490 \sum_{v\notin K}\mathbf v(v).
1491 \]
1492 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.
1493 \end{definition}
1494 
1495 \begin{proposition}[Zero verification loss can coexist with positive discovery loss]
1496 \label{res:9:2}
1497 There exist proof fields and certificates $K$ for which the verification coordinate of $\Loss(\Pcal,K)$ is zero while the discovery and bridge coordinates are positive.
1498 \end{proposition}
1499 
1500 \begin{proof}
1501 Take an AND-DAG certificate from $A$ to $B$ and add an optional example node $E$ that is not an ancestor of $B$. Assign positive discovery and bridge values to $E$ and zero verification value. The unique core omits $E$ while preserving the entire verification ancestry. The verification loss is zero and the other declared losses are positive.
1502 \end{proof}
1503 
1504 \begin{figure}[htbp]
1505 \centering
1506 \includegraphics[width=\linewidth]{fig_06_loss_vectors.pdf}
1507 \caption{Exact retained and lost values for the canonical AND-DAG certificate. The numbers are declared values, not measured universal units of meaning. Zero verification loss coexists with loss of seven discovery units and eight bridge units. All auditability values in this example were declared zero.}
1508 \label{fig:loss}
1509 \end{figure}
1510 
1511 No claim is made that all value coordinates are additive. Additivity is a transparent baseline. Interactions can be represented by hyperedge values, submodular utilities, or task-specific decoders when the application requires them.
1512 
1513 
1514 \section{Compression debt}
1515 \label{sec:old10}
1516 
1517 Compression may postpone work rather than eliminate it. A later task may require reconstruction of material that was omitted from the current representation.
1518 
1519 \begin{definition}[Future task model]
1520 \label{res:10:1}
1521 Let $\Tcal$ be a finite task set with probabilities $p_t\ge0$ satisfying $\sum_t p_t=1$. Let $R_t\subseteq V$ be the node set required by task $t$, and let $c(v)\ge0$ be the recovery cost of node $v$ when it is absent.
1522 \end{definition}
1523 
1524 \begin{definition}[Expected compression debt]
1525 \label{res:10:2}
1526 The expected compression debt of retained set $K$ is
1527 \[
1528 \Debt(K)
1529 =
1530 \sum_{t\in\Tcal}p_t
1531 \sum_{v\in R_t\setminus K}c(v).
1532 \]
1533 \end{definition}
1534 
1535 \begin{proposition}[Debt is monotone under retention]
1536 \label{res:10:3}
1537 If $K_1\subseteq K_2$, then
1538 \[
1539 \Debt(K_2)\le\Debt(K_1).
1540 \]
1541 \end{proposition}
1542 
1543 \begin{proof}
1544 For every task $t$, the missing set $R_t\setminus K_2$ is contained in $R_t\setminus K_1$. Recovery costs are nonnegative. The taskwise cost cannot increase, and neither can its probability-weighted sum.
1545 \end{proof}
1546 
1547 \begin{corollary}[Irreversible compression accumulates debt]
1548 \label{res:10:4}
1549 For a descending sequence of retained sets
1550 \[
1551 K_0\supseteq K_1\supseteq\cdots\supseteq K_r,
1552 \]
1553 the expected debt is nondecreasing.
1554 \end{corollary}
1555 
1556 A recovery archive can change the cost function. If an omitted node has a stable provenance pointer and a reproducible generator, its recovery cost may be small. If it survives only in memory, its recovery cost may be effectively infinite.
1557 
1558 
1559 \section{A proof ecology rather than one ideal form}
1560 \label{sec:old11}
1561 
1562 The same theorem can support several legitimate representations:
1563 \[
1564 \Rcal(B)=
1565 \{R_{\mathrm{cert}},R_{\mathrm{journal}},R_{\mathrm{teach}},
1566 R_{\mathrm{formal}},R_{\mathrm{discovery}},R_{\mathrm{archive}}\}.
1567 \]
1568 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.
1569 
1570 \begin{definition}[Representation portfolio]
1571 \label{res:11:1}
1572 A representation portfolio is a family of proof representations together with stable claim identifiers, translation maps, and a shared status ledger.
1573 \end{definition}
1574 
1575 \begin{proposition}[Portfolio robustness]
1576 \label{res:11:2}
1577 For representation schemes $C_i:\mathscr A\to R_i$, retain the tagged portfolio $C(\Pcal)=(C_i(\Pcal))_i$. Every task recoverable from any one $C_i$ is recoverable from $C$.
1578 \end{proposition}
1579 
1580 \begin{proof}
1581 If $q=d_i\circ C_i$, compose $d_i$ with the $i$th 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.
1582 \end{proof}
1583 
1584 Redundancy is useful when it is heterogeneous. Storing six copies of the same compressed certificate adds little. Storing a certificate, an expanded explanation, a formal dependency graph, and a reproducible notebook may preserve genuinely different values.
1585 
1586 
1587 \section{Proof compilers and shared ledgers}
1588 \label{sec:old12}
1589 
1590 A proof compiler generates a representation for a specified purpose from one canonical proof field. The connection between source and readable exposition also motivates literate programming \cite{knuth}.
1591 
1592 \begin{definition}[Proof compiler]
1593 \label{res:12:1}
1594 Let $g$ be a presentation goal and let $\Pcal$ be a versioned proof field. A proof compiler is a map on the declared archive class
1595 \[
1596 \Gamma_g:\mathscr A\longrightarrow R_g
1597 \]
1598 that selects, orders, and renders the material required by $g$ while preserving links to canonical claim and justification identifiers.
1599 \end{definition}
1600 
1601 Typical goals include certificate, journal, teaching, discovery, formal verification, and archive. The compiler does not invent logical status. It reads status from the canonical ledger.
1602 
1603 \begin{proposition}[Shared-ledger consistency]
1604 \label{res:12:2}
1605 Suppose every compiled representation is generated from one canonical ledger and every rendered claim retains its ledger identifier. Then a status correction can be propagated consistently to every compiled representation containing that claim by updating the ledger and recompiling.
1606 \end{proposition}
1607 
1608 \begin{proof}
1609 The stable identifier determines every occurrence of the claim across the compiled outputs. Updating the canonical record changes the source value associated with that identifier. Recompilation reads the updated record in every view. A stale status can persist only in an output detached from the canonical ledger or not recompiled.
1610 \end{proof}
1611 
1612 This proposition is operationally important. A monograph, a formal library, and a teaching site should not maintain independent truth labels for the same claim.
1613 
1614 
1615 \section{Latent bridge graphs}
1616 \label{sec:old13}
1617 
1618 A proof field records certified dependencies. A latent bridge graph records possible future transfers. The two graphs have different logical roles.
1619 
1620 \begin{definition}[Latent bridge graph]
1621 \label{res:13:1}
1622 A latent bridge graph is a finite directed graph
1623 \[
1624 \Bcal=(W,E_B)
1625 \]
1626 whose nodes include retained proof objects, omitted proof objects, and anticipated future targets. An edge $x\to 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.
1627 \end{definition}
1628 
1629 Let $S\subseteq W$ be the retained starting set. Let $F\subseteq W$ be a future target set with weights $w_f\ge0$.
1630 
1631 \begin{definition}[Future reach utility]
1632 \label{res:13:2}
1633 The weighted future reach of $S$ is
1634 \[
1635 U(S)=\sum_{f\in F}w_f\,
1636 \mathbf 1\{f\in\Reach_{\Bcal}(S)\}.
1637 \]
1638 \end{definition}
1639 
1640 This quantity measures declared reach, not truth. A conjectural edge can increase modeled reach without certifying the target. The ledger must keep those statuses separate.
1641 
1642 \subsection{Bridge criticality and dominators}
1643 
1644 \begin{definition}[Bridge-critical node]
1645 \label{res:13:3}
1646 A node $v$ is bridge critical for target $f$ relative to starts $S$ when $f$ is reachable from $S$ in $\Bcal$ and becomes unreachable after $v$ is removed.
1647 \end{definition}
1648 
1649 In graph language, $v$ dominates an initially reachable $f$ relative to $S$ when every directed path from $S$ to $f$ passes through $v$. Paths of length zero are allowed in the reachability convention. Standard graph terminology is used throughout \cite{diestel}.
1650 
1651 \begin{theorem}[Criticality equals domination]
1652 \label{res:13:4}
1653 Assume $f$ is reachable from $S$. A node $v\notin S$ is bridge critical for $f$ if and only if $v$ dominates $f$ relative to $S$.
1654 \end{theorem}
1655 
1656 \begin{proof}
1657 If $v$ dominates $f$, every path from $S$ to $f$ uses $v$. Removing $v$ removes every such path, so $f$ becomes unreachable. Conversely, if removing $v$ makes $f$ unreachable, then there could not have been a path from $S$ to $f$ avoiding $v$. Therefore every path used $v$, which is exactly domination.
1658 \end{proof}
1659 
1660 \begin{corollary}[Weighted criticality]
1661 \label{res:13:5}
1662 For $v\notin S$, the utility lost by deleting $v$ is the total weight of initially reachable future targets dominated by $v$:
1663 \[
1664 U(S)-U_{\Bcal\setminus\{v\}}(S)
1665 =\sum_{\substack{f\in F\cap\Reach_{\Bcal}(S)\\v\text{ dominates }f}}w_f.
1666 \]
1667 Deleted target vertices are counted as unreachable.
1668 \end{corollary}
1669 
1670 \begin{figure}[htbp]
1671 \centering
1672 \includegraphics[width=\linewidth]{fig_07_bridge_dominators.pdf}
1673 \caption{A 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.}
1674 \label{fig:dominator}
1675 \end{figure}
1676 
1677 A node may have low verification value for the current theorem and high domination value for future targets. This is the precise form of the claim that a forgotten step can remain mathematically important after it has lost its role in the original certificate.
1678 
1679 
1680 \section{Retention under a budget}
1681 \label{sec:old14}
1682 
1683 An archive cannot retain every object at full resolution. The first mathematically controlled retention problem is to choose a finite supplement that preserves as much future reach as possible.
1684 
1685 Let $C\subseteq W$ be the candidate nodes that may be retained and let $M$ be a mandatory base set. For $S\subseteq C$, define
1686 \[
1687 U_M(S)=U(M\cup S).
1688 \]
1689 The bridge graph remains fixed: retention changes the starting set, not the available intermediate vertices or edges. Deleting unretained intermediate vertices would define a different objective, for which the coverage proof below need not apply.
1690 
1691 \begin{theorem}[Bridge coverage is monotone and submodular]
1692 \label{res:14:1}
1693 \label{thm:bridge-submodular}
1694 The future reach utility $U_M$ is a nonnegative monotone submodular set function on $C$.
1695 \end{theorem}
1696 
1697 \begin{proof}
1698 For each candidate $x\in C$, let $R_x\subseteq F$ be the set of future targets reachable from $M\cup\{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
1699 \[
1700 U_M(S)=
1701 \sum_{f\in R_M\cup\bigcup_{x\in S}R_x}w_f.
1702 \]
1703 Adding a candidate cannot remove a reachable target, so $U_M$ is monotone.
1704 
1705 Now let $S\subseteq T\subseteq C$ and let $x\in C\setminus T$. The marginal gain of adding $x$ is the total weight of targets in $R_x$ that are not already covered. Since $T$ covers at least every target covered by $S$, the set newly covered from $T$ is contained in the set newly covered from $S$. Therefore
1706 \[
1707 U_M(S\cup\{x\})-U_M(S)
1708 \ge
1709 U_M(T\cup\{x\})-U_M(T),
1710 \]
1711 which is submodularity.
1712 \end{proof}
1713 
1714 \begin{theorem}[Greedy cardinality guarantee]
1715 \label{res:14:2}
1716 \label{thm:bridge-greedy}
1717 Let $k$ be an integer with $1\leq k\leq|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
1718 \[
1719 U_M(S_k)-U_M(\varnothing)
1720 \ge
1721 \left(1-\left(1-\frac1k\right)^k\right)
1722 \bigl(U_M(O_k)-U_M(\varnothing)\bigr),
1723 \]
1724 and therefore the greedy gain is at least $(1-1/e)$ times the optimal gain.
1725 \end{theorem}
1726 
1727 \begin{proof}
1728 Write $G_i=U_M(S_i)-U_M(\varnothing)$ and $G^*=U_M(O_k)-U_M(\varnothing)$. 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
1729 \[
1730 G^*-G_{i+1}
1731 \le
1732 \left(1-\frac1k\right)(G^*-G_i).
1733 \]
1734 Iterating from $G_0=0$ gives
1735 \[
1736 G^*-G_k
1737 \le
1738 \left(1-\frac1k\right)^kG^*.
1739 \]
1740 Rearranging gives the first bound. The inequality $(1-1/k)^k\le e^{-1}$ gives the second.
1741 \end{proof}
1742 
1743 \begin{warning}[Arbitrary costs]
1744 \label{res:14:3}
1745 For $k=0$, both gains are zero without using the displayed division by $k$. For a budget at least $|C|$, retaining all candidates is optimal. The displayed theorem is the cardinality form of the standard submodular greedy bound \cite{nemhauser}. A gain-per-cost rule for unequal costs is a different algorithm and does not inherit this guarantee. Zero-cost candidates also need an explicit convention.
1746 \end{warning}
1747 
1748 \begin{figure}[H]
1749 \centering
1750 \includegraphics[width=\linewidth]{fig_08_submodular_greedy.pdf}
1751 \caption{Greedy and exact retention coincide on the committed finite instance. The square and circle marks are deliberately overlaid. The general cardinality guarantee is $1-1/e$, not equality with the optimum on every graph.}
1752 \label{fig:greedy}
1753 \end{figure}
1754 
1755 
1756 \monographpart{Revision, review, and inquiry}{Revision and inquiry}{A mathematical archive has a continuing life. Revisions, shared error, and finite checking capacity change its use without changing the standard of proof.}
1757 
1758 \section{Versioned proof objects}
1759 \label{sec:old15}
1760 \label{sec:versioned}
1761 
1762 A proof archive changes. Claims are strengthened, corrected, refuted, or split. A reproducible theory therefore needs stable identifiers and explicit version relations.
1763 
1764 \begin{definition}[Versioned proof object]
1765 \label{res:15:1}
1766 A versioned proof object is a sequence
1767 \[
1768 \Pcal_0\longrightarrow\Pcal_1\longrightarrow\cdots
1769 \]
1770 whose nodes and justifications carry stable identifiers. Each transition records additions, removals, altered scopes, evidence changes, and a digest of its parent version.
1771 \end{definition}
1772 
1773 \begin{definition}[Append-only certified update]
1774 \label{res:15:2}
1775 An update $\Pcal_i\to\Pcal_{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.
1776 \end{definition}
1777 
1778 \begin{theorem}[Derivability is monotone under append-only updates]
1779 \label{res:15:3}
1780 Every target derivable in $\Pcal_i$ remains derivable in $\Pcal_{i+1}$ under an append-only certified update.
1781 \end{theorem}
1782 
1783 \begin{proof}
1784 A certificate in $\Pcal_i$ uses only nodes and certified justifications that remain unchanged in $\Pcal_{i+1}$. The same selected subfield therefore satisfies the same derivability closure in the later version.
1785 \end{proof}
1786 
1787 Retractions and semantic changes are not append-only. They require invalidation analysis.
1788 
1789 \begin{definition}[Syntactic affected set]
1790 \label{res:15:4}
1791 For a changed node set $X\subseteq V$, define
1792 \[
1793 \operatorname{Aff}(X)=X\cup\Desc(X),
1794 \]
1795 where descendants are computed in the declared dependency graph.
1796 \end{definition}
1797 
1798 \begin{theorem}[Minimal closed syntactic review set]
1799 \label{res:15:5}
1800 The set $\operatorname{Aff}(X)$ is the unique smallest node set $Y$ such that $X\subseteq Y$ and $Y$ is closed under outgoing dependency edges: whenever $u\in Y$ and $u\to v$ is a declared dependency edge, then $v\in Y$.
1801 \end{theorem}
1802 
1803 \begin{proof}
1804 By construction, every node reachable from $X$ lies in $\operatorname{Aff}(X)$, so the set contains $X$ and is closed under outgoing edges. Let $Y$ be any other set with those two properties. Every directed path beginning in $X$ remains inside $Y$ by induction on path length. Hence every descendant of $X$ lies in $Y$, and $\operatorname{Aff}(X)\subseteq Y$.
1805 \end{proof}
1806 
1807 \begin{figure}[htbp]
1808 \centering
1809 \includegraphics[width=\linewidth]{fig_09_version_invalidation.pdf}
1810 \caption{Changing $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.}
1811 \label{fig:invalidation}
1812 \end{figure}
1813 
1814 The theorem is intentionally syntactic. A descendant can survive after rechecking. The affected set says where review is required, not where falsehood is guaranteed.
1815 
1816 
1817 \FloatBarrier
1818 \section{Evidence ledgers and provenance}
1819 \label{sec:old16}
1820 
1821 \Needspace{9\baselineskip}
1822 A claim ledger should answer five questions without reconstructing the entire research history.
1823 
1824 \begin{enumerate}
1825 \item What is the exact claim identifier?
1826 \item What is its current status and scope?
1827 \item Which justifications depend on it?
1828 \item Which evidence records support or challenge it?
1829 \item Which versions and compiled documents contain it?
1830 \end{enumerate}
1831 
1832 \begin{definition}[Evidence ledger]
1833 \label{res:16:1}
1834 An evidence ledger is an appendable collection of typed, scoped records linked to claim and justification identifiers. A record may certify, support, challenge, interpret, or refute an object. Its role is explicit rather than inferred from prose placement.
1835 \end{definition}
1836 
1837 \begin{definition}[Provenance digest]
1838 \label{res:16:2}
1839 A provenance digest is a cryptographic hash of a canonical serialization of the claim identifier, content, scope, evidence references, parent version, and relevant build inputs.
1840 \end{definition}
1841 
1842 A digest does not prove a theorem. A changed digest establishes that the hashed byte sequence changed. An unchanged digest is an integrity check only subject to the possibility of collisions. Canonical serialization gives different representations a common byte-level reference.
1843 
1844 \begin{proposition}[Digest stability]
1845 \label{res:16:3}
1846 Fix a deterministic serialization $s$ and a deterministic hash function $h$. Identical serialized byte sequences have identical digests under $h$. Distinct serialized byte sequences have distinct digests unless they form a collision under $h$. Detecting a record change additionally requires that the change alter its serialized bytes.
1847 \end{proposition}
1848 
1849 \begin{proof}
1850 If $s(r)=s(r')$, applying the function $h$ gives equal digests. If $s(r)\ne 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.
1851 \end{proof}
1852 
1853 
1854 The serialization contract must state which fields, types, and distinctions it preserves and which differences it intentionally normalizes. Loss during serialization and a collision during hashing are separate mechanisms.
1855 
1856 For example, joining string parts with a separator is ambiguous if the same separator may occur inside a part. The tuples $(\texttt{a|b},\texttt{c})$ and $(\texttt{a},\texttt{b|c})$ both become \texttt{a|b|c}. No hash function can recover the lost tuple boundary. The earlier \path{provenance_digest} helper had this defect with a control-character separator. Python release 1.4.0 replaces that encoding with a versioned, domain-separated JSON array of strings. Historical digests must retain their earlier format and version. The snapshot digest has its own unchanged serialization contract.
1857 
1858 \begin{proposition}[Hashing cannot add recoverable tasks]
1859 \label{res:new:hash}
1860 Let $s:\mathscr A\to B$ be serialization and $h:B\to D$ be any deterministic map. Every task recoverable from $h\circ s$ is recoverable from $s$. If $h$ is injective on the attained set $s(\mathscr A)$, the two encodings support exactly the same tasks.
1861 \end{proposition}
1862 \begin{proof}
1863 If $s(a)=s(b)$, then $h(s(a))=h(s(b))$. Any task constant on the digest fibers is therefore constant on the serialization fibers, and Theorem~\ref{res:new:factorization} supplies its decoder. If $h$ is injective on attained serializations, equality of digests conversely implies equality of serializations, so the two fiber partitions coincide and the same criterion applies in both directions.
1864 \end{proof}
1865 
1866 The module \path{ProofPath.Recovery} checks both implications. The injectivity condition is a conditional mathematical hypothesis, not a claim that a fixed-length cryptographic hash is injective on arbitrary inputs. A hash cannot repair an ambiguity introduced before hashing. It may introduce additional collisions, which must be kept separate from the serializer's preservation contract.
1867 
1868 \section{Correlated review}
1869 \label{sec:old17}
1870 \label{sec:correlated-review}
1871 
1872 Several reviews are not equivalent to several independent reviews. Reviewers may share training, notation, examples, software, or an unnoticed premise.
1873 
1874 Let $X_i=\theta+\varepsilon_i$ be numerical estimates of a fixed quantity $\theta$. Assume $\mathbb E\varepsilon_i=0$, $\operatorname{Var}(\varepsilon_i)=\sigma^2>0$, and common pairwise correlation $\rho$. For $n>1$, assume $-1/(n-1)<\rho\leq1$, so the mean has positive variance. These variables model estimates, not proof truth values. The mean has variance
1875 \[
1876 \operatorname{Var}(\bar X)
1877 =
1878 \sigma^2\left(\frac{1-\rho}{n}+\rho\right).
1879 \]
1880 
1881 \begin{theorem}[Effective reviewer count]
1882 \label{res:17:1}
1883 \label{thm:review-count}
1884 Under the equicorrelated model, define the variance-equivalent reviewer count by
1885 \[
1886 \boxed{
1887  n_{\mathrm{eff}}
1888  =
1889  \frac{n}{1+(n-1)\rho}
1890 }
1891 \]
1892 so that $\operatorname{Var}(\bar X)=\sigma^2/n_{\mathrm{eff}}$. This effective count is a positive real number and need not be an integer.
1893 \end{theorem}
1894 
1895 \begin{proof}
1896 The mean of $m$ independent reviewers of variance $\sigma^2$ has variance $\sigma^2/m$. Equating this with the correlated mean variance gives
1897 \[
1898 \frac{\sigma^2}{m}
1899 =
1900 \sigma^2\left(\frac{1-\rho}{n}+\rho\right)
1901 =
1902 \sigma^2\frac{1+(n-1)\rho}{n}.
1903 \]
1904 Solving for $m$ gives the formula.
1905 \end{proof}
1906 
1907 For $n=1$, the effective count is one. At the excluded boundary $\rho=-1/(n-1)$, the mean has zero variance and there is no finite variance-equivalent count. For fixed $0<\rho\leq1$, $n_{\mathrm{eff}}\to1/\rho$ as $n\to\infty$. Negative correlations can give $n_{\mathrm{eff}}>n$, but a fixed negative correlation is not admissible for arbitrarily large $n$.
1908 
1909 \begin{figure}[htbp]
1910 \centering
1911 \includegraphics[width=\linewidth]{fig_10_effective_reviewers.pdf}
1912 \caption{Effective reviewer count under the specified equicorrelation model. The logarithmic vertical scale keeps all four curves visible. At $n=100$ and $\rho=0.1$, the effective count is about $9.17$. This formula models variance reduction, not the probability that a mathematical claim is true.}
1913 \label{fig:reviewers}
1914 \end{figure}
1915 
1916 For a general positive definite covariance matrix $\Sigma$, consider unbiased linear aggregates $w^\top X$ with $\mathbf 1^\top w=1$.
1917 
1918 \begin{theorem}[Minimum-variance covariance-aware weights]
1919 \label{res:17:2}
1920 The unique minimum-variance unbiased linear aggregate has weights
1921 \[
1922 w^*
1923 =
1924 \frac{\Sigma^{-1}\mathbf 1}
1925 {\mathbf 1^\top\Sigma^{-1}\mathbf 1}.
1926 \]
1927 Its variance is
1928 \[
1929 \frac{1}{\mathbf 1^\top\Sigma^{-1}\mathbf 1}.
1930 \]
1931 \end{theorem}
1932 
1933 \begin{proof}
1934 Minimize $w^\top\Sigma w$ subject to $\mathbf 1^\top w=1$. The Lagrangian is
1935 \[
1936 L(w,\lambda)=w^\top\Sigma w-2\lambda(\mathbf 1^\top w-1).
1937 \]
1938 Stationarity gives $\Sigma w=\lambda\mathbf 1$, hence $w=\lambda\Sigma^{-1}\mathbf 1$. The constraint gives
1939 \[
1940 \lambda=(\mathbf 1^\top\Sigma^{-1}\mathbf 1)^{-1}.
1941 \]
1942 Positive definiteness makes the objective strictly convex, so the solution is unique. Substitution gives the variance formula.
1943 \end{proof}
1944 
1945 \begin{warning}[Bias is not covariance]
1946 \label{res:17:3}
1947 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$.
1948 \end{warning}
1949 
1950 Under the model, dependence rather than nominal count determines the variance reduction. Whether a particular review process has this covariance structure is an empirical question. The formula alone neither endorses nor discredits a community judgment.
1951 
1952 
1953 \section{Shared interpretation, review dependence, and identification}
1954 \label{sec:old25}
1955 \label{sec:interpretation}
1956 
1957 The distinction between proof and proof field also matters when many people assess the same mathematics. An individual can evaluate a theorem through the notation, examples, expectations, and disciplinary assumptions available to them. Different reviewers may share these influences. Agreement therefore need not provide independent evidence, although substantive criticism can still identify a real defect. The mathematical contribution of a model lies in making its assumptions explicit, not in diagnosing the motives of reviewers.
1958 
1959 \subsection{Correlated noise and persistent common bias}
1960 
1961 The covariance model of Section~\ref{sec:correlated-review} measures how dependence reduces the effective information in repeated estimates. It cannot remove a common offset. The next proposition puts both effects into one equation.
1962 
1963 \begin{proposition}[MSE with a shared interpretive offset]
1964 \label{res:25:1}
1965 Suppose reviewers report $J_i=\theta+b+\varepsilon_i$, where $\theta$ is the target quantity, $b$ is a fixed shared offset, $\mathbb E\varepsilon_i=0$, $\operatorname{Var}(\varepsilon_i)=\sigma^2$, and $\operatorname{Cov}(\varepsilon_i,\varepsilon_j)=\rho\sigma^2$ for $i\ne j$. For admissible $\rho$, the mean squared error of the reviewer average is
1966 \[
1967 \boxed{\mathbb E(\overline J_n-\theta)^2=b^2+\sigma^2\left(\rho+\frac{1-\rho}{n}\right).}
1968 \]
1969 For fixed $\rho\ge0$, it approaches $b^2+\rho\sigma^2$ as $n\to\infty$.
1970 \end{proposition}
1971 \begin{proof}
1972 The estimation error is $\overline J_n-\theta=b+\overline\varepsilon_n$. Its mean is $b$, and its variance is $\sigma^2\big((1-\rho)/n+\rho\big)$ by summing all diagonal and off-diagonal covariance entries. Mean squared error is variance plus squared bias. Taking the limit completes the proof.
1973 \end{proof}
1974 
1975 This formula complements, rather than replaces, the effective reviewer count. Adding reviewers may reduce independent error while leaving the common offset untouched. The existing Python routine \path{shared_bias_mse} computes this model and permits an additional declared variance term for a shared random lens. Its input parameters are model choices, not measured facts about a given intellectual community.
1976 
1977 \subsection{When an identity effect can actually be measured}
1978 
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 assignments. Then the difference of the two sample means is unbiased for $N^{-1}\sum_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 the second, so linearity of expectation gives that identity.
1980 
1981 This conclusion concerns the assigned reviewers. Generalizing to a broader population requires a sampling model. Missing responses, shared discussion, or changes to the argument itself can invalidate the simple interpretation. None of these comparisons determines whether the proof is correct. Correctness requires its own mathematical audit.
1982 
1983 This distinction is central to a proposed application of Proof Path Theory. One may observe that a presentation changes which branches reviewers explore or how they estimate importance. Those differences become evidence of a contextual effect only after alternative explanations have been addressed. A skeptical review can be correct. Agreement can be justified. The mere presence of community influence neither validates nor invalidates a theorem.
1984 
1985 The research opportunity is to connect a typed archive of mathematical claims with controlled studies of how proof paths are selected, compressed, and interpreted. A certified proof core would be held fixed while the accompanying discovery field or contextual labels change. The questions are which alternatives readers recognize, which obstructions they find, and how their subsequent mathematical exploration differs. These are empirical targets for future work, not conclusions established by this finite model.
1986 
1987 \subsection{Interpretation and mathematical validity}
1988 
1989 The ambient field records exploratory trajectories, the realization theory determines whether specified local models assemble, and the review model describes the effect of declared dependence among numerical judgments. They address different questions. Their common archive makes comparison possible without identifying agreement, coherence, and deductive validity.
1990 
1991 These constructions do not yield a general solver for mathematical conjectures, a unique numerical measure of mathematical meaning, a canonical global proof field, or an empirical diagnosis of actual mathematical communities. They provide explicit finite questions with checkable answers and identify the conditions needed for stronger generalizations. Most importantly, they preserve the difference between a valid result and the circumstances through which people discover or evaluate it.
1992 
1993 
1994 
1995 \section{Verification bandwidth and audit queues}
1996 \label{sec:old18}
1997 
1998 Let $a_t\geq0$ be candidate arrivals during audit cycle $t$, let $s_t\geq0$ be service capacity, and let $B_t\geq0$ be the unresolved backlog. Suppose arrivals in a cycle are available to that cycle's service. The basic deterministic queue is
1999 \[
2000 B_{t+1}=\max\{0,B_t+a_t-s_t\}.
2001 \]
2002 
2003 \begin{theorem}[Constant-rate audit regimes]
2004 \label{res:18:1}
2005 \label{thm:audit-rates}
2006 Suppose $a_t\equiv\lambda$ and $s_t\equiv\mu$.
2007 \begin{enumerate}[label=\textup{(\roman*)}]
2008 \item If $\lambda<\mu$, every finite initial backlog reaches zero after finitely many cycles.
2009 \item If $\lambda=\mu$, the backlog remains constant.
2010 \item If $\lambda>\mu$, the backlog grows linearly with slope $\lambda-\mu$.
2011 \end{enumerate}
2012 \end{theorem}
2013 
2014 \begin{proof}
2015 Before the truncation at zero, each cycle adds $\lambda-\mu$. 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(\lambda-\mu)$.
2016 \end{proof}
2017 
2018 \begin{figure}[htbp]
2019 \centering
2020 \includegraphics[width=\linewidth]{fig_11_audit_queues.pdf}
2021 \caption{The committed audit example starts with backlog ten and capacity five. Four arrivals per cycle clear the queue, five preserve the backlog, and six increase it. Direct labels replace a separate legend. These are exact trajectories for the declared constant-rate model.}
2022 \label{fig:auditqueue}
2023 \end{figure}
2024 
2025 A simple audit priority score is
2026 \[
2027 P(x)
2028 =
2029 \frac{p_{\mathrm{err}}(x)\,c_{\mathrm{consequence}}(x)
2030 \bigl(1+r_{\mathrm{dependency}}(x)\bigr)}
2031 {c_{\mathrm{audit}}(x)}.
2032 \]
2033 Here $p_{\mathrm{err}}(x)\in[0,1]$, the consequence and dependency factors are nonnegative, and $c_{\mathrm{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.
2034 
2035 
2036 \FloatBarrier
2037 \section{Recursive proof cubes and expansion depth}
2038 \label{sec:old19}
2039 
2040 A visible proof step is rarely atomic. A lemma opens into definitions and sublemmas. A computation opens into algorithms, parameters, and exact checks. A citation opens into another dependency graph. Proof Path Theory treats this as recursive refinement.
2041 
2042 \begin{definition}[Proof packet and refinement]
2043 \label{res:19:1}
2044 A proof packet is a node presented at one resolution. A refinement replaces that node by a finite subfield whose certified target reconstructs the original node on the declared scope.
2045 \end{definition}
2046 
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\to\mathcal R_d$ be the representation scheme at depth $d$. A sufficient condition is a map
2048 \[
2049 \pi_d:R_{d+1}(\mathscr A)\longrightarrow R_d(\mathscr A)
2050 \qquad\text{with}\qquad R_d=\pi_d\circ R_{d+1}.
2051 \]
2052 If a task factors as $q=d_q\circ R_d$, then
2053 \[
2054 q=(d_q\circ\pi_d)\circ R_{d+1}.
2055 \]
2056 Hence $R_d\preceq_{\Qcal}R_{d+1}$. Repeated refinements satisfying this condition give the recoverability chain. For a restricted task family, preserving its supported tasks directly can suffice without recovering the entire preceding representation.
2057 
2058 A longer derivation is not automatically a richer archive. It may reconstruct the same conclusion while omitting an example, a failed approach, or a provenance record. Those losses must be assessed against the declared task family.
2059 
2060 Let $r_d\geq0$ be a declared unresolved-work score and $c_d\geq0$ the cumulative cost. These are model inputs. A small $r_d$ is not, without another theorem, a certificate of a nearly valid proof. The word cube names the layered presentation, not a cubical complex supplied with additional geometric axioms.
2061 
2062 \begin{definition}[Goal-relative depth objective]
2063 \label{res:19:2}
2064 For goal $g$ with weights $\alpha_g,\beta_g\ge0$, define
2065 \[
2066 J_g(d)=\alpha_g r_d+\beta_g c_d.
2067 \]
2068 An optimal expansion depth is any minimizer of $J_g$.
2069 \end{definition}
2070 
2071 \begin{theorem}[Expansion depth is goal dependent]
2072 \label{res:19:3}
2073 The same proof object can have different optimal expansion depths for different goals.
2074 \end{theorem}
2075 
2076 \begin{proof}
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
2078 \[
2079 \alpha_g(r_{d_1}-r_{d_2})>\beta_g(c_{d_2}-c_{d_1}).
2080 \]
2081 The goal $(\alpha_g,\beta_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.
2082 \end{proof}
2083 
2084 A practical stopping rule selects the first depth satisfying
2085 \[
2086 r_d\le\varepsilon\qquad\text{or}\qquad
2087 \frac{r_{d-1}-r_d}{c_d-c_{d-1}}<\tau.
2088 \]
2089 The first condition uses a declared tolerance. The second applies only at $d\geq1$ 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.
2090 
2091 Figure~\ref{fig:refinement} and the worked example in Section~\ref{sec:depth-example} give explicit costs and unresolved-work scores for three goals.
2092 
2093 Deeper is not automatically better. A formal checker may need primitive steps. A specialist paper may cite a standard theorem. A teaching account may expand only the conceptual bottleneck. An archive may retain a failed branch that neither certificate requires.
2094 
2095 
2096 \monographpart{Examples, implementation, and boundaries}{Examples and scope}{The final layer is inspectable: source records, computations, certificates, and evidence. Each check has a declared scope, and the open problems remain separate from the implemented finite theory.}
2097 
2098 \section{Worked finite examples}
2099 \label{sec:old20}
2100 
2101 The accompanying repository contains three canonical JSON proof fields and several auxiliary models. The examples are small enough to inspect by hand and complete enough to exercise the formal distinctions.
2102 
2103 \subsection{A fixed AND-DAG}
2104 
2105 The field \texttt{examples/and\_dag.json} has required premise $A$, a definition $D$, lemmas $L_1$ and $L_2$, and target $B$. It also contains a worked example, a failed route, and a boundary case. The unique verification core is
2106 \[
2107 \{A,D,L_1,L_2,B\}.
2108 \]
2109 The optional nodes have zero declared verification value for $B$ and positive discovery, meaning, or bridge value. This is the executable instance behind Figure~\ref{fig:loss}.
2110 
2111 \subsection{Two certified proofs}
2112 
2113 The field \texttt{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
2114 \[
2115 A\longrightarrow L_{\mathrm{short}}\longrightarrow B
2116 \]
2117 when the objective is storage cost alone. A teaching compiler may rationally choose the other route because it uses a different objective.
2118 
2119 \subsection{Set Cover encoded as certificate selection}
2120 
2121 The field \texttt{examples/set\_cover\_certificate.json} contains four optional source lemmas and four obligations. Exact search returns the certificate using $S_1$ and $S_3$, with total cost $2$. The particular optimum is not important. The example demonstrates how local alternative derivations create a global combinatorial selection problem.
2122 
2123 \subsection{Bridge retention}
2124 
2125 The bridge experiment uses ten candidate nodes and sixteen weighted future targets. For budgets zero through five, the script computes both the exact optimum and the greedy solution. The generated data are stored in \texttt{data/retention\_comparison.csv}. On this instance the two curves coincide. The theorem guarantees only the worst-case $(1-1/e)$ factor.
2126 
2127 \subsection{Correlated review and audit capacity}
2128 
2129 For one hundred equicorrelated reviewers with $\rho=0.1$,
2130 \[
2131 n_{\mathrm{eff}}
2132 =
2133 \frac{100}{1+99(0.1)}
2134 \approx 9.17.
2135 \]
2136 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.
2137 
2138 \begin{table}[H]
2139 \centering
2140 \caption{Canonical finite examples and their mathematical roles.}
2141 \begin{tabular}{@{}lll@{}}
2142 \toprule
2143 Object & Computed result & Mathematical role\\
2144 \midrule
2145 AND-DAG & unique five-node core & Theorem~\ref{thm:and-core}\\
2146 Alternative field & minimum cost $1$ & exact finite search\\
2147 Set Cover field & minimum cost $2$ & Theorem~\ref{thm:minimum-certificate} encoding\\
2148 Bridge model & greedy and exact curves & Theorems~\ref{thm:bridge-submodular}--\ref{thm:bridge-greedy}\\
2149 Review model & $n_{\mathrm{eff}}$ formula & Theorem~\ref{thm:review-count}\\
2150 Audit model & three queue regimes & Theorem~\ref{thm:audit-rates}\\
2151 \bottomrule
2152 \end{tabular}
2153 \end{table}
2154 
2155 
2156 \subsection{An expansion-depth calculation}
2157 \label{sec:depth-example}
2158 For depths $0$ through $6$, take unresolved-work scores
2159 $(1,0.55,0.30,0.18,0.12,0.09,0.075)$ and costs
2160 $(0,0.25,0.65,1.2,2.1,3.5,5.5)$. The declared weights
2161 $(\alpha,\beta)=(1,0.75)$, $(2.5,0.35)$, and $(5,0.15)$ give
2162 minimizing depths $1$, $3$, and $4$, respectively. Their minimum objective
2163 values are $0.7375$, $0.87$, and $0.915$. These follow by evaluating
2164 $\alpha r_d+\beta c_d$ at the seven available depths. The labels certificate,
2165 teaching, and archive name these three supplied objectives rather than
2166 measured preferences of actual readers.
2167 
2168 \begin{figure}[htbp]
2169 \centering
2170 \includegraphics[width=\linewidth]{fig_12_refinement_goals.pdf}
2171 \caption{Three declared objectives on the same finite depth set. Square markers select the exact minimum: depth one for certificate, three for teaching, and four for archive. The weights define these tasks; they are not estimates of how every reader should study a proof.}
2172 \label{fig:refinement}
2173 \end{figure}
2174 
2175 \Needspace{12\baselineskip}
2176 \subsection{An independently checkable decoder}
2177 
2178 Take two archives with the same certificate output but different retained side answers. The following code executes the collision alternative. It then checks the result without running the producer again.
2179 \begin{lstlisting}[language=Python]
2180 from proof_path_theory import factor_task, verify_factorization
2181 encoding = {"archive0": "certificate", "archive1": "certificate"}
2182 task = {"archive0": "0", "archive1": "1"}
2183 result = factor_task(encoding, task)
2184 assert not result.sufficient
2185 assert verify_factorization(encoding, task, result)
2186 \end{lstlisting}
2187 The witness names both archives. It is evidence that this declared task cannot be recovered from this encoding on this domain. It says nothing about whether the shared proof certificate is valid. The package's new worked script also prints the positive decoder, the protected-rule obstruction, and the semantic-cover derivations.
2188 
2189 \section{Reference implementation}
2190 \label{sec:old21}
2191 
2192 The repository implements the finite theory as the Python package \texttt{proof\_path\_theory}. The public modules are organized by mathematical responsibility.
2193 
2194 \begingroup\small
2195 \begin{longtable}{@{}p{0.24\linewidth}p{0.68\linewidth}@{}}
2196 \toprule
2197 Module & Responsibility\\
2198 \midrule
2199 \endhead
2200 \texttt{model.py} & Typed nodes, justifications, evidence records, acyclicity, ancestry, and finite derivability.\\
2201 \texttt{certificate.py} & Certificate validation, unique AND-DAG cores, exact minimum certificate search, and certificate cost.\\
2202 \texttt{compression.py} & Task sufficiency, recoverability preorder, loss reports, compression debt, representation utilities, and Pareto fronts.\\
2203 \texttt{bridges.py} & Reachability, domination-based criticality, exact retention, greedy retention, and finite submodularity checks.\\
2204 \texttt{review.py} & Equicorrelated covariance, effective reviewer count, generalized least squares, and shared-bias mean squared error.\\
2205 \texttt{audit.py} & Audit queue simulation, rate regimes, and explicit priority scores.\\
2206 \texttt{refinement.py} & Goal-relative refinement decisions, optimal depth, and stopping rules.\\
2207 \texttt{versioning.py} & Affected descendants, append-only checks, ledger snapshots, and provenance digests.\\
2208 \texttt{ambient.py} & Finite declared view fibers, restriction checks, and arrow-cover gluing.\\
2209 \texttt{realization.py} & Exact binary elimination, protected fibers, obstruction witnesses, and observation gain.\\
2210 \texttt{views.py} & Local field models, whole-support gluing, declared countermodels, and intersection diagrams.\\
2211 \texttt{extension.py} & Least models preserving true and false observations, with replayable forbidden-node derivations.\\
2212 \path{semantic_cover.py} & Entailment certificates for redundant supports, countermodels to universal gluing, and checked semantic gluing.\\
2213 \texttt{recovery.py} & Factorization on explicit archive families, collision witnesses, joint task schemes, and decoder composition.\\
2214 \path{trace_codec.py} & Versioned indexed exchange, strict and causal trace replay, and an independent result checker.\\
2215 \texttt{io.py} & Stable JSON import and export for proof fields and certificates.\\
2216 \texttt{cli.py} & Command-line validation, core extraction, minimum certificate search, and certificate audit.\\
2217 \bottomrule
2218 \end{longtable}
2219 \endgroup
2220 
2221 \subsection{Command-line interface}
2222 
2223 The main commands are:
2224 
2225 \begin{lstlisting}[language=bash]
2226 proof-path validate examples/and_dag.json
2227 proof-path core examples/and_dag.json --output core.json
2228 proof-path minimum examples/alternative_proofs.json --output minimum.json
2229 proof-path audit examples/and_dag.json core.json
2230 \end{lstlisting}
2231 
2232 
2233 
2234 \subsection{JSON contract}
2235 
2236 A proof field file contains:
2237 \begin{itemize}
2238 \item a schema version and metadata.
2239 \item required premises and targets.
2240 \item typed nodes with value and cost vectors.
2241 \item typed evidence records with scope and certification flags.
2242 \item justifications with premise sets, conclusions, rules, evidence references, and certification flags.
2243 \end{itemize}
2244 
2245 The named proof-field schema is intentionally plain. It can be produced by a proof assistant adapter, a research notebook, a theorem ledger, or a hand-written example. The positional trace-exchange format in Section~\ref{sec:trace-wire} is a separate, versioned contract. Neither an imported certification flag nor a successful schema check establishes semantic validity.
2246 
2247 \subsection{Tests and build discipline}
2248 
2249 The regression suite covers graph validation, derivability, certificate extraction, alternative proofs, schema boundaries, and input validation. It also exercises loss vectors, task sufficiency, bridge coverage, retention, review covariance, audit queues, refinement, version propagation, JSON round trips, and the command line. The dated verification record gives the executed count for each edition.
2250 
2251 A separate deterministic cross-check compares the exact certificate solver with brute-force enumeration over eighteen cost profiles, tests the greedy cardinality guarantee on one hundred generated coverage instances, verifies 1,024 retention-algebra identities, and compares the effective-reviewer formula with direct covariance calculations in 114 parameter settings.
2252 
2253 The extension cross-check exhausts all forward rule subsets on three ordered nodes, every admitted-leaf set, every positive and negative observation set, and every node-covering patch family. An independent truth-table calculation checks feasibility and universal gluing. A separate enumeration compares encodings, task fibers, joint task partitions, and decoder composition on archive domains of at most four elements. These are bounded finite comparisons, not empirical models of mathematical practice.
2254 
2255 The trace conformance suite adds independently enumerated finite models, canonical JSON records, and malformed or altered certificates. Its actual byte stream is processed by the Lean checker built in the current formal run. The report records each verdict and the exact input and output hashes. Rejection of a malformed record is not counted as a proof of an impossible mathematical request.
2256 
2257 The general Lean proofs now establish the specified trace checker and typed codec. The Python producer, Python checker implementation, standard text parser, and source-address adapter retain separate conformance evidence.
2258 
2259 The tests and cross-checks verify the implementation of finite definitions and examples. They do not replace the proofs in this monograph. Conversely, the proofs do not guarantee that a software implementation is free of defects. The release keeps both forms of verification.
2260 
2261 
2262 \section{What the theory establishes}
2263 \label{sec:old26}
2264 
2265 The finite theory establishes the following structural facts.
2266 
2267 \begin{enumerate}
2268 \item A proof field can represent conjunction within a justification and alternatives among justifications without confusing candidate edges with certified edges.
2269 \item Derivability in a finite acyclic selected subfield is well defined and computable in topological order.
2270 \item A fixed AND-DAG, expanded only outside its admitted leaves, has a least certificate pair.
2271 \item Alternative derivations make minimum certificate selection NP-complete in general.
2272 \item Compression is meaningful only relative to a task family.
2273 \item Task-relative recoverability forms a preorder and a quotient partial order.
2274 \item Verification loss, discovery loss, meaning loss, bridge loss, and audit loss can diverge.
2275 \item Expected reconstruction debt decreases monotonically as more required material is retained.
2276 \item Bridge criticality is domination in the declared future-reach graph.
2277 \item Weighted future reach is monotone and submodular.
2278 \item Greedy cardinality retention has the standard $(1-1/e)$ guarantee.
2279 \item Append-only certified updates preserve existing derivability.
2280 \item The forward dependency closure is the least set containing the changed nodes and closed under outgoing dependency edges. It marks potential review, not automatic falsehood.
2281 \item Positive review dependence lowers the variance-equivalent count. Under a positive definite covariance model, generalized least squares gives the minimum-variance unbiased linear aggregate.
2282 \item Constant-rate audit queues have an exact stable, critical, or unstable classification.
2283 \item Optimal proof expansion depth depends on the presentation goal.
2284 \end{enumerate}
2285 
2286 These results turn the original methodological insight into a finite mathematical branch with explicit objects, algorithms, complexity, and failure boundaries.
2287 
2288 The extension results add three further capabilities. A protected rule-model request returns its least feasible model or a derivation of a forbidden node. A cover has universal gluing exactly when its visible rules entail every original rule. A representation admits a task decoder exactly when equal encodings have equal task answers. These outputs are respectively model witnesses, rule derivations, and decoding or collision witnesses. None can replace the others merely because it is called a certificate.
2289 
2290 
2291 \noindent The realization theory gives the proof field a contravariant diagram of local models and an explicit equivalence with its coherent sections. Whole-support gluing proves extension from suitably covering patches. The protected linear alternative classifies feasible fibers and supplies normalized witnesses for infeasibility. Exact finite-field counts yield an information formula only after a uniform distribution is chosen. The native exporter supplies syntactic dependencies from compiled declarations, not the complete history of discovery.
2292 
2293 
2294 \section{Limitations and claim boundaries}
2295 \label{sec:old27}
2296 
2297 Proof Path Theory does not establish a theorem by preserving the history of an argument. A richly documented wrong proof remains wrong. Bridge value is not validity. Explanatory power is not validity. Consensus is not validity. The certified subfield remains the object that carries deductive force.
2298 
2299 The dependency graph is a declared model. It records the dependencies that were formalized, not every historical influence on discovery. Tacit knowledge, visual intuition, unrecorded conversations, and changes in vocabulary may be absent.
2300 
2301 The value and cost coordinates are task models. Verification can often be specified sharply. Meaning and future bridge value are partly prospective. Their use is justified when assumptions are stated, not when the numbers are treated as intrinsic physical constants.
2302 
2303 The finite bridge graph does not predict every future theorem. It supports conditional statements of the form: under these declared future targets and transfer edges, this retention policy preserves this amount of modeled reach.
2304 
2305 The exact minimum certificate algorithm is exponential in the worst case. The package makes this limitation explicit through a search-state bound.
2306 
2307 The review and queue models are deliberately elementary. They isolate dependence and capacity effects, but they do not model every institutional or psychological feature of mathematical review.
2308 
2309 Finally, the monograph does not claim that graphs, hypergraphs, proof theory, submodular optimization, covariance-aware aggregation, or queueing recurrences were invented here. The contribution is the formal assembly of these structures around proof compression, discovery fields, mathematical memory, and versioned proof portfolios.
2310 
2311 
2312 \paragraph{The remaining implementation boundary.} Theorem~\ref{res:trace:json} proves the meaning of an accepted decoded answer. It does not prove that every named-field export preserves its source, or that the text parser and Python producer always realize that contract. Those are the next refinement obligations, not hypotheses silently supplied by successful tests.
2313 
2314 \section{Open theorem program}
2315 \label{sec:old28}
2316 
2317 The finite protected-extension, semantic-cover, and attained-decoder problems developed in this edition are closed under their stated hypotheses. The questions below concern stronger interfaces. In particular, the rule transport sends one source rule to one target rule and is not asserted to be a general equivalence of proof fields. A transport into a derived target proof, executable correctness of the producers, and richer semantic objects remain distinct next steps.
2318 
2319 
2320 \begin{problem}[Proof-path view functors and comparison]
2321 \label{res:28:1}
2322 The declared-field local-model functor and whole-support gluing are established here. Extend the checked interface to richer proof-state representations, and verify the implementation of general proof assistant adapters. Determine when objects with symmetry require nonabelian or higher descent rather than the strict set-valued construction.
2323 \end{problem}
2324 
2325 \begin{problem}[Counterfactual proof-search observations]
2326 \label{res:28:2}
2327 Study which observations on a finite realization fiber yield the greatest task-relative reduction of uncertainty per unit cost. Extend the binary rank theorem to controlled infinite or nonlinear settings only after specifying distributions, admissible questions, and the semantics of proof state.
2328 \end{problem}
2329 
2330 \begin{problem}[Collective evaluation without shared-context confounding]
2331 \label{res:28:3}
2332 Design preregistered evaluations of identical certified mathematics under randomized labels and alternative explanatory contexts. Separate measurement of interpretation differences from independent verification of correctness, and test whether models of correlated review predict actual audit errors.
2333 \end{problem}
2334 
2335 
2336 
2337 Further directions include the following problems.
2338 
2339 \begin{problem}[Infinite proof fields]
2340 \label{res:28:4}
2341 Develop locally finite and countable proof fields with conditions guaranteeing that finite certificates approximate an infinite derivation without losing domain or convergence information.
2342 \end{problem}
2343 
2344 \begin{problem}[Parameterized certificate complexity]
2345 \label{res:28:5}
2346 Classify minimum certificate selection by treewidth, number of alternative justifications, justification arity, shared-subproof width, and target count. Identify fixed-parameter tractable regimes and approximation bounds.
2347 \end{problem}
2348 
2349 \begin{problem}[Probabilistic bridge calibration]
2350 \label{res:28:6}
2351 Replace declared bridge weights by calibrated posterior models while keeping conjectural reach separate from certified derivability.
2352 \end{problem}
2353 
2354 \begin{problem}[Proof assistant interoperability]
2355 \label{res:28:7}
2356 Construct adapters that export stable claim identifiers, primitive dependencies, scopes, and proof terms from existing formal systems into the common proof-field schema.
2357 \end{problem}
2358 
2359 \begin{problem}[Higher proof transformations]
2360 \label{res:28:8}
2361 Model transformations between proofs, transformations between transformations, and coherent compiler pipelines in a higher categorical setting.
2362 \end{problem}
2363 
2364 \begin{problem}[Privacy and attribution]
2365 \label{res:28:9}
2366 Design proof archives that preserve provenance and priority while allowing private notes, embargoed routes, and sensitive collaboration records to remain access controlled.
2367 \end{problem}
2368 
2369 \begin{problem}[Empirical validation]
2370 \label{res:28:10}
2371 Study real mathematical projects to estimate recovery costs, audit bottlenecks, and the predictive value of bridge-retention scores. Such work should test the models rather than assume them.
2372 \end{problem}
2373 
2374 \begin{problem}[Distributed audit systems]
2375 \label{res:28:11}
2376 Extend the queue model to heterogeneous reviewers, dependent tasks, rework, priority classes, and claims whose audit cost changes after neighboring claims are resolved.
2377 \end{problem}
2378 
2379 
2380 \clearpage
2381 \section{Conclusion}
2382 \label{sec:old29}
2383 
2384 A proof certificate and its surrounding proof field answer different mathematical questions. The field need not consist only of viable derivations. It can retain failed strategies and genuine local refutations without allowing either to masquerade as global unprovability. A checked contravariant system of local field models gives an explicit bridge to Komorebi Space. Whole-support coverage identifies a constraint that pairwise dependencies can miss. The semantic-cover criterion now determines exactly when visible rules recover a missing constraint. In the linear finite case, protected observations admit exact success or failure certificates and a measurable information gain. A separate review model distinguishes proof correctness from correlated social interpretation.
2385 
2386 
2387 
2388 A final proof is indispensable, but it is not always the whole mathematical object. The theory distinguishes the certificate from the declared field in which it is recorded. It gives that field typed nodes, alternative justifications, evidence records, task-relative compressions, bridge graphs, version histories, and explicit audit models.
2389 
2390 The central distinction is between derivability within a declared inference system and the wider information retained by its archive. Certified closure records which claims follow from admitted leaves and accepted rules. Its interpretation as mathematical validity depends on the soundness of those leaves and rules. Discovery information serves different tasks: explaining a definition, locating a failed method, preserving a comparison, or opening a route to another problem.
2391 
2392 Compression can preserve the present derivation while losing those other capabilities. Proof Path Theory makes that difference explicit through task families, recovery maps, extension problems, and versioned evidence. The certificate and the surrounding field should therefore be maintained together, with their logical roles kept distinct.
2393 
2394 The final thesis is therefore:
2395 \[
2396 \boxed{\begin{minipage}{0.88\linewidth}
2397 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.
2398 \end{minipage}}
2399 \]
2400 
2401 
2402 \FloatBarrier
2403 \clearpage
2404 \appendix
2405 \markboth{Reference material}{Reference material}
2406 \section{Notation and hypotheses}
2407 \label{app:notation}
2408 
2409 Letters are local to a section. In particular, $A$ denotes required premises in a proof field, but a matrix in the binary examples. The type declarations, not the letter alone, determine the object.
2410 
2411 \begingroup\small
2412 \begin{longtable}{@{}L{0.24\linewidth}L{0.71\linewidth}@{}}
2413 \toprule
2414 Symbol & Meaning \\
2415 \midrule
2416 \endhead
2417 $\Pcal$, $V$, $\Jcal$ & A declared proof field, its nodes, and its justifications. \\
2418 $A$, $L$, $T_0$ & Required premises, admissible leaves, and requested targets, with $A\subseteq L$. \\
2419 $(K,H)$ & Selected nodes and certified justification records. Only usable rules contribute to derivability. \\
2420 $D_{\mathrm{cert}}(K,H)$ & The least certified closure in the selected record. \\
2421 $\Anc_L(T_0)$ & Backward ancestry expanded only outside the admissible leaves. \\
2422 $\mathcal M_F(U)$ & Local models on patch $U$ satisfying all certified rules supported entirely in $U$. \\
2423 $\Gamma(\mathcal M_F)$ & Coherent families of those local models under restriction. \\
2424 $\operatorname{cl}_F(S)$ & The least declared rule model containing the positive observations $S$ and all admitted leaves. \\
2425 $\operatorname{Ext}_F(S,N)$ & Rule models containing $S$ and avoiding the negative observations $N$. \\
2426 $F_{\mathcal U}$ & The same field with only rules whose entire supports appear in a covering patch. \\
2427 $Q(a)=(q_i(a))_i$ & The joint task representation, least in retained distinctions for its task family. \\
2428 $\mathscr A$, $C$, $q$ & A class of possible archives, an encoding scheme, and a task on that class. \\
2429 $P_K(S)=S\cap K$ & Pure retention of records selected by a fixed mask. \\
2430 $D:E\to R$, $p:E\to S$ & A linear defect and a protected observable. The repair condition is $Dy=0$, $p(y)=p(x)$. \\
2431 $H=\ker D\cap\ker p$ & The ambiguity space of a nonempty protected fiber. This $H$ is not a set of justifications. \\
2432 $U_M(S)$ & Weighted target reach from the mandatory starts and a selected supplement, in a fixed directed bridge graph. \\
2433 $n_{\mathrm{eff}}$ & A real, variance-equivalent review count in the specified covariance model. \\
2434 \bottomrule
2435 \end{longtable}
2436 \endgroup
2437 
2438 \subsection*{Assumptions that change the conclusions}
2439 The unique-core theorem uses backward expansion that stops at admissible leaves and proves a least \emph{pair} of record sets. The compression results quantify over a whole archive class with one decoder for each task. Weighted domination counts only targets reachable before deletion. The greedy ratio requires a positive cardinality budget, with zero and saturated budgets handled separately.
2440 
2441 Whole-support gluing is sufficient when the patches cover all nodes and every complete certified rule support. More generally, node coverage and entailment of every original rule by the visible rules are necessary and sufficient for universal gluing. Merely covering pairwise dependencies is not sufficient in general. The linear alternative requires a field. General algebraic functionals need not be bounded under an added topology. The information formula requires a finite field, a finite-dimensional feasible affine fiber, and a uniform distribution.
2442 
2443 Endpoint equivalence fixes the complete assumption context. A refinement chain preserves the chosen tasks only when the corresponding recovery condition holds. The unrestricted positive-rule model always contains the full node set as a model. Nonempty global model spaces can still have empty prescribed extension fibers. Provenance change detection distinguishes information lost during serialization from collisions of different serialized bytes.
2444 
2445 The review mean is unbiased only when its error means vanish. Its effective count requires positive marginal variance and positive variance of the mean. A minimum-variance aggregate allows real weights and assumes a known positive definite covariance matrix. No probability of mathematical correctness follows from these assumptions alone.
2446 
2447 
2448 
2449 \clearpage
2450 \section{Theorem ledger}
2451 \label{app:ledger}
2452 
2453 \emph{Written} denotes a written proof. \emph{Lean} denotes the specified interface with fresh compiler and kernel-replay evidence in this edition, not a formalization of the entire monograph. \emph{Mixed} distinguishes checked counts from their written probabilistic interpretation. The separate Lean concordance lists every source declaration and its scope.
2454 
2455 \begingroup\small
2456 \renewcommand{\arraystretch}{1.04}
2457 \begin{longtable}{@{}L{0.115\linewidth}L{0.70\linewidth}L{0.105\linewidth}@{}}
2458 \toprule
2459 {\sffamily\small ID} & {\sffamily\small RESULT AND IMPLEMENTATION SUPPORT} & {\sffamily\small EVIDENCE}\\
2460 \midrule
2461 \endfirsthead
2462 \toprule
2463 {\sffamily\small ID} & {\sffamily\small RESULT AND IMPLEMENTATION SUPPORT} & {\sffamily\small EVIDENCE}\\
2464 \midrule
2465 \endhead
2466 \bottomrule
2467 \endfoot
2468 PPT-001 & Finite derivability is unique and computable in topological order.\newline{\footnotesize\color{KomorebiMuted}\path{ProofField.derive}} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2469 PPT-002 & An AND-DAG has a least certificate pair, stopping at admissible leaves.\newline{\footnotesize\color{KomorebiMuted}\path{unique_and_dag_certificate}} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2470 PPT-003 & AND-DAG core extraction is linear with indexed adjacency.\newline{\footnotesize\color{KomorebiMuted}graph algorithm, not a runtime certificate} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2471 PPT-004 & Minimum Certificate Decision is NP-complete.\newline{\footnotesize\color{KomorebiMuted}Set Cover example} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2472 PPT-005 & Certified paths transport functorially.\newline{\footnotesize\color{KomorebiMuted}structural theorem} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2473 PPT-006 & Local auditable certificates compose under a certificate functor.\newline{\footnotesize\color{KomorebiMuted}structural theorem} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2474 PPT-007 & Task information loss follows from compression collisions.\newline{\footnotesize\color{KomorebiMuted}task API} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2475 PPT-008 & Recoverability is a preorder.\newline{\footnotesize\color{KomorebiMuted}\path{recoverability_preorder}} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2476 PPT-009 & The quotient by mutual recoverability is a partial order.\newline{\footnotesize\color{KomorebiMuted}equivalence API} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2477 PPT-010 & Least sufficient retention masks depend on the task family.\newline{\footnotesize\color{KomorebiMuted}finite countermodel} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2478 PPT-011 & Zero verification loss can coexist with positive discovery loss.\newline{\footnotesize\color{KomorebiMuted}AND-DAG example} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2479 PPT-012 & Compression debt is monotone under retention.\newline{\footnotesize\color{KomorebiMuted}\path{compression_debt}} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2480 PPT-013 & Bridge criticality equals target domination.\newline{\footnotesize\color{KomorebiMuted}\path{dominated_targets}} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2481 PPT-014 & Weighted future reach is monotone and submodular.\newline{\footnotesize\color{KomorebiMuted}exhaustive finite checker} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2482 PPT-015 & Greedy cardinality retention achieves at least $1-1/e$ for positive feasible cardinality budgets.\newline{\footnotesize\color{KomorebiMuted}greedy and exact solvers} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2483 PPT-016 & Append-only certified updates preserve derivability.\newline{\footnotesize\color{KomorebiMuted}versioning check} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2484 \pagebreak
2485 PPT-017 & Forward dependency closure is the minimal closed syntactic review set.\newline{\footnotesize\color{KomorebiMuted}\path{affected_descendants}} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2486 PPT-018 & Equicorrelated review has the stated effective count.\newline{\footnotesize\color{KomorebiMuted}covariance implementation} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2487 PPT-019 & GLS weights minimize unbiased linear review variance.\newline{\footnotesize\color{KomorebiMuted}\path{generalized_least_squares_weights}} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2488 PPT-020 & Constant-rate audit queues have exact stable, critical, and unstable regimes.\newline{\footnotesize\color{KomorebiMuted}queue simulation} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2489 PPT-021 & Optimal expansion depth depends on the goal.\newline{\footnotesize\color{KomorebiMuted}refinement implementation} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2490 PPT-022 & Pure retention projections commute and are idempotent.\newline{\footnotesize\color{KomorebiMuted}\path{retention_projection}} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2491 PPT-023 & Retention masks form a Boolean lattice.\newline{\footnotesize\color{KomorebiMuted}\path{retention_meet}, \path{retention_join}} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2492 PPT-024 & A locally refuted route can coexist with another certified route.\newline{\footnotesize\color{KomorebiMuted}Alternative justification field} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2493 PPT-025 & A checked local refutation persists under unchanged interpretation.\newline{\footnotesize\color{KomorebiMuted}Scoped witness principle} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2494 PPT-026 & Finite arrow-covered matching views glue uniquely.\newline{\footnotesize\color{KomorebiMuted}\path{FiniteViewSystem.glue}} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2495 PPT-027 & Protected realizations admit exact solutions or obstruction witnesses, with classified fibers.\newline{\footnotesize\color{KomorebiMuted}\path{analyze_affine_realizations}} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2496 PPT-028 & Finite affine fibers have exact observation counts. Uniform entropy is a written corollary.\newline{\footnotesize\color{KomorebiMuted}Lean counts and binary tests} & {\sffamily\small\color{KomorebiTeal}Mixed}\\[0pt]
2497 PPT-029 & Common offset and correlated error have the displayed reviewer MSE.\newline{\footnotesize\color{KomorebiMuted}\path{shared_bias_mse}} & {\sffamily\small\color{KomorebiTeal}Written}\\[0pt]
2498 PPT-030 & Declared derivability equals membership in every declared field model.\newline{\footnotesize\color{KomorebiMuted}Closure and countermodels} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2499 PPT-031 & Local models form a contravariant diagram with an explicit realization equivalence.\newline{\footnotesize\color{KomorebiMuted}\path{Field.modelEquivSections}} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2500 PPT-032 & Whole-support matching local models glue. Pairwise coverage can fail.\newline{\footnotesize\color{KomorebiMuted}Proof-field views and counterexample} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2501 \pagebreak
2502 PPT-033 & All predicate tasks are sufficient exactly for injective encodings.\newline{\footnotesize\color{KomorebiMuted}Compression collision theorem} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2503 PPT-034 & Attained decoding is equivalent to fiber constancy. The decoder is unique on attained values.\newline{\footnotesize\color{KomorebiMuted}Recovery and finite decoder checks} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2504 PPT-035 & Joint tasks are sufficient exactly when each coordinate task is. Recovery maps compose.\newline{\footnotesize\color{KomorebiMuted}Recovery and joint partitions} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2505 PPT-036 & Protected rule data have an extension exactly when their least closure avoids the forbidden nodes.\newline{\footnotesize\color{KomorebiMuted}Extension and independent trace replay} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2506 PPT-037 & Closing earlier data before later data preserves the closure. Adding observations preserves obstructions.\newline{\footnotesize\color{KomorebiMuted}Extension} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2507 PPT-038 & A cover has universal gluing exactly when its visible rules entail every original rule.\newline{\footnotesize\color{KomorebiMuted}SemanticCover and finite cover certificates} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2508 PPT-039 & Typed rule transports preserve derivations, pull models back, and transport obstruction witnesses.\newline{\footnotesize\color{KomorebiMuted}RuleTransport} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2509 PPT-040 & A valid rule transport can collapse compatible source observations into an impossible target request.\newline{\footnotesize\color{KomorebiMuted}ExtensionExamples} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2510 PPT-041 & Hashing cannot add recoverable tasks. Restricted injectivity prevents further task loss.\newline{\footnotesize\color{KomorebiMuted}Recovery} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2511 PPT-042 & Executable trace replay preserves derivability and composes.\newline{\footnotesize\color{KomorebiMuted}Trace and TraceCompleteness} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2512 PPT-043 & Accepted complete traces identify the least seeded model.\newline{\footnotesize\color{KomorebiMuted}Trace and TraceCompleteness} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2513 PPT-044 & Accepted forbidden-node witnesses exist exactly for infeasible protected requests.\newline{\footnotesize\color{KomorebiMuted}Trace and TraceCompleteness} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2514 PPT-045 & Typed JSON encoding has a left inverse and is injective.\newline{\footnotesize\color{KomorebiMuted}Trace.Wire} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2515 PPT-046 & Accepted JSON records certify the exact decoded protected answer.\newline{\footnotesize\color{KomorebiMuted}Trace.Wire} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2516 PPT-047 & Valid indexed problems derive only bounded node addresses.\newline{\footnotesize\color{KomorebiMuted}Trace.Wire} & {\sffamily\small\color{KomorebiTeal}Lean}\\[0pt]
2517 \end{longtable}
2518 \renewcommand{\arraystretch}{1.0}
2519 \endgroup
2520 
2521 \clearpage
2522 \section{Reproduction and verification records}
2523 \label{app:reproduction}
2524 
2525 The package includes written proofs, exact finite producers and independent result checkers, and a fresh pinned Lean run. All eighteen modules were rebuilt and replayed. The mathematical imports remain cached and are not represented as freshly rebuilt dependencies. The current compiler record is \path{evidence/formal_1.8.0/}, while older evidence retains its original version. Source changes and the new mathematical environments are listed in the current progress ledger and publication report.
2526 
2527 Before modifying the extracted package, check the delivered files:
2528 \begin{lstlisting}[language=bash]
2529 python scripts/check_manifest.py
2530 \end{lstlisting}
2531 Then run the finite and publication checks:
2532 \begin{lstlisting}[language=bash]
2533 python -m pip install -e ".[release]" --no-build-isolation
2534 python -m pytest -o addopts='' -q
2535 python scripts/deep_validation.py
2536 python scripts/verify_bridge.py
2537 python scripts/check_recovery_extension.py
2538 python scripts/check_trace_exchange.py
2539 python scripts/verify_publication_edition.py
2540 \end{lstlisting}
2541 
2542 Regenerate the exact figures with:
2543 \begin{lstlisting}[language=bash]
2544 python scripts/design_figures.py
2545 \end{lstlisting}
2546 The publication edition is 1.8.0 and the Python distribution is 1.6.0. This distribution adds a versioned trace-exchange codec, an independent indexed checker, and export/check commands without changing the existing named-field schema or provenance byte format. Its historical migration remains documented in \path{docs/PROVENANCE_FORMAT.md}. Installation may obtain build and numerical dependencies unless they are already supplied locally.
2547 
2548 The manuscript can be rebuilt independently from \path{docs/}:
2549 \begin{lstlisting}[language=bash]
2550 cd docs
2551 pdflatex -interaction=nonstopmode -halt-on-error Proof_Path_Theory.tex
2552 pdflatex -interaction=nonstopmode -halt-on-error Proof_Path_Theory.tex
2553 pdflatex -interaction=nonstopmode -halt-on-error Proof_Path_Theory.tex
2554 \end{lstlisting}
2555 
2556 \clearpage
2557 \subsection*{Formal and cross-language replay}
2558 A separate formal replay, with the pinned runtime already available, uses:
2559 \begin{lstlisting}[language=bash]
2560 python scripts/verify_lean.py --runtime /path/to/portable-kit
2561 \end{lstlisting}
2562 
2563 For PowerShell, extraction precedes installation:
2564 \begin{lstlisting}[language={},basicstyle=\ttfamily\fontsize{9.5}{11.4}\selectfont]
2565 $zip = '.\Proof_Path_Theory_Monograph_1.8.0.zip'
2566 Expand-Archive -LiteralPath $zip -DestinationPath '.\proof-path-release'
2567 Set-Location '.\proof-path-release\Proof_Path_Theory_Monograph_v1.8.0'
2568 python scripts/check_manifest.py
2569 python -m pip install -e ".[release]" --no-build-isolation
2570 python -m pytest -o addopts='' -q
2571 \end{lstlisting}
2572 
2573 The trace interface can be exercised without a Lean runtime:
2574 \begin{lstlisting}[language=bash]
2575 proof-path wire-export examples/and_dag.json --negative B --output-prefix trial
2576 proof-path wire-check trial.problem.json trial.certificate.json
2577 \end{lstlisting}
2578 The export writes the fixed indexed problem, the checked result, and the node/rule address book separately. The general AST theorem is in \path{ProofPath.TraceWire}. The executed byte adapter is \path{formal/CheckTraceJson.lean}; the fresh formal verifier runs it against the generated canonical exchange cases. The address book must still be checked against the intended source snapshot.
2579 
2580 The dated report identifies the commands actually run. These checks do not supply independent peer review, universal software verification, or empirical validation of the social models. The redistribution-license decision remains open.
2581 
2582 \clearpage
2583 \section{A complete minimal proof-field record}
2584 \label{app:schema}
2585 
2586 The following record defines both its premise and its target. It is a complete importable example rather than a schema fragment with an unresolved target reference. The rule is explicitly assumed for this demonstration. Its declared certification must not be mistaken for a proof of an arbitrary implication between the displayed labels.
2587 
2588 \begin{lstlisting}[language={},basicstyle=\ttfamily\fontsize{9.5}{11.4}\selectfont]
2589 {
2590   "schema_version": "1.0",
2591   "premises": ["A"],
2592   "targets": ["B"],
2593   "nodes": [
2594     {"id": "A", "label": "Premise A", "kind": "premise"},
2595     {"id": "B", "label": "Target B", "kind": "claim"}
2596   ],
2597   "evidence": [
2598     {
2599       "id": "e-rule",
2600       "kind": "assumption",
2601       "source": "Declared demonstration rule A implies B",
2602       "scope": "This finite inference model only",
2603       "certifies": true
2604     }
2605   ],
2606   "justifications": [
2607     {
2608       "id": "j1",
2609       "premises": ["A"],
2610       "conclusion": "B",
2611       "rule": "assumed implication",
2612       "certified": true,
2613       "evidence_ids": ["e-rule"]
2614     }
2615   ]
2616 }
2617 \end{lstlisting}
2618 
2619 The file \path{examples/minimal_monograph.json} contains this record. The public importer checks its identifiers and Boolean fields, and declared closure reaches \texttt{B}. Mathematical soundness still requires the explicit interpretation contract of Section~\ref{sec:old24}.
2620 
2621 \clearpage
2622 \phantomsection
2623 \addcontentsline{toc}{section}{References}
2624 \begin{thebibliography}{99}
2625 
2626 \bibitem{komorebi-space}
2627 Komorebi P.
2628 \textit{Komorebi Space: Coherent Realizations, Obstructions, and Descent}.
2629 Monograph, 2026. The finite proof-field view construction here is a relative application of its strict coherent realization principle, not a claim of unrestricted semantic completeness.
2630 
2631 \bibitem{buss}
2632 S. R. Buss, editor.
2633 \textit{Handbook of Proof Theory}.
2634 Elsevier, 1998.
2635 
2636 \bibitem{cover-thomas}
2637 T. M. Cover and J. A. Thomas.
2638 \textit{Elements of Information Theory}.
2639 Second edition, Wiley, 2006.
2640 
2641 \bibitem{diestel}
2642 R. Diestel.
2643 \textit{Graph Theory}.
2644 Fifth edition, Springer, 2017.
2645 
2646 \bibitem{garey-johnson}
2647 M. R. Garey and D. S. Johnson.
2648 \textit{Computers and Intractability: A Guide to the Theory of NP-Completeness}.
2649 W. H. Freeman, 1979.
2650 
2651 \bibitem{knuth}
2652 D. E. Knuth.
2653 \textit{Literate Programming}.
2654 CSLI Publications, 1992.
2655 
2656 \bibitem{maclane}
2657 S. Mac Lane.
2658 \textit{Categories for the Working Mathematician}.
2659 Second edition, Springer, 1998.
2660 
2661 \bibitem{nemhauser}
2662 G. L. Nemhauser, L. A. Wolsey, and M. L. Fisher.
2663 An analysis of approximations for maximizing submodular set functions I.
2664 \textit{Mathematical Programming}, 14:265--294, 1978.
2665 
2666 \bibitem{troelstra}
2667 A. S. Troelstra and H. Schwichtenberg.
2668 \textit{Basic Proof Theory}.
2669 Second edition, Cambridge University Press, 2000.
2670 
2671 \end{thebibliography}
2672 
2673 \end{document}

Back to source controls

Back to Proof Path Theory