1. Three kinds of evidence
A distributed archive can verify a passage before it can certify the final ranked answer or recover the original PDF. Each conclusion has its own certificate. This distinction lets a query remain useful during a network partition while reporting the scope it has actually searched. The attached full paper develops the proofs, binary grammar, threat model, and reproducible examples.
A pinned context $\gamma$ consists of an archive ID, a signed snapshot, the authorized policy, and an operation with its fixed evaluator. A search context also names the query normalization, ranking mode, model and corpus statistics, $K$, and a total tie order. Its finite universe of obligations $R_\gamma$ can be the eligible index slots. A PDF restoration context has typed fragment slots and a per-stripe threshold. The publisher key is pinned through a trusted side channel. Cryptographic binding is relative to that authority and snapshot.
A hit commits to a document digest, physical PDF page and optional passage index, derived text or OCR status, and a score under the pinned evaluator. It does not certify global rank. Full search verifies a committed representation for every eligible shard or verifies a sound exclusion bound for every omitted candidate. Recovery verifies the document digest after decoding. A search certificate for the index may be complete before any cited PDF is retrievable.
2. Space-valued descent and effective readiness
Let $\mathcal B_\gamma=\mathcal P(R_\gamma)$ with inclusions and the topology in which a family of subobjects covers when its union is the target. Intersection gives pullback stability. At each coordinate $r$, form a category $T_r$ of finite accepted verification transcripts with arrows generated by permitted rewrites. Let $W_r$ consist of designated reversible-for-the-observation refinements, such as removal of redundant local checks. Every rewrite preserves the verified assertion. A physical write, revocation or ordered audit event is outside this inversion rule. Localize as an infinity-category and take its maximal groupoid $E_r=(T_r[W_r^{-1}])^\simeq$. Define $E_\gamma(U)=\prod_{r\in U} E_r$.
Descent theorem. For a cover $(U_i\to U)$, the Čech limit of the values on its iterated intersections is equivalent to $E_\gamma(U)$. Consequently the infinity-topos of sheaves on this finite site is equivalent to $\mathcal S^{R_\gamma}$.
Proof. Fix $r\in U$. Indices $i$ with $r\in U_i$ form a nonempty set $I_r$. The coordinate contributes the cosimplicial diagram $E_r^{I_r^{p+1}}$. The simplicial indexing nerve with $p$-simplices $I_r^{p+1}$ is contractible because it is the nerve of the groupoid with exactly one arrow between every pair. The cotensor limit is $E_r$. Products give descent. Conversely, the singleton cover expresses any sheaf value as the product of its singleton values, since all mixed intersections are empty and a sheaf takes the empty view to a terminal object. These product equivalences are natural. This construction deliberately places shared constraints in the pinned context. A requirement with independent cross-coordinate constraints needs an additional obligation or a different site.
The verifier is effective in the operational sense. Given a finite candidate witness, it terminates with a verified assertion or rejection. Propositional truncation of $E_r$ expresses readiness and an accepted finite transcript realizes it. The sheaf retains verification provenance when the observation distinguishes it. For example, two peers can supply the same bytes with distinct delivery records. A commutation of independent hash and signature checks does not change the order of signed log entries. The localization construction follows Dwyer and Kan and Barwick and Kan. The descent semantics uses spaces as in Higher Topos Theory.
Staggered completion. If $C_t$ is the set of obligations with retained valid witnesses at step $t$, the pinned context and durable cache make $C_t$ monotone. For finite $U\subseteq\bigcup_t C_t$, the maximum of the first acceptance times for $r\in U$ witnesses $U\subseteq C_{t_*}$. This also proves completion for a monotone threshold predicate with finite support. Witnesses can come from nonoverlapping online windows. A silent shard and opaque commitment alone cannot certify an absence or a rank cutoff. The same finite prefix can precede permanent withholding or later delivery of matching committed bytes. A timeout can suspend the job; it cannot supply the missing evidence.
3. Original bytes and exact hybrid ranking
The signed manifest commits to original bytes, ordered fragment identities, and separately to page and index records. Canonical length-delimited framing separates cryptographic domains. The reference uses SHA-256 and Ed25519.
Reconstruction theorem. Use a Reed–Solomon generator $G=VV_0^{-1}$ over $\mathbb F_{2^8}$, with $V$ the Vandermonde matrix for distinct evaluation points and $V_0$ its first $k$ rows. Every $k$-row submatrix $G_I$ is invertible. If a valid manifest binds a codeword, a client verifies each slot against its type, stripe and ordinal commitment and treats a rejected response as an erasure. For $k$ distinct valid slots the unique candidate column is $G_I^{-1}y_I$. Unpadding and checking the final document digest binds the returned PDF to the committed bytes, subject to digest and signature security. Re-encoding and checking the destination slot commitment establishes the correct replacement bytes. The code uses the erasure principle in RFC 5510 and its own framing.
Extract text from a digital page or rasterize and run versioned OCR for image-only pages. Preserve the original bytes independently. Record extraction failure or uncertainty and include it in the declared scope of completeness. Keyword search can use normalized token predicates or BM25 with shared snapshot statistics. Semantic search can use a frozen sentence encoder with pinned weights, tokenizer and numeric rules. A hybrid score can combine these with a fixed global order. Model and extraction changes define a new snapshot. Model-relative exactness and measured human relevance remain separate. See the PDF 2.0 specification, Tesseract, BM25, Sentence-BERT and BEIR.
Top-$K$ merge theorem. For stable candidate identities and one fixed total order, $$ \operatorname{Top}_K(X\cup Y)=\operatorname{Top}_K(\operatorname{Top}_K(X)\cup\operatorname{Top}_K(Y)). $$ A candidate omitted from one local top-$K$ has $K$ distinct better candidates there, all still present after union. Every global winner therefore survives local truncation. On sets of size at most $K$ the merge is commutative, associative and idempotent. Pair it with union of verified coverage coordinates. Coverage grows while intermediate rank positions may change. A worker signature alone does not prove that it evaluated every row. The reference verifies full index blocks and recomputes scores. A proof-carrying optimized profile must establish a bound below the final cutoff for every omitted candidate, with ties included in the order. If fewer than $K$ matches are returned, it must exclude every uncovered eligible match. Approximate nearest-neighbor candidates may be verified hits while exact completeness remains unproven.
Local top lists of ranking channels need not suffice to compute reciprocal rank fusion. In channel orders $(a,x,y,b)$ and $(b,x,y,a)$, the fused winner is $x$ at fusion constant $c>2$ since $2/(c+2)>1/(c+1)+1/(c+4)$ and $2/(c+2)>2/(c+3)$. Neither top-one list contains $x$. The merge theorem applies after the globally comparable fused order is defined. See threshold aggregation and reciprocal rank fusion.
4. Probabilistic progress without synchronous deadlines
Let $T_r$ be first durable valid arrival, possibly infinity, and $D$ first verified manifest availability. Full-block search finishes at the maximum of $D$ and the index arrival times. A single stripe finishes at the maximum of $D$ and the $k$-th verified fragment arrival; take a further maximum across stripes. For independent per-slot delivery probabilities $p_i(t)$, the recovery CDF is the Poisson-binomial upper tail. A shard served by $r$ independent replicas with equal probability $p(t)$ has coverage probability $1-(1-p(t))^r$. Across arbitrarily dependent requirements, subtract the sum of the marginal failure probabilities from one and truncate at zero. A separate cryptographic failure term can be subtracted for the event that delivery is both accepted and correct.
Dependent retry theorem. If, conditional on every reachable history where completion has not yet occurred by $t_{j-1}$, the chance of completing by $t_j$ is at least $a_j$, then $$ \Pr(T>t_m\mid T>t_0)\leq\prod_{j=1}^m(1-a_j). $$ Condition on the previous history and iterate on nested noncompletion events. If $\sum_j a_j=\infty$, continuity of probability and $1-a_j\leq e^{-a_j}$ give almost-sure completion. This requires conditional opportunities and retained progress. High marginal availability in repeated rounds cannot compensate for permanent isolation.
In the full paper's analytic scenario, a $(6,4)$ stripe and eight index shards with three replicas each share a directory requirement. With per-replica valid-delivery probability .92, directory probability .99 and independence of those requirements, joint one-day completion is .9776. A common outage preventing completion with probability .20 reduces it to .7820 when the same conditional model applies outside the outage. These values are illustrative inputs and calculated outcomes, with no claimed field benchmark. The system permits any finite latency and can remain unresolved indefinitely under withholding. Fair retries can suspend and resume by job ID without silently changing the snapshot.
5. Audit, repairs and participation
Every peer must perform the specified hash and audit checks and prove possession of its authorized identity key. The admission contract requires known-answer cryptographic tests and positive and negative audit fixtures. A challenge is fresh and bound to the peer and archive context. The role also needs the applicable network, durable I/O, and extraction or inference interfaces. A VM port whose crypto or audit verifier fails is ineligible to serve.
A production log can authenticate a checkpoint by epoch, log ID, tree size and Merkle root and verify inclusion and prefix consistency with the constructions in RFC 9162. The reference replays a signed hash chain against a locally retained prefix. Two isolated clients can each be shown a valid but different signed branch. A fixed set of $3f+1$ witnesses requiring $2f+1$ signatures prevents acceptance of incompatible prefixes if at most $f$ are Byzantine and every honest witness signs only durable, verified extensions. Any two signer sets intersect in at least $f+1$ witnesses, so at least one honest witness would have had to sign incompatible prefixes. A quorum unavailable during a partition can delay the checkpoint. Signed commitments and read challenges make different claims about custody.
Scrubbing samples or reads committed bytes. For $b$ corrupt blocks among $B$ and an unpredictable uniform sample of $s$ distinct blocks, the chance of finding corruption is $1-\binom{B-b}{s}/\binom{B}{s}$. Rebuild from a valid threshold while it remains obtainable. A production repair intent durably binds the slot and expected replacement before its write, and an idempotent completion record closes the intent after verification. The reference repair command separately commits the object and signed log event. Distributed predecessors include OceanStore and LOCKSS.
6. Platform interpretation and evidence
Abstract states carry the pinned manifest, evidence maps, job state and audit pins. A guarded trace presentation uses finite command traces as 1-cells and invertible coherence cells for checked swaps of independent operations. A platform interpretation maps its verified transcripts to the same evidence space coordinatewise. Restriction commutes with this map, so evidence from distinct admissible platforms may glue in a common context.
For each concrete transition a forward simulation supplies a finite abstract path with the same visible observations and related endpoints. These simulations compose. Replace each intermediate step by its abstract path and concatenate. Induction on trace length then transports the coverage, recovery and audit prefix safety guards to any conforming backend. Liveness additionally requires a retry and persistence policy that realizes the opportunity hypotheses. The theorem is a backend proof obligation, with no mechanized proof of the JVM or operating system.
The build combines the profile's portable payload with the host VM, launcher, role adapters and admission checks. The included Java 17 implementation compiles to a JAR and provides a platform-native build via jpackage. The reference uses full-block exact evaluation, an English concept model and token search, Poppler/Tesseract ingestion, static signed placement, and caller-driven polls and repair. Both the JAR and a Linux x86-64 native launcher passed the synthetic three-process fixture. It checks index coverage across separate peer windows, concept matches without keyword overlap, keyword retrieval from an image-only PDF, byte-exact restoration after a corrupt fragment, successful repair and rejection of changed signatures and audit rollback. The finite checks cover 2,825 erasure subset round trips and a same-key fork against a pinned head. The latency estimates are mathematical examples. Retrieval at field scale and conformance on other hosts are outside the reported tests.
Reproducibility and responsibility
The attached PDF gives the full proofs, protocol and bibliography. The versioned companion contains the manuscript source, compiled JAR, Java sources, native build script, synthetic tests and verification output. The responsible human contributor uses an anonymous byline and authorized the submission. An AI assistant assisted with drafting, implementation and checks. No corpus data or long-lived keys are included.