paper v0.15: the dichotomy named, the question aligned

Two edits. (1) The alternatives paragraph of section 1 now states the
frame the site opens with, in paper register: each alternative fails on
one of two sides — checking cost stays with the consumer, or it
disappears because belief in a label is demanded — and the primitive
studied occupies the point between. (2) The introduction's italic
question said 'opaque provider verdict' where the abstract says
'label'; aligned to label, consistent with the v0.13 verdict/label
separation. Gate green, 25pp, page 2 eye-checked.

README.md

@@ -212,12 +212,12 @@ The log uses:
 
 The deployed instance ([ltl.zkdefi.org](https://ltl.zkdefi.org),
 mirror [`lean-transparency-log`](https://github.com/saymrwulf/lean-transparency-log))
-is live at **19 leaves** (2026-08-08). Entry 12 (2026-07-16) attests the log's own
+is live at **19 leaves** (2026-08-08). Leaf 12 (2026-07-16) attests the log's own
 accumulator machinery — a kernel-checked mechanization of the log's
 security analysis ([`ltl-accumulator-verified`](https://github.com/saymrwulf/ltl-accumulator-verified)),
 appended into the log itself and scoped to the mechanized model; entries
-13–16 re-attest the four Ed25519 forks at 44 certificates each, entry 17
-the accumulator's hardened model, and entry 18 the SLH-DSA verify path —
+13–16 re-attest the four Ed25519 forks at 44 certificates each, leaf 17
+the accumulator's hardened model, and leaf 18 the SLH-DSA verify path —
 the log's first post-quantum entry. The
 producer path that generated it now emits a `scope` block into each leaf
 (guarantees / exclusions / deployment-constraints), so a leaf carries its

paper/README.md

@@ -1,12 +1,20 @@
 # Which file is current?
 
-**`ltl.pdf` / `ltl.tex` — the current paper (v0.11, revised August 2026).**
+**`ltl.pdf` / `ltl.tex` — the current paper (v0.15, revised August 2026).**
 The review process concluded in August 2026. v0.10 folded in the
 corrections queued during the freeze (the closed consistency-verifier
 divergence with its `sn = 0` root cause, replay-harness-integrity
-limitation, claim-matrix row); v0.11 brings the paper up to the live
+limitation, claim-matrix row); v0.11 brought the paper up to the live
 system: the nineteen-leaf dual-signed deployment, the SLH-DSA (FIPS 205)
-verify-path instantiation, and its certificate appendix. The
+verify-path instantiation, and its certificate appendix; v0.12 unified
+entry numbering on 0-based leaf indices; v0.13 is the approachability
+revision from an external-persona referee pass (house terms defined at
+first use, theorem statements carry their own scoping, notation
+collisions resolved, FIPS 205 reference added); v0.14 completes that pass after a
+full-document eye inspection of the published PDF (notation-table rows
+for C and b, HIST chain length renamed to avoid the split-point k); v0.15 names the
+two-sided dilemma explicitly in the introduction and aligns the
+introduction's question with the abstract (label, not verdict). The
 version submitted for review (July 17, 2026, sha256 `7f140356…`) is
 preserved unchanged in this repository's git history. The live copy at
 <https://ltl.zkdefi.org/paper> serves the current revision.

paper/ltl.tex

@@ -48,7 +48,7 @@ showstringspaces=false,breaklines=true,xleftmargin=.5em,xrightmargin=.5em}
 \large A Transparency Model and the Lean Transparency Log}
 \author{Olaf Horvath\\
 \small Olaf.Horvath@zkdefi.org \quad ORCID 0009-0004-8008-5805}
-\date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.11}}
+\date{July 2026 \\ {\normalsize Revised: August 2026 --- v0.15}}
 
 \begin{document}
 \maketitle
@@ -82,11 +82,12 @@ project-specific uninterpreted SHA-256 boundary axiom) and, as its newest
 entry, eleven certificates over the SLH-DSA-SHA2-128s verifier. Since tree
 size 14 every signed head additionally carries a deterministic SLH-DSA
 co-signature --- produced with the parameter set whose verification path the
-log itself attests. The mechanization effort also exposed,
-via differential testing, a nontrivial implementation boundary --- the
-deployed iterative consistency verifier is not extensionally equal to the
-recursive model on malformed size claims --- and the leaf records this
-limitation explicitly. The contribution is a cryptographic distribution
+log itself attests. The mechanization effort also exposed, via
+differential testing, a nontrivial model/implementation divergence --- on
+malformed size claims, the deployed iterative consistency verifier was not
+extensionally equal to the recursive model proved in Lean (since closed;
+this paper reports the pre-closure measurements) --- recorded explicitly
+in the corresponding log entry. The contribution is a cryptographic distribution
 model for machine-checked correctness evidence, with an end-to-end deployed
 instantiation that carries scoped proofs about its own accountability
 machinery.
@@ -111,7 +112,7 @@ This creates a problem that is logically downstream of proof construction:
 \begin{quote}
 \emph{How can a consumer that cannot execute the prover obtain precise,
 accountable evidence about a proof replay, without collapsing the result into
-an opaque provider verdict?}
+an opaque provider label?}
 \end{quote}
 
 A detached signature on the word ``verified'' authenticates an issuer but does
@@ -122,7 +123,10 @@ portability objective. Committees distribute trust but do not themselves fix
 the semantics of the attested result. Succinct proofs of verifier execution
 would provide validity rather than mere accountability, but require a circuit or
 verified-VM representation of the prover and are not yet the deployment
-assumption of the artifacts studied here.
+assumption of the artifacts studied here. Each alternative thus fails on
+one of two sides: the cost of checking stays with the consumer, or it
+disappears because belief in a label is demanded. The primitive studied
+here occupies the point between.
 
 We therefore study a narrower primitive: \emph{accountable delegation of
 deterministic proof replay}. The operator still observes the replay. The
@@ -146,8 +150,10 @@ The Lean Transparency Log (LTL)\footnote{The acronym collides with linear
 temporal logic~\cite{pnueli}; we note the collision once and rely on context.}
 is the complete instantiation evaluated in this paper. Its subjects are four
 Rust Ed25519 codebases with Lean~4~\cite{lean4} certificates against extracted
-models. Its thirteenth public leaf attests the Lean corpus
-that mechanizes the log's own accumulator arguments. Thus the paper's central
+models. Leaf 12 --- its thirteenth entry --- attests the Lean corpus
+that mechanizes the security arguments of the log's own Merkle accumulator
+(the tree of \S\ref{sec:construction} together with its inclusion and
+consistency verifiers). The paper's central
 claim survives replacement of Lean, Ed25519, or RFC~9162 by other components;
 what is essential is the distribution and accountability model.
 
@@ -169,9 +175,9 @@ those observations with their own policy; operator labels can veto but cannot
 grant acceptance. We state clearly that axiom-name equality is not semantic
 identity of theorem statements.
 \item \textbf{A deployed cryptographic case study.}
-The log contains nineteen leaves: three four-fork replay generations for the
-Ed25519 codebases (the newest at 44 certificates per fork), two attestations
-of the accumulator's own Lean corpus (entry 13 carries an environment-derived
+The log contains nineteen leaves: three replay generations across the four
+Ed25519 codebases (the newest at 44 certificates per fork; a \emph{certificate} throughout this paper is one theorem's kernel-checked proof together with its recorded axiom cone), two attestations
+of the accumulator's own Lean corpus (leaf 12 carries an environment-derived
 audit inventory of 222 compiled constants, 61 human-reviewed certificate
 cones, and a single uninterpreted SHA-256 axiom; leaf 17 re-attests the
 hardened state), and --- as leaf 18 --- the log's first post-quantum subject:
@@ -183,7 +189,7 @@ verifier and the recursive model proved in Lean are not extensionally equal:
 there are malformed size/root combinations accepted only by the deployed
 verifier. We characterize 3,867 divergences in 73,573 pinned boundary tests
 --- every one deployed-accepts-only --- and scope the public attestation
-accordingly. (Post-submission closure, July 2026: the divergence was traced to
+accordingly. (Subsequently closed: the divergence was traced to
 the deployed verifier omitting RFC~9162 \S2.1.4.2 Step~7's terminal
 $sn=0$ condition; restoring that one conjunct removes every divergence in the
 pinned family, confirmed by a three-way regression against an independent
@@ -197,16 +203,18 @@ binary correspondence, compiler correctness, extraction faithfulness,
 side-channel resistance, SHA-512 correctness, or execution provenance of the
 signing binary. The present leaf schema identifies theorem declarations by
 repository commit and name, not by a canonical digest of their elaborated Lean
-types. These are explicit boundaries, not hidden qualifications.
+types. These are explicit boundaries, not hidden qualifications
+(Appendix~\ref{app:matrix} tabulates every consumer-facing claim with its
+establishing mechanism and remaining assumption).
 
 \section{The distribution problem}\label{sec:problem}
 
 \subsection{Three evidence modes}
 
 Let a subject repository at commit $g$ contain theorem declarations
-$T_1,\dots,T_q$. A deterministic verifier execution produces an observation
-$O_g$ containing success/failure and the reported assumption cone of each
-$T_i$ --- the set of axioms the checked proof of $T_i$ ultimately rests on. There are three natural ways to consume this result.
+$\Theta_1,\dots,\Theta_q$. A deterministic verifier execution produces an observation
+$O_g$ containing success/failure and the reported \emph{axiom cone} (synonymously, the observed axiom-name set) of each
+$\Theta_i$ --- the set of axioms the checked proof of $\Theta_i$ ultimately rests on. There are three natural ways to consume this result.
 
 \begin{description}[leftmargin=1.5em,itemsep=4pt]
 \item[Direct replay.] The consumer reconstructs the verifier environment and
@@ -293,7 +301,8 @@ A replay attestation $a$ contains at least
 \]
 where $N_i$ is a declaration name, $s_i$ is replay status, and $A_i$ is the
 observed axiom-name set. The deployed schema additionally carries diagnostics,
-resource controls, scope, and exclusions.
+resource controls, a machine-readable \emph{scope block} (the deployed
+leaf-12 instance is quoted verbatim in Appendix~\ref{app:entry13}), and exclusions.
 
 \begin{definition}[Attestation-transparency scheme]
 An attestation-transparency scheme is a~\mbox{tuple}
@@ -304,7 +313,7 @@ An attestation-transparency scheme is a~\mbox{tuple}
 over a hash function and signature scheme. $\mathsf{Append}$ commits the
 canonical serialization of an attestation as the next leaf and returns a signed
 tree head. $\mathsf{Verdict}$ is parameterized by consumer-local policy and
-does not consume an operator verdict as positive evidence.
+does not consume an operator label as positive evidence.
 \end{definition}
 
 \begin{definition}[Accountable replay distribution]
@@ -315,9 +324,10 @@ determined leaf value at its claimed position; (ii) a
 consumer accepts a later view only as the same view or a verified extension;
 (iii) two valid equal-size heads with unequal roots, in one log and protocol
 context, form transferable evidence
-that the key holder signed incompatible views; and (iv) positive acceptance of
+that the key holder signed incompatible views, except under signature
+forgery; and (iv) positive acceptance of
 a theorem boundary is a function of recorded observations and consumer-local
-policy, not of an operator verdict.
+policy, not of an operator label.
 \end{definition}
 
 The definition is intentionally an accountability property, not a validity
@@ -389,8 +399,8 @@ of the operator public key.
 
 The model deliberately does not cryptographically exclude fabricated kernel
 observations; the same holds when the operator's replay harness is defective
-rather than dishonest. That is a statement about a physical execution on the operator's
-machine. The mechanism instead makes the claimed execution target precise
+rather than dishonest. Whether the kernel actually ran as claimed is a
+fact about a physical execution on the operator's machine. The mechanism instead makes the claimed execution target precise
 enough for a third party to replay.
 
 \subsection{Consumer goals}
@@ -407,7 +417,7 @@ a later view only if it is the same view or a verified extension. Two valid
 heads of equal size and unequal roots, in one log context, are transferable
 evidence that the key holder signed incompatible views. Unequal-size forks
 require retained history, gossip, or a witness. The transition discipline
-itself is syntactic, enforced by the pin rule by construction; the semantic
+itself is syntactic, enforced by the pin rule (\S4.3) by construction; the semantic
 content --- an opened position cannot change value across accepted views ---
 is a theorem (\S\ref{sec:games}).
 \item[G3: Policy separation.] The operator's positive label cannot make a
@@ -459,15 +469,17 @@ consistency proofs are the RFC~9162 algorithms~\cite{ct2}.
 A tree head contains schema-version and type tags, a log identifier, tree
 size, root hash, timestamp, and hash-algorithm identifier. The canonical JSON serialization of
 those fields is signed with Ed25519. The log identifier and version tag prevent
-cross-log and cross-protocol replay.
+cross-log and cross-protocol replay. We call the leaf history a head
+commits to a \emph{view}, and write \emph{signed view} for that history
+as represented by its signed head.
 
 Since tree size 14, every head additionally carries a \emph{deterministic}
 SLH-DSA-SHA2-128s (FIPS~205) signature over the same payload. The
 co-signature is additive: the Ed25519 signature remains the one every
 consumer must verify, and heads published before size 14 carry no
-post-quantum signature --- the standalone verifier reports them as absent
-rather than failing them, because an append-only log keeps the history of
-its own signature scheme. Determinism is chosen as an audit primitive: a
+post-quantum signature --- the standalone verifier reports the co-signature as
+absent on such heads rather than rejecting them: an append-only log
+necessarily preserves the history of its own signature-scheme upgrades. Determinism is chosen as an audit primitive: a
 deterministic re-sign of the same payload is byte-comparable, so ``same
 input, same signature'' becomes a diff rather than an assurance. The
 co-signature closes a further loop: its parameter set is exactly the one
@@ -491,6 +503,9 @@ same-size fork evidence;
 \item larger size: accept iff a consistency proof verifies, then update;
 \item smaller size: reject as rollback.
 \end{itemize}
+
+We call this transition discipline the \emph{pin rule}, and the persisted
+pair $(n_{\mathrm{pin}},r_{\mathrm{pin}})$ the \emph{pin-store}.
 Freshness is an external availability policy. A persisted pin detects rollback
 relative to local history; it does not prove that a client sees the globally
 latest signed head.
@@ -506,7 +521,8 @@ $D$, $d$, $m$, $n$ & leaf list; leaf bytes; leaf index; tree size \\
 $\MTH(D)$;\ $k$ & Merkle root; split point (largest power of two below $n$) \\
 $\Path(m,D)$;\ $\Root(v,m,n,P)$ & inclusion path (leaf to root); path refold \\
 $\mathsf{Open}(d,m,n,P,r)$ & accepting opening: $m<n$ and $\Root(\hleaf(d),m,n,P)=r$ \\
-$\ConsRec$;\ $\mathsf{Ext}$ & recursive consistency verifier; pin-rule transition \\
+$\ConsRec$;\ $\mathsf{Ext}$ & recursive consistency verifier; pin-rule transition (\S\ref{sec:games}) \\
+$C$;\ $b$ & consistency proof; flag: old root is the pinned $r_0$ ($\top$) vs read from $C$ \\
 $\Obs_a(c)$;\ $\Policy(c)$ & axiom names recorded in leaf $a$; consumer's allowed set \\
 $\chi_{\rm enc}$;\ $\chi=(\chi_{\rm enc},pk)$ & payload-encoded head context; full context with the key \\
 $h=(n,r,t;\sigma)$;\ $\mathsf{Vf}_{pk}$ & signed head (size, root, timestamp); signature check \\
@@ -523,9 +539,10 @@ This section states the consumer-facing arguments in the form used by the Lean
 mechanization. The proofs are elementary but explicit: successful false
 openings yield concrete SHA-256 collisions rather than appealing to an informal
 ``Merkle trees are secure'' statement. The explicitness is load-bearing: over a
-fixed-width hash a bare ``some collision exists'' is vacuously true by
-counting, so each soundness statement is about a named extractor function, and
-the corpus pins a machine-checked non-vacuity guard for every extractor.
+fixed-width hash, ``some collision exists'' is trivially true by counting;
+each soundness statement therefore names an explicit extractor function,
+and the corpus pins a machine-checked guard that each extractor's output
+really is a collision (distinct preimages, equal digests).
 
 \subsection{Inclusion}
 
@@ -588,7 +605,9 @@ $|D_0|=n_0\le n_1=|D_1|$, $D_0\neq D_1[0{:}n_0]$, and
 \ConsRec(n_0,n_1,C,\top,\MTH(D_0))
    =(\MTH(D_0),\MTH(D_1)),
 \]
-$\mathcal{E}_{\rm cons}(D_0,D_1,C)$ returns a SHA-256 collision.
+$\mathcal{E}_{\rm cons}(D_0,D_1,C)$ returns a SHA-256 collision. (The hypothesis supplies the honest
+$\MTH(D_0)$ as the pinned value; \S5.3 measures the deployed flow, which
+has no such mechanized supplier.)
 \end{theorem}
 \begin{proof}
 The new-root component is a hash fold over the shape of the $n_1$ tree. Compare
@@ -602,13 +621,16 @@ collision.
 \end{proof}
 
 The theorem's hypothesis pins the honest old root $\MTH(D_0)$. The deployed
-flow has no mechanized supplier of that pin; the next subsection measures what
-the iterative verifier does when size claims alone steer its walk.
+flow contains nothing mechanized that guarantees the pinned value is the
+honest old root; the next subsection measures the iterative verifier's
+behavior when only the claimed sizes constrain its reconstruction.
 
 \begin{proposition}[Pin-store safety]
 Assume EUF-CMA security of the head signature and collision resistance of
 SHA-256. A consumer following the pin transition accepts only a nondecreasing
-sequence of sizes whose exhibited leaf lists are prefix-related. Two accepted
+sequence of sizes; if leaf lists are exhibited for two accepted heads,
+they are prefix-related except under collision (see the mapping paragraph
+of \S\ref{sec:games}). Two accepted
 heads under the same key, in one log context, with equal size and unequal
 roots are transferable evidence that the key holder signed incompatible
 views.
@@ -616,7 +638,8 @@ views.
 \begin{proof}
 Rollback is rejected syntactically. At equal size the transition is accepted
 only with equal roots; if the two exhibited equal-length leaf lists differed,
-whole-tree binding would extract a SHA-256 collision, so under collision
+whole-tree root binding (each root determines its committed leaf list up
+to collision) would extract a SHA-256 collision, so under collision
 resistance the lists are equal. A larger head is accepted only after a
 consistency proof, so non-prefix acceptance yields a collision by the previous
 theorem. Equal-size unequal roots in one log context, with valid signatures, are two
@@ -630,7 +653,7 @@ certificate is a function only of $\Obs_a(c)$ and $\Policy(c)$. An operator
 label cannot change a nonconforming observation into a conforming one.
 \end{proposition}
 \begin{proof}
-The comparison is set equality and takes no positive operator verdict as input.
+The comparison is set equality and takes no positive operator label as input.
 A deployment may conservatively treat an operator failure label as a veto, but
 a veto cannot grant acceptance.
 \end{proof}
@@ -917,9 +940,9 @@ In the smallest growth case $2\to3$ --- the log's own transition in
 old tree and $P_0$ is simply the opening's within-prefix tail.
 
 \paragraph{Game $\mathsf{HIST}$ (local history binding).}
-$\mathcal{A}$ outputs a chain of head values $h_0,\dots,h_k$, transition
-proofs $C_1,\dots,C_k$ with $\mathsf{Ext}(n_{i-1},r_{i-1},n_i,r_i,C_i)=1$
-for every $1\le i\le k$, indices $0\le a<b\le k$, an index $m<n_a$, and
+$\mathcal{A}$ outputs a chain of head values $h_0,\dots,h_\ell$, transition
+proofs $C_1,\dots,C_\ell$ with $\mathsf{Ext}(n_{i-1},r_{i-1},n_i,r_i,C_i)=1$
+for every $1\le i\le \ell$, indices $0\le a<b\le \ell$, an index $m<n_a$, and
 openings with
 $\mathsf{Open}(d,m,n_a,P,r_a)=\mathsf{Open}(d',m,n_b,P',r_b)=1$ and
 $d\neq d'$. $\mathcal{A}$ wins iff everything verifies. (The chain is the
@@ -930,7 +953,7 @@ transcripts regardless of provenance.)
 \begin{theorem}[History binding]\label{thm:hist}
 There is an explicit algorithm $\mathcal{B}_{\rm hist}$ that, whenever
 $\mathcal{A}$ wins $\mathsf{HIST}$, outputs a SHA-256 collision, using
-$O(k\log n_k)$ hash evaluations.
+$O(\ell\log n_\ell)$ hash evaluations.
 \end{theorem}
 \begin{proof}
 By Lemma~\ref{lem:mono}, $m<n_a\le n_i$ for all $i\ge a$. Walk $t$ from $b$
@@ -943,7 +966,7 @@ at $h_a$ yields two accepting openings of $d\neq d'$ at $m$ under
 $(n_a,r_a)$, and Theorem~\ref{thm:pb} extracts the collision. Accepted
 transcripts have their RFC-determined logarithmic length --- malformed
 lengths reject --- so the walk costs at most the evaluations of replaying the
-$k$ transition transcripts and the two openings.
+$\ell$ transition transcripts and the two openings.
 \end{proof}
 
 \paragraph{Game $\mathsf{HEAD}$ (head authenticity).}
@@ -989,7 +1012,7 @@ queried to the signing oracle; its valid signature is an existential forgery,
 which $\mathcal{B}_{\rm fr}$ outputs.
 \end{proof}
 
-\begin{lemma}[Policy separation]\label{lem:policy}
+\begin{lemma}[Policy separation --- Proposition~2 restated for the scheme package]\label{lem:policy}
 For every leaf $a$ and certificate $c$, the verdict computed by
 $\mathsf{Verdict}$ equals $[\Obs_a(c)=\Policy(c)]$; it reads no operator
 label, and acceptance consults the operator's status only as a veto. This is
@@ -1008,11 +1031,11 @@ separation.
 \end{definition}
 
 \begin{theorem}[Collision-extractable accountability of the construction]\label{thm:main}
-The LTL construction --- the RFC~9162 tree, the canonical signed heads of
-\S4.2 in their fixed context $\chi$, the pin rule of \S4.3, and the policy
+The LTL construction with the recursive verifiers of \S\ref{sec:security}
+--- the RFC~9162 tree, the canonical signed heads of \S4.2 in their fixed context $\chi$, the pin rule of \S4.3, and the policy
 verdict of \S\ref{sec:model} --- is collision-extractably accountable, with
 $\mathcal{B}_{\rm pb}$ ($\le 2(\lceil\log_2 n\rceil{+}1)$ hash evaluations),
-$\mathcal{B}_{\rm hist}$ ($O(k\log n_k)$), and the one-forgery reductions
+$\mathcal{B}_{\rm hist}$ ($O(\ell\log n_\ell)$), and the one-forgery reductions
 $\mathcal{B}_{\rm ha},\mathcal{B}_{\rm fr}$ of
 Theorems~\ref{thm:pb}--\ref{thm:fork}.
 \end{theorem}
@@ -1051,7 +1074,7 @@ operator as first-class adversary, policy separation added.
 
 \begin{remark}[What is mechanized, what is not]\label{rem:gamescope}
 The games are stated for the scheme's specified verifiers --- the recursive
-model whose honest-reference specializations are kernel-checked in entry~13
+model whose honest-reference specializations are kernel-checked in leaf~12
 (the named extractors and per-step pin safety). The two-transcript
 comparisons and the transport induction are paper-level proofs in the same
 discipline --- the induction reuses the corpus's mechanized
@@ -1088,52 +1111,58 @@ per fork --- the log records both generations as separate leaves), covering:
 mathematical point equation.
 \end{itemize}
 
-The signature apex can be summarized as follows. Let $k$ be the challenge
-scalar produced by an opaque SHA-512 boundary and let $r_1$ be the raw $R$ bytes
+The signature apex is organized as four tiers T1--T4
+(Appendix~\ref{app:tiers}). Let $c$ be the challenge scalar produced by an opaque SHA-512 boundary and let $\bar R$ be the raw $R$ bytes
 from the signature. The corpus separates:
 \begin{description}[leftmargin=1.5em,itemsep=2pt]
 \item[T1:] acceptance iff the verifier's recomputed compressed bytes equal
-$r_1$;
+$\bar R$;
 \item[T2:] those recomputed bytes are the canonical encoding of
-$[k](-A)+[s]B$;
+$[c](-A)+[s]B$;
 \item[T3:] canonical encoding is injective on valid curve points;
 \item[T4:] acceptance iff constructive decompression of $R$ yields
-$[k](-A)+[s]B$.
+$[c](-A)+[s]B$.
 \end{description}
 
 The separation keeps residual assumptions visible. SHA-512 and selected
 wire-format interfaces are opaque boundaries at the apex; lower arithmetic and
 group certificates use the foundational Lean axioms observed in the corpus.
 
-\subsection{The SLH-DSA verify path: the method on second terrain}\label{sec:slhdsa}
+\subsection{A second instantiation: the SLH-DSA verify path}\label{sec:slhdsa}
 
-The second campaign extracts the verification path of SLH-DSA (FIPS~205,
+The second campaign extracts the verification path of SLH-DSA
+(FIPS~205~\cite{fips205},
 parameter set SHA2-128s) from a pinned pure-Rust implementation through the
 same Charon/Aeneas route, starting from one monomorphic entry point with the
 five hash primitives marked opaque at the extraction boundary. The corpus is
-eleven certificates: ten loop-fidelity theorems (chain walking, WOTS
-recomputation and checksum, XMSS and FORS Merkle ascent, hypertree layering,
-digit/byte plumbing) and an acceptance characterization,
+eleven certificates: ten \emph{loop-fidelity} theorems --- each stating
+that an extracted loop computes the same value as a reference recursive
+fold --- covering chain walking, WOTS recomputation and checksum, XMSS and
+FORS Merkle ascent, hypertree layering, and digit/byte plumbing
+(Appendix~\ref{app:slhtiers} lists each with its exact cone) and an acceptance characterization,
 \code{slh_verify_128s_accepts_iff}: for every message digest, signature, and
 public key at these parameters, the extracted verifier accepts exactly when
 the recomputed hypertree root byte-equals the public key's root --- no other
 acceptance path exists.
 
 The terrain differs from Ed25519 in one structural way, and the leaf says so.
-The Ed25519 bridges land in an independent second semantics
-($\mathbb{Z}/p\mathbb{Z}$, which the proof library understands without ever
-seeing the extracted code); SLH-DSA verification is hash chains and Merkle
-nodes all the way down, so the reference folds are built from the same five
-uninterpreted hash oracles (\code{h_msg}, \code{f}, \code{h},
-\code{t_l}, \code{t_len}, modeling the SHA-256 instantiations) that the
-extracted loops call. Each loop certificate therefore makes the extracted
+For Ed25519, each theorem relates extracted code to an independent
+mathematical semantics (arithmetic over $\mathbb{Z}/p\mathbb{Z}$,
+formalized with no reference to the extracted code); SLH-DSA verification
+is hash chains and Merkle nodes all the way down, so its reference
+specifications are folds over the same five uninterpreted hash oracles
+(\code{h_msg}, \code{f}, \code{h}, \code{t_l}, \code{t_len}, modeling
+the SHA-256 instantiations --- uninterpreted function symbols in the
+logic, not random oracles) that the extracted loops call --- there is no
+independent second semantics to land in. Each loop certificate therefore makes the extracted
 control flow \emph{visible} --- small, sequential, checkable against the
 standard's algorithms --- while the reading of fold against FIPS~205 remains
 a declared human step. The audit enforces every certificate's axiom set
 exactly in both directions, and the cone \emph{grows} up the pyramid ---
 pure bit arithmetic rests on the kernel alone; the apex carries all five
 oracles (Appendix~\ref{app:slhtiers}). Scope, stated in the leaf: the proved
-subject is a monomorphic facade whose bridge to the deployed generic verifier
+subject is a monomorphic facade (the fixed-parameter entry point above)
+whose bridge to the deployed generic verifier
 is a 137-case differential test; one inner digit-extraction loop carries no
 certificate; signing and key generation were never extracted.
 
@@ -1181,13 +1210,15 @@ Every signed head issued since public mirroring began is retained --- twelve
 heads, at tree sizes 8 through 19, dual-signed from size 14 on --- together
 with every leaf and receipt, in an append-only Git mirror; a clone
 re-verifies the entire log offline with the repository's standalone verifier.
-The first twelve leaves are three four-fork replay generations. Leaves 0--3
+The first twelve leaves are three replay generations across the four
+Ed25519 codebases. Leaves 0--3
 record a failed audit run and remain permanently visible. Leaves 4--7 record a
 clean replay. Leaves 8--11 re-attest rewritten repository histories rather
 than replacing the old leaves. Leaf 12 attests the accumulator's own Lean
 corpus (\S\ref{sec:deployment}, E3); leaves 13--16 re-attest the four
 Ed25519 corpora at 44 certificates each; leaf 17 re-attests the accumulator
-corpus at its hardened state; and leaf 18 attests the SLH-DSA-SHA2-128s
+corpus at its hardened state (the same corpus after closure of external
+review findings); and leaf 18 attests the SLH-DSA-SHA2-128s
 verification path --- the log's first post-quantum subject, and the scheme
 that has co-signed every head since size 14. A leaf whose pinned commit ceases to be
 distributed decays from a replayable claim to a historical record; consumers
@@ -1249,10 +1280,11 @@ path. Heads are dual-signed from size 14 on.}
 
 \subsection{Mechanization coverage}
 
-Entry 13 is not a claim that the whole service is formally verified. The Lean
+Leaf 12 is not a claim that the whole service is formally verified. The Lean
 corpus covers the recursive Merkle model, inclusion completeness and
 collision-extracting soundness, the consistency extractor, and the Merkle-layer
-share of pin-store safety. The abstract root-binding lemma from the paper is
+share of pin-store safety. The folklore whole-tree root-binding property (a root determines its
+committed leaf list up to SHA-256 collision) is
 mechanized through the specializations needed by the extractors rather than as
 one quantified hash-fold theorem. Signature unforgeability, execution
 provenance, the full signed-head state machine, asymptotic cost, and the
@@ -1269,7 +1301,7 @@ Inclusion & completeness and named collision extractor & collision resistance in
 Consistency & recursive-model soundness and extractor & no general consistency-completeness theorem \\
 Pinning & per-step monotonicity and prefix correctness & signature layer and multi-step closure external \\
 Deployment refinement & finite differential harness & no theorem for iterative verifier under authentic-pair invariant \\
-Policy separation & deterministic tooling logic and regression tests & not mechanized in the entry-13 corpus \\
+Policy separation & deterministic tooling logic and regression tests & not mechanized in the leaf-12 corpus \\
 Scheme-level games (\S\ref{sec:games}) & paper-level explicit reductions & two-transcript comparisons and prefix transport not mechanized \\
 \bottomrule
 \end{tabularx}
@@ -1278,9 +1310,10 @@ Scheme-level games (\S\ref{sec:games}) & paper-level explicit reductions & two-t
 \subsection{Cost and reproducibility}
 
 A replay of one Ed25519 fork requires approximately 30 minutes of end-to-end
-guarded replay time under the pinned environment, a figure corroborated by the
+resource-guarded (memory- and time-capped) replay time under the pinned environment, a figure corroborated by the
 inter-leaf issuance spacing visible in the published log. Receipt verification requires one Ed25519
-signature and a logarithmic number of SHA-256 node computations. The
+signature and a logarithmic number of SHA-256 node computations (the
+complete inclusion core is printed as Appendix~\ref{app:verifier}). The
 accumulator corpus is independently reviewable with a pinned public Lean
 release; an environment-derived inventory fails closed on added, removed, or
 axiom-smuggling declarations.
@@ -1374,15 +1407,16 @@ about their replay.
 
 \paragraph{Verification of transparency protocols.}
 Cheval et al. mechanize transparency-protocol reasoning~\cite{cheval}.
-The entry-13 corpus approaches the composition from the opposite direction: it
+The leaf-12 corpus approaches the composition from the opposite direction: it
 mechanizes accumulator arguments and then logs that replay result. The
 remaining refinement from the deployed state machine to the recursive model is
 explicitly open.
 
 \section{Limitations and research agenda}\label{sec:limitations}
 
-The subject corpus maintains a numbered ledger of fifteen known gaps together
-with their closure options; this section groups the load-bearing ones.
+The subject corpus maintains a numbered public file, \code{KNOWN-GAPS},
+of fifteen gaps with their closure options (the scope block of
+Appendix~\ref{app:entry13} cites its items 14 and 15); this section groups the load-bearing ones.
 
 \paragraph{Operator observation trust.}
 A malicious operator can fabricate a replay report. Signatures and Merkle
@@ -1416,7 +1450,7 @@ isolated clients to receive that view. Independent witnesses or gossip are the
 natural next deployment step.
 
 \paragraph{Consistency refinement.}
-The recursive model is proved; the iterative deployment diverges from it on
+The recursive model is proved; the iterative deployment diverged from it on
 malformed inputs, every observed divergence being deployed-accepts-only. The strongest closure is either to deploy
 $\ConsRec$-equivalent semantics or to mechanize the signed-head and pin-store
 flow and prove the authentic-pair refinement theorem.
@@ -1446,7 +1480,7 @@ become attributable when compared.
 The Lean Transparency Log demonstrates the complete construction. It amortizes
 expensive replay over lightweight consumers, retains failed and superseded
 observations, and carries a scoped attestation of the accumulator's own Lean
-corpus as entry 13. Just as importantly, the mechanization and differential
+corpus as leaf 12. Just as importantly, the mechanization and differential
 harness exposed a mismatch between the recursive model and the deployed
 consistency verifier. Recording that mismatch in the public leaf is not a
 failure of the method; it is evidence that the trust decomposition is doing
@@ -1460,7 +1494,7 @@ replay attestation provides an immediate infrastructure layer while those
 stronger validity mechanisms are developed.
 
 \section*{Artifact availability}
-The live service is \url{https://ltl.zkdefi.org}. Entry 13 has leaf hash
+The live service is \url{https://ltl.zkdefi.org}. Leaf 12 (the log's thirteenth entry) has leaf hash
 \begin{center}\small\ttfamily
 8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a
 \end{center}
@@ -1486,7 +1520,7 @@ The author designed the system and is responsible for every claim. Claude
 tooling, and manuscript review. Their output was not accepted as evidence;
 claims were retained only after human review or reproducible artifact checks.
 
-\begin{thebibliography}{22}
+\begin{thebibliography}{23}
 \itemsep2pt
 \bibitem{ct1} B. Laurie, A. Langley, E. K\"asper. Certificate Transparency.
 RFC 6962, 2013.
@@ -1566,6 +1600,9 @@ Collision-Resistant Hashing without the Keys. VIETCRYPT, LNCS 4341, pp.
 Verification Pipeline with AI Provers: An Experience Report. arXiv:2605.30106,
 2026.
 
+\bibitem{fips205} National Institute of Standards and Technology.
+Stateless Hash-Based Digital Signature Standard. FIPS 205, August 2024.
+
 \end{thebibliography}
 
 % Appendix policy (declared 2026-08-16): the appendix block starts on a
@@ -1605,8 +1642,8 @@ Claimed signer implementation produced STH & not established & execution provena
 \end{tabularx}
 \end{center}
 
-\section{Deployed entry-13 scope}\label{app:entry13}
-The thirteenth public leaf contains the following deployment constraint,
+\section{Deployed leaf-12 scope}\label{app:entry13}
+Leaf 12 contains the following deployment constraint,
 quoted verbatim, in its machine-readable scope block:
 \begin{quote}\small
 Attestation scope: this corpus kernel-checks the listed theorems about the
@@ -1682,6 +1719,11 @@ T4 & constructive decompression lift & \code{verify_accepts_iff_decompress} \\
 \end{tabular}
 \end{center}
 
+All four tiers share one opaque boundary --- the SHA-512 challenge hash
+and the selected wire-format interfaces (\S\ref{sec:instantiation});
+the arithmetic and group certificates beneath them rest on Lean's
+foundational axioms alone.
+
 \section{SLH-DSA verification certificates and their cones}\label{app:slhtiers}
 
 Eleven certificates over the extracted SLH-DSA-SHA2-128s verify path
@@ -1715,10 +1757,10 @@ The oracles model the parameter set's SHA-256 hash-suite instantiations:
 \code{h} (Merkle node), \code{t_l} and \code{t_len} (the WOTS and FORS
 compressors --- two axioms over what is one Rust primitive, deliberately
 conservative, with the source's naming inversion against the standard's
-$T_\ell$/$T_k$ documented at the declarations). The acceptance
-characterization is a structural factorization, not a composition of the
-loop theorems: it would remain provable if any of the ten were deleted,
-and each loop certificate is meaningful exactly to the extent its
-reference fold has been read against FIPS~205.
+$T_\ell$/$T_k$ documented at the declarations). The acceptance characterization is proved directly from the verifier's
+structure, not by composing the ten loop theorems --- it would remain
+provable if any of the ten were deleted. Conversely, each loop
+certificate carries assurance only insofar as a human has checked its
+reference fold against the corresponding FIPS~205 algorithm.
 
 \end{document}

paper/reinvention-outline.md

@@ -1,122 +0,0 @@
-# Paper reinvention — working outline (post second ePrint rejection)
-
-Status: approved direction (operator order 2026-07-16: "entry 13 and
-paper reinvention"); this outline is the committed starting point for
-the full rewrite. Diagnosis it responds to: both external analyses
-(GPT-5.6 rejection post-mortem; round-6 reviewer aside) converge on
-POSITIONING, not correctness — five papers compressed into one, the
-novelty (trust decomposition) occupying less space than its supporting
-machinery, and the honest "components unchanged" refrain reading as
-"nothing new" in a thirty-second editorial skim.
-
-## 0. The one sentence (everything else exists to support it)
-
-> We define and instantiate a cryptographic distribution model for
-> machine-checked correctness evidence, enabling lightweight consumers
-> to obtain accountable assurance without executing the original
-> verifier — and demonstrate it end to end with a deployed log that
-> carries kernel-checked proofs of its own accountability machinery as
-> an entry in itself.
-
-The second clause is the only-this-paper claim; it becomes literally
-true at entry 13 and the paper should be finalized AFTER that append so
-the abstract can cite the live leaf.
-
-## 1. Title candidates (working)
-
-- "Accountable Distribution of Machine-Checked Correctness Evidence"
-- "Transparency for Theorem Provers: Distributing Formal Verification
-  to Consumers Who Cannot Replay It"
-- (subtitle either way): "…with a deployed log that notarizes the
-  proofs of its own machinery"
-
-"The Lean Transparency Log" becomes the *system's* name, not the
-paper's identity.
-
-## 2. Inverted structure
-
-1. **Problem.** Theorem provers solve the PRODUCTION of correctness
-   evidence; nothing standard solves scalable DISTRIBUTION and
-   CONSUMPTION by clients that cannot run the prover (no toolchain, no
-   hours of replay, no trust in the operator's word). State it as the
-   gap between "verified" and "verifiable by you."
-2. **Model.** The trust decomposition, presented abstractly:
-   (a) producer performs expensive deterministic verification once;
-   (b) the result becomes a precise attestation object (subject commit,
-   toolchain, certificates with exact assumption cones, scope);
-   (c) a transparency structure supplies persistence, consistency, and
-   equivocation-evidence; (d) consumers apply policy locally without
-   executing the verifier; (e) the residual trust is enumerated, not
-   waved at. Define the accountability property: misbehavior
-   manufactures transferable evidence.
-3. **Design space** (the section the old paper lacked). Position
-   against: reproducible replay services; succinct proofs of proof
-   checking (SNARKed kernels); checkpoint/cosigning committees;
-   witness cosigning; downloadable proof artifacts; proof-carrying
-   code; cached prover environments/containers. Axis of comparison:
-   consumer cost, operator trust, accountability (evidence on
-   misbehavior), incrementality, and what happens when the operator
-   disappears. The log wins on accountability-per-consumer-cost; be
-   honest where SNARKed checking would win (validity vs
-   accountability) and why it is not yet practical for a full kernel.
-4. **Instantiation: the LTL.** Lean 4 + Aeneas corpora as producers;
-   Ed25519 heads signed by the dogfooded verified signer
-   (self_inclusion); RFC 9162 accumulator; pin-store consumers.
-   Compressed from old §4–5; the four ed25519 subject corpora become a
-   TABLE + pointer to project documentation, not sections.
-5. **Security of the instantiation.** The mechanized model (61
-   certificates, single opaque-SHA-256 axiom, environment-derived audit
-   surface); Theorems 1–3 + Prop 1 in one page each of STATEMENT (the
-   proofs live in the repo; the paper sells the statements). Present
-   gap 14/15 as a RESULT, not a confession: the model/deployment seam
-   located, measured (3,867 one-sided divergences), fenced by pinned
-   tests, and bridged by an explicitly stated operational invariant —
-   this is what honest mechanization boundaries look like.
-6. **Exhibit A: the log attests itself.** Entry 13 as the paper's
-   demonstration: the accountability machinery's own proofs, carried by
-   the machinery, verifiable end to end by one command from a stock
-   toolchain. Include the leaf hash + head root; a reader can check
-   inclusion in seconds.
-7. **Deployment & consumers.** Live service; warden (quorum custody
-   wallet) as the internal consumer; Swiss Post e-voting PoC as the
-   prospective external consumer (dalek-family transport). Replay
-   economics (measured ~1,800 s/fork) as the cost the model amortizes.
-8. **Related work.** CT lineage (RFC 6962/9162, CONIKS, sigstore);
-   optimistic-rollup analogy (accountability-over-validity; the
-   fraud-proof reading of Theorem 3 — from
-   ltl-accumulator-verified/docs/optimistic-accountability.md);
-   proof-carrying code; reproducible builds/SLSA; in-toto.
-9. **Limitations** = the 15-gap ledger, grouped (assumption base /
-   scope lines / unmechanized bridge), each one sentence, pointer to
-   the repo ledger.
-
-## 3. What moves OUT of the paper
-
-- Ed25519 corpus construction details → project docs / possible
-  separate implementation report ("Paper C" in the GPT taxonomy).
-- Curriculum, wallet internals, agent-native surfaces → out entirely.
-- Appendix A/B verbatim-leaf material → shrink to one leaf excerpt
-  (entry 13 itself, naturally).
-- The §8 operational-history narrative → compress to the
-  retrievability-decay paragraph + one table.
-
-## 4. Sequencing & venues
-
-1. Entry 13 lands (prerequisite for the abstract's second clause).
-2. Rewrite per this outline (fresh tex, new title; old ltl.tex remains
-   hosted as the system report at /paper — versioned, not erased).
-3. arXiv (cs.CR) immediately for timestamp + citability.
-4. Venue: CPP/ITP (mechanization framing) or SCORED/SecDev
-   (supply-chain framing) or RWC talk (deployment framing) — decide
-   after the rewrite settles which face leads.
-5. All queued wording fixes (Lemma-2 specializations, fidelity =
-   pinned families, §10(i)/(v), Remark 1, pinned-pair side condition)
-   are ABSORBED by the rewrite rather than patched into the old text.
-
-## 5. Success criterion
-
-A hurried editor can answer "what is the contribution?" from the title
-+ first paragraph alone, and the thought-experiment inversion holds:
-remove any single supporting component (Lean, Ed25519, RFC 9162) and
-the CLAIM survives; remove the trust-decomposition model and nothing is
-left. That is the opposite polarity of the rejected manuscript.

provider/src/pacta_provider/web.py

@@ -20,6 +20,39 @@ from .transparency_log import TransparencyLog
 
 API_VERSION = "v1"
 
+def _openapi_document(base: str) -> dict:
+    """The machine interface, described the industry-standard way (OpenAPI 3)
+    instead of a hand-written endpoint box on the human docs page."""
+    q = lambda name, desc, req=True: {"name": name, "in": "query", "required": req,
+                                      "description": desc, "schema": {"type": "string"}}
+    ok = {"200": {"description": "success"}}
+    return {
+        "openapi": "3.0.3",
+        "info": {"title": "Lean Transparency Log",
+                 "description": "Read-only CT-style interface of the LTL. "
+                                "Heads are signed offline; this service holds no key material.",
+                 "version": API_VERSION},
+        "servers": [{"url": "https://ltl.zkdefi.org" + base}],
+        "paths": {
+            "/log-public-key": {"get": {"summary": "Required Ed25519 public key (PEM)", "responses": ok}},
+            "/log-slhdsa-public-key": {"get": {"summary": "Post-quantum SLH-DSA public key (PEM)", "responses": ok}},
+            "/healthz": {"get": {"summary": "Liveness and current tree size", "responses": ok}},
+            "/paper": {"get": {"summary": "The current paper (PDF)", "responses": ok}},
+            f"/{API_VERSION}/metadata": {"get": {"summary": "Log identity", "responses": ok}},
+            f"/{API_VERSION}/sth": {"get": {"summary": "Latest Signed Tree Head", "responses": ok}},
+            f"/{API_VERSION}/sth-history": {"get": {"summary": "Every Signed Tree Head ever issued (witness material)", "responses": ok}},
+            f"/{API_VERSION}/sth-consistency": {"get": {"summary": "Consistency proof from a pinned size",
+                "parameters": [q("first", "your pinned old tree size")], "responses": ok}},
+            f"/{API_VERSION}/proof": {"get": {"summary": "Inclusion proof (freshly issued receipt)",
+                "parameters": [q("component", "component name", False), q("leaf_hash", "leaf hash (hex)", False)], "responses": ok}},
+            f"/{API_VERSION}/attestation": {"get": {"summary": "Newest attestation for a component",
+                "parameters": [q("component", "component name")], "responses": ok}},
+            f"/{API_VERSION}/entries": {"get": {"summary": "Raw leaves in [start, end)",
+                "parameters": [q("start", "first index", False), q("end", "one past last index", False)], "responses": ok}},
+        },
+    }
+
+
 
 def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdfs: dict[str, bytes] | None = None):
     paper_pdfs = paper_pdfs or {}
@@ -78,6 +111,8 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
                 self.send_header("Content-Length", str(len(body)))
                 self.end_headers()
                 self.wfile.write(body)
+            elif route == "/openapi.json":
+                self._send(200, _openapi_document(base))
             elif route == "/healthz":
                 self._send(200, {"ok": True, "tree_size": len(log.entries())})
             elif route == f"/{API_VERSION}/metadata":
@@ -153,6 +188,7 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
                         f"{base}/log-public-key",
                         f"{base}/log-slhdsa-public-key",
                         f"{base}/healthz",
+                        f"{base}/openapi.json",
                         f"{base}/{API_VERSION}/metadata",
                         f"{base}/{API_VERSION}/sth",
                         f"{base}/{API_VERSION}/sth-history",

provider/src/pacta_provider/webdocs.py

@@ -21,7 +21,8 @@ _STYLE = """
  h2{font-size:1.2rem;margin-top:2.6rem;border-bottom:2px solid var(--line);padding-bottom:.3rem}
  .tagline{font-size:1.05rem;color:var(--ink2);max-width:46rem}
  code,pre{font-family:ui-monospace,Menlo,Consolas,monospace;background:#eef0f3;border-radius:4px}
- code{padding:.1rem .3rem;font-size:.9em} pre{padding:.9rem;overflow-x:auto;font-size:.85rem}
+ code{padding:.1rem .3rem;font-size:.9em;overflow-wrap:anywhere}
+ pre{padding:.9rem;overflow-x:auto;font-size:.85rem;max-width:100%}
  table{border-collapse:collapse;width:100%;font-size:.93rem;background:#fff}
  td,th{border:1px solid var(--line);padding:.5rem .7rem;text-align:left;vertical-align:top}
  th{background:var(--accentbg)}
@@ -41,7 +42,6 @@ _STYLE = """
  .sw{display:inline-block;width:.8rem;height:.8rem;border-radius:3px;vertical-align:-1px;margin-right:.3rem}
 """
 
-
 def _leaf_ok(entry: LogEntry) -> bool:
     certificates = ((entry.leaf.get("attestation") or {}).get("certificates")) or []
     return bool(certificates) and all(
@@ -49,6 +49,11 @@ def _leaf_ok(entry: LogEntry) -> bool:
         for certificate in certificates
     )
 
+def _leaf_short(component: str) -> str:
+    """Compact display name for a leaf box at small spans."""
+    return (component.replace("-ed25519-verified", "")
+            .replace("ltl-accumulator-verified", "accum")
+            .replace("fips205-slhdsa-verified", "slh-dsa"))
 
 def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str, head_label: str = "Ed25519") -> str:
     """The accumulator, drawn from its real leaves."""
@@ -77,12 +82,22 @@ def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str, head
                 ok = _leaf_ok(entry)
                 component = (((entry.leaf.get("attestation") or {}).get("subject")) or {}).get("component", "?")
                 fill, stroke = ("#e2f2e9", "#1e7f4f") if ok else ("#f4f4f6", "#8a93a0")
-                out.append(f'<rect x="{x-56}" y="{y-22}" width="112" height="44" rx="5" fill="{fill}" stroke="{stroke}" stroke-width="1.4"/>')
-                out.append(f'<text x="{x}" y="{y-6}" text-anchor="middle" fill="#333">leaf {node_index}</text>')
-                short = escape(str(component).replace("-ed25519-verified", ""))
+                # Boxes must FIT the per-leaf span at any tree size (the
+                # 2026-08-16 lesson: fixed 112px boxes shingled at 19
+                # leaves). Rich boxes while they fit, compact ones after.
+                box_w = min(112.0, span * 0.94)
+                compact = box_w < 100
+                short = escape(_leaf_short(str(component)))
                 label = short if ok else f"{short} ✗"
-                out.append(f'<text x="{x}" y="{y+8}" text-anchor="middle" fill="{stroke}">{label}</text>')
-                out.append(f'<text x="{x}" y="{y+19}" text-anchor="middle" fill="#999" font-size="9">{node.hex()[:10]}…</text>')
+                if compact:
+                    out.append(f'<rect x="{x-box_w/2:.1f}" y="{y-18}" width="{box_w:.1f}" height="36" rx="4" fill="{fill}" stroke="{stroke}" stroke-width="1.2"/>')
+                    out.append(f'<text x="{x}" y="{y-4}" text-anchor="middle" fill="#333" font-size="8">leaf {node_index}</text>')
+                    out.append(f'<text x="{x}" y="{y+9}" text-anchor="middle" fill="{stroke}" font-size="7">{label}</text>')
+                else:
+                    out.append(f'<rect x="{x-box_w/2:.1f}" y="{y-22}" width="{box_w:.1f}" height="44" rx="5" fill="{fill}" stroke="{stroke}" stroke-width="1.4"/>')
+                    out.append(f'<text x="{x}" y="{y-6}" text-anchor="middle" fill="#333">leaf {node_index}</text>')
+                    out.append(f'<text x="{x}" y="{y+8}" text-anchor="middle" fill="{stroke}">{label}</text>')
+                    out.append(f'<text x="{x}" y="{y+19}" text-anchor="middle" fill="#999" font-size="9">{node.hex()[:10]}…</text>')
             else:
                 is_root = level_index == len(levels) - 1
                 out.append(f'<rect x="{x-50}" y="{y-15}" width="100" height="30" rx="5" fill="{"#eef0f7" if is_root else "#fff"}" stroke="{"#3b4d8f" if is_root else "#bbb"}" stroke-width="{1.6 if is_root else 1}"/>')
@@ -91,16 +106,23 @@ def _svg_tree(entries: list[LogEntry], root_hex: str, signing_backend: str, head
                 for child in (2 * node_index, 2 * node_index + 1):
                     if (level_index - 1, child) in positions:
                         cx, cy = positions[(level_index - 1, child)]
-                        out.append(f'<line x1="{x}" y1="{y+15}" x2="{cx}" y2="{cy-22 if level_index==1 else cy-15}" stroke="#ccc"/>')
+                        leaf_top = 18 if len(entries) > 9 else 22
+                        out.append(f'<line x1="{x}" y1="{y+15}" x2="{cx}" y2="{cy-leaf_top if level_index==1 else cy-15}" stroke="#ccc"/>')
     root_x, root_y = positions[(len(levels) - 1, 0)]
-    out.append(f'<rect x="{root_x-190}" y="{root_y-72}" width="380" height="34" rx="6" fill="#e2f2e9" stroke="#1e7f4f" stroke-width="1.6"/>')
-    out.append(f'<text x="{root_x}" y="{root_y-58}" text-anchor="middle" fill="#1e7f4f" font-weight="bold">Signed Tree Head — {escape(head_label)}({root_hex[:12]}…)</text>')
-    out.append(f'<text x="{root_x}" y="{root_y-46}" text-anchor="middle" fill="#1e7f4f" font-size="9">signed by: {escape(signing_backend)} (verify path attested; signing itself not proven)</text>')
+    # The head box sizes itself to its longest line (the 2026-08-16
+    # lesson: a fixed 380px box let a growing caption spill both sides).
+    title = f"Signed Tree Head — {head_label}({root_hex[:12]}…)"
+    line2 = f"signed by: {signing_backend}"
+    line3 = "(verify path attested; signing itself not proven)"
+    head_w = max(len(title) * 7.0, len(line2) * 5.3, len(line3) * 5.3) + 28
+    out.append(f'<rect x="{root_x-head_w/2:.1f}" y="{root_y-84}" width="{head_w:.1f}" height="46" rx="6" fill="#e2f2e9" stroke="#1e7f4f" stroke-width="1.6"/>')
+    out.append(f'<text x="{root_x}" y="{root_y-70}" text-anchor="middle" fill="#1e7f4f" font-weight="bold">{escape(title)}</text>')
+    out.append(f'<text x="{root_x}" y="{root_y-58}" text-anchor="middle" fill="#1e7f4f" font-size="9">{escape(line2)}</text>')
+    out.append(f'<text x="{root_x}" y="{root_y-47}" text-anchor="middle" fill="#1e7f4f" font-size="9">{escape(line3)}</text>')
     out.append(f'<line x1="{root_x}" y1="{root_y-38}" x2="{root_x}" y2="{root_y-15}" stroke="#1e7f4f" stroke-width="1.4"/>')
     out.append("</svg>")
     return "".join(out)
 
-
 def _trust_anchor_html(log: TransparencyLog, metadata: dict[str, Any], base: str, mirror: str) -> str:
     """The provider public key, displayed in full on the front page. The key
     is the one thing a consumer takes on trust, once - hiding it behind a
@@ -125,11 +147,10 @@ def _trust_anchor_html(log: TransparencyLog, metadata: dict[str, Any], base: str
         slh_pem = escape(slh_path.read_text(encoding="utf-8").strip())
         slh_fp = _h.sha256(slh_path.read_bytes()).hexdigest()
         slh_block = f"""<hr style="border:none;border-top:1px solid #ddd;margin:.8rem 0">
-<p style="margin-top:0"><strong>Second, additive anchor — post-quantum.</strong> Heads from
-tree&nbsp;14 on additionally carry a deterministic <strong>SLH-DSA-SHA2-128s</strong> (FIPS&nbsp;205)
-signature over the same payload. The Ed25519 signature above remains the one every consumer must
-check; this one is checked where tooling allows (OpenSSL&nbsp;≥&nbsp;3.5). Its verify path is the
-proof subject of leaf&nbsp;18.</p>
+<p style="margin-top:0"><strong>Key&nbsp;2 — SLH-DSA (FIPS&nbsp;205), post-quantum.</strong> Heads from tree size&nbsp;14 on carry a second signature from this key;
+older heads legitimately have none — an append-only log keeps its history. Check it where your
+tooling allows (OpenSSL&nbsp;≥&nbsp;3.5). The kind of code that verifies such signatures is itself
+a proof subject of this log (entry&nbsp;18).</p>
 <pre style="margin-bottom:.4rem">{slh_pem}</pre>
 <p class="muted" style="margin:.2rem 0 0">SHA-256 fingerprint <code>{slh_fp}</code>
 &nbsp;·&nbsp; raw: <a href="{base}/log-slhdsa-public-key"><code>{base or ''}/log-slhdsa-public-key</code></a>
@@ -137,20 +158,20 @@ proof subject of leaf&nbsp;18.</p>
     else:
         slh_block = ""
     return f"""<div class="card">
-<p style="margin-top:0">This key is the <strong>sole cryptographic identity anchor</strong>: it
-authenticates that these statements were made by the operator (the same party the artifacts call “the provider”). It does not, by itself, make
-those statements true — each attestation's truth additionally rests on the replay, theorem,
-extraction and toolchain assumptions stated in that leaf (one signed entry of the tree below). Every tree head and attestation is
-signature-checked against this key.
-Pin it (save your own copy; from then on trust only what checks against that copy), and compare this copy byte-for-byte with the independently hosted
-<a href="{mirror}/blob/main/provider.ed25519.pub">mirror copy</a>; they must be identical. The first fetch is trust-on-first-use; the two-host byte-comparison is what bounds it.</p>
+<p style="margin-top:0"><strong>Two keys sign everything in this log.</strong> Neither makes a
+claim <em>true</em>; they prove a claim comes from this operator, unchanged. Save your own copy
+of both — that is called <em>pinning</em>: from then on you trust only what verifies against
+your saved copies. Fetch each key from this page AND from the independently hosted mirror and
+compare byte-for-byte; the copies must be identical. (The first fetch is trust-on-first-use;
+comparing two independent hosts is what bounds it.)</p>
+<p><strong>Key&nbsp;1 — Ed25519, required.</strong> Every signed head and every attestation must
+verify against it.</p>
 <pre style="margin-bottom:.4rem">{pem}</pre>
 <p class="muted" style="margin:.2rem 0 0">SHA-256 fingerprint <code>{escape(fingerprint)}</code>
 &nbsp;·&nbsp; raw: <a href="{base}/log-public-key"><code>{base or ''}/log-public-key</code></a>
 &nbsp;·&nbsp; <code>curl -s https://ltl.zkdefi.org/log-public-key</code></p>
 {slh_block}</div>"""
 
-
 def render_docs(log: TransparencyLog, base_path: str) -> str:
     base = "/" + base_path.strip("/") if base_path.strip("/") else ""
     metadata = log.metadata()
@@ -196,24 +217,100 @@ def render_docs(log: TransparencyLog, base_path: str) -> str:
 · <a href="https://zkdefi.org/saymrwulf">code</a>
 · <a href="https://zkdefi.com/">cv</a></p>
 <h1>LTL — the Lean Transparency Log</h1>
-<p class="tagline"><strong>One sentence:</strong> a public, append-only Merkle
-accumulator (a hash tree that only ever grows) of <em>signed statements that the <a href="https://lean-lang.org">Lean&nbsp;4</a> formal proofs of specific
-cryptographic Rust libraries, at specific git commits, re-check by machine with exactly
-their documented assumptions</em> — so that you can trust a proof result by checking
-<strong>one required signature (Ed25519) and ~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes in
-milliseconds</strong>, instead of running a theorem prover for hours.</p>
+<p><strong>Every known way of consuming formal verification fails on one of two
+sides: either the cost stays with you (re-running a theorem prover), or the cost
+disappears because you are asked to believe a label. This site holds the point in
+between — it makes machine-checked proof results as cheap to check as one
+signature and a handful of hashes, without turning them into trust. Every claim
+the operator ever makes is recorded here permanently, bound to his key, and
+scoped to its exact assumptions: he can never be believed, only held
+accountable.</strong></p>
 
-<h2>The trust anchor — pin this key</h2>
+<p>Concretely: a proof assistant — <a href="https://lean-lang.org">Lean&nbsp;4</a>, a
+program that checks mathematical proofs mechanically — has verified precise
+statements about the code that <em>checks signatures</em>: in four widely deployed
+<strong>Ed25519</strong> libraries, in an implementation of <strong>SLH-DSA</strong>
+(FIPS&nbsp;205, the hash-based post-quantum signature standard), and in <strong>the
+Merkle-tree machinery of this log itself</strong>. Each completed proof check is one
+signed, numbered entry that can never be altered or removed — {len(entries)} entries
+so far, drawn live further down this page. How much of our work you re-verify is
+your choice, from milliseconds to everything:</p>
+
+<h2>Choose where you stand — the trust ladder</h2>
+
+<div class="steps">
+<div class="card"><strong>Hold a copy of the history.</strong> — anyone; one minute.<br>
+You still trust: the content of every claim. You defeat: silent rewriting.<br>
+You need: Python&nbsp;3 and the <code>openssl</code> command (preinstalled on most Linux and macOS systems).
+<pre>git clone https://github.com/saymrwulf/lean-transparency-log &amp;&amp; cd lean-transparency-log &amp;&amp; python3 verify.py --all</pre>
+<span class="muted">This fetches the log&rsquo;s public mirror — a git repository holding every entry
+and every signed head ever issued (a head is the signed root fingerprint of the tree at a
+given size) — and re-computes every hash and signature in it. A green
+result means the history you now hold is internally consistent and signed. Keep the folder:
+if the operator ever shows a different history to anyone else, your copy proves it. A log
+that shows different histories to different people (a &ldquo;split view&rdquo;) survives only until
+two holders compare.</span></div>
+
+<div class="card"><strong>Check that a claim is real and binding.</strong> — milliseconds.<br>
+You still trust: that the operator&rsquo;s recorded observation is honest.<br>
+You need: four small files from the tables below — the two public keys, plus one library&rsquo;s
+claim file (&ldquo;attestation&rdquo;) and its proof of inclusion (&ldquo;receipt&rdquo;).
+<pre>pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub --slhdsa-public-key provider.slhdsa.pub</pre>
+<span class="muted">Your machine checks the required Ed25519 signature, the second (post-quantum) signature
+(needs OpenSSL&nbsp;≥&nbsp;3.5; drop the second flag to skip it), and
+~{max(1,(latest.get('tree_size') or 1).bit_length())} hashes — no proof assistant involved.
+The <code>pacta</code> tool ships in the
+<a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a>
+(<code>pip install .</code> from a clone); about forty lines of ordinary Python do the same
+check, and the mirror&rsquo;s <code>verify.py</code> contains exactly that core. Afterwards the
+claim — which repository, which exact source version, which theorems, which assumptions —
+is bound to the operator&rsquo;s key inside a history he can neither rewrite nor deny.</span></div>
+
+<div class="card"><strong>Judge by your own standards.</strong> — minutes.<br>
+Every entry records more than pass/fail: it lists the exact assumptions each proof rests on
+(its <em>axiom cone</em>). So you may ignore the operator&rsquo;s verdicts entirely: write down
+which assumptions <em>you</em> accept, and have your tooling compare list against list, name
+by name. <code>pacta</code> automates the comparison; lecture&nbsp;11 of the Jupyter course (same
+repository) teaches it step by step.
+<span class="muted">Afterwards every verdict is your verdict — the operator&rsquo;s labels can at
+most veto, never grant. The section &ldquo;You hold the ruler&rdquo; below is this rung in full.</span></div>
+
+<div class="card"><strong>Re-run the proof check yourself.</strong> — about 30&nbsp;minutes per library.<br>
+You still trust: that the published Lean statements mean what they say.<br>
+You need: a Lean&nbsp;4 toolchain (free).
+<span class="muted">Every attested repository ships one script, <code>verification/check.sh</code>.
+Clone the repository at the exact source version recorded in its log entry and run the script:
+the proof assistant re-checks every theorem on your machine and prints every assumption list.
+The operator is now out of the loop entirely.</span></div>
+
+<div class="card"><strong>Rebuild everything from source.</strong> — weeks.<br>
+What remains trusted: Lean&rsquo;s proof kernel, the Rust-to-Lean translation tools (Charon and
+Aeneas), and your compiler — the floor, which we name rather than hide.
+<span class="muted">Every repository documents its full path: the pinned upstream Rust code,
+the extraction script that regenerates the Lean definitions byte-for-byte, and the theorem
+statements to read against the standards themselves (FIPS&nbsp;205, RFC&nbsp;9162, the curve
+equations). Reproduce any part; compare with what is published. After this rung you no longer
+need this site — that is the point. There is no rung&nbsp;6: even here you trust a kernel, a
+compiler, and your hardware.</span></div>
+</div>
+
+<h2>Two keys sign this log — pin these keys</h2>
 {_trust_anchor_html(log, metadata, base, mirror)}
 
 <h2>The accumulator, live</h2>
+<p>The log is a <strong>Merkle tree</strong>: every entry (&ldquo;leaf&rdquo;) is hashed, hashes pair
+up level by level, and a single 32-byte root fingerprints the entire history; the operator signs
+that root. Changing any past entry would change the root — that is the tamper evidence. Each leaf
+records one proof run: a batch of <strong>certificates</strong> — one machine-checked theorem
+each, together with its exact assumption list. This
+picture is computed from the live log at page render — the leaf hashes, nodes, root, and
+signature are the real ones:</p>
 {tree_svg}
 <p class="legend">
-<span><span class="sw" style="background:#e2f2e9;border:1px solid #1e7f4f"></span>verified attestation (all certificates proven, axiom cones boundary-exact)</span>
+<span><span class="sw" style="background:#e2f2e9;border:1px solid #1e7f4f"></span>verified attestation — every certificate proven, every assumption list exactly as declared</span>
 <span><span class="sw" style="background:#f4f4f6;border:1px solid #8a93a0"></span>historical audit-failure attestation — kept forever; an append-only ledger does not erase its bad day (leaves&nbsp;0–3: an early audit round that failed; leaves&nbsp;4–7 re-attest the same four libraries cleanly)</span>
 </p>
-<p class="muted">Every box above is computed from the live log at page render — leaf hashes,
-internal nodes, the root, and the signature are the real ones. The library that signs the log is itself an entry in the log — what that entry proves is its <em>verify</em> path (no signing code is proven, here or anywhere) — and it checks its own entry before signing. In detail: before signing this
+<p class="muted">The library that signs the log is itself an entry in the log — what that entry proves is its <em>verify</em> path (no signing code is proven, here or anywhere) — and it checks its own entry before signing. In detail: before signing this
 root, the provider Merkle-verified its own signing library's leaf
 (index {provenance.get('signing_library_leaf_index','?')},
 certificates {escape(str(provenance.get('signing_library_certificates_proven','?')))})
@@ -225,11 +322,12 @@ log id <code>{escape(str(metadata.get('log_id',''))[:16])}…</code>.</p>
 
 <h2>What do I download? — the three artifacts, unambiguously</h2>
 <p>To benefit from the accumulator you need <strong>exactly three files</strong> per
-library, plus optionally the whole mirror. Nothing else.</p>
+library, plus optionally the post-quantum key
+(<code>provider.slhdsa.pub</code>) and the whole mirror. Nothing else.</p>
 <table>
 <tr><th>#</th><th>Artifact</th><th>What it is</th><th>Where</th></tr>
 <tr><td><b>1</b></td><td><code>provider.ed25519.pub</code></td>
-<td><strong>The identity anchor.</strong> The provider's public key — the sole cryptographic
+<td><strong>The identity anchor.</strong> The provider's public key — the required cryptographic
 identity you pin. It authenticates the operator's statements; their truth rests on each leaf's
 stated assumptions. Fetch it from BOTH independent locations and compare; the copies must be
 identical.</td>
@@ -239,11 +337,13 @@ identical.</td>
 which observed axiom cones (the exact set of assumptions each proof ultimately rests on), what machine protection — signed by the provider.</td>
 <td>table below, or <a href="{mirror}">mirror</a> <code>entries/</code></td></tr>
 <tr><td><b>3</b></td><td><code>&lt;library&gt;.receipt.json</code></td>
-<td><strong>The proof of inclusion.</strong> Binds artifact&nbsp;2 into the signed tree:
-leaf index, sibling hashes, the Signed Tree Head (STH). A one-page Python core verifies it — printed as Appendix&nbsp;C of the paper; the shipped <code>verify.py</code> wraps that core with full fail-closed binding checks (stdlib hashing; signature checks shell out to the <code>openssl</code> binary).</td>
+<td><strong>The proof of inclusion.</strong> Binds the claim into the signed tree:
+leaf index, sibling hashes, the Signed Tree Head (STH). About forty lines of ordinary
+Python verify it; the mirror&rsquo;s <code>verify.py</code> contains exactly that core, wrapped in
+fail-closed safety checks (stdlib hashing; signature checks shell out to the <code>openssl</code> binary).</td>
 <td>table below, or <a href="{mirror}">mirror</a> <code>receipts/</code></td></tr>
 <tr><td>+</td><td>the full mirror clone</td>
-<td><strong>Maximal benefit: become a witness.</strong> Every leaf + every signed head
+<td><strong>Maximal benefit: hold the complete history yourself (rung&nbsp;1 of the ladder).</strong> Every leaf + every signed head
 ever issued + <code>verify.py</code> (Python stdlib + the <code>openssl</code> binary for
 signatures; fails closed without them). <code>python3 verify.py --all</code>
 recomputes the entire tree and every historical head — you then hold a retained view that can
@@ -254,33 +354,8 @@ consumers.)</td>
 </table>
 
 <h2>Attested libraries</h2>
-<table><tr><th>component</th><th>artifact 2</th><th>artifact 3</th><th>status</th></tr>{rows}</table>
+<table><tr><th>library</th><th>claim (attestation)</th><th>proof of inclusion (receipt)</th><th>certificates proven</th></tr>{rows}</table>
 
-<p class="muted">One certificate = one machine-checked theorem together with its exact assumption set (its axiom cone).</p>
-
-<h2>Three ways to use it</h2>
-<div class="steps">
-<div class="card"><strong>Quick check</strong> (any machine, milliseconds): download
-artifacts 1–3, then<br>
-<code>pacta receipt-verify --attestation … --receipt … --log-public-key provider.ed25519.pub</code>
-<br><span class="muted">No Lean, no Rust, no account. The <code>pacta</code> CLI ships in the <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a> (<code>pip install .</code> from a clone). Add <code>--sth-store pins.json</code> to remember every Signed Tree Head (STH) you accept — your defense against a split view (the operator showing different histories to different consumers).</span></div>
-<div class="card"><strong>Zero-install audit</strong>: <code>git clone {mirror} &amp;&amp; cd lean-transparency-log &amp;&amp; python3 verify.py --all</code>
-<br><span class="muted">Standard-library Python plus the system <code>openssl</code> binary (signature checks fail closed without it). You become a witness of the whole history.</span></div>
-<div class="card"><strong>Autonomous agent</strong>: the <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta</a>
-tool adds STH pinning, freshness policy, online refresh from this service, risk scoring
-(R0–R5, six named residual-risk classes) with policy-gated consequences, and optionally verifies every signature through
-the proof-attested Ed25519 code path itself (<code>--require-verified-verifier</code>).</div>
-</div>
-
-<h2>API</h2>
-<pre>GET {base}/v1/sth                      latest Signed Tree Head
-GET {base}/v1/sth-history              the published head history (witness material)
-GET {base}/v1/sth-consistency?first=N  consistency proof from your pinned size
-GET {base}/v1/proof?component=NAME     inclusion proof (artifact 3, freshly issued)
-GET {base}/v1/attestation?component=NAME   the claim (artifact 2)
-GET {base}/v1/entries?start=N&amp;end=M    raw leaves
-GET {base}/v1/metadata                 log identity
-GET {base}/healthz</pre>
 
 <h2>What a verified inclusion means — and what it does not</h2>
 <div class="card"><span class="pill ok">means</span> The provider whose key you hold
@@ -292,16 +367,19 @@ view.</div>
 proofs cover Rust <em>source</em>; clone the attested commit (the commit id identifies the
 committed git tree — not external dependencies, toolchain downloads, or generated artifacts) and
 build it yourself — compiler and build are declared trusted base (assumed, not proven)
-until the reproducible-builds program lands and retires risk class R5. Every attestation carries its full
+until the reproducible-builds program lands. Every attestation carries its full
 residual-risk list — the enumerated assumptions inside its <code>attestation.json</code>. Honesty about the boundary is the product.</div>
 
 <h2>You hold the ruler</h2>
 <div class="card">The list of assumptions a certificate is <em>allowed</em> to rest on
 is not something this site hands you at verification time — it is a
-<strong>requirements card</strong> that lives in <em>your</em> tooling, on
+<strong>requirements card</strong> — a short plain-text file listing, by name, the
+assumptions you accept — that lives in <em>your</em> tooling, on
 <em>your</em> disk, and that you can read in five minutes or rewrite from first
 principles: Lean's three foundational axioms, plus — for the signature tiers only (the top proof layers, where full signature verification is proven) —
-named placeholders for SHA-512 and the wire format. Your tooling ignores this
+named placeholders for SHA-512 (the hash function Ed25519 uses internally —
+the proofs treat it as an assumption, not as proven) and the byte-level wire
+format. Your tooling ignores this
 operator's pass/fail labels entirely and re-derives every verdict by comparing the
 attestation's <em>observed</em> axiom list (its cone) against <em>your</em> card, name by name.
 The operator is trusted to copy down what the proof kernel printed — never to
@@ -319,7 +397,7 @@ our roadmap.</strong> (The full walk-through is lecture&nbsp;11 of the Jupyter c
 <h2>The paper</h2>
 <div class="card"><a href="{base}/paper"><strong>Accountable Distribution of Machine-Checked
 Correctness Evidence: A Transparency Model and the Lean Transparency Log</strong></a>
-(PDF, 25 pages, <strong>v0.11 — revised August&nbsp;2026</strong>; the version is printed on the
+(PDF, 25 pages, <strong>v0.15 — revised August&nbsp;2026</strong>; the version is printed on the
 title page) — the trust decomposition (expensive verification produces an
 observation; transparency makes the observation accountable; consumer-local policy decides
 acceptance), collision-extracting soundness for inclusion and consistency, scheme-level
@@ -330,18 +408,16 @@ operator labels can veto but never grant acceptance, and the measured model/depl
 divergence reported as a result rather than hidden — now together with its closure: the
 divergence traced to one omitted RFC&nbsp;9162 conjunct (Step&nbsp;7's <code>sn&nbsp;=&nbsp;0</code>),
 zero divergences after the one-line restoration, confirmed by a three-way regression.
-New in v0.11: the deployment evaluated to its current nineteen-leaf, dual-signed state, an
+New in the August 2026 revisions: the deployment evaluated to its current nineteen-leaf, dual-signed state, an
 instantiation section for the SLH-DSA (FIPS&nbsp;205) verify path — eleven certificates,
 five uninterpreted hash oracles, exact cones — and a certificate appendix mirroring the
 Ed25519 tiers.</div>
 
-<div class="card"><strong>Paper and log, one story.</strong> Since v0.11 the paper
-describes this deployment as it runs — nineteen leaves, dual-signed heads, the
-post-quantum verify path as leaf&nbsp;18 with its own certificate appendix. The log is
-append-only and keeps growing past any paper revision; every number the paper states
-stays checkable against the retained history: <code>python3 verify.py --all</code>
-re-verifies all of it, paper-era and after, from a clone of the mirror.</div>
 
 <p class="muted">Log heads are signed offline; this service is read-only and holds no
-key material. Provider tooling, agent tooling, and the full Jupyter course live in the <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a>.</p>
+key material. Provider tooling, agent tooling, and the full Jupyter course live in the
+<a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">pacta repository</a>.
+Software integrators: the machine interface behind every link on this page is described by the
+OpenAPI document at <a href="{base}/openapi.json"><code>/openapi.json</code></a> — the
+<code>pacta</code> tool builds on it (head pinning, freshness policy, risk scoring R0–R5).</p>
 </body></html>"""

src/pacta/cli.py

@@ -137,6 +137,7 @@ def build_parser() -> argparse.ArgumentParser:
     receipt_verify.add_argument("--receipt", required=True)
     receipt_verify.add_argument("--log-public-key", required=True)
     receipt_verify.add_argument("--require-signatures", choices=["ed25519", "both"], default="ed25519")
+    receipt_verify.add_argument("--slhdsa-public-key", help="Also verify the second (post-quantum, SLH-DSA) head signature against this public key (OpenSSL >= 3.5; heads before tree size 14 report absent, not failed).")
     receipt_verify.add_argument("--sth-store", help="Path to the local STH pin store (split-view/rollback defense).")
     receipt_verify.add_argument("--consistency-proof", help="File with a hex consistency proof from the pinned tree size (provider: log-consistency).")
     receipt_verify.add_argument("--max-sth-age-seconds", type=int, help="Reject signed tree heads older than this (freshness policy).")
@@ -476,7 +477,8 @@ def cmd_score(args: argparse.Namespace) -> int:
 def cmd_receipt_verify(args: argparse.Namespace) -> int:
     attestation = load_attestation(args.attestation)
     receipt = load_receipt(args.receipt)
-    result = verify_receipt(attestation, receipt, args.log_public_key, require_signatures=args.require_signatures)
+    result = verify_receipt(attestation, receipt, args.log_public_key, require_signatures=args.require_signatures,
+                            slhdsa_public_key_path=args.slhdsa_public_key)
     accountability_diagnostics = _log_accountability_checks(
         receipt,
         sth_store=args.sth_store,

src/pacta/transparency.py

@@ -256,6 +256,7 @@ def verify_receipt(
     receipt: dict[str, Any],
     log_public_key_path: str | Path,
     require_signatures: str = "ed25519",
+    slhdsa_public_key_path: str | Path | None = None,
 ) -> ReceiptVerificationResult:
     diagnostics: list[str] = []
     if receipt.get("type") != RECEIPT_TYPE:
@@ -266,6 +267,29 @@ def verify_receipt(
     sth = receipt.get("sth") or {}
     sth_ok, sth_diagnostics, statuses = verify_signed_tree_head(sth, log_public_key_path, require_signatures=require_signatures)
     diagnostics.extend(sth_diagnostics)
+    if slhdsa_public_key_path is not None:
+        # The additive post-quantum co-signature (heads from tree size 14
+        # on). Absent on older heads is NOT a failure - an append-only log
+        # keeps its history; a present-but-bad signature fails closed.
+        from .slhdsa import verify_payload_slhdsa
+
+        slh = (sth.get("signatures") or {}).get("slh_dsa") or {}
+        if str(slh.get("status") or "absent") == "signed":
+            try:
+                slh_ok, slh_error = verify_payload_slhdsa(
+                    signed_tree_head_payload(sth),
+                    str(slh.get("signature_base64") or ""),
+                    slhdsa_public_key_path,
+                )
+            except Exception as exc:  # old OpenSSL, unreadable key: fail closed
+                slh_ok, slh_error = False, f"SLH-DSA verification unavailable: {exc}"
+            if slh_ok:
+                statuses["slh_dsa"] = "verified"
+            else:
+                statuses["slh_dsa"] = "failed"
+                diagnostics.append(f"SLH-DSA head co-signature did not verify: {slh_error}")
+        else:
+            statuses["slh_dsa"] = "absent"
     try:
         tree_size = int(receipt.get("tree_size"))
         leaf_index = int(receipt.get("leaf_index"))

tests/test_transparency.py

@@ -145,3 +145,42 @@ def test_requiring_both_signatures_fails_without_ml_dsa_backend(tmp_path):
     assert not result.accepted
     assert result.signatures["ed25519"] == "verified"
     assert result.signatures["ml_dsa"] != "verified"
+
+
+def test_receipt_verify_checks_slhdsa_cosignature(tmp_path):
+    # Rung 2 of the site promises both head signatures are checkable;
+    # this binds the promise to the tool (operator-caught 2026-08-16).
+    import pytest
+
+    from pacta import slhdsa
+
+    try:
+        slhdsa.generate_slhdsa_keypair(tmp_path / "slh.key", tmp_path / "slh.pub")
+    except Exception:
+        pytest.skip("OpenSSL without SLH-DSA support on this host")
+    attestation, private_key, public_key = _signed_attestation(tmp_path)
+    from pacta.yamlio import dump_data
+
+    dump_data(attestation, tmp_path / "attestation.yaml")
+    log = TransparencyLog(tmp_path / "log")
+    log.init("local-test-provider", public_key)
+    receipt = log.append_attestation(
+        tmp_path / "attestation.yaml", private_key, public_key,
+        receipt_out=tmp_path / "receipt.yaml",
+        slhdsa_private_key_path=tmp_path / "slh.key",
+        slhdsa_public_key_path=tmp_path / "slh.pub",
+    )
+    result = verify_receipt(attestation, receipt, public_key,
+                            slhdsa_public_key_path=tmp_path / "slh.pub")
+    assert result.accepted, result.diagnostics
+    assert result.signatures["slh_dsa"] == "verified"
+
+    tampered = __import__("copy").deepcopy(receipt)
+    sig = tampered["sth"]["signatures"]["slh_dsa"]["signature_base64"]
+    import base64 as _b64
+    raw = bytearray(_b64.b64decode(sig)); raw[0] ^= 0xFF
+    tampered["sth"]["signatures"]["slh_dsa"]["signature_base64"] = _b64.b64encode(bytes(raw)).decode()
+    bad = verify_receipt(attestation, tampered, public_key,
+                         slhdsa_public_key_path=tmp_path / "slh.pub")
+    assert not bad.accepted
+    assert bad.signatures["slh_dsa"] == "failed"

tests/test_web_and_witness.py

@@ -80,7 +80,7 @@ def test_web_endpoints_and_online_proof_roundtrip(tmp_path):
         with urllib.request.urlopen(base + "/docs", timeout=10) as r:
             page = r.read().decode()
         assert "BEGIN PUBLIC KEY" in page
-        assert "pin this key" in page.lower()
+        assert "pin these keys" in page.lower()
         # operator-dropped documents: served by bare name, absent from the
         # endpoint index, traversal-safe
         site = tmp_path / "log" / "site"
@@ -181,3 +181,45 @@ def test_webdocs_source_carries_no_stale_paper_claims():
     # first-use glosses the page promised: STH and axiom cones
     assert "Signed Tree Head (STH)" in text
     assert "axiom cones (the exact set of assumptions" in text
+
+
+def test_svg_tree_boxes_never_overlap_or_spill():
+    # Regression for 2026-08-16: fixed-width leaf boxes shingled once the
+    # log outgrew the 8-leaf design, and a fixed head box let its caption
+    # spill. Render the tree at several sizes and assert geometry.
+    import re
+
+    from pacta_provider.webdocs import _svg_tree
+
+    class _E:
+        def __init__(self, i):
+            self.leaf_hash = f"{i:02x}" * 32
+            self.leaf = {"attestation": {"subject": {"component": "betrusted-ed25519-verified"},
+                                         "certificates": [{"status": "proven", "axiom_status": "clean"}]}}
+
+    for n in (8, 19, 33):
+        svg = _svg_tree([_E(i) for i in range(n)], "ab" * 32, "verified-dalek-serial")
+        rects = [(float(m.group(1)), float(m.group(2)), float(m.group(3)))
+                 for m in re.finditer(r'<rect x="([-0-9.]+)" y="([0-9.]+)" width="([0-9.]+)"', svg)]
+        leaf_y = max(y for _, y, _ in rects)
+        leaves = sorted((x, w) for x, y, w in rects if y == leaf_y)
+        assert len(leaves) == n
+        for (x1, w1), (x2, _w2) in zip(leaves, leaves[1:]):
+            assert x1 + w1 <= x2 + 0.01, f"leaf boxes overlap at n={n}"
+        # head caption must fit its box: longest line estimated at 5.3px/char
+        head = re.search(r'<rect x="[-0-9.]+" y="[0-9.]+" width="([0-9.]+)" height="46"', svg)
+        title = re.search(r'font-weight="bold">([^<]+)</text>', svg).group(1)
+        assert len(title) * 7.0 <= float(head.group(1)), "head title spills"
+
+
+def test_openapi_document_served_and_valid():
+    # The machine interface is published the industry-standard way
+    # (operator order 2026-08-16: no endpoint box on the human page).
+    import json as _json
+
+    from pacta_provider.web import _openapi_document
+
+    doc = _openapi_document("")
+    assert doc["openapi"].startswith("3.")
+    assert "/v1/sth" in doc["paths"] and "/log-public-key" in doc["paths"]
+    _json.dumps(doc)  # serializable