diff --git a/paper/ltl-v0.2.pdf b/paper/ltl-v0.2.pdf
new file mode 100644
index 0000000..2747bf4
Binary files /dev/null and b/paper/ltl-v0.2.pdf differ
diff --git a/paper/ltl-v0.2.tex b/paper/ltl-v0.2.tex
new file mode 100755
index 0000000..54c3c60
--- /dev/null
+++ b/paper/ltl-v0.2.tex
@@ -0,0 +1,1344 @@
+% LTL paper, v4 = merge of two independent hostile reviews (2026-07-10).
+% Review A (second Fable instance): frontier hash-fold framework (the
+% lemma did not cover its own uses as written), dangling R4/R5 labels,
+% deny-only label semantics, Table 1 caption, r_1 as raw bytes, exact
+% RFC 9162 figure. Review B (GPT-5.6): G2/abstract narrowed to what
+% Prop 1 proves, residual-trust sentence at honest width, freshness and
+% self-reference disclaimers, softened novelty/mechanization claims,
+% head-encoding documented, claim-matrix table. Both reviews' findings
+% independently re-verified before adoption.
+\documentclass[11pt]{article}
+\usepackage[a4paper,margin=1.1in]{geometry}
+\usepackage{amsmath,amssymb,amsthm}
+\usepackage{xcolor}
+\usepackage[colorlinks=true,linkcolor=blue!60!black,citecolor=blue!60!black,urlcolor=blue!60!black]{hyperref}
+\usepackage{enumitem}
+\usepackage{booktabs}
+\usepackage{lmodern}
+\usepackage{microtype}
+% this TeX install's format ships righthyphenmin=1 ('it-s'); restore standard
+\lefthyphenmin=2 \righthyphenmin=3
+\usepackage{tikz}
+\usetikzlibrary{fit,positioning,decorations.pathreplacing}
+
+\newtheorem{theorem}{Theorem}
+\newtheorem{lemma}{Lemma}
+\newtheorem{proposition}{Proposition}
+\newtheorem{corollary}{Corollary}
+\newtheorem{definition}{Definition}
+\theoremstyle{remark}
+\newtheorem{remark}{Remark}
+
+\newcommand{\authortodo}[1]{\textcolor{red}{\textbf{[AUTHOR TODO: #1]}}}
+\newcommand{\hash}{\mathsf{H}}
+\newcommand{\hleaf}{\mathsf{h}_{\mathsf{leaf}}}
+\newcommand{\hnode}{\mathsf{h}_{\mathsf{node}}}
+\newcommand{\MTH}{\mathsf{MTH}}
+\newcommand{\Root}{\mathsf{Root}}
+\newcommand{\ConsRec}{\mathsf{ConsRec}}
+\newcommand{\Path}{\mathsf{Path}}
+\newcommand{\obs}{\mathsf{obs}}
+\newcommand{\allowed}{\mathsf{allowed}}
+\newcommand{\clean}{\mathsf{clean}}
+\newcommand{\accept}{\mathsf{accept}}
+\newcommand{\Fp}{\mathbb{F}_{2^{255}-19}}
+
+\title{The Lean Transparency Log:\\ Distributing Kernel-Checked Correctness Evidence\\ for Deployed Ed25519 Implementations}
+\author{Olaf Horvath\\
+\small Olaf.Horvath@zkdefi.org \quad ORCID 0009-0004-8008-5805
+% \authortodo{if you have any institutional or personal-domain affiliation,
+% use it here instead of / alongside the zkdefi.org address}
+}
+\date{July 2026 (revised)}
+
+\begin{document}
+\maketitle
+
+\begin{abstract}
+Interactive theorem provers can certify functional correctness of deployed
+cryptographic code, but the resulting assurance is expensive to consume:
+re-checking a realistic proof corpus requires a proof toolchain and hours of
+kernel time, which excludes almost every downstream user. We describe the
+Lean Transparency Log (LTL), an RFC~9162-style transparency log whose leaves
+are \emph{replay attestations}: signed statements that the Lean~4 proofs of a
+specific Rust repository, at a specific git commit, re-check with exactly
+their documented axiom sets. Consumers verify one signature and a logarithmic
+inclusion proof in milliseconds; the kernel time is paid once, by the log
+operator.
+
+This paper makes the trust model precise and proves the consumer-facing
+security claims. We define the attestation-transparency setting, give an
+explicit adversary model in which the operator may be malicious, and prove:
+completeness and soundness of the inclusion verifier (soundness via an
+explicit reduction extracting a SHA-256 collision), the analogous consistency
+statement, safety of the consumer's head-pinning state machine (same-size
+equivocation yields transferable evidence, and local pinning rejects
+inconsistent extensions), and \emph{verdict
+integrity}---consumers re-derive verification verdicts locally from observed
+axiom cones, so the operator is trusted only for \emph{observations}, never
+for \emph{verdicts}. A further design choice ties the log to its own subject
+matter: tree heads are signed by a binary built from the very Ed25519
+implementation whose correctness certificates are leaves of the log. We
+report a small production deployment covering four verified production
+Ed25519 implementations, state exactly what the accumulated evidence does and
+does not establish, and outline the mechanization of this paper's theorems in
+Lean as the natural next step.
+\end{abstract}
+
+\section{Introduction}\label{sec:intro}
+
+Formal verification of deployed cryptographic code has matured from research
+prototypes to substantial artifacts: verified-by-construction libraries such
+as HACL*~\cite{hacl} and Fiat-Crypto~\cite{fiatcrypto} ship in mainstream
+software, and post-hoc verification pipelines such as Aeneas~\cite{aeneas}
+make it possible to state and prove theorems about existing production Rust
+code. The corpus underlying this paper is of the latter kind: four production
+Ed25519 implementations---upstream \texttt{curve25519-dalek}/%
+\texttt{ed25519-dalek} (one implementation: the curve crate and the
+signature crate atop it) and three deployed forks (Solana, RISC~Zero,
+Betrusted)---each carry Lean~4~\cite{lean4} certificates, proven against that
+fork's own extracted model, covering field arithmetic over $\Fp$, the
+complete twisted Edwards laws~\cite{edwards,twisted}, scalar arithmetic
+mod~$\ell$, encoding/decoding with constructive point decompression, and a
+four-tier characterization of signature verification~\cite{eddsa,rfc8032}
+whose strongest tier states: the extracted verifier accepts iff the
+signature's $R$ component decompresses to a valid curve point equal to
+$[k](-A) + [s]B$. Section~\ref{sec:corpus} states these theorems precisely.
+
+The economics of \emph{consuming} such evidence are poor: re-checking one
+fork's certificates takes ${\approx}30$ minutes of Lean kernel time and a
+pinned toolchain. A wallet, a package manager, or an autonomous agent
+choosing a cryptographic backend cannot pay this per decision---and need not:
+a deterministic re-check yields a fact that can be attested once and
+distributed. This is the classic transparency-log trade---Certificate
+Transparency~\cite{ct1,ct2} for certificate issuance, Sigstore's
+Rekor~\cite{sigstore} for signing events and supply-chain
+attestations~\cite{intoto}, key transparency~\cite{coniks}, checksum
+databases---applied to a payload with different trust semantics: evidence of
+machine-checked mathematical truth, together with its exact assumption set.
+
+\paragraph{Contributions.} The hash structure and proof algorithms are
+RFC~9162 verbatim, and we claim no novelty for any individual component. The
+contributions are:
+\begin{enumerate}[itemsep=1pt]
+\item \textbf{A precise trust model for attestation transparency over
+  machine-checked proofs} (\S\ref{sec:model}), in which the log operator is
+  trusted for \emph{observations} (``this is what the kernel printed'') but
+  never for \emph{verdicts} (``these proofs are acceptable''), because
+  consumers re-derive every verdict locally from the observed axiom cones
+  carried in each attestation.
+\item \textbf{Security proofs for the consumer-facing claims}
+  (\S\ref{sec:security}): completeness and soundness of the RFC~9162
+  inclusion verifier as used here (soundness as an explicit extractor that
+  turns any accepting proof for a non-member leaf into a SHA-256 collision),
+  the analogous consistency statement, safety of the consumer's pin-store
+  state machine, and verdict integrity. The statements are elementary but,
+  written out, they pin down exactly which assumption carries which claim.
+\item \textbf{Boundary-exact axiom auditing} (\S\ref{sec:construction}):
+  observed axiom cones are matched against per-theorem documented boundaries
+  \emph{exactly, in both directions}---an unexpected axiom and a missing
+  boundary axiom are both flagged.
+\item \textbf{A self-referential (not circular) signing design and a deployed
+  instance} (\S\ref{sec:selfref}, \S\ref{sec:deployment}): tree heads are
+  signed by a binary built from the pinned source of exactly the Ed25519
+  implementation attested in the log, with the operator's own Merkle
+  self-check of that leaf published alongside every signed head; and a small,
+  reproducible production deployment over the four-fork corpus, including a
+  measurement of proof portability across real forks.
+\end{enumerate}
+
+\paragraph{Non-claims.} The LTL does not mechanize cryptographic security
+proofs---that bridge is being built by EasyCrypt and its
+relatives~\cite{easycrypt}. It does not establish correctness of any binary,
+of SHA-512, of wire-format parsers, of the signing path, or any side-channel
+property; \S\ref{sec:deployment} enumerates the assumption set in full. It
+bridges an adjacent, mostly empty gap: type-theory-certified artifacts
+lack distribution infrastructure, and we are unaware of a deployed
+transparency log designed to carry kernel-replay attestations together
+with theorem-level assumption boundaries.\footnote{The
+acronym LTL collides with linear temporal logic~\cite{pnueli}; the collision
+is acknowledged.}
+
+\section{Background: the proof corpus}\label{sec:corpus}
+
+The corpus is a stack of theorems about extracted code, each stated through
+a denotation from machine representation to mathematics. Field elements are
+five 51-bit limbs denoting
+$[\![(a_0,\dots,a_4)]\!] = \sum_i a_i 2^{51i} \bmod p$ with
+$p = 2^{255}-19$, and every operation carries a two-clause
+specification---the value is right \emph{and} the representation invariant
+is preserved, e.g.
+\[
+\forall a\, b.\;\; \mathsf{bnd}\,a \Rightarrow \mathsf{bnd}\,b \Rightarrow
+\exists c.\;\; \mathsf{mul}\,a\,b = \mathsf{ok}\,c \,\wedge\,
+\mathsf{bnd}\,c \,\wedge\, [\![c]\!] = [\![a]\!]\cdot[\![b]\!].
+\]
+Point operations are proven to implement the complete twisted Edwards
+addition law on $E : -x^2+y^2 = 1+d\,x^2y^2$ over $\Fp$,
+\[
+(x_1,y_1)+(x_2,y_2) \;=\;
+\left(\frac{x_1y_2+x_2y_1}{1+d\,x_1x_2y_1y_2},\;
+      \frac{y_1y_2+x_1x_2}{1-d\,x_1x_2y_1y_2}\right),
+\]
+including the completeness fact that makes it branch-free ($a=-1$ is a
+square and $d$ a non-square in $\Fp$, so the denominators never
+vanish~\cite{edwards}).
+
+\paragraph{The signature apex as a lifting ladder.} The signature-tier
+result is not one theorem but a ladder of four, each lifting the previous
+one to a stronger domain; the payload the log distributes is the
+\emph{conjunction} of the four, and their separation is what makes the
+residual hypotheses legible. Write $\accept(A,m,R,s)$ for ``the extracted
+verifier returns \textsf{ok}'', let $k$ be the scalar produced by the hash
+oracle $H(R,A,m)$ with \emph{no properties assumed of $H$}, and let $r_1$
+be the 32-byte $R$ component exactly as it appears in the signature (raw
+bytes; no canonicity of them is presupposed). Each
+tier is proven for the extracted code under the wire-format
+hypotheses~$\mathcal{W}$ (the signature parses to an internal
+representation and the relevant compressed points re-encode; these
+outcomes are assumed, not proven---their byte-level specifications are
+part of the open frontier recorded in \S\ref{sec:limitations}).
+\begin{description}[itemsep=3pt,leftmargin=1.6em]
+\item[T1 (byte apex).] $\accept(A,m,R,s) \Leftrightarrow
+  \mathsf{compress}([s]B-[k]A) = r_1$. Acceptance is byte-equality of the
+  verifier's recomputed encoding with the signature's $R$ bytes---a
+  statement purely about the extracted control flow.
+\item[T2 (canonical half-lift).] The recomputed bytes
+  $\mathsf{compress}([s]B-[k]A)$ \emph{are} the canonical encoding of the
+  group element $[k](-A)+[s]B$; that is, $\mathsf{compress}$ agrees on this
+  input with the mathematical canonical-encoding function. T1 and T2 give
+  $\accept \Leftrightarrow \mathsf{enc}([k](-A)+[s]B) = r_1$.
+\item[T3 (injectivity / point equation).] Canonical encodings are
+  injective on $E(\Fp)$: if a valid curve point $P$ has $\mathsf{enc}(P) =
+  r_1$ then $P = [k](-A)+[s]B$. Injectivity is exactly where
+  non-squareness of $d$ re-enters---it keeps $1 + d y^2 \neq 0$, so the
+  curve equation determines $x^2$ from $y$ and the encoding is one-to-one.
+\item[T4 (constructive full lift).] $\accept(A,m,R,s) \Leftrightarrow
+  \mathsf{decompress}(R) = [k](-A)+[s]B$, with the extracted
+  $\mathsf{decompress}$ proven to realize the mathematical inverse of
+  $\mathsf{enc}$: exact byte parsing, the $(p+3)/8$-power square root, and
+  sign-bit root selection (for $x \neq 0$ the two roots $x$ and $p-x$
+  differ in parity since $p$ is odd, so the stored sign bit selects
+  correctly; at $x = 0$ the roots coincide and a set sign bit is rejected,
+  per RFC~8032---the theorem, an \emph{iff} over the extracted code,
+  covers this branch by construction).
+\end{description}
+The lift is monotone in strength---T1 is about bytes the code emits, T4 is
+about the group element a third party would recover from $R$---and each
+step names precisely one new mathematical fact (canonicity, injectivity,
+constructive inversion). A consumer that only trusts byte equality can
+stop at T1; a consumer reasoning about the underlying group element relies
+on T4. Both are in the corpus, separately certified, and the log carries
+all four so the consumer chooses the tier, not the operator.
+
+\paragraph{Axiom cones.} Each theorem's \emph{axiom cone}---the set of
+axioms its proof ultimately depends on, as reported by Lean's
+\texttt{\#print axioms}---is pinned exactly: the standard three axioms for
+the foundational certificates, plus an enumerated oracle boundary
+(SHA-512 and the wire-format types) at the four apex tiers. It is this
+exact set, not a pass/fail label, that each leaf carries and each consumer
+re-checks (\S\ref{sec:auditing}). Appendix~\ref{app:tiers} restates the
+ladder with the Lean theorem names; Appendix~\ref{app:axioms} lists the
+per-fork allowed sets verbatim.
+
+\section{Related work}\label{sec:related}
+
+Certificate Transparency~\cite{ct1,ct2} supplies the data structure and
+proof algorithms, used here unchanged; the underlying history-tree technique
+originates with Crosby and Wallach~\cite{crosby}. Dowling, G\"unther, Herath
+and Stebila~\cite{dghs} give formal security definitions and proofs for the
+CT primitives (logging schemes, inclusion, consistency); the analysis in
+\S\ref{sec:security} is in the same spirit, specialized to this system's
+verifier and stated so that each claim can later be mechanized in Lean
+(\S\ref{sec:next}). Rekor within Sigstore~\cite{sigstore} is the closest
+deployed system: a transparency log over signing events and supply-chain
+attestations such as in-toto~\cite{intoto} link metadata; its payloads attest
+\emph{process} (who signed, how an artifact was built), whereas LTL leaves
+attest kernel-checked mathematical statements together with their assumption
+sets, and the consumer re-derives verdicts rather than trusting labels. Key
+transparency~\cite{coniks} and checksum databases share the pattern with
+different payloads. Proof-carrying code~\cite{pcc} ships proofs to consumers
+who check them; the LTL serves consumers who cannot run any checker,
+replacing proof transport with attestation, inclusion, and signature---at
+the cost of trusting the operator's kernel run, a cost the design minimizes
+(\S\ref{sec:model}) but does not eliminate. Cheval, Moreira and Ryan
+formally verify transparency protocols themselves~\cite{cheval}; our
+direction is the complement (we log the verification), and \S\ref{sec:next}
+proposes meeting in the middle. Verified Merkle tree implementations exist,
+notably in EverCrypt~\cite{evercrypt}; \S\ref{sec:next} builds on that
+precedent rather than claiming it.
+
+\section{System and trust model}\label{sec:model}
+
+\subsection{Roles and scheme syntax}
+
+The system has exactly two roles with deliberately asymmetric costs and
+capabilities. The \emph{operator} (one per log) owns a Lean toolchain,
+replays proof corpora, holds the log's signing key, and bears append-only
+obligations. \emph{Consumers} (unbounded in number) hold the operator's
+public key, receive small evidence files, and verify: the Merkle
+inclusion core is roughly 25 lines of standard-library code
+(Appendix~\ref{app:verifier}); the full standalone consumer---head
+signature, consistency, mirror audit---is ${\approx}150$ lines
+(\S\ref{sec:pinstore}), atop an Ed25519 backend. Nothing a consumer
+does requires a theorem prover.
+
+We phrase the system as an \emph{attestation-transparency scheme}, in the
+style of the logging schemes of Dowling et al.~\cite{dghs}, so that the
+security goals below can name its algorithms precisely.
+
+\begin{definition}[Attestation-transparency scheme]\label{def:scheme}
+A scheme $\Pi$ is a tuple of algorithms over a hash function $\hash$ and a
+signature scheme $\mathsf{Sig}$:
+\begin{itemize}[itemsep=1pt,leftmargin=1.4em]
+\item $\mathsf{KeyGen} \to (sk, pk)$: the operator's head-signing keypair.
+\item $\mathsf{Append}(sk, \mathbf{D}, a) \to (\mathbf{D}', \sigma)$:
+  appends attestation-leaf $a$ to the ordered leaf list $\mathbf{D}$,
+  returning the new list and a signed tree head
+  $\sigma = \mathsf{Sig}.\mathsf{Sign}(sk, (|\mathbf{D}'|, \MTH(\mathbf{D}'), t))$.
+\item $\mathsf{ProveIncl}(\mathbf{D}, m) \to P$ and
+  $\mathsf{VerifyIncl}(pk, d, m, \sigma, P) \to \{0,1\}$: the membership
+  proof and its verifier (\S\ref{sec:tree}, Appendix~\ref{app:verifier}).
+\item $\mathsf{ProveCons}(\mathbf{D}, n_0) \to C$ and
+  $\mathsf{VerifyCons}(pk, \sigma_0, \sigma_1, C) \to \{0,1\}$: the
+  append-only (consistency) proof between two signed heads and its verifier
+  (\S\ref{sec:tree}).
+\item $\mathsf{Verdict}(\allowed, a) \to \{\clean, \neg\clean,
+  \bot\}^{|a|}$: the consumer's per-certificate verdict function
+  (\S\ref{sec:auditing}), parameterized by the consumer's \emph{own}
+  allowed-axiom table $\allowed$ and taking \emph{no} operator label as
+  input.
+\end{itemize}
+$\MTH$, $\mathsf{ProveIncl/VerifyIncl}$ and $\mathsf{ProveCons/VerifyCons}$
+are the RFC~9162 algorithms, defined in \S\ref{sec:tree}; $\mathsf{Append}$
+and $\mathsf{Verdict}$ are specific to this system.
+\end{definition}
+
+\subsection{Adversary model}
+
+We consider a probabilistic polynomial-time adversary $\mathcal{A}$ that
+controls the network (may reorder, replay, drop, or forge messages to
+consumers) and may \emph{be} the operator. A malicious operator may sign
+arbitrary tree heads, construct arbitrary leaves, present different views to
+different consumers, and label attestations arbitrarily. The single
+capability we do \emph{not} model cryptographically is falsification of
+kernel observations: an operator who reports an axiom cone that the Lean
+kernel never printed is lying about a physical event on its own machine, and
+no log structure can exclude this; \S\ref{sec:model:residual} isolates this
+residual trust precisely. Standard assumptions: SHA-256 is collision
+resistant; Ed25519 (as instantiated by the signing binary) is EUF-CMA
+secure; the consumer obtained the operator's true public key (trust on first
+use; \S\ref{sec:limitations}).
+
+\subsection{Security goals}\label{sec:model:goals}
+
+These goals are what per-item signatures alone cannot supply: a set of
+individually signed attestations cannot evidence a silent deletion
+(nothing commits to completeness), cannot expose two-faced service
+(independently valid views are incomparable), and offers no single value
+a consumer can pin and demand extensions of. The Merkle tree is chosen
+for these dishonesty-evidence properties, not for proof-size scaling,
+which at this deployment's size is immaterial.
+
+\begin{description}[itemsep=2pt]
+\item[G1 (Membership).] If a consumer accepts a receipt for attestation $a$
+  against a signed head, then $a$ is a leaf of the tree committed by that
+  head---any other outcome exhibits a SHA-256 collision or an Ed25519
+  forgery. (Theorem~\ref{thm:sound}, Proposition~\ref{prop:pin}.)
+\item[G2 (Append-only with fork evidence).] A consumer's accepted view of
+  the log only ever grows by extension, and two accepted heads of
+  \emph{equal} tree size with different roots are, together, transferable
+  publicly verifiable evidence of equivocation. Unequal-size split views
+  are not exposed by the head pair alone; they are exposed by the public
+  leaf mirror (\S\ref{sec:pinstore}), from which any party recomputes
+  every prefix root (itself operator-published, hence witness-dependent;
+  \S\ref{sec:limitations}), or by an external witness.
+  (Theorem~\ref{thm:consistency}, Proposition~\ref{prop:pin}.)
+\item[G3 (Verdict integrity).] The verdict a consumer derives for a
+  certificate depends only on the observed axiom cone in the leaf and the
+  consumer's \emph{own} copy of the allowed axiom sets; the operator's
+  pass/fail labels can deny (a certificate the operator does not itself
+  mark proven never counts) but can never grant.
+  (Proposition~\ref{prop:verdict}.)
+\end{description}
+
+\subsection{The residual trust, isolated}\label{sec:model:residual}
+
+Goals G1--G3 reduce the operator's trusted role to a single sentence,
+which we state at its honest width: \emph{``the operator executed the
+declared replay procedure against the exact pinned source and dependency
+state, using the declared toolchain, and bound the resulting kernel
+outputs faithfully to the correct theorem entries of the attestation.''}
+Checkout, dependency state, theorem-to-entry binding, and output parsing
+are all inside this observation pipeline---the first deployed run failed
+on precisely such a defect (\S\ref{sec:deployment}). Everything
+else---membership, history, verdicts---is either cryptographically
+enforced or locally re-derived. An
+operator that labels a dirty cone ``clean'' gains nothing (G3); an
+attestation that omits observed cones is treated as unverifiable; an
+operator that rewrites history is caught with transferable evidence (G2).
+An operator that fabricates observations can only be caught by independent
+replay, which any party with a Lean toolchain can perform from the pinned
+commit---the design makes such an audit cheap to \emph{target} (the claim
+is exact: repository, commit, toolchain, expected cones) even though it is
+expensive to \emph{run}.
+
+\subsection{Verdicts are the consumer's, not the operator's}\label{sec:model:card}
+
+The design choice behind G3 is what most distinguishes this system from
+prior attestation transparency, so we state it as a principle rather than
+a mechanism. In systems like Rekor~\cite{sigstore} a consumer learns
+\emph{that} something was attested and trusts the issuer's assessment of
+it; the payload's meaning is the issuer's to declare. Here the payload is
+a set of \emph{observations}---the literal \texttt{\#print axioms} output
+per theorem---and the assessment ($\clean$ or not) is computed by
+$\mathsf{Verdict}$ (Definition~\ref{def:scheme}) from those observations
+against the consumer's own table $\allowed$. Concretely:
+\begin{itemize}[itemsep=1pt,leftmargin=1.4em]
+\item The allowed set $\allowed(c)$ is not shipped by the operator at
+  verification time; it is part of the consumer's tooling, small enough to
+  audit by hand (Appendix~\ref{app:axioms}: 7--11 axiom names per fork),
+  and re-derivable \emph{up to naming} from the theorem statements---%
+  Lean's foundational three, plus, for the apex tiers, placeholders for
+  exactly those primitives the theorem deliberately leaves opaque (the
+  hash, the wire format); the placeholder \emph{names} themselves are
+  fixed by the fork's extracted surface and read off from
+  Appendix~\ref{app:axioms}.
+\item That an independently written $\allowed$ meets the deployed
+  observations \emph{exactly} is engineered, not coincidental: the corpus
+  is minimized so that every axiom in a cone earns its place, and any
+  reasonable reconstruction of ``what a correct proof of this statement
+  must assume,'' once the fork's extraction naming is fixed, lands on the
+  same finite set. When the consumer's requirement meets the supply
+  exactly, verification is a set equality.
+\item When it does not---a consumer who additionally requires SHA-512
+  itself proven, say---the gap is exact and itemized (the boundary axioms
+  of Appendix~\ref{app:axioms}), and the consumer's options are honest:
+  accept a \emph{named} residual, decline, or discharge the missing
+  boundary and let the resulting certificate enter the log. The log is
+  additive in the same way requirements are; a stricter table is a roadmap,
+  not a rejection.
+\end{itemize}
+The operator, in this picture, is not a judge whose verdict one trusts but
+a witness whose \emph{observations} one re-adjudicates. G3
+(\S\ref{sec:model:goals}, Proposition~\ref{prop:verdict}) is the formal
+statement that this re-adjudication takes no positive input from the
+operator's opinion: labels act, if at all, only as a conservative veto.
+
+\section{The log construction}\label{sec:construction}
+
+\subsection{Leaves: replay attestations}\label{sec:leaves}
+
+A leaf is the canonical JSON serialization of an attestation recording: the
+subject repository URL and git commit (which pins the entire source
+tree through git's object identifiers---hardened SHA-1, noted here
+because it is a weaker primitive than the log's own SHA-256); the
+toolchain versions; the resource-control regime
+under which the replay ran; and, per certificate, its name, replay status,
+and the \emph{observed axiom cone}---the exact output of Lean's
+\texttt{\#print axioms} for that theorem. For the corpus of
+\S\ref{sec:corpus} each attestation carries 16 certificates.
+Appendix~\ref{app:leaf} gives the leaf schema.
+
+\subsection{Boundary-exact auditing}\label{sec:auditing}
+
+Every certificate $c$ has a documented allowed axiom set $\allowed(c)$.
+Foundational certificates must carry exactly Lean's three standard axioms
+(\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}); the four
+signature-tier certificates additionally carry a per-fork, explicitly
+enumerated boundary (an opaque SHA-512 oracle and opaque wire-format
+types---e.g., eleven axioms in total for the upstream fork). Writing
+$\obs(c)$ for the observed cone recorded in the leaf, define
+\[
+\clean(c) \;:\Longleftrightarrow\; \obs(c) = \allowed(c)
+\quad\text{(equality of finite sets).}
+\]
+Deviation in \emph{either} direction---an unexpected axiom, or a missing
+boundary axiom---falsifies $\clean$. The second direction matters for
+these \emph{oracle} boundaries: a missing boundary axiom signals that the
+theorem no longer consumes a primitive it deliberately left opaque. The
+verifier does not attempt to distinguish the readings of that drift (a
+genuinely strengthened proof; a changed theorem; a hash oracle discharged
+by a placeholder rather than kept opaque; stale policy): it refuses to
+classify, and rejects. Each
+source repository enforces the same discipline in its own check scripts; the
+log mirrors those sets, and consumers carry their own copies.
+
+\subsection{Tree, heads, receipts}\label{sec:tree}
+
+Let $\hash$ be SHA-256. Define, for a byte string $d$ and 256-bit values
+$x,y$:
+\[
+\hleaf(d) = \hash(\texttt{0x00} \,\|\, d), \qquad
+\hnode(x,y) = \hash(\texttt{0x01} \,\|\, x \,\|\, y).
+\]
+For a leaf list $D = [d_0,\dots,d_{n-1}]$ the RFC~9162 tree head is
+\[
+\begin{aligned}
+\MTH([\,]) &= \hash(\varepsilon), \qquad
+\MTH([d]) = \hleaf(d),\\
+\MTH(D) &= \hnode\bigl(\MTH(D[0{:}k]),\, \MTH(D[k{:}n])\bigr),
+\end{aligned}
+\]
+where $k$ is the largest power of two strictly less than $n$. The
+\emph{inclusion path} for index $m$ is
+\[
+\Path(m, [d]) = [\,], \qquad
+\Path(m, D) =
+\begin{cases}
+\Path(m, D[0{:}k]) \,\|\, [\MTH(D[k{:}n])] & m < k,\\
+\Path(m-k, D[k{:}n]) \,\|\, [\MTH(D[0{:}k])] & m \ge k,
+\end{cases}
+\]
+and the consumer's root-reconstruction function $\Root(v, m, n, P)$ is the
+evident dual (Appendix~\ref{app:verifier}): fold the path back up, choosing
+left/right by comparing $m$ with $k$ at each level.
+
+\paragraph{Consistency.} A consistency proof $C$ lets a consumer check
+that a size-$n_1$ tree \emph{extends} a size-$n_0$ tree it already pinned,
+$0 < n_0 \le n_1$. We give the verifier as a function $\ConsRec$ that
+reconstructs \emph{both} committed roots from $C$; it is the recursive
+counterpart of RFC~9162~\S2.1.4, and we use this form (rather than the
+RFC's iterative one) because the proofs of \S\ref{sec:security} induct on
+it. On a proof $C$ interpreted as a list of nodes, with a flag $b$
+recording whether the size-$n_0$ subtree's root is carried implicitly (the
+pinned root) or explicitly in $C$:
+\[
+\ConsRec(n_0, n, C, b, r) =
+\begin{cases}
+(r, r) & n_0 = n,\ b,\ C = [\,],\\
+(s, s) & n_0 = n,\ \neg b,\ C = [s],\\
+\bigl(x,\, \hnode(y, s)\bigr) & n_0 \le k,\ C = C' \| [s],\\
+\bigl(\hnode(s, x'),\, \hnode(s, y')\bigr) & n_0 > k,\ C = C' \| [s],
+\end{cases}
+\]
+where $k$ is the largest power of two below $n$, $(x,y) =
+\ConsRec(n_0, k, C', b, r)$ in the third case, and $(x',y') =
+\ConsRec(n_0 - k, n - k, C', \bot, r)$ in the fourth (any shape mismatch
+rejects). The consumer accepts $C$ between signed heads $(n_0, r_0)$ and
+$(n_1, r_1)$ iff $n_0 = 0$, or $\ConsRec(n_0, n_1, C, \top, r_0) =
+(r_0, r_1)$. We verified that this recursive form agrees with the deployed
+iterative RFC~9162 verifier by \emph{exhaustive} differential testing over
+every pinned/current size pair $1 \le n_0 \le n_1 \le 256$, each with the
+honest proof and four adversarial mutations (wrong old root, wrong new
+root, truncated and padded proofs): $164{,}224$ verifier invocations,
+full agreement. The inclusion verifier of Appendix~\ref{app:verifier} was
+checked the same way ($164{,}479$ invocations over all $m < n \le 256$).
+
+The operator signs tree heads $(n, \MTH(D), t)$ with Ed25519; a
+\emph{receipt} for a leaf is its index, its sibling path, and a signed
+head. The signed payload is not the bare triple but the canonical JSON
+serialization (sorted keys, fixed separators, UTF-8---injective on the
+field set) of the head record, which additionally carries a protocol
+version tag (\texttt{pacta.transparency.signed\_tree\_head.v1}) and the
+log identity;
+a head signature therefore transfers neither across logs nor across
+protocol versions.
+
+\subsection{The consumer pin store}\label{sec:pinstore}
+
+Each consumer maintains a local pin $(n_{\mathrm{pin}}, r_{\mathrm{pin}})$,
+updated by the following state machine on receiving a validly signed head
+$(n', r')$:
+\begin{itemize}[itemsep=1pt]
+\item $n' = n_{\mathrm{pin}}$: accept iff $r' = r_{\mathrm{pin}}$; a
+  mismatch is reported as \emph{equivocation}, the pair of signed heads is
+  retained as evidence, and the state is poisoned (unrecoverable).
+\item $n' > n_{\mathrm{pin}}$: accept iff a consistency proof from
+  $(n_{\mathrm{pin}}, r_{\mathrm{pin}})$ to $(n', r')$ verifies; then update
+  the pin.
+\item $n' < n_{\mathrm{pin}}$: reject (rollback).
+\end{itemize}
+A freshness policy bounds head age; freshness, however, is an
+availability policy, not an append-only property---the construction
+detects rollback relative to a persisted pin, but does not prove that a
+consumer sees the newest issued head (an operator can re-issue fresh
+timestamps over a frozen tree). The full log is also published as a git
+repository: one file per leaf, plus the signed head history since
+publication began (heads signed before the mirror existed were not
+retained). Any cloner can therefore recompute every prefix root from the
+public leaves and check every published head against its prefix root and
+signature without consistency proofs---a low-infrastructure witness
+mechanism~\cite{ct2}; a standalone ${\approx}150$-line standard-library
+verifier ships in the mirror.
+
+\section{Security analysis}\label{sec:security}
+
+This section proves the claims G1--G3 of \S\ref{sec:model:goals}. The
+statements are not deep---inclusion and consistency security for RFC
+6962/9162 trees is folklore, and was treated formally by Dowling et
+al.~\cite{dghs}---but writing them out for \emph{this} system serves two
+purposes: it pins down exactly which assumption carries which consumer-facing
+claim, and it produces statements in a form ready for mechanization in Lean
+(\S\ref{sec:next}), where they will re-enter the log as leaves.
+
+We write $\Root(v, m, n, P)$ for the consumer's root reconstruction: it is
+defined by $\Root(v, m, 1, [\,]) = v$ and, for $n > 1$ with $k$ the largest
+power of two below $n$ and $P = P' \| [s]$,
+\[
+\Root(v, m, n, P) =
+\begin{cases}
+\hnode\bigl(\Root(v, m, k, P'),\, s\bigr) & m < k,\\
+\hnode\bigl(s,\, \Root(v, m-k, n-k, P')\bigr) & m \ge k,
+\end{cases}
+\]
+rejecting on any length mismatch. The consumer accepts a receipt
+$(d, m, P)$ against a head $(n, r)$ iff $m < n$ and
+$\Root(\hleaf(d), m, n, P) = r$.
+
+\begin{lemma}[Domain separation]\label{lem:domsep}
+No leaf preimage equals a node preimage as a byte string: for all $d, x, y$,
+$\texttt{0x00} \| d \neq \texttt{0x01} \| x \| y$.
+\end{lemma}
+\begin{proof}
+The first byte differs.
+\end{proof}
+
+Lemma~\ref{lem:domsep} forecloses the classic cross-type confusion in which
+an adversary presents an interior node's 64-byte child concatenation as a
+``leaf'' (or vice versa) to move a value between levels of the
+tree~\cite{crosby,dghs}; it guarantees that whenever a leaf preimage and
+a node preimage are compared, they already differ as strings, so equal
+hash values across the two types constitute a collision.
+
+\begin{theorem}[Inclusion completeness]\label{thm:complete}
+For every non-empty leaf list $D$ with $|D| = n$ and every $m < n$,
+\[
+\Root\bigl(\hleaf(D[m]),\, m,\, n,\, \Path(m, D)\bigr) = \MTH(D).
+\]
+\end{theorem}
+\begin{proof}
+Structural induction on $n$. For $n = 1$: $\Path(0, [d]) = [\,]$ and
+$\Root(\hleaf(d), 0, 1, [\,]) = \hleaf(d) = \MTH([d])$. For $n > 1$ with
+split point $k$, suppose $m < k$ (the case $m \ge k$ is symmetric). Then
+$\Path(m, D) = \Path(m, D[0{:}k]) \,\|\, [\MTH(D[k{:}n])]$, and by the
+induction hypothesis
+\[
+\Root\bigl(\hleaf(D[m]),\, m,\, k,\, \Path(m, D[0{:}k])\bigr)
+  = \MTH(D[0{:}k]),
+\]
+so the outer step yields
+$\hnode(\MTH(D[0{:}k]), \MTH(D[k{:}n])) = \MTH(D)$.
+\end{proof}
+
+Both soundness theorems below rest on a single collision-extraction fact,
+which we isolate first. Fix the honest Merkle tree $T$ of a leaf list $D$.
+A \emph{hash-fold over $T$} is a computation shaped by a connected
+sub-tree $S$ of $T$ containing $T$'s root: at every internal node of $T$
+lying in $S$ it emits $\hnode$ of its two children's values; each child
+lying outside $S$ is an \emph{input}, consumed as an opaque value; at
+every leaf of $T$ lying in $S$ it emits $\hleaf$ of an input leaf value.
+All inputs may be adversarial; only the shape is $T$'s. Three
+instantiations recur below: the inclusion reconstruction
+$\Root(\hleaf(\cdot), m, n, \cdot)$ ($S$ is the root path of leaf $m$;
+the consumed inputs are the path's siblings); the new-root component of
+the consistency verifier $\ConsRec$ (\S\ref{sec:tree}) ($S$ reaches down
+to the perfect subtrees covering $[0, n_0)$; the consumed inputs are the
+proof nodes and, on the leftmost spine, the pinned root); and the honest
+computation of $\MTH(D')$ for any $D'$ with $|D'| = |D|$ ($S$ is all of
+$T$; the inputs are the leaves of $D'$).
+
+\begin{lemma}[Root binding]\label{lem:bind}
+Let $F$ be a hash-fold over the honest Merkle tree $T$ of a leaf list $D$,
+and suppose $F$'s output equals $\MTH(D)$. Then either (i)~at some node of
+$S$, $F$'s hash argument differs from $T$'s while the two hash values
+agree---an explicit SHA-256 collision---or (ii)~$F$'s computation
+coincides with $T$ node-for-node: every value $F$ emits, \emph{every
+input it consumes}, and every leaf input it takes equals, respectively,
+the corresponding node value of $T$ and the corresponding leaf of $D$.
+\end{lemma}
+\begin{proof}
+Top-down induction on $S$, maintaining at each visited node the invariant
+that $F$'s value there equals $T$'s. At the root both equal $\MTH(D)$ by
+hypothesis. At an internal node of $S$ where the invariant holds, both
+values are $\hnode$ of an argument pair (65-byte preimages); if the pairs
+differ we are in case (i); if they coincide, each child's value is
+pinned: a child inside $S$ inherits the invariant and we recurse, while a
+child outside $S$ is a consumed input now known to equal $T$'s node value
+there---no descent needed. At a leaf of $S$ the invariant reads
+$\hleaf(d') = \hleaf(D[j])$: either $d' = D[j]$, or the two leaf preimages
+differ and we are in case (i). If case (i) never fires, the accumulated
+equalities at every node of $S$ are exactly claim (ii). Because $F$'s
+shape is $T$'s, every comparison above is leaf-to-leaf or node-to-node;
+Lemma~\ref{lem:domsep} additionally ensures that even a cross-type value
+coincidence would be a collision of distinct strings, which matters in
+the deployed protocol, where the same hash function commits leaves and
+nodes across trees of attacker-influenced sizes~\cite{crosby,dghs}.
+\end{proof}
+
+\begin{theorem}[Inclusion soundness: position binding]\label{thm:sound}
+There is an explicit algorithm $\mathcal{E}$ (running in time $O(n)$ hash
+evaluations) such that: whenever an adversary outputs a leaf list $D$ with
+$|D| = n$, an index $m < n$, a leaf $d \neq D[m]$, and a path $P$ with
+$\Root(\hleaf(d), m, n, P) = \MTH(D)$, $\mathcal{E}(D, m, d, P)$ outputs a
+SHA-256 collision.
+\end{theorem}
+\begin{proof}
+$F = \Root(\hleaf(d), m, n, \cdot)$ applied to $P$ is a hash-fold over the
+honest tree $T_D$ whose sub-tree $S$ is the root path of leaf $m$, with
+consumed inputs the entries of $P$ and leaf input $d$; by hypothesis its
+output is $\MTH(D)$. Apply Lemma~\ref{lem:bind}. Case (ii) includes the
+claim that the leaf input equals $D[m]$, contradicting $d \neq D[m]$; so
+case (i) fires. $\mathcal{E}$ recomputes $T_D$ ($O(n)$ hashes), replays
+the fold to locate the disagreeing pair, and outputs it.
+\end{proof}
+
+\begin{remark}
+Both soundness statements are unconditional in the same sense: they do not
+assert forgery is infeasible, they \emph{construct} a SHA-256 collision
+from any successful forgery, so append-only and position security are
+\emph{precisely} ``SHA-256 is collision resistant''---no more, no less. The
+two theorems share Lemma~\ref{lem:bind}, the only place hashing is reasoned
+about; this factoring is deliberate, as Lemma~\ref{lem:bind} is exactly
+what the Lean mechanization of \S\ref{sec:next} will carry, with collision
+resistance entering only as a documented boundary axiom, audited by the log
+like the SHA-512 oracle in the Ed25519 tiers.
+\end{remark}
+
+\begin{theorem}[Consistency soundness]\label{thm:consistency}
+There is an explicit algorithm $\mathcal{E}'$, running in $O(n_1)$ hash
+evaluations, such that: whenever an adversary outputs leaf lists $D_0, D_1$
+with $|D_0| = n_0 \le n_1 = |D_1|$ and $D_0 \neq D_1[0{:}n_0]$, together
+with a proof $C$ that the consumer's verifier of \S\ref{sec:tree} accepts,
+i.e.\ $\ConsRec(n_0, n_1, C, \top, \MTH(D_0)) = (\MTH(D_0), \MTH(D_1))$,
+$\mathcal{E}'(D_0, D_1, C)$ outputs a SHA-256 collision.
+\end{theorem}
+\begin{proof}
+$\ConsRec$ returns a pair; acceptance equates its second component with
+$\MTH(D_1)$ and its first with $\MTH(D_0)$. Reading the four cases, the
+second component emits $\hnode$ at every split it traverses of the
+size-$n_1$ tree and bottoms out on consumed values---it is a hash-fold
+over the honest tree $T_1$, with consumed inputs the proof nodes and, on
+the leftmost spine, the pinned root---while the first component reuses a
+sub-list of those same values, namely the ones covering the index range
+$[0, n_0)$, and folds \emph{only} those. We use the two components
+differently, so the delicate first component never enters the lemma.
+
+\emph{Step 1 (the transcript values are genuine).} Apply
+Lemma~\ref{lem:bind} to the second component against $T_1$. Either it hits
+case (i)---output that collision---or (case ii) every value it emitted and
+every input it consumed---each proof node, and the pinned root where the
+fold bottoms out on it---equals the corresponding node of $T_1$. Assume
+the latter; the consumed values are now known to be genuine nodes of the
+honest tree $T_1$.
+
+\emph{Step 2 (the prefix roots collide).} The consumed values covering
+$[0, n_0)$ sit at the canonical RFC~9162 decomposition of that range into
+maximal perfect subtrees of $T_1$; by Step~1 they are genuine, so folding
+them---which is exactly what the first component does (degenerately, when
+the old tree is itself a perfect subtree of $T_1$, the ``fold'' is the
+consumed pinned root alone)---yields the root of $D_1[0{:}n_0]$,
+i.e.\ the first component equals $\MTH(D_1[0{:}n_0])$. But acceptance also
+equates the first component with $\MTH(D_0)$. Hence
+$\MTH(D_0) = \MTH(D_1[0{:}n_0])$ while $D_0 \neq D_1[0{:}n_0]$.
+
+\emph{Step 3 (descend).} Since $|D_0| = |D_1[0{:}n_0]| = n_0$, the two
+honest trees have identical shape, so the honest computation of
+$\MTH(D_1[0{:}n_0])$ is a hash-fold over $T_{D_0}$ ($S$ the whole tree;
+leaf inputs the leaves of
+$D_1[0{:}n_0]$). Its output is $\MTH(D_1[0{:}n_0]) = \MTH(D_0)$ by Step~2,
+so Lemma~\ref{lem:bind} applies with $D = D_0$. Case (ii) would force the
+leaf inputs to equal $D_0$, i.e.\ $D_1[0{:}n_0] = D_0$, contradicting the
+premise; so case (i) fires---an explicit collision. $\mathcal{E}'$ outputs
+whichever collision was found; recomputing $T_0$ and $T_1$, it runs in
+$O(n_1)$ hash evaluations.
+\end{proof}
+
+\begin{proposition}[Pin-store safety]\label{prop:pin}
+Assume Ed25519 EUF-CMA security for the head-signing key and consider the
+state machine of \S\ref{sec:pinstore}. Then, except with the probability of
+a signature forgery or a SHA-256 collision:
+\begin{enumerate}[itemsep=1pt]
+\item (\emph{Monotonicity}) If a consumer's pin evolves through states
+$(n_1, r_1), \dots, (n_t, r_t)$, then $n_1 \le \dots \le n_t$, and for any
+leaf lists $D_i$ the operator can exhibit with $\MTH(D_i) = r_i$,
+$|D_i| = n_i$, each $D_i$ is a prefix of $D_{i+1}$.
+\item (\emph{Fork evidence}) If two consumers with the same pinned key ever
+hold accepted heads $(n, r)$ and $(n, r')$ with $r \neq r'$, the pair of
+signed heads is transferable, publicly verifiable evidence that the key
+holder signed two conflicting views.
+\end{enumerate}
+\end{proposition}
+\begin{proof}
+(1) The machine accepts a larger size only with a verified consistency
+proof, so by Theorem~\ref{thm:consistency} any exhibited leaf lists are
+prefix-ordered unless a collision is found; rollback is rejected
+syntactically. (2) Both heads carry valid signatures under the pinned key;
+under EUF-CMA, both were produced by the key holder, and $r \neq r'$ at
+equal size is precisely a split view. The evidence is transferable because
+verification requires only the public key.
+\end{proof}
+
+\begin{proposition}[Verdict integrity]\label{prop:verdict}
+Fix a consumer with local allowed-set table $\allowed(\cdot)$. For every
+attestation leaf $a$ and certificate $c$ in it, the consumer's
+\emph{cleanliness verdict} is
+the predicate $\clean(c) \Leftrightarrow \obs_a(c) = \allowed(c)$, a
+function of the leaf's observed cones and the consumer's table only; the
+operator's embedded pass/fail labels are not an input to it. The
+consumer's \emph{acceptance policy} consults those labels at most
+negatively: no operator assertion can upgrade any verdict or acceptance.
+\end{proposition}
+\begin{proof}
+By construction of the consumer tooling: the verdict function takes
+$(\obs_a, \allowed)$ and ignores the label fields in every branch; a
+certificate lacking an observed cone is mapped to \textsf{unverifiable},
+not to a verdict. The acceptance policy applies the operator's
+proven/failed \texttt{status} label only as a veto---a certificate the
+operator does not itself mark proven can never count---and a veto cannot
+upgrade; hence labels can deny but never grant.
+\end{proof}
+
+\paragraph{What is \emph{not} proven.} Propositions~\ref{prop:pin} and
+\ref{prop:verdict} together with Theorems~\ref{thm:complete}--%
+\ref{thm:consistency} discharge G1--G3. They do not---and cannot---exclude
+an operator who fabricates observations (\S\ref{sec:model:residual}), and
+they say nothing about the mathematical content of the attested corpus,
+whose guarantees rest on the Lean kernel and the assumption set enumerated
+in \S\ref{sec:deployment}. The division of labor is deliberate: the
+cryptographic layer makes the operator's claims \emph{exact, immutable, and
+attributable}; the deductive layer is what makes them \emph{true}.
+Table~\ref{tab:claims} decomposes the end-to-end chain: each consumer
+conclusion, the mechanism that establishes it, and the assumption that
+remains. The architecture does not pretend to eliminate trust; it
+decomposes trust into independently visible components---including two
+rows it deliberately does \emph{not} establish.
+
+\begin{table}[t]
+\centering\small
+\begin{tabular}{@{}p{0.31\textwidth}p{0.28\textwidth}p{0.33\textwidth}@{}}
+\toprule
+consumer conclusion & established by & remaining assumption \\
+\midrule
+leaf bytes sit at index $m$ under head $h$ & inclusion proof (Thm~\ref{thm:sound}) & SHA-256 collision resistance; authentic head \\
+head was authorized under the log key & Ed25519 verification & correct key pin; EUF-CMA \\
+new local head extends the old one & consistency proof (Thm~\ref{thm:consistency}) & SHA-256 collision resistance \\
+equal-size heads conflict: equivocation & two valid signatures, unequal roots (Prop~\ref{prop:pin}) & correct key pin \\
+observed cone matches local policy & set equality (Prop~\ref{prop:verdict}) & semantic identity of the named declarations at the pinned commit \\
+the kernel produced the observation & operator replay attestation & replay-pipeline honesty, or independent replay (\S\ref{sec:model:residual}) \\
+deployed binary matches verified source & \emph{not established} & reproducible build / binary attestation \\
+signing binary is the claimed implementation & \emph{not established} & execution provenance (\S\ref{sec:selfref}) \\
+\bottomrule
+\end{tabular}
+\caption{The end-to-end claim matrix. Every consumer conclusion, what
+establishes it, and what remains assumed. The last two rows are
+deliberate non-claims (\S\ref{sec:intro}, \S\ref{sec:limitations}).}
+\label{tab:claims}
+\end{table}
+
+\section{The self-referential signing loop}\label{sec:selfref}
+
+Tree heads are Ed25519 signatures, and this creates an opportunity for
+coherence: the log contains correctness certificates for an Ed25519
+implementation. The LTL's heads are therefore signed by a binary built from
+the pinned source tree of exactly the implementation attested in the log
+(serial backend pinned, matching the verified extraction), and---before
+signing---the operator runs the same Merkle inclusion verification a
+consumer runs, on the newest leaf attesting the signing implementation,
+against the tree about to be signed. The verdict is embedded in the
+signature block:
+\begin{quote}\ttfamily\small
+signing\_backend: verified-dalek-serial\\
+signing\_library\_source\_commit: aa0f6ab...\\
+signing\_library\_leaf\_index: 8\\
+signing\_library\_certificates\_proven: 16/16\\
+self\_inclusion: verified
+\end{quote}
+(These provenance fields ride alongside the signature as operator-provided
+context; they are not part of the signed payload, and a consumer relies on
+none of them---the acyclic chain below rests only on the signature and the
+leaf's inclusion.)
+The signature vouches for the tree; the tree vouches for the code that
+produced the signature; and the two vouchings are different proof modalities
+(cryptographic and deductive), so the loop is self-referential without being
+circular. Concretely, a consumer's verification order is a directed acyclic
+chain, no step trusting its own output: pin the operator key (assumed, once)
+$\to$ check the head signature (EUF-CMA) $\to$ verify the signing library's
+leaf is included in that head (hashes only, no signature) $\to$ optionally
+rebuild that library from its pinned commit and re-check its certificates
+(Lean kernel). The self-reference is only that the code producing signatures
+also \emph{appears as a subject} in the log; no check consumes the result it
+is establishing. The self-check always references the \emph{newest} leaf
+attesting the signing library: after the re-attestation of
+\S\ref{sec:deployment}, the referenced index advanced from~4 to~8
+automatically, the loop re-anchoring itself to the fresh attestation
+without operator intervention.
+
+\paragraph{The honest extent of this claim.} The Lean certificates cover
+the \emph{verification} path of the library (the theorems' subject is the
+extraction image of that path); the \emph{signing} path is not covered by
+any certificate and is declared trusted base. The deployed operator
+\emph{enforces and records} the invariant that the signing binary is
+built from the attested artifact rather than an unrelated third
+implementation; a consumer can check that the claimed source is attested
+in the signed tree, but---an Ed25519 signature reveals nothing about the
+program that produced it---cannot independently establish that this
+binary produced a given signature. Establishing that would require
+reproducible builds or execution attestation
+(\S\ref{sec:limitations}). Signature verification
+on consumer machines can optionally run through the same certified-source
+binary, with the backend that actually ran recorded in every result and a
+fail-closed policy flag available. First-append bootstrapping is handled
+honestly: heads signed before the signing library's attestation enters the
+log record \texttt{self\_inclusion: library\_not\_in\_log}.
+
+\section{Deployment and evidence}\label{sec:deployment}
+
+The LTL is deployed\footnote{Service: \url{https://ltl.zkdefi.org}
+(read-only HTTP API and documentation). Mirror:
+\url{https://github.com/saymrwulf/lean-transparency-log}. Operator and
+consumer tooling: \url{https://github.com/saymrwulf/proof-aware-crypto-tooling-agent}.
+The underlying proof corpora are in the
+\texttt{saymrwulf/*-ed25519-verified} repositories; every claim in this
+paper is re-checkable from these artifacts.} with twelve leaves,
+produced by three full replay runs (one attestation per fork per run;
+58--64 Lean files and ${\approx}1{,}800$\,s per fork, under hard memory
+caps and core pinning; the per-fork duration is corroborated by the
+inter-leaf \texttt{issued\_at} spacing in the published log, whose
+uninterrupted within-run gaps fall between 29m35s and 30m40s). Each
+successful run reports 16/16 certificates
+proven with boundary-exact cones, pinned to exact commits. The three runs
+correspond to three states of the world, and their coexistence in one
+append-only ledger is the point of the system:
+
+\begin{itemize}[itemsep=2pt]
+\item \textbf{Leaves 0--3 (failed run).} The first run's audit step failed
+  on two defects in the operator tooling (a path issue and a parser that
+  mishandled Lean's line-wrapped axiom lists for the eleven-axiom cones).
+  The operator signed attestations \emph{recording the failure} rather
+  than suppressing the run. Both defects were fail-closed: valid proofs
+  were rejected, invalid ones never accepted.
+\item \textbf{Leaves 4--7 (clean run).} After the fix, all four forks
+  attested 16/16 boundary-exact at that day's commits.
+\item \textbf{Leaves 8--11 (clean run, new commits).} A subsequent
+  documentation-only rewrite of the subject repositories' histories
+  changed their commit hashes. Because a leaf pins an exact commit
+  (\S\ref{sec:leaves}), the operator re-ran the full corpus and appended
+  fresh attestations at the new commits rather than editing leaves 4--7.
+  That the proof \emph{files} survived the rewrite unchanged is
+  corroborated from the log itself: leaves 4--7 and 8--11 carry identical
+  certificate lists and identical observed axiom cones, re-checked by the
+  kernel at both commit generations. (The pre-rewrite trees themselves are
+  no longer distributed, so a direct tree diff is not among the public
+  artifacts.)
+\end{itemize}
+
+\noindent This last event is a live exercise of the append-only
+discipline (G2): a change that a naive operator would have hidden by
+overwriting is instead absorbed by \emph{addition}, leaving a permanent,
+publicly verifiable record that the subject histories changed and that
+the mathematics survived the change. The ledger---four failure leaves and
+eight success leaves across two commit generations---is a feature of the
+trust model, not clutter to be pruned (Figure~\ref{fig:tree}).
+
+\begin{figure}[t]
+\centering
+\begin{tikzpicture}[
+  every node/.style={font=\footnotesize},
+  leaf/.style={draw, minimum width=0.62cm, minimum height=0.42cm, inner sep=1pt},
+  fail/.style={leaf, draw=black!45, text=black!55, fill=black!7},
+  ok/.style={leaf, draw=black!85, fill=black!3},
+  node/.style={draw, circle, minimum size=0.34cm, inner sep=0pt, fill=black!4},
+  edge/.style={draw=black!55}, xscale=0.92]
+  % leaves 0..11
+  \foreach \i in {0,...,3} \node[fail] (l\i) at (\i,0) {\i};
+  \foreach \i in {4,...,11} \node[ok] (l\i) at (\i,0) {\i};
+  % exact RFC 9162 shape for n = 12: root splits 8 | 4
+  \foreach \i/\a/\b in {0/0/1, 1/2/3, 2/4/5, 3/6/7, 4/8/9, 5/10/11}
+    \node[node] (m\i) at ({(\a+\b)/2},1.0) {};
+  \node[node] (q0) at (1.5,1.95) {};   % leaves 0-3
+  \node[node] (q1) at (5.5,1.95) {};   % leaves 4-7
+  \node[node] (q2) at (9.5,1.95) {};   % leaves 8-11
+  \node[node] (o0) at (3.5,2.9)  {};   % leaves 0-7
+  \node[node, minimum size=0.4cm] (root) at (6.5,3.85) {};
+  \node[right=1pt of root, font=\small] {\ signed tree head $\;\sigma = \mathrm{Sig}(sk,(12,r,t))$};
+  % edges
+  \foreach \i/\a/\b in {0/0/1, 1/2/3, 2/4/5, 3/6/7, 4/8/9, 5/10/11}
+    { \draw[edge] (l\a)--(m\i); \draw[edge] (l\b)--(m\i); }
+  \draw[edge] (m0)--(q0); \draw[edge] (m1)--(q0);
+  \draw[edge] (m2)--(q1); \draw[edge] (m3)--(q1);
+  \draw[edge] (m4)--(q2); \draw[edge] (m5)--(q2);
+  \draw[edge] (q0)--(o0); \draw[edge] (q1)--(o0);
+  \draw[edge] (o0)--(root); \draw[edge] (q2)--(root);
+  % brackets under leaf ranges
+  \draw[decorate,decoration={brace,mirror,raise=3pt}, black!45]
+    (l0.south west) -- (l3.south east)
+    node[midway,below=7pt, black!55]{run 1: failed audit};
+  \draw[decorate,decoration={brace,mirror,raise=3pt}, black!70]
+    (l4.south west) -- (l7.south east)
+    node[midway,below=7pt]{run 2: clean, commits $g_1$};
+  \draw[decorate,decoration={brace,mirror,raise=3pt}, black!70]
+    (l8.south west) -- (l11.south east)
+    node[midway,below=7pt]{run 3: clean, commits $g_2$};
+\end{tikzpicture}
+\caption{The deployed twelve-leaf log. Grey leaves 0--3 record the first
+run's audit failure (retained, not erased); leaves 4--7 and 8--11 are two
+clean runs, at commit generations $g_1$ and $g_2$ across a subject-history
+rewrite. The interior is the exact RFC~9162 shape of \S\ref{sec:tree} for
+$n = 12$ (root split $8 \mid 4$; $r$ denotes the root value). Every value
+in the figure is recomputable from the public leaves.}
+\label{fig:tree}
+\end{figure}
+
+\begin{table}[t]
+\centering\small
+\begin{tabular}{@{}lrrl@{}}
+\toprule
+fork & Lean files & apex cone (axioms, total) & SHA-512 in the boundary \\
+\midrule
+upstream \texttt{dalek} & 64 & 11 & 3-call streaming (\texttt{new/update/finalize}) \\
+Solana (\texttt{anza})  & 58 & \phantom{0}7 & one \texttt{ed\_sigs.sha512\_hash3} \\
+RISC~Zero               & 63 & \phantom{0}8 & one \texttt{verifying.sha512\_hash3} \\
+Betrusted               & 63 & \phantom{0}8 & one \texttt{verifying.sha512\_hash3} \\
+\bottomrule
+\end{tabular}
+\caption{The four subject implementations. Each replay re-checks 16
+certificates in ${\approx}1{,}800$\,s under memory caps and core pinning.
+The apex-cone count is the full allowed axiom set at the signature
+tiers---Lean's three standard axioms plus the fork's enumerated oracle
+boundary (Appendix~\ref{app:axioms}); it differs by fork because the
+SHA-512 surface and the byte-accessor shape differ. Proof-script
+divergence across forks is quantified in the portability paragraph below;
+the pure-mathematics files are byte-identical across all four.}
+\label{tab:forks}
+\end{table}
+
+\paragraph{What a verified receipt establishes.} Under the assumptions
+enumerated below, a consumer who verifies a receipt knows: \emph{the
+operator whose key I pinned attests that the Lean certificates of repository
+$X$ at commit $Y$ re-check, with per-certificate observed axiom cones as
+included---and this statement is part of the log presented to every other
+consumer.} Combined with local verdict re-derivation
+(Proposition~\ref{prop:verdict}), this yields source-level assurance for the
+pinned commit. It deliberately does \emph{not} establish: correctness of any
+binary (consumers build from the pinned source; compilers are trusted base),
+correctness of SHA-512 (an opaque oracle in the theorems), correctness of
+the wire-format parsers (their outcomes are hypotheses of the signature
+tiers), signing-side correctness, or side-channel properties.
+
+\paragraph{The assumption set, in full.} The Lean kernel and its three
+axioms plus mathlib; faithfulness of the Charon/Aeneas
+extraction~\cite{aeneas}; each fork's documented oracle boundary; operator
+key custody and trust-on-first-use key distribution (mitigated by publishing
+the key in two independent locations); collision resistance of SHA-256 for
+the log (Theorems~\ref{thm:sound}, \ref{thm:consistency}); unforgeability
+of Ed25519 for the heads (Proposition~\ref{prop:pin}); and the consumer's
+own ${\approx}25$-line verifier (Appendix~\ref{app:verifier}).
+
+\paragraph{An observational by-product: proof portability.} Because the
+four corpora prove the same theorems against four independent extractions,
+the diff between proof files measures how portable proofs are across real
+forks. Pure-mathematics files (e.g., a carry-telescope lemma file) are
+byte-identical across all four; extraction-facing proof scripts diverge
+sharply where the forks' code or the extractor's naming differs (e.g., 215
+changed lines for the byte-parser proofs on the two forks whose extraction
+produces a closure-based loader; 121 lines for the signature-glue proofs on
+the same-crate fork; 27 lines between the two structurally closest forks,
+tracking one fork's \texttt{black\_box} optimization barrier and the
+operation reordering it induces). Per-target
+verification, in other words, is doing
+measurable work exactly where the targets actually differ.
+
+\section{Limitations}\label{sec:limitations}
+
+The deployment is small (one operator, twelve leaves, four subject
+repositories) and the operator is a single party; split-view defense
+currently rests on consumer-side pinning (Proposition~\ref{prop:pin}) plus
+the public git mirror rather than an independent witness network. Key
+distribution is trust-on-first-use. The signing path of the dogfood binary
+is unverified (declared, not proven). The residual trust of
+\S\ref{sec:model:residual}---honesty of the operator's kernel
+observations---is mitigated only by targeted independent replay, and
+replayability presupposes retrievability: a leaf whose pinned commit is
+no longer distributed (leaves 0--7 after the subject-history rewrite,
+\S\ref{sec:deployment}) decays from a replayable claim to a historical
+record, and consumers act on the newest, retrievable attestations. The corpus
+itself stops at source-level assurance: reproducible builds and side-channel
+evidence remain open, and ML-DSA slots in the head format are deliberately
+recorded as unavailable rather than backed by an unverified implementation.
+
+\section{Next step: verifying the accumulator itself}\label{sec:next}
+
+The natural continuation applies the corpus's own discipline to the log's
+cryptographic half. Theorems~\ref{thm:complete}--\ref{thm:consistency} and
+Proposition~\ref{prop:pin} were stated so as to make their mechanization
+direct; we expect the principal work to be specification alignment and
+proof engineering rather than new cryptographic argument: (i) inclusion completeness
+(Theorem~\ref{thm:complete}) is assumption-free; (ii) inclusion soundness
+becomes the explicit extractor of Theorem~\ref{thm:sound}, with SHA-256
+collision resistance a documented boundary axiom audited exactly like the
+SHA-512 oracle in the Ed25519 tiers; (iii) likewise consistency
+(Theorem~\ref{thm:consistency}); (iv) domain separation
+(Lemma~\ref{lem:domsep}) is a one-line lemma; and (v) total correctness of
+the consumer's pin-store state machine (Proposition~\ref{prop:pin}).
+Verified Merkle implementations in F*~\cite{evercrypt} and machine-checked
+transparency-protocol analyses~\cite{cheval} show these proofs are well
+within reach; the LTL-specific closure is where the certificates go:
+\emph{into the log they defend, checked by the certified checker they
+specify}, alongside a consumer policy flag requiring the certified verifier.
+At that point both proving traditions in the composition run on certified
+code, and the remaining trusted base is two hash assumptions, a compiler, an
+extraction pipeline, and one key.
+
+\section*{Acknowledgments}
+
+The author designed the system, directed the verification effort, and is
+solely accountable for every claim in this paper. Claude (Anthropic) was
+used as an assistant in developing the proof corpora, tooling, and text,
+and adversarial reviews by both Claude and GPT (OpenAI) shaped the final
+manuscript; all
+proofs, measurements, and claims have been reviewed by the author and are
+independently re-checkable from the public artifacts and the referenced
+check scripts.
+% \authortodo{The sentence above must be true before you submit it.
+% Review every proof in Section 6 line by line and re-run every number in
+% Section 8 yourself.}
+
+\begin{thebibliography}{20}
+\itemsep2pt
+
+\bibitem{ct1} B. Laurie, A. Langley, E. K\"asper. Certificate Transparency.
+RFC 6962, 2013.
+
+\bibitem{ct2} B. Laurie, E. Messeri, R. Stradling. Certificate Transparency
+Version 2.0. RFC 9162, 2021.
+
+\bibitem{crosby} S. A. Crosby, D. S. Wallach. Efficient Data Structures for
+Tamper-Evident Logging. USENIX Security, pp. 317--334, 2009.
+
+\bibitem{dghs} B. Dowling, F. G\"unther, U. Herath, D. Stebila. Secure
+Logging Schemes and Certificate Transparency. ESORICS, LNCS 9879, pp.
+140--158, 2016.
+
+\bibitem{sigstore} Z. Newman, J. S. Meyers, S. Torres-Arias. Sigstore:
+Software Signing for Everybody. ACM CCS, pp. 2353--2367, 2022.
+
+\bibitem{intoto} S. Torres-Arias, H. Afzali, T. K. Kuppusamy, R. Curtmola,
+J. Cappos. in-toto: Providing farm-to-table guarantees for bits and bytes.
+USENIX Security, pp. 1393--1410, 2019.
+
+\bibitem{coniks} M. S. Melara, A. Blankstein, J. Bonneau, E. W. Felten,
+M. J. Freedman. CONIKS: Bringing Key Transparency to End Users. USENIX
+Security, pp. 383--398, 2015.
+
+\bibitem{pcc} G. C. Necula. Proof-Carrying Code. ACM POPL, pp. 106--119,
+1997.
+
+\bibitem{cheval} V. Cheval, J. Moreira, M. Ryan. Automatic verification of
+transparency protocols. IEEE EuroS\&P, pp. 107--121, 2023.
+doi:10.1109/EuroSP57164.2023.00016. arXiv:2303.04500.
+
+\bibitem{easycrypt} G. Barthe, B. Gr\'egoire, S. Heraud, S. Zanella
+B\'eguelin. Computer-Aided Security Proofs for the Working Cryptographer.
+CRYPTO, LNCS 6841, pp. 71--90, 2011.
+
+\bibitem{aeneas} S. Ho, J. Protzenko. Aeneas: Rust verification by
+functional translation. Proc. ACM Program. Lang. 6 (ICFP): 711--741, 2022.
+
+\bibitem{lean4} L. de Moura, S. Ullrich. The Lean 4 Theorem Prover and
+Programming Language. CADE-28, LNCS 12699, pp. 625--635, 2021.
+
+\bibitem{hacl} J.-K. Zinzindohou\'e, K. Bhargavan, J. Protzenko,
+B. Beurdouche. HACL*: A Verified Modern Cryptographic Library. ACM CCS,
+pp. 1789--1806, 2017.
+
+\bibitem{evercrypt} J. Protzenko et al. EverCrypt: A Fast, Verified,
+Cross-Platform Cryptographic Provider. IEEE S\&P, pp. 983--1002, 2020.
+
+\bibitem{fiatcrypto} A. Erbsen, J. Philipoom, J. Gross, R. Sloan,
+A. Chlipala. Simple High-Level Code for Cryptographic Arithmetic---With
+Proofs, Without Compromises. IEEE S\&P, pp. 1202--1219, 2019.
+
+\bibitem{eddsa} D. J. Bernstein, N. Duif, T. Lange, P. Schwabe, B.-Y. Yang.
+High-speed high-security signatures. J. Cryptographic Engineering 2(2):
+77--89, 2012.
+
+\bibitem{rfc8032} S. Josefsson, I. Liusvaara. Edwards-Curve Digital
+Signature Algorithm (EdDSA). RFC 8032, 2017.
+
+\bibitem{edwards} D. J. Bernstein, T. Lange. Faster addition and doubling on
+elliptic curves. ASIACRYPT, LNCS 4833, pp. 29--50, 2007.
+
+\bibitem{twisted} D. J. Bernstein, P. Birkner, M. Joye, T. Lange,
+C. Peters. Twisted Edwards curves. AFRICACRYPT, LNCS 5023, pp. 389--405,
+2008.
+
+\bibitem{pnueli} A. Pnueli. The temporal logic of programs. IEEE FOCS, pp.
+46--57, 1977.
+
+\end{thebibliography}
+
+\appendix
+
+\section{Leaf schema}\label{app:leaf}
+
+Each leaf is the canonical JSON serialization (sorted keys, no
+insignificant whitespace, UTF-8) of an attestation. Below is leaf~8 of
+the deployed log---the re-attestation of the upstream fork. The
+16-certificate array is elided to its first (foundational) and last
+(apex) entries; long values (hashes, timestamps, version strings,
+paths) are shortened, and omitted fields are marked, with ellipses; and
+fields are shown in logical rather than canonical (sorted-key) order
+for readability. The
+field names and values shown, and the axiom lists, are verbatim, and the
+unelided leaf is one \texttt{jq} invocation away in the public mirror.
+\begin{quote}\ttfamily\scriptsize
+\{ "type": "pacta.attestation", "schema\_version": 1,\\
+\hspace*{0.6em}"attestation": \{\\
+\hspace*{1.2em}"provider": "local-pacta-provider",\\
+\hspace*{1.2em}"issued\_at": "2026-07-07T...Z",\\
+\hspace*{1.2em}"subject": \{ "component": "dalek-ed25519-verified",\\
+\hspace*{2.4em}"repo\_commit": "33fb8bb2311c70ead2e83c0...",\\
+\hspace*{2.4em}"repo\_url": ..., "verified\_backend": "serial/u64",\\
+\hspace*{2.4em}... \},\\
+\hspace*{1.2em}"environment": \{\\
+\hspace*{2.4em}"lean\_version": "Lean (version 4.30.0-rc2, ...)",\\
+\hspace*{2.4em}"lake\_version": ..., "env\_script": ...,\\
+\hspace*{2.4em}"lean\_project\_dir": ... \},\\
+\hspace*{1.2em}"machine\_protection": \{ "lean\_guard": ...,\\
+\hspace*{2.4em}"note": "All Lean compiles route through the\\
+\hspace*{2.4em}repo's lean-guard (memory cap, core pinning,\\
+\hspace*{2.4em}timeout, single-flight lock) ..." \},\\
+\hspace*{1.2em}"replay": \{ "checked\_files": 64, "failed\_files": [],\\
+\hspace*{2.4em}"check\_ok": true, "axiom\_ok": true, ... \},\\
+\hspace*{1.2em}"certificates": [\\
+\hspace*{2.4em}\{ "name": "CurveFieldProofs.fieldImplementation",\\
+\hspace*{3.0em}"status": "proven", "axiom\_status": "clean",\\
+\hspace*{3.0em}"observed\_axioms": ["propext",\\
+\hspace*{3.6em}"Classical.choice","Quot.sound"],\\
+\hspace*{3.0em}"expected\_axioms": [...], ... \},\\
+\hspace*{2.4em}... \; \emph{(14 certificates elided)} \; ...\\
+\hspace*{2.4em}\{ "name":\\
+\hspace*{3.0em}"CurveFieldProofs.verify\_accepts\_iff\_decompress",\\
+\hspace*{3.0em}"status": "proven", "axiom\_status": "clean",\\
+\hspace*{3.0em}"observed\_axioms": ["propext","Classical.choice",\\
+\hspace*{3.6em}"Quot.sound","ed25519.Signature","sha2.Sha512",\\
+\hspace*{3.6em}"verifying.sha512\_finalize\_bytes",\\
+\hspace*{3.6em}"verifying.sha512\_new","verifying.sha512\_update",\\
+\hspace*{3.6em}"ed25519.Signature.to\_bytes",\\
+\hspace*{3.6em}"signature.error.Error",\\
+\hspace*{3.6em}"signature.error.Error.new"], ... \} ],\\
+\hspace*{1.2em}"signature": \{ "scheme": "openssl-ed25519", ... \},\\
+\hspace*{1.2em}... \} \}
+\end{quote}
+The \texttt{observed\_axioms} field is the exact output of
+\texttt{\#print axioms} for that theorem. Operator labels
+(\texttt{replay.check\_ok}, per-certificate \texttt{status} and
+\texttt{axiom\_status}) are recorded for the audit trail, but the
+cleanliness verdict is $\obs = \allowed$ computed against the consumer's
+own table in every case, with a missing cone mapped to
+\textsf{unverifiable} (Proposition~\ref{prop:verdict}). The
+\texttt{status} label is consulted only \emph{negatively}: a certificate
+the operator itself does not mark proven can never count toward
+acceptance, so labels can deny but never grant.
+
+\section{The consumer verifier}\label{app:verifier}
+
+The consumer-side inclusion check, in full (Python, standard library only);
+this is the recursive form proved in \S\ref{sec:security} and is equivalent
+to the iterative algorithm of RFC~9162 \S2.1.3.2.
+
+\begin{quote}\ttfamily\small
+import hashlib\\[2pt]
+def H(b): return hashlib.sha256(b).digest()\\
+def h\_leaf(d): return H(b'\textbackslash x00' + d)\\
+def h\_node(x, y): return H(b'\textbackslash x01' + x + y)\\[2pt]
+def largest\_pow2\_below(n):\\
+\hspace*{1em}k = 1\\
+\hspace*{1em}while 2 * k < n: k *= 2\\
+\hspace*{1em}return k\\[2pt]
+def root(v, m, n, path):\\
+\hspace*{1em}if n == 1:\\
+\hspace*{2em}if path: raise ValueError\\
+\hspace*{2em}return v\\
+\hspace*{1em}if not path: raise ValueError\\
+\hspace*{1em}*rest, s = path\\
+\hspace*{1em}k = largest\_pow2\_below(n)\\
+\hspace*{1em}if m < k:\\
+\hspace*{2em}return h\_node(root(v, m, k, rest), s)\\
+\hspace*{1em}return h\_node(s, root(v, m - k, n - k, rest))\\[2pt]
+def verify\_inclusion(leaf, m, n, path, head\_root):\\
+\hspace*{1em}return m < n and root(h\_leaf(leaf), m, n, path) == head\_root
+\end{quote}
+Signature verification of the head (Ed25519) and the pin-store logic of
+\S\ref{sec:pinstore} complete the consumer; the deployed
+${\approx}150$-line standalone verifier in the mirror additionally checks
+consistency proofs and recomputes prefix roots from the public leaves.
+
+\section{Allowed axiom sets}\label{app:axioms}
+
+Foundational certificates (12 of 16) must carry exactly Lean's three
+standard axioms:
+\begin{quote}\ttfamily\small
+propext \quad Classical.choice \quad Quot.sound
+\end{quote}
+The four signature-tier certificates additionally carry a per-fork
+enumerated boundary: an opaque SHA-512 oracle and opaque wire-format
+types (the signature type, its byte accessors, and---where the fork's
+API surfaces it---the error type). The
+boundary is not identical across forks---it reflects each fork's actual
+extracted surface---and auditing is exact against the fork's own set. The
+three distinct boundaries in the deployed corpus, verbatim from the
+repositories' check scripts, are as follows (the three standard axioms
+above, plus):
+
+\smallskip
+\noindent\textbf{Upstream \texttt{curve25519-dalek}} (11 axioms total;
+this fork exposes SHA-512 as three streaming operations):
+\begin{quote}\ttfamily\scriptsize
+ed25519.Signature \quad sha2.Sha512\\
+verifying.sha512\_finalize\_bytes\\
+verifying.sha512\_new \quad verifying.sha512\_update\\
+ed25519.Signature.to\_bytes\\
+signature.error.Error \quad signature.error.Error.new
+\end{quote}
+
+\noindent\textbf{RISC~Zero and Betrusted forks} (8 axioms total;
+identical to each other---SHA-512 is a single \texttt{hash3} oracle):
+\begin{quote}\ttfamily\scriptsize
+ed25519.Signature \quad verifying.sha512\_hash3\\
+ed25519.Signature.to\_bytes\\
+signature.error.Error \quad signature.error.Error.new
+\end{quote}
+
+\noindent\textbf{Solana (anza) fork} (7 axioms total; its own
+\texttt{ed\_sigs} namespace, and \texttt{R}/\texttt{s} byte accessors
+rather than a whole-signature encoder):
+\begin{quote}\ttfamily\scriptsize
+ed25519.Signature \quad ed\_sigs.sha512\_hash3\\
+ed25519.Signature.r\_bytes \quad ed25519.Signature.s\_bytes
+\end{quote}
+
+A consumer's local table (\S\ref{sec:auditing}) contains exactly these
+sets. That a boundary differs by fork is itself audited: an
+upstream-shaped cone appearing under the anza label, or vice versa, fails
+$\clean$ in the ``unexpected axiom'' direction.
+
+\section{The four verification tiers: Lean theorem names}\label{app:tiers}
+
+The lifting ladder T1--T4 and the mathematical facts it turns on are
+stated in \S\ref{sec:corpus}. For reproducibility we record here the
+verbatim Lean theorem name backing each tier in the upstream corpus
+(namespace \texttt{CurveFieldProofs} elided; the forks use the same names
+against their own extractions); a reader can
+\texttt{\#print axioms} any of these to reproduce the cones of
+Appendix~\ref{app:axioms}.
+\begin{center}\small
+\begin{tabular}{@{}ll@{}}
+\toprule
+tier (\S\ref{sec:corpus}) & Lean theorem \\
+\midrule
+T1 \enspace byte apex          & \texttt{verify\_accepts\_iff} \\
+T2 \enspace canonical half-lift & \texttt{verify\_accepts\_iff\_point} \\
+T3 \enspace injectivity / point eq. & \texttt{verify\_accepts\_iff\_point\_eq} \\
+T4 \enspace constructive full lift & \texttt{verify\_accepts\_iff\_decompress} \\
+\bottomrule
+\end{tabular}
+\end{center}
+All four are proven under the wire-format hypotheses $\mathcal{W}$ of
+\S\ref{sec:corpus}; a consumer reasoning about the underlying group
+element relies on their conjunction (the ladder up to T4), and all four
+cones are audited against the same per-fork boundary of
+Appendix~\ref{app:axioms}.
+
+\end{document}
diff --git a/paper/ltl.pdf b/paper/ltl.pdf
index 2747bf4..21dbda7 100644
Binary files a/paper/ltl.pdf and b/paper/ltl.pdf differ
diff --git a/paper/ltl.tex b/paper/ltl.tex
index 54c3c60..f18444f 100755
--- a/paper/ltl.tex
+++ b/paper/ltl.tex
@@ -1,1102 +1,924 @@
-% LTL paper, v4 = merge of two independent hostile reviews (2026-07-10).
-% Review A (second Fable instance): frontier hash-fold framework (the
-% lemma did not cover its own uses as written), dangling R4/R5 labels,
-% deny-only label semantics, Table 1 caption, r_1 as raw bytes, exact
-% RFC 9162 figure. Review B (GPT-5.6): G2/abstract narrowed to what
-% Prop 1 proves, residual-trust sentence at honest width, freshness and
-% self-reference disclaimers, softened novelty/mechanization claims,
-% head-encoding documented, claim-matrix table. Both reviews' findings
-% independently re-verified before adoption.
+% Reconstructed directly from the 1344-line rejected ltl.tex and its PDF,
+% using reinvention-outline.md and the live 13-leaf deployment as factual patch.
 \documentclass[11pt]{article}
-\usepackage[a4paper,margin=1.1in]{geometry}
-\usepackage{amsmath,amssymb,amsthm}
-\usepackage{xcolor}
-\usepackage[colorlinks=true,linkcolor=blue!60!black,citecolor=blue!60!black,urlcolor=blue!60!black]{hyperref}
+\usepackage[a4paper,margin=1.02in]{geometry}
+\usepackage{amsmath,amssymb,amsthm,mathtools}
+\usepackage{booktabs,tabularx,array}
 \usepackage{enumitem}
-\usepackage{booktabs}
+\usepackage{xcolor}
 \usepackage{lmodern}
 \usepackage{microtype}
-% this TeX install's format ships righthyphenmin=1 ('it-s'); restore standard
-\lefthyphenmin=2 \righthyphenmin=3
+\usepackage{listings}
 \usepackage{tikz}
-\usetikzlibrary{fit,positioning,decorations.pathreplacing}
+\usetikzlibrary{arrows.meta,positioning,fit,decorations.pathreplacing,calc}
+\usepackage[colorlinks=true,linkcolor=blue!55!black,citecolor=blue!55!black,urlcolor=blue!55!black]{hyperref}
+\hypersetup{pdftitle={Accountable Distribution of Machine-Checked Correctness Evidence: A Transparency Model and the Lean Transparency Log},pdfauthor={Olaf Horvath},pdfsubject={Transparency distribution of formal-verification replay evidence},pdfkeywords={formal verification, transparency log, Lean, Ed25519, Merkle tree, attestation}}
+\lefthyphenmin=2 \righthyphenmin=3
 
+\newtheorem{definition}{Definition}
 \newtheorem{theorem}{Theorem}
 \newtheorem{lemma}{Lemma}
 \newtheorem{proposition}{Proposition}
 \newtheorem{corollary}{Corollary}
-\newtheorem{definition}{Definition}
 \theoremstyle{remark}
 \newtheorem{remark}{Remark}
 
-\newcommand{\authortodo}[1]{\textcolor{red}{\textbf{[AUTHOR TODO: #1]}}}
-\newcommand{\hash}{\mathsf{H}}
-\newcommand{\hleaf}{\mathsf{h}_{\mathsf{leaf}}}
-\newcommand{\hnode}{\mathsf{h}_{\mathsf{node}}}
+\newcommand{\Hh}{\mathsf{H}}
+\newcommand{\hleaf}{\mathsf{h}_{\rm leaf}}
+\newcommand{\hnode}{\mathsf{h}_{\rm node}}
 \newcommand{\MTH}{\mathsf{MTH}}
 \newcommand{\Root}{\mathsf{Root}}
-\newcommand{\ConsRec}{\mathsf{ConsRec}}
 \newcommand{\Path}{\mathsf{Path}}
-\newcommand{\obs}{\mathsf{obs}}
-\newcommand{\allowed}{\mathsf{allowed}}
-\newcommand{\clean}{\mathsf{clean}}
-\newcommand{\accept}{\mathsf{accept}}
+\newcommand{\ConsRec}{\mathsf{ConsRec}}
+\newcommand{\Obs}{\mathsf{Obs}}
+\newcommand{\Policy}{\mathsf{Policy}}
 \newcommand{\Fp}{\mathbb{F}_{2^{255}-19}}
+\newcommand{\code}[1]{\texttt{\detokenize{#1}}}
 
-\title{The Lean Transparency Log:\\ Distributing Kernel-Checked Correctness Evidence\\ for Deployed Ed25519 Implementations}
+\definecolor{deepblue}{RGB}{43,61,112}
+\definecolor{deepgreen}{RGB}{28,111,71}
+\definecolor{softgray}{RGB}{245,247,249}
+
+\lstset{basicstyle=\ttfamily\small,frame=single,rulecolor=\color{black!15},
+backgroundcolor=\color{softgray},columns=fullflexible,keepspaces=true,
+showstringspaces=false,breaklines=true,xleftmargin=.5em,xrightmargin=.5em}
+
+\title{\textbf{Accountable Distribution of Machine-Checked Correctness Evidence}\\[3pt]
+\large A Transparency Model and the Lean Transparency Log}
 \author{Olaf Horvath\\
-\small Olaf.Horvath@zkdefi.org \quad ORCID 0009-0004-8008-5805
-% \authortodo{if you have any institutional or personal-domain affiliation,
-% use it here instead of / alongside the zkdefi.org address}
-}
-\date{July 2026 (revised)}
+\small Olaf.Horvath@zkdefi.org \quad ORCID 0009-0004-8008-5805}
+\date{July 2026 \quad (v0.3)}
 
 \begin{document}
 \maketitle
 
 \begin{abstract}
-Interactive theorem provers can certify functional correctness of deployed
-cryptographic code, but the resulting assurance is expensive to consume:
-re-checking a realistic proof corpus requires a proof toolchain and hours of
-kernel time, which excludes almost every downstream user. We describe the
-Lean Transparency Log (LTL), an RFC~9162-style transparency log whose leaves
-are \emph{replay attestations}: signed statements that the Lean~4 proofs of a
-specific Rust repository, at a specific git commit, re-check with exactly
-their documented axiom sets. Consumers verify one signature and a logarithmic
-inclusion proof in milliseconds; the kernel time is paid once, by the log
-operator.
+Formal verification produces machine-checkable evidence, but consuming that
+evidence usually requires the original prover, dependency graph, source
+checkout, and substantial replay time. This paper studies a distinct
+cryptographic problem: how can a lightweight consumer obtain precise and
+accountable assurance about a deterministic proof replay without executing the
+verifier and without reducing the result to an opaque provider label?
 
-This paper makes the trust model precise and proves the consumer-facing
-security claims. We define the attestation-transparency setting, give an
-explicit adversary model in which the operator may be malicious, and prove:
-completeness and soundness of the inclusion verifier (soundness via an
-explicit reduction extracting a SHA-256 collision), the analogous consistency
-statement, safety of the consumer's head-pinning state machine (same-size
-equivocation yields transferable evidence, and local pinning rejects
-inconsistent extensions), and \emph{verdict
-integrity}---consumers re-derive verification verdicts locally from observed
-axiom cones, so the operator is trusted only for \emph{observations}, never
-for \emph{verdicts}. A further design choice ties the log to its own subject
-matter: tree heads are signed by a binary built from the very Ed25519
-implementation whose correctness certificates are leaves of the log. We
-report a small production deployment covering four verified production
-Ed25519 implementations, state exactly what the accumulated evidence does and
-does not establish, and outline the mechanization of this paper's theorems in
-Lean as the natural next step.
+We define \emph{accountable replay attestation}. A specialized operator performs
+an expensive replay once and publishes a structured observation through a
+signed append-only log. Consumers verify a signed tree head and logarithmic
+inclusion proof, pin history, and apply their own policy to the exact assumptions
+reported for each theorem. The construction does not prove that the operator's
+observation is true. It makes the claim immutable within a signed view,
+comparable across consumers, and attributable when incompatible views are
+presented.
+
+We instantiate the model as the Lean Transparency Log (LTL), using Lean~4 replay
+attestations and an RFC~9162 Merkle tree. We give explicit
+collision-extracting arguments for inclusion and consistency, formalize the
+consumer pinning and policy boundaries, and evaluate a live deployment over four
+production Ed25519 codebases. The public log contains thirteen leaves; its thirteenth
+leaf attests a Lean mechanization of the accumulator's own security arguments
+(222 inventoried environment constants, 61 human-reviewed assumption cones,
+and a single uninterpreted SHA-256 axiom). The mechanization also exposed a nontrivial implementation
+boundary: the deployed iterative consistency verifier is not extensionally
+equal to the stricter recursive model on malformed size claims. The leaf records
+this limitation explicitly. The resulting contribution is a cryptographic
+distribution model for machine-checked correctness evidence, together with an
+end-to-end deployed instantiation that carries scoped proofs about its own
+accountability machinery.
 \end{abstract}
 
 \section{Introduction}\label{sec:intro}
 
-Formal verification of deployed cryptographic code has matured from research
-prototypes to substantial artifacts: verified-by-construction libraries such
-as HACL*~\cite{hacl} and Fiat-Crypto~\cite{fiatcrypto} ship in mainstream
-software, and post-hoc verification pipelines such as Aeneas~\cite{aeneas}
-make it possible to state and prove theorems about existing production Rust
-code. The corpus underlying this paper is of the latter kind: four production
-Ed25519 implementations---upstream \texttt{curve25519-dalek}/%
-\texttt{ed25519-dalek} (one implementation: the curve crate and the
-signature crate atop it) and three deployed forks (Solana, RISC~Zero,
-Betrusted)---each carry Lean~4~\cite{lean4} certificates, proven against that
-fork's own extracted model, covering field arithmetic over $\Fp$, the
-complete twisted Edwards laws~\cite{edwards,twisted}, scalar arithmetic
-mod~$\ell$, encoding/decoding with constructive point decompression, and a
-four-tier characterization of signature verification~\cite{eddsa,rfc8032}
-whose strongest tier states: the extracted verifier accepts iff the
-signature's $R$ component decompresses to a valid curve point equal to
-$[k](-A) + [s]B$. Section~\ref{sec:corpus} states these theorems precisely.
+Formal verification has made it possible to connect production cryptographic
+software to machine-checked mathematics. Systems such as HACL*, EverCrypt,
+Fiat-Crypto, and Aeneas demonstrate different routes from implementation to
+proof~\cite{hacl,evercrypt,fiatcrypto,aeneas}. Yet the standard assurance story
+quietly assumes a capable consumer: one that can retrieve the exact source,
+reconstruct the verifier environment, resolve dependencies, and spend minutes
+or hours replaying a corpus.
 
-The economics of \emph{consuming} such evidence are poor: re-checking one
-fork's certificates takes ${\approx}30$ minutes of Lean kernel time and a
-pinned toolchain. A wallet, a package manager, or an autonomous agent
-choosing a cryptographic backend cannot pay this per decision---and need not:
-a deterministic re-check yields a fact that can be attested once and
-distributed. This is the classic transparency-log trade---Certificate
-Transparency~\cite{ct1,ct2} for certificate issuance, Sigstore's
-Rekor~\cite{sigstore} for signing events and supply-chain
-attestations~\cite{intoto}, key transparency~\cite{coniks}, checksum
-databases---applied to a payload with different trust semantics: evidence of
-machine-checked mathematical truth, together with its exact assumption set.
+That assumption is often false. A package resolver selecting a cryptographic
+backend, a deployment controller enforcing a proof requirement, or an
+autonomous custody agent may have milliseconds and a small trusted computing
+base, not a theorem prover and thirty minutes of kernel time per candidate.
+This creates a problem that is logically downstream of proof construction:
 
-\paragraph{Contributions.} The hash structure and proof algorithms are
-RFC~9162 verbatim, and we claim no novelty for any individual component. The
-contributions are:
-\begin{enumerate}[itemsep=1pt]
-\item \textbf{A precise trust model for attestation transparency over
-  machine-checked proofs} (\S\ref{sec:model}), in which the log operator is
-  trusted for \emph{observations} (``this is what the kernel printed'') but
-  never for \emph{verdicts} (``these proofs are acceptable''), because
-  consumers re-derive every verdict locally from the observed axiom cones
-  carried in each attestation.
-\item \textbf{Security proofs for the consumer-facing claims}
-  (\S\ref{sec:security}): completeness and soundness of the RFC~9162
-  inclusion verifier as used here (soundness as an explicit extractor that
-  turns any accepting proof for a non-member leaf into a SHA-256 collision),
-  the analogous consistency statement, safety of the consumer's pin-store
-  state machine, and verdict integrity. The statements are elementary but,
-  written out, they pin down exactly which assumption carries which claim.
-\item \textbf{Boundary-exact axiom auditing} (\S\ref{sec:construction}):
-  observed axiom cones are matched against per-theorem documented boundaries
-  \emph{exactly, in both directions}---an unexpected axiom and a missing
-  boundary axiom are both flagged.
-\item \textbf{A self-referential (not circular) signing design and a deployed
-  instance} (\S\ref{sec:selfref}, \S\ref{sec:deployment}): tree heads are
-  signed by a binary built from the pinned source of exactly the Ed25519
-  implementation attested in the log, with the operator's own Merkle
-  self-check of that leaf published alongside every signed head; and a small,
-  reproducible production deployment over the four-fork corpus, including a
-  measurement of proof portability across real forks.
+\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?}
+\end{quote}
+
+A detached signature on the word ``verified'' authenticates an issuer but does
+not bind an ordered history, expose silent replacement, or give consumers a
+compact state that can be pinned and required to grow. Shipping the complete
+proof and checker preserves direct verification but may defeat the cost and
+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.
+
+We therefore study a narrower primitive: \emph{accountable delegation of
+deterministic proof replay}. The operator still observes the replay. The
+cryptographic layer does not make that observation true. Instead, it makes the
+observation exact, persistent, attributable, and locally policy-checkable.
+Independent replay remains the mechanism for challenging a fabricated
+observation.
+
+\paragraph{Central thesis.}
+The contribution is not a new Merkle tree and not a new theorem prover. It is a
+trust decomposition for distributing machine-checked correctness evidence:
+
+\begin{center}
+\fbox{\parbox{0.91\linewidth}{
+\textbf{Expensive deterministic verification produces an observation.
+Transparency makes that observation accountable. Consumer-local policy decides
+whether the observation is acceptable.}}}
+\end{center}
+
+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
+claim survives replacement of Lean, Ed25519, or RFC~9162 by other components;
+what is essential is the distribution and accountability model.
+
+\paragraph{Contributions.}
+\begin{enumerate}[leftmargin=1.7em,itemsep=3pt]
+\item \textbf{A distribution model for machine-checked evidence.}
+We define replay attestations, distinguish observation from verdict, and state
+what a lightweight consumer learns without executing Lean.
+\item \textbf{A cryptographic accountability layer.}
+Using the RFC~9162 tree unchanged, we define signed views, inclusion receipts,
+local history pinning, and transferable same-size fork evidence. We give
+explicit collision-extracting soundness arguments specialized to the consumer
+algorithms.
+\item \textbf{Boundary-conformance policy.}
+Each leaf records the exact axiom names reported by Lean. Consumers compare
+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 twelve historical replay leaves for four verified Ed25519
+codebases and a thirteenth leaf for the accumulator's own Lean corpus. The
+entry-13 corpus carries an environment-derived audit inventory of 222 compiled
+constants, 61 human-reviewed certificate cones, and a single uninterpreted
+SHA-256 axiom.
+\item \textbf{A negative deployment result.}
+Differential testing found that the deployed iterative RFC-style consistency
+verifier accepts strictly more malformed size/root combinations than the
+recursive model proved in Lean. We characterize 3,867 one-sided divergences in
+73,573 boundary tests and scope the public attestation accordingly.
 \end{enumerate}
 
-\paragraph{Non-claims.} The LTL does not mechanize cryptographic security
-proofs---that bridge is being built by EasyCrypt and its
-relatives~\cite{easycrypt}. It does not establish correctness of any binary,
-of SHA-512, of wire-format parsers, of the signing path, or any side-channel
-property; \S\ref{sec:deployment} enumerates the assumption set in full. It
-bridges an adjacent, mostly empty gap: type-theory-certified artifacts
-lack distribution infrastructure, and we are unaware of a deployed
-transparency log designed to carry kernel-replay attestations together
-with theorem-level assumption boundaries.\footnote{The
-acronym LTL collides with linear temporal logic~\cite{pnueli}; the collision
-is acknowledged.}
+\paragraph{Non-claims.}
+LTL does not prove that the operator honestly reported a kernel run; independent
+replay remains the way to detect a fabricated observation. It does not prove
+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.
 
-\section{Background: the proof corpus}\label{sec:corpus}
+\section{The distribution problem}\label{sec:problem}
 
-The corpus is a stack of theorems about extracted code, each stated through
-a denotation from machine representation to mathematics. Field elements are
-five 51-bit limbs denoting
-$[\![(a_0,\dots,a_4)]\!] = \sum_i a_i 2^{51i} \bmod p$ with
-$p = 2^{255}-19$, and every operation carries a two-clause
-specification---the value is right \emph{and} the representation invariant
-is preserved, e.g.
-\[
-\forall a\, b.\;\; \mathsf{bnd}\,a \Rightarrow \mathsf{bnd}\,b \Rightarrow
-\exists c.\;\; \mathsf{mul}\,a\,b = \mathsf{ok}\,c \,\wedge\,
-\mathsf{bnd}\,c \,\wedge\, [\![c]\!] = [\![a]\!]\cdot[\![b]\!].
-\]
-Point operations are proven to implement the complete twisted Edwards
-addition law on $E : -x^2+y^2 = 1+d\,x^2y^2$ over $\Fp$,
-\[
-(x_1,y_1)+(x_2,y_2) \;=\;
-\left(\frac{x_1y_2+x_2y_1}{1+d\,x_1x_2y_1y_2},\;
-      \frac{y_1y_2+x_1x_2}{1-d\,x_1x_2y_1y_2}\right),
-\]
-including the completeness fact that makes it branch-free ($a=-1$ is a
-square and $d$ a non-square in $\Fp$, so the denominators never
-vanish~\cite{edwards}).
+\subsection{Three evidence modes}
 
-\paragraph{The signature apex as a lifting ladder.} The signature-tier
-result is not one theorem but a ladder of four, each lifting the previous
-one to a stronger domain; the payload the log distributes is the
-\emph{conjunction} of the four, and their separation is what makes the
-residual hypotheses legible. Write $\accept(A,m,R,s)$ for ``the extracted
-verifier returns \textsf{ok}'', let $k$ be the scalar produced by the hash
-oracle $H(R,A,m)$ with \emph{no properties assumed of $H$}, and let $r_1$
-be the 32-byte $R$ component exactly as it appears in the signature (raw
-bytes; no canonicity of them is presupposed). Each
-tier is proven for the extracted code under the wire-format
-hypotheses~$\mathcal{W}$ (the signature parses to an internal
-representation and the relevant compressed points re-encode; these
-outcomes are assumed, not proven---their byte-level specifications are
-part of the open frontier recorded in \S\ref{sec:limitations}).
-\begin{description}[itemsep=3pt,leftmargin=1.6em]
-\item[T1 (byte apex).] $\accept(A,m,R,s) \Leftrightarrow
-  \mathsf{compress}([s]B-[k]A) = r_1$. Acceptance is byte-equality of the
-  verifier's recomputed encoding with the signature's $R$ bytes---a
-  statement purely about the extracted control flow.
-\item[T2 (canonical half-lift).] The recomputed bytes
-  $\mathsf{compress}([s]B-[k]A)$ \emph{are} the canonical encoding of the
-  group element $[k](-A)+[s]B$; that is, $\mathsf{compress}$ agrees on this
-  input with the mathematical canonical-encoding function. T1 and T2 give
-  $\accept \Leftrightarrow \mathsf{enc}([k](-A)+[s]B) = r_1$.
-\item[T3 (injectivity / point equation).] Canonical encodings are
-  injective on $E(\Fp)$: if a valid curve point $P$ has $\mathsf{enc}(P) =
-  r_1$ then $P = [k](-A)+[s]B$. Injectivity is exactly where
-  non-squareness of $d$ re-enters---it keeps $1 + d y^2 \neq 0$, so the
-  curve equation determines $x^2$ from $y$ and the encoding is one-to-one.
-\item[T4 (constructive full lift).] $\accept(A,m,R,s) \Leftrightarrow
-  \mathsf{decompress}(R) = [k](-A)+[s]B$, with the extracted
-  $\mathsf{decompress}$ proven to realize the mathematical inverse of
-  $\mathsf{enc}$: exact byte parsing, the $(p+3)/8$-power square root, and
-  sign-bit root selection (for $x \neq 0$ the two roots $x$ and $p-x$
-  differ in parity since $p$ is odd, so the stored sign bit selects
-  correctly; at $x = 0$ the roots coincide and a set sign bit is rejected,
-  per RFC~8032---the theorem, an \emph{iff} over the extracted code,
-  covers this branch by construction).
+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$. 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
+checks $O_g$ itself. This gives the strongest provenance, but has high
+operational cost.
+\item[Detached attestation.] A provider signs $O_g$. This is cheap to consume,
+but provides no append-only history and no common value for clients to pin.
+\item[Transparent attestation.] The provider signs a tree head committing
+$O_g$ as one leaf among an ordered history. A consumer verifies inclusion and
+persists a head. Incompatible views become attributable when compared.
 \end{description}
-The lift is monotone in strength---T1 is about bytes the code emits, T4 is
-about the group element a third party would recover from $R$---and each
-step names precisely one new mathematical fact (canonicity, injectivity,
-constructive inversion). A consumer that only trusts byte equality can
-stop at T1; a consumer reasoning about the underlying group element relies
-on T4. Both are in the corpus, separately certified, and the log carries
-all four so the consumer chooses the tier, not the operator.
 
-\paragraph{Axiom cones.} Each theorem's \emph{axiom cone}---the set of
-axioms its proof ultimately depends on, as reported by Lean's
-\texttt{\#print axioms}---is pinned exactly: the standard three axioms for
-the foundational certificates, plus an enumerated oracle boundary
-(SHA-512 and the wire-format types) at the four apex tiers. It is this
-exact set, not a pass/fail label, that each leaf carries and each consumer
-re-checks (\S\ref{sec:auditing}). Appendix~\ref{app:tiers} restates the
-ladder with the Lean theorem names; Appendix~\ref{app:axioms} lists the
-per-fork allowed sets verbatim.
+The third mode is useful precisely when replay is expensive but the result is
+stable and deterministic. It does not dominate direct replay: it replaces
+local computation with a narrower trust in the replay provider.
 
-\section{Related work}\label{sec:related}
+\subsection{Why transparency rather than a signature database?}
 
-Certificate Transparency~\cite{ct1,ct2} supplies the data structure and
-proof algorithms, used here unchanged; the underlying history-tree technique
-originates with Crosby and Wallach~\cite{crosby}. Dowling, G\"unther, Herath
-and Stebila~\cite{dghs} give formal security definitions and proofs for the
-CT primitives (logging schemes, inclusion, consistency); the analysis in
-\S\ref{sec:security} is in the same spirit, specialized to this system's
-verifier and stated so that each claim can later be mechanized in Lean
-(\S\ref{sec:next}). Rekor within Sigstore~\cite{sigstore} is the closest
-deployed system: a transparency log over signing events and supply-chain
-attestations such as in-toto~\cite{intoto} link metadata; its payloads attest
-\emph{process} (who signed, how an artifact was built), whereas LTL leaves
-attest kernel-checked mathematical statements together with their assumption
-sets, and the consumer re-derives verdicts rather than trusting labels. Key
-transparency~\cite{coniks} and checksum databases share the pattern with
-different payloads. Proof-carrying code~\cite{pcc} ships proofs to consumers
-who check them; the LTL serves consumers who cannot run any checker,
-replacing proof transport with attestation, inclusion, and signature---at
-the cost of trusting the operator's kernel run, a cost the design minimizes
-(\S\ref{sec:model}) but does not eliminate. Cheval, Moreira and Ryan
-formally verify transparency protocols themselves~\cite{cheval}; our
-direction is the complement (we log the verification), and \S\ref{sec:next}
-proposes meeting in the middle. Verified Merkle tree implementations exist,
-notably in EverCrypt~\cite{evercrypt}; \S\ref{sec:next} builds on that
-precedent rather than claiming it.
+Suppose an operator signs every replay result independently. Authenticity of
+an individual record follows from signature verification, but four properties
+are absent:
+\begin{enumerate}[leftmargin=1.7em,itemsep=2pt]
+\item no signed value commits to the ordered set of all records;
+\item deletion or replacement of an old result leaves no cryptographic trace;
+\item two consumers cannot compare a single compact view identifier;
+\item a consumer cannot demand that its previously accepted history only grow.
+\end{enumerate}
+An append-only Merkle tree supplies these missing interfaces. At the current
+deployment size, logarithmic proof size is not the decisive benefit;
+\emph{history binding} is.
 
-\section{System and trust model}\label{sec:model}
+\subsection{Design alternatives}
 
-\subsection{Roles and scheme syntax}
+\begin{table}[t]
+\centering\small
+\begin{tabularx}{\textwidth}{@{}lXXXX@{}}
+\toprule
+Mechanism & Consumer cost & Semantic checker & History accountability & Main residual cost \\
+\midrule
+Local replay & high & consumer & local only & prover/toolchain deployment \\
+Proof transport / PCC & medium--high & consumer checker & optional & proof/checker portability \\
+Detached signed result & low & provider & none & replaceable history \\
+Committee replay & low & committee & threshold-dependent & membership trust \\
+Succinct proof of replay & low & circuit/VM verifier & optional & proving the prover \\
+LTL & low & provider observes; consumer applies policy & signed append-only views & observation honesty \\
+\bottomrule
+\end{tabularx}
+\caption{Evidence-distribution alternatives. LTL targets low-cost consumers
+while retaining an attributable history; it does not remove trust in the
+replay observation.}
+\label{tab:alternatives}
+\end{table}
 
-The system has exactly two roles with deliberately asymmetric costs and
-capabilities. The \emph{operator} (one per log) owns a Lean toolchain,
-replays proof corpora, holds the log's signing key, and bears append-only
-obligations. \emph{Consumers} (unbounded in number) hold the operator's
-public key, receive small evidence files, and verify: the Merkle
-inclusion core is roughly 25 lines of standard-library code
-(Appendix~\ref{app:verifier}); the full standalone consumer---head
-signature, consistency, mirror audit---is ${\approx}150$ lines
-(\S\ref{sec:pinstore}), atop an Ed25519 backend. Nothing a consumer
-does requires a theorem prover.
+\section{Model and trust decomposition}\label{sec:model}
 
-We phrase the system as an \emph{attestation-transparency scheme}, in the
-style of the logging schemes of Dowling et al.~\cite{dghs}, so that the
-security goals below can name its algorithms precisely.
+\subsection{Roles and objects}
 
-\begin{definition}[Attestation-transparency scheme]\label{def:scheme}
-A scheme $\Pi$ is a tuple of algorithms over a hash function $\hash$ and a
-signature scheme $\mathsf{Sig}$:
-\begin{itemize}[itemsep=1pt,leftmargin=1.4em]
-\item $\mathsf{KeyGen} \to (sk, pk)$: the operator's head-signing keypair.
-\item $\mathsf{Append}(sk, \mathbf{D}, a) \to (\mathbf{D}', \sigma)$:
-  appends attestation-leaf $a$ to the ordered leaf list $\mathbf{D}$,
-  returning the new list and a signed tree head
-  $\sigma = \mathsf{Sig}.\mathsf{Sign}(sk, (|\mathbf{D}'|, \MTH(\mathbf{D}'), t))$.
-\item $\mathsf{ProveIncl}(\mathbf{D}, m) \to P$ and
-  $\mathsf{VerifyIncl}(pk, d, m, \sigma, P) \to \{0,1\}$: the membership
-  proof and its verifier (\S\ref{sec:tree}, Appendix~\ref{app:verifier}).
-\item $\mathsf{ProveCons}(\mathbf{D}, n_0) \to C$ and
-  $\mathsf{VerifyCons}(pk, \sigma_0, \sigma_1, C) \to \{0,1\}$: the
-  append-only (consistency) proof between two signed heads and its verifier
-  (\S\ref{sec:tree}).
-\item $\mathsf{Verdict}(\allowed, a) \to \{\clean, \neg\clean,
-  \bot\}^{|a|}$: the consumer's per-certificate verdict function
-  (\S\ref{sec:auditing}), parameterized by the consumer's \emph{own}
-  allowed-axiom table $\allowed$ and taking \emph{no} operator label as
-  input.
-\end{itemize}
-$\MTH$, $\mathsf{ProveIncl/VerifyIncl}$ and $\mathsf{ProveCons/VerifyCons}$
-are the RFC~9162 algorithms, defined in \S\ref{sec:tree}; $\mathsf{Append}$
-and $\mathsf{Verdict}$ are specific to this system.
+The system has three logical roles.
+\begin{description}[leftmargin=1.5em,itemsep=4pt]
+\item[Subject maintainer.] Publishes source and proof artifacts at a commit.
+\item[Replay operator.] Executes the declared verifier procedure, constructs
+an attestation, appends it to the log, and signs tree heads.
+\item[Consumer.] Holds the log public key and a local policy; verifies receipts
+and optionally persists a previous head.
+\end{description}
+
+A replay attestation $a$ contains at least
+\[
+(\textsf{repo},g,\textsf{toolchain},\textsf{environment},
+  [(N_i,s_i,A_i)]_{i=1}^{q}),
+\]
+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.
+
+\begin{definition}[Attestation-transparency scheme]
+An attestation-transparency scheme is a tuple
+\[
+\Pi=(\mathsf{KeyGen},\mathsf{Append},\mathsf{ProveIncl},
+\mathsf{VerifyIncl},\mathsf{ProveCons},\mathsf{VerifyCons},\mathsf{Verdict})
+\]
+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.
 \end{definition}
 
+\begin{definition}[Accountable replay distribution]
+Fix an operator public key and a consumer that persists accepted signed heads.
+A replay-distribution scheme is \emph{accountable} if the following hold:
+(i) every accepted attestation is position-bound to a signed view; (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 form transferable evidence
+that the key holder signed incompatible views; and (iv) positive acceptance of
+a theorem boundary is a function of recorded observations and consumer-local
+policy, not of an operator verdict.
+\end{definition}
+
+The definition is intentionally an accountability property, not a validity
+property. It says when conflicting claims become attributable; it does not
+cryptographically prove that the replay observation was honestly produced.
+
+\begin{figure}[t]
+\centering
+\begin{tikzpicture}[
+  node distance=8mm and 8mm,
+  b/.style={draw,rounded corners=2pt,align=center,minimum height=10mm,minimum width=29mm,font=\small},
+  a/.style={-{Latex[length=2mm]},thick,draw=black!60}
+]
+\node[b,fill=blue!6] (subject) {subject source\\and proof corpus};
+\node[b,fill=green!7,right=of subject] (replay) {expensive\\deterministic replay};
+\node[b,fill=yellow!10,right=of replay] (att) {structured replay\\observation};
+\node[b,fill=blue!6,right=of att] (log) {signed append-only\\view};
+\node[b,fill=green!7,below=12mm of log] (consumer) {lightweight consumer\\signature + hashes + policy};
+\draw[a] (subject)--(replay);
+\draw[a] (replay)--(att);
+\draw[a] (att)--(log);
+\draw[a] (log)--(consumer);
+\draw[a,dashed] (consumer.west) -| node[pos=.25,below,font=\scriptsize]{targeted independent replay} (replay.south);
+\end{tikzpicture}
+\caption{Trust decomposition. The log authenticates and orders the replay
+operator's observation; it does not replace the theorem prover or make the
+observation true.}
+\label{fig:decomposition}
+\end{figure}
+
+\subsection{What is and is not transferred}
+
+A verified receipt establishes a statement of the form:
+\begin{quote}
+The holder of public key $pk$ signed a tree head committing, at position $m$,
+to a leaf in which the operator reports that the named declarations at commit
+$g$ replayed with the recorded axiom-name sets.
+\end{quote}
+It does not establish that the operator's report is true. Nor does it identify
+the semantics of a theorem from its name alone. This separation is central:
+
+\begin{center}\small
+\begin{tabular}{@{}ll@{}}
+\toprule
+Layer & What it contributes \\
+\midrule
+Lean kernel & validity of a checked term relative to declarations and axioms \\
+Replay pipeline & binding of source, toolchain, theorem names, and observations \\
+Attestation signature & attribution of one replay statement \\
+Merkle log & position binding and append-only view commitments \\
+Consumer policy & acceptability of the recorded boundary \\
+Independent replay & detection of fabricated operator observations \\
+\bottomrule
+\end{tabular}
+\end{center}
+
 \subsection{Adversary model}
 
-We consider a probabilistic polynomial-time adversary $\mathcal{A}$ that
-controls the network (may reorder, replay, drop, or forge messages to
-consumers) and may \emph{be} the operator. A malicious operator may sign
-arbitrary tree heads, construct arbitrary leaves, present different views to
-different consumers, and label attestations arbitrarily. The single
-capability we do \emph{not} model cryptographically is falsification of
-kernel observations: an operator who reports an axiom cone that the Lean
-kernel never printed is lying about a physical event on its own machine, and
-no log structure can exclude this; \S\ref{sec:model:residual} isolates this
-residual trust precisely. Standard assumptions: SHA-256 is collision
-resistant; Ed25519 (as instantiated by the signing binary) is EUF-CMA
-secure; the consumer obtained the operator's true public key (trust on first
-use; \S\ref{sec:limitations}).
+The network adversary may replay, delay, suppress, or substitute messages. The
+operator may be malicious: it may construct arbitrary leaves, sign arbitrary
+heads, label results arbitrarily, and present different signed views to
+different consumers. We assume collision resistance of SHA-256 for the log,
+EUF-CMA security of the head-signature scheme, and correct initial acquisition
+of the operator public key.
 
-\subsection{Security goals}\label{sec:model:goals}
+The model deliberately does not cryptographically exclude fabricated kernel
+observations. That is a statement 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.
 
-These goals are what per-item signatures alone cannot supply: a set of
-individually signed attestations cannot evidence a silent deletion
-(nothing commits to completeness), cannot expose two-faced service
-(independently valid views are incomparable), and offers no single value
-a consumer can pin and demand extensions of. The Merkle tree is chosen
-for these dishonesty-evidence properties, not for proof-size scaling,
-which at this deployment's size is immaterial.
+\subsection{Consumer goals}
 
-\begin{description}[itemsep=2pt]
-\item[G1 (Membership).] If a consumer accepts a receipt for attestation $a$
-  against a signed head, then $a$ is a leaf of the tree committed by that
-  head---any other outcome exhibits a SHA-256 collision or an Ed25519
-  forgery. (Theorem~\ref{thm:sound}, Proposition~\ref{prop:pin}.)
-\item[G2 (Append-only with fork evidence).] A consumer's accepted view of
-  the log only ever grows by extension, and two accepted heads of
-  \emph{equal} tree size with different roots are, together, transferable
-  publicly verifiable evidence of equivocation. Unequal-size split views
-  are not exposed by the head pair alone; they are exposed by the public
-  leaf mirror (\S\ref{sec:pinstore}), from which any party recomputes
-  every prefix root (itself operator-published, hence witness-dependent;
-  \S\ref{sec:limitations}), or by an external witness.
-  (Theorem~\ref{thm:consistency}, Proposition~\ref{prop:pin}.)
-\item[G3 (Verdict integrity).] The verdict a consumer derives for a
-  certificate depends only on the observed axiom cone in the leaf and the
-  consumer's \emph{own} copy of the allowed axiom sets; the operator's
-  pass/fail labels can deny (a certificate the operator does not itself
-  mark proven never counts) but can never grant.
-  (Proposition~\ref{prop:verdict}.)
+\begin{description}[leftmargin=1.5em,itemsep=5pt]
+\item[G1: Position-bound membership.] If a consumer accepts leaf $d$ at index
+$m$ against signed head $(n,r)$, then $d$ occupies position $m$ in a leaf list
+committed by $r$, except under hash collision or signature forgery.
+\item[G2: Local append-only history.] A consumer that persists $(n,r)$ accepts
+a later view only if it is the same view or a verified extension. Two valid
+heads of equal size and unequal roots are transferable evidence that the key
+holder signed incompatible views. Unequal-size forks require retained
+history, gossip, or a witness.
+\item[G3: Policy separation.] The operator's positive label cannot make a
+certificate acceptable. The consumer recomputes boundary conformance from
+observations and local policy. Operator failure labels may be treated as a
+conservative veto.
 \end{description}
 
-\subsection{The residual trust, isolated}\label{sec:model:residual}
+\subsection{Boundary conformance, not semantic identity}
 
-Goals G1--G3 reduce the operator's trusted role to a single sentence,
-which we state at its honest width: \emph{``the operator executed the
-declared replay procedure against the exact pinned source and dependency
-state, using the declared toolchain, and bound the resulting kernel
-outputs faithfully to the correct theorem entries of the attestation.''}
-Checkout, dependency state, theorem-to-entry binding, and output parsing
-are all inside this observation pipeline---the first deployed run failed
-on precisely such a defect (\S\ref{sec:deployment}). Everything
-else---membership, history, verdicts---is either cryptographically
-enforced or locally re-derived. An
-operator that labels a dirty cone ``clean'' gains nothing (G3); an
-attestation that omits observed cones is treated as unverifiable; an
-operator that rewrites history is caught with transferable evidence (G2).
-An operator that fabricates observations can only be caught by independent
-replay, which any party with a Lean toolchain can perform from the pinned
-commit---the design makes such an audit cheap to \emph{target} (the claim
-is exact: repository, commit, toolchain, expected cones) even though it is
-expensive to \emph{run}.
+For certificate $c$, let $\Obs_a(c)$ be the axiom-name set recorded in leaf
+$a$, and let $\Policy(c)$ be the consumer's allowed set. Define
+\[
+\mathsf{boundary\_ok}_a(c) \iff \Obs_a(c)=\Policy(c).
+\]
+Exact equality detects both additional assumptions and drift in the declared
+assurance interface. A missing expected axiom is not automatically a logical
+defect: it may indicate a strengthened theorem, a changed statement, a bypassed
+abstraction boundary, or stale policy. The consumer therefore rejects or
+requires review rather than interpreting the drift.
 
-\subsection{Verdicts are the consumer's, not the operator's}\label{sec:model:card}
+This predicate is intentionally narrower than ``the intended theorem was
+proved.'' The deployed system identifies a declaration by repository commit
+and name. A stronger future schema should include canonical digests of the
+elaborated theorem type and of the types of declarations in its axiom cone.
 
-The design choice behind G3 is what most distinguishes this system from
-prior attestation transparency, so we state it as a principle rather than
-a mechanism. In systems like Rekor~\cite{sigstore} a consumer learns
-\emph{that} something was attested and trusts the issuer's assessment of
-it; the payload's meaning is the issuer's to declare. Here the payload is
-a set of \emph{observations}---the literal \texttt{\#print axioms} output
-per theorem---and the assessment ($\clean$ or not) is computed by
-$\mathsf{Verdict}$ (Definition~\ref{def:scheme}) from those observations
-against the consumer's own table $\allowed$. Concretely:
-\begin{itemize}[itemsep=1pt,leftmargin=1.4em]
-\item The allowed set $\allowed(c)$ is not shipped by the operator at
-  verification time; it is part of the consumer's tooling, small enough to
-  audit by hand (Appendix~\ref{app:axioms}: 7--11 axiom names per fork),
-  and re-derivable \emph{up to naming} from the theorem statements---%
-  Lean's foundational three, plus, for the apex tiers, placeholders for
-  exactly those primitives the theorem deliberately leaves opaque (the
-  hash, the wire format); the placeholder \emph{names} themselves are
-  fixed by the fork's extracted surface and read off from
-  Appendix~\ref{app:axioms}.
-\item That an independently written $\allowed$ meets the deployed
-  observations \emph{exactly} is engineered, not coincidental: the corpus
-  is minimized so that every axiom in a cone earns its place, and any
-  reasonable reconstruction of ``what a correct proof of this statement
-  must assume,'' once the fork's extraction naming is fixed, lands on the
-  same finite set. When the consumer's requirement meets the supply
-  exactly, verification is a set equality.
-\item When it does not---a consumer who additionally requires SHA-512
-  itself proven, say---the gap is exact and itemized (the boundary axioms
-  of Appendix~\ref{app:axioms}), and the consumer's options are honest:
-  accept a \emph{named} residual, decline, or discharge the missing
-  boundary and let the resulting certificate enter the log. The log is
-  additive in the same way requirements are; a stricter table is a roadmap,
-  not a rejection.
+\section{Construction}\label{sec:construction}
+
+\subsection{RFC 9162 tree}
+
+Let $\Hh$ be SHA-256. For byte string $d$ and 32-byte values $x,y$ define
+\[
+\hleaf(d)=\Hh(\mathtt{0x00}\parallel d),\qquad
+\hnode(x,y)=\Hh(\mathtt{0x01}\parallel x\parallel y).
+\]
+For leaf list $D=[d_0,\ldots,d_{n-1}]$:
+\[
+\MTH([])=\Hh(\epsilon),\qquad \MTH([d])=\hleaf(d),
+\]
+and for $n>1$,
+\[
+\MTH(D)=\hnode(\MTH(D[0{:}k]),\MTH(D[k{:}n])),
+\]
+where $k$ is the largest power of two strictly smaller than $n$. Inclusion and
+consistency proofs are the RFC~9162 algorithms~\cite{ct2}.
+
+\subsection{Signed tree heads}
+
+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.
+
+The current implementation records signing-backend provenance alongside the
+signature, but that provenance is not execution attestation: an Ed25519
+signature does not identify the program that produced it. The public system
+therefore treats the claimed signing implementation as operator-reported
+context, not as a property proved by the signature.
+
+\subsection{Receipts and pinning}
+
+A receipt contains the leaf index, sibling path, and signed head. A consumer
+first verifies the head signature and then reconstructs the root. For history,
+a local pin $(n_{\rm pin},r_{\rm pin})$ evolves as follows:
+\begin{itemize}[leftmargin=1.6em,itemsep=2pt]
+\item same size: accept iff roots match; otherwise retain both signed heads as
+same-size fork evidence;
+\item larger size: accept iff a consistency proof verifies, then update;
+\item smaller size: reject as rollback.
 \end{itemize}
-The operator, in this picture, is not a judge whose verdict one trusts but
-a witness whose \emph{observations} one re-adjudicates. G3
-(\S\ref{sec:model:goals}, Proposition~\ref{prop:verdict}) is the formal
-statement that this re-adjudication takes no positive input from the
-operator's opinion: labels act, if at all, only as a conservative veto.
-
-\section{The log construction}\label{sec:construction}
-
-\subsection{Leaves: replay attestations}\label{sec:leaves}
-
-A leaf is the canonical JSON serialization of an attestation recording: the
-subject repository URL and git commit (which pins the entire source
-tree through git's object identifiers---hardened SHA-1, noted here
-because it is a weaker primitive than the log's own SHA-256); the
-toolchain versions; the resource-control regime
-under which the replay ran; and, per certificate, its name, replay status,
-and the \emph{observed axiom cone}---the exact output of Lean's
-\texttt{\#print axioms} for that theorem. For the corpus of
-\S\ref{sec:corpus} each attestation carries 16 certificates.
-Appendix~\ref{app:leaf} gives the leaf schema.
-
-\subsection{Boundary-exact auditing}\label{sec:auditing}
-
-Every certificate $c$ has a documented allowed axiom set $\allowed(c)$.
-Foundational certificates must carry exactly Lean's three standard axioms
-(\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}); the four
-signature-tier certificates additionally carry a per-fork, explicitly
-enumerated boundary (an opaque SHA-512 oracle and opaque wire-format
-types---e.g., eleven axioms in total for the upstream fork). Writing
-$\obs(c)$ for the observed cone recorded in the leaf, define
-\[
-\clean(c) \;:\Longleftrightarrow\; \obs(c) = \allowed(c)
-\quad\text{(equality of finite sets).}
-\]
-Deviation in \emph{either} direction---an unexpected axiom, or a missing
-boundary axiom---falsifies $\clean$. The second direction matters for
-these \emph{oracle} boundaries: a missing boundary axiom signals that the
-theorem no longer consumes a primitive it deliberately left opaque. The
-verifier does not attempt to distinguish the readings of that drift (a
-genuinely strengthened proof; a changed theorem; a hash oracle discharged
-by a placeholder rather than kept opaque; stale policy): it refuses to
-classify, and rejects. Each
-source repository enforces the same discipline in its own check scripts; the
-log mirrors those sets, and consumers carry their own copies.
-
-\subsection{Tree, heads, receipts}\label{sec:tree}
-
-Let $\hash$ be SHA-256. Define, for a byte string $d$ and 256-bit values
-$x,y$:
-\[
-\hleaf(d) = \hash(\texttt{0x00} \,\|\, d), \qquad
-\hnode(x,y) = \hash(\texttt{0x01} \,\|\, x \,\|\, y).
-\]
-For a leaf list $D = [d_0,\dots,d_{n-1}]$ the RFC~9162 tree head is
-\[
-\begin{aligned}
-\MTH([\,]) &= \hash(\varepsilon), \qquad
-\MTH([d]) = \hleaf(d),\\
-\MTH(D) &= \hnode\bigl(\MTH(D[0{:}k]),\, \MTH(D[k{:}n])\bigr),
-\end{aligned}
-\]
-where $k$ is the largest power of two strictly less than $n$. The
-\emph{inclusion path} for index $m$ is
-\[
-\Path(m, [d]) = [\,], \qquad
-\Path(m, D) =
-\begin{cases}
-\Path(m, D[0{:}k]) \,\|\, [\MTH(D[k{:}n])] & m < k,\\
-\Path(m-k, D[k{:}n]) \,\|\, [\MTH(D[0{:}k])] & m \ge k,
-\end{cases}
-\]
-and the consumer's root-reconstruction function $\Root(v, m, n, P)$ is the
-evident dual (Appendix~\ref{app:verifier}): fold the path back up, choosing
-left/right by comparing $m$ with $k$ at each level.
-
-\paragraph{Consistency.} A consistency proof $C$ lets a consumer check
-that a size-$n_1$ tree \emph{extends} a size-$n_0$ tree it already pinned,
-$0 < n_0 \le n_1$. We give the verifier as a function $\ConsRec$ that
-reconstructs \emph{both} committed roots from $C$; it is the recursive
-counterpart of RFC~9162~\S2.1.4, and we use this form (rather than the
-RFC's iterative one) because the proofs of \S\ref{sec:security} induct on
-it. On a proof $C$ interpreted as a list of nodes, with a flag $b$
-recording whether the size-$n_0$ subtree's root is carried implicitly (the
-pinned root) or explicitly in $C$:
-\[
-\ConsRec(n_0, n, C, b, r) =
-\begin{cases}
-(r, r) & n_0 = n,\ b,\ C = [\,],\\
-(s, s) & n_0 = n,\ \neg b,\ C = [s],\\
-\bigl(x,\, \hnode(y, s)\bigr) & n_0 \le k,\ C = C' \| [s],\\
-\bigl(\hnode(s, x'),\, \hnode(s, y')\bigr) & n_0 > k,\ C = C' \| [s],
-\end{cases}
-\]
-where $k$ is the largest power of two below $n$, $(x,y) =
-\ConsRec(n_0, k, C', b, r)$ in the third case, and $(x',y') =
-\ConsRec(n_0 - k, n - k, C', \bot, r)$ in the fourth (any shape mismatch
-rejects). The consumer accepts $C$ between signed heads $(n_0, r_0)$ and
-$(n_1, r_1)$ iff $n_0 = 0$, or $\ConsRec(n_0, n_1, C, \top, r_0) =
-(r_0, r_1)$. We verified that this recursive form agrees with the deployed
-iterative RFC~9162 verifier by \emph{exhaustive} differential testing over
-every pinned/current size pair $1 \le n_0 \le n_1 \le 256$, each with the
-honest proof and four adversarial mutations (wrong old root, wrong new
-root, truncated and padded proofs): $164{,}224$ verifier invocations,
-full agreement. The inclusion verifier of Appendix~\ref{app:verifier} was
-checked the same way ($164{,}479$ invocations over all $m < n \le 256$).
-
-The operator signs tree heads $(n, \MTH(D), t)$ with Ed25519; a
-\emph{receipt} for a leaf is its index, its sibling path, and a signed
-head. The signed payload is not the bare triple but the canonical JSON
-serialization (sorted keys, fixed separators, UTF-8---injective on the
-field set) of the head record, which additionally carries a protocol
-version tag (\texttt{pacta.transparency.signed\_tree\_head.v1}) and the
-log identity;
-a head signature therefore transfers neither across logs nor across
-protocol versions.
-
-\subsection{The consumer pin store}\label{sec:pinstore}
-
-Each consumer maintains a local pin $(n_{\mathrm{pin}}, r_{\mathrm{pin}})$,
-updated by the following state machine on receiving a validly signed head
-$(n', r')$:
-\begin{itemize}[itemsep=1pt]
-\item $n' = n_{\mathrm{pin}}$: accept iff $r' = r_{\mathrm{pin}}$; a
-  mismatch is reported as \emph{equivocation}, the pair of signed heads is
-  retained as evidence, and the state is poisoned (unrecoverable).
-\item $n' > n_{\mathrm{pin}}$: accept iff a consistency proof from
-  $(n_{\mathrm{pin}}, r_{\mathrm{pin}})$ to $(n', r')$ verifies; then update
-  the pin.
-\item $n' < n_{\mathrm{pin}}$: reject (rollback).
-\end{itemize}
-A freshness policy bounds head age; freshness, however, is an
-availability policy, not an append-only property---the construction
-detects rollback relative to a persisted pin, but does not prove that a
-consumer sees the newest issued head (an operator can re-issue fresh
-timestamps over a frozen tree). The full log is also published as a git
-repository: one file per leaf, plus the signed head history since
-publication began (heads signed before the mirror existed were not
-retained). Any cloner can therefore recompute every prefix root from the
-public leaves and check every published head against its prefix root and
-signature without consistency proofs---a low-infrastructure witness
-mechanism~\cite{ct2}; a standalone ${\approx}150$-line standard-library
-verifier ships in the mirror.
+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.
 
 \section{Security analysis}\label{sec:security}
 
-This section proves the claims G1--G3 of \S\ref{sec:model:goals}. The
-statements are not deep---inclusion and consistency security for RFC
-6962/9162 trees is folklore, and was treated formally by Dowling et
-al.~\cite{dghs}---but writing them out for \emph{this} system serves two
-purposes: it pins down exactly which assumption carries which consumer-facing
-claim, and it produces statements in a form ready for mechanization in Lean
-(\S\ref{sec:next}), where they will re-enter the log as leaves.
+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.
 
-We write $\Root(v, m, n, P)$ for the consumer's root reconstruction: it is
-defined by $\Root(v, m, 1, [\,]) = v$ and, for $n > 1$ with $k$ the largest
-power of two below $n$ and $P = P' \| [s]$,
-\[
-\Root(v, m, n, P) =
-\begin{cases}
-\hnode\bigl(\Root(v, m, k, P'),\, s\bigr) & m < k,\\
-\hnode\bigl(s,\, \Root(v, m-k, n-k, P')\bigr) & m \ge k,
-\end{cases}
-\]
-rejecting on any length mismatch. The consumer accepts a receipt
-$(d, m, P)$ against a head $(n, r)$ iff $m < n$ and
-$\Root(\hleaf(d), m, n, P) = r$.
+\subsection{Inclusion}
 
-\begin{lemma}[Domain separation]\label{lem:domsep}
-No leaf preimage equals a node preimage as a byte string: for all $d, x, y$,
-$\texttt{0x00} \| d \neq \texttt{0x01} \| x \| y$.
+Let $\Root(v,m,n,P)$ recursively fold value $v$ at position $m$ through proof
+path $P$ using the same largest-power-of-two decomposition as $\MTH$.
+
+\begin{lemma}[Domain separation]
+For all byte strings $d$ and 32-byte values $x,y$,
+$\mathtt{0x00}\parallel d \neq \mathtt{0x01}\parallel x\parallel y$.
 \end{lemma}
 \begin{proof}
 The first byte differs.
 \end{proof}
 
-Lemma~\ref{lem:domsep} forecloses the classic cross-type confusion in which
-an adversary presents an interior node's 64-byte child concatenation as a
-``leaf'' (or vice versa) to move a value between levels of the
-tree~\cite{crosby,dghs}; it guarantees that whenever a leaf preimage and
-a node preimage are compared, they already differ as strings, so equal
-hash values across the two types constitute a collision.
-
-\begin{theorem}[Inclusion completeness]\label{thm:complete}
-For every non-empty leaf list $D$ with $|D| = n$ and every $m < n$,
+\begin{theorem}[Inclusion completeness]
+For every non-empty $D$, every $m<|D|$,
 \[
-\Root\bigl(\hleaf(D[m]),\, m,\, n,\, \Path(m, D)\bigr) = \MTH(D).
+\Root(\hleaf(D[m]),m,|D|,\Path(m,D))=\MTH(D).
 \]
 \end{theorem}
 \begin{proof}
-Structural induction on $n$. For $n = 1$: $\Path(0, [d]) = [\,]$ and
-$\Root(\hleaf(d), 0, 1, [\,]) = \hleaf(d) = \MTH([d])$. For $n > 1$ with
-split point $k$, suppose $m < k$ (the case $m \ge k$ is symmetric). Then
-$\Path(m, D) = \Path(m, D[0{:}k]) \,\|\, [\MTH(D[k{:}n])]$, and by the
-induction hypothesis
+By structural induction on $|D|$. The singleton case is immediate. For a split
+$D=L\|R$, the honest path is the recursive path inside the side containing $m$
+followed by the other side's root. The induction hypothesis reconstructs the
+selected child root, and the final node hash reconstructs $\MTH(D)$.
+\end{proof}
+
+\begin{theorem}[Inclusion soundness: position binding]
+There is an explicit extractor $\mathcal{E}_{\rm incl}$ such that, given $D$,
+$m<|D|$, $d\neq D[m]$, and a path $P$ satisfying
 \[
-\Root\bigl(\hleaf(D[m]),\, m,\, k,\, \Path(m, D[0{:}k])\bigr)
-  = \MTH(D[0{:}k]),
+\Root(\hleaf(d),m,|D|,P)=\MTH(D),
 \]
-so the outer step yields
-$\hnode(\MTH(D[0{:}k]), \MTH(D[k{:}n])) = \MTH(D)$.
-\end{proof}
-
-Both soundness theorems below rest on a single collision-extraction fact,
-which we isolate first. Fix the honest Merkle tree $T$ of a leaf list $D$.
-A \emph{hash-fold over $T$} is a computation shaped by a connected
-sub-tree $S$ of $T$ containing $T$'s root: at every internal node of $T$
-lying in $S$ it emits $\hnode$ of its two children's values; each child
-lying outside $S$ is an \emph{input}, consumed as an opaque value; at
-every leaf of $T$ lying in $S$ it emits $\hleaf$ of an input leaf value.
-All inputs may be adversarial; only the shape is $T$'s. Three
-instantiations recur below: the inclusion reconstruction
-$\Root(\hleaf(\cdot), m, n, \cdot)$ ($S$ is the root path of leaf $m$;
-the consumed inputs are the path's siblings); the new-root component of
-the consistency verifier $\ConsRec$ (\S\ref{sec:tree}) ($S$ reaches down
-to the perfect subtrees covering $[0, n_0)$; the consumed inputs are the
-proof nodes and, on the leftmost spine, the pinned root); and the honest
-computation of $\MTH(D')$ for any $D'$ with $|D'| = |D|$ ($S$ is all of
-$T$; the inputs are the leaves of $D'$).
-
-\begin{lemma}[Root binding]\label{lem:bind}
-Let $F$ be a hash-fold over the honest Merkle tree $T$ of a leaf list $D$,
-and suppose $F$'s output equals $\MTH(D)$. Then either (i)~at some node of
-$S$, $F$'s hash argument differs from $T$'s while the two hash values
-agree---an explicit SHA-256 collision---or (ii)~$F$'s computation
-coincides with $T$ node-for-node: every value $F$ emits, \emph{every
-input it consumes}, and every leaf input it takes equals, respectively,
-the corresponding node value of $T$ and the corresponding leaf of $D$.
-\end{lemma}
-\begin{proof}
-Top-down induction on $S$, maintaining at each visited node the invariant
-that $F$'s value there equals $T$'s. At the root both equal $\MTH(D)$ by
-hypothesis. At an internal node of $S$ where the invariant holds, both
-values are $\hnode$ of an argument pair (65-byte preimages); if the pairs
-differ we are in case (i); if they coincide, each child's value is
-pinned: a child inside $S$ inherits the invariant and we recurse, while a
-child outside $S$ is a consumed input now known to equal $T$'s node value
-there---no descent needed. At a leaf of $S$ the invariant reads
-$\hleaf(d') = \hleaf(D[j])$: either $d' = D[j]$, or the two leaf preimages
-differ and we are in case (i). If case (i) never fires, the accumulated
-equalities at every node of $S$ are exactly claim (ii). Because $F$'s
-shape is $T$'s, every comparison above is leaf-to-leaf or node-to-node;
-Lemma~\ref{lem:domsep} additionally ensures that even a cross-type value
-coincidence would be a collision of distinct strings, which matters in
-the deployed protocol, where the same hash function commits leaves and
-nodes across trees of attacker-influenced sizes~\cite{crosby,dghs}.
-\end{proof}
-
-\begin{theorem}[Inclusion soundness: position binding]\label{thm:sound}
-There is an explicit algorithm $\mathcal{E}$ (running in time $O(n)$ hash
-evaluations) such that: whenever an adversary outputs a leaf list $D$ with
-$|D| = n$, an index $m < n$, a leaf $d \neq D[m]$, and a path $P$ with
-$\Root(\hleaf(d), m, n, P) = \MTH(D)$, $\mathcal{E}(D, m, d, P)$ outputs a
-SHA-256 collision.
+$\mathcal{E}_{\rm incl}(D,m,d,P)$ returns two distinct SHA-256 preimages with
+the same digest.
 \end{theorem}
 \begin{proof}
-$F = \Root(\hleaf(d), m, n, \cdot)$ applied to $P$ is a hash-fold over the
-honest tree $T_D$ whose sub-tree $S$ is the root path of leaf $m$, with
-consumed inputs the entries of $P$ and leaf input $d$; by hypothesis its
-output is $\MTH(D)$. Apply Lemma~\ref{lem:bind}. Case (ii) includes the
-claim that the leaf input equals $D[m]$, contradicting $d \neq D[m]$; so
-case (i) fires. $\mathcal{E}$ recomputes $T_D$ ($O(n)$ hashes), replays
-the fold to locate the disagreeing pair, and outputs it.
+Recompute the honest tree and replay the accepting reconstruction from the root
+downward. At each visited internal node, compare the adversarial and honest
+node preimages. If they differ while their digests agree, output the collision.
+Otherwise both child values agree and descent continues along the path. At the
+terminal leaf, equality of digests with $d\neq D[m]$ yields a leaf-hash
+collision. Domain separation rules out interpreting a leaf preimage as a node
+preimage without already producing a collision.
 \end{proof}
 
-\begin{remark}
-Both soundness statements are unconditional in the same sense: they do not
-assert forgery is infeasible, they \emph{construct} a SHA-256 collision
-from any successful forgery, so append-only and position security are
-\emph{precisely} ``SHA-256 is collision resistant''---no more, no less. The
-two theorems share Lemma~\ref{lem:bind}, the only place hashing is reasoned
-about; this factoring is deliberate, as Lemma~\ref{lem:bind} is exactly
-what the Lean mechanization of \S\ref{sec:next} will carry, with collision
-resistance entering only as a documented boundary axiom, audited by the log
-like the SHA-512 oracle in the Ed25519 tiers.
-\end{remark}
+\subsection{Consistency}
 
-\begin{theorem}[Consistency soundness]\label{thm:consistency}
-There is an explicit algorithm $\mathcal{E}'$, running in $O(n_1)$ hash
-evaluations, such that: whenever an adversary outputs leaf lists $D_0, D_1$
-with $|D_0| = n_0 \le n_1 = |D_1|$ and $D_0 \neq D_1[0{:}n_0]$, together
-with a proof $C$ that the consumer's verifier of \S\ref{sec:tree} accepts,
-i.e.\ $\ConsRec(n_0, n_1, C, \top, \MTH(D_0)) = (\MTH(D_0), \MTH(D_1))$,
-$\mathcal{E}'(D_0, D_1, C)$ outputs a SHA-256 collision.
+The recursive verifier $\ConsRec(n_0,n_1,C,b,r_0)$ reconstructs an old and new
+root from proof $C$, a flag $b$ indicating whether the old root is implicit,
+and pinned value $r_0$. Malformed shapes return rejection.
+
+\begin{theorem}[Consistency soundness of the recursive model]
+There is an explicit extractor $\mathcal{E}_{\rm cons}$ such that, whenever
+$|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.
 \end{theorem}
 \begin{proof}
-$\ConsRec$ returns a pair; acceptance equates its second component with
-$\MTH(D_1)$ and its first with $\MTH(D_0)$. Reading the four cases, the
-second component emits $\hnode$ at every split it traverses of the
-size-$n_1$ tree and bottoms out on consumed values---it is a hash-fold
-over the honest tree $T_1$, with consumed inputs the proof nodes and, on
-the leftmost spine, the pinned root---while the first component reuses a
-sub-list of those same values, namely the ones covering the index range
-$[0, n_0)$, and folds \emph{only} those. We use the two components
-differently, so the delicate first component never enters the lemma.
-
-\emph{Step 1 (the transcript values are genuine).} Apply
-Lemma~\ref{lem:bind} to the second component against $T_1$. Either it hits
-case (i)---output that collision---or (case ii) every value it emitted and
-every input it consumed---each proof node, and the pinned root where the
-fold bottoms out on it---equals the corresponding node of $T_1$. Assume
-the latter; the consumed values are now known to be genuine nodes of the
-honest tree $T_1$.
-
-\emph{Step 2 (the prefix roots collide).} The consumed values covering
-$[0, n_0)$ sit at the canonical RFC~9162 decomposition of that range into
-maximal perfect subtrees of $T_1$; by Step~1 they are genuine, so folding
-them---which is exactly what the first component does (degenerately, when
-the old tree is itself a perfect subtree of $T_1$, the ``fold'' is the
-consumed pinned root alone)---yields the root of $D_1[0{:}n_0]$,
-i.e.\ the first component equals $\MTH(D_1[0{:}n_0])$. But acceptance also
-equates the first component with $\MTH(D_0)$. Hence
-$\MTH(D_0) = \MTH(D_1[0{:}n_0])$ while $D_0 \neq D_1[0{:}n_0]$.
-
-\emph{Step 3 (descend).} Since $|D_0| = |D_1[0{:}n_0]| = n_0$, the two
-honest trees have identical shape, so the honest computation of
-$\MTH(D_1[0{:}n_0])$ is a hash-fold over $T_{D_0}$ ($S$ the whole tree;
-leaf inputs the leaves of
-$D_1[0{:}n_0]$). Its output is $\MTH(D_1[0{:}n_0]) = \MTH(D_0)$ by Step~2,
-so Lemma~\ref{lem:bind} applies with $D = D_0$. Case (ii) would force the
-leaf inputs to equal $D_0$, i.e.\ $D_1[0{:}n_0] = D_0$, contradicting the
-premise; so case (i) fires---an explicit collision. $\mathcal{E}'$ outputs
-whichever collision was found; recomputing $T_0$ and $T_1$, it runs in
-$O(n_1)$ hash evaluations.
+The new-root component is a hash fold over the shape of the $n_1$ tree. Compare
+it with the honest $D_1$ tree. Either the first differing preimage gives a
+collision, or every consumed proof node equals the corresponding honest node.
+In the latter case, the old-root component is the canonical fold of the honest
+prefix $D_1[0{:}n_0]$, so acceptance implies
+$\MTH(D_0)=\MTH(D_1[0{:}n_0])$. The two equal-sized leaf lists differ; descend
+through their identically shaped honest trees to extract the first hash
+collision.
 \end{proof}
 
-\begin{proposition}[Pin-store safety]\label{prop:pin}
-Assume Ed25519 EUF-CMA security for the head-signing key and consider the
-state machine of \S\ref{sec:pinstore}. Then, except with the probability of
-a signature forgery or a SHA-256 collision:
-\begin{enumerate}[itemsep=1pt]
-\item (\emph{Monotonicity}) If a consumer's pin evolves through states
-$(n_1, r_1), \dots, (n_t, r_t)$, then $n_1 \le \dots \le n_t$, and for any
-leaf lists $D_i$ the operator can exhibit with $\MTH(D_i) = r_i$,
-$|D_i| = n_i$, each $D_i$ is a prefix of $D_{i+1}$.
-\item (\emph{Fork evidence}) If two consumers with the same pinned key ever
-hold accepted heads $(n, r)$ and $(n, r')$ with $r \neq r'$, the pair of
-signed heads is transferable, publicly verifiable evidence that the key
-holder signed two conflicting views.
-\end{enumerate}
+\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
+heads under the same key with equal size and unequal roots are transferable
+evidence that the key holder signed incompatible views.
 \end{proposition}
 \begin{proof}
-(1) The machine accepts a larger size only with a verified consistency
-proof, so by Theorem~\ref{thm:consistency} any exhibited leaf lists are
-prefix-ordered unless a collision is found; rollback is rejected
-syntactically. (2) Both heads carry valid signatures under the pinned key;
-under EUF-CMA, both were produced by the key holder, and $r \neq r'$ at
-equal size is precisely a split view. The evidence is transferable because
-verification requires only the public key.
+Rollback is rejected syntactically. 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 with valid signatures are two conflicting
+statements attributable to the key holder, except under signature forgery.
 \end{proof}
 
-\begin{proposition}[Verdict integrity]\label{prop:verdict}
-Fix a consumer with local allowed-set table $\allowed(\cdot)$. For every
-attestation leaf $a$ and certificate $c$ in it, the consumer's
-\emph{cleanliness verdict} is
-the predicate $\clean(c) \Leftrightarrow \obs_a(c) = \allowed(c)$, a
-function of the leaf's observed cones and the consumer's table only; the
-operator's embedded pass/fail labels are not an input to it. The
-consumer's \emph{acceptance policy} consults those labels at most
-negatively: no operator assertion can upgrade any verdict or acceptance.
+\begin{proposition}[Policy separation]
+For fixed local policy $\Policy$, the boundary-conformance result for every
+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}
-By construction of the consumer tooling: the verdict function takes
-$(\obs_a, \allowed)$ and ignores the label fields in every branch; a
-certificate lacking an observed cone is mapped to \textsf{unverifiable},
-not to a verdict. The acceptance policy applies the operator's
-proven/failed \texttt{status} label only as a veto---a certificate the
-operator does not itself mark proven can never count---and a veto cannot
-upgrade; hence labels can deny but never grant.
+The comparison is set equality and takes no positive operator verdict as input.
+A deployment may conservatively treat an operator failure label as a veto, but
+a veto cannot grant acceptance.
 \end{proof}
 
-\paragraph{What is \emph{not} proven.} Propositions~\ref{prop:pin} and
-\ref{prop:verdict} together with Theorems~\ref{thm:complete}--%
-\ref{thm:consistency} discharge G1--G3. They do not---and cannot---exclude
-an operator who fabricates observations (\S\ref{sec:model:residual}), and
-they say nothing about the mathematical content of the attested corpus,
-whose guarantees rest on the Lean kernel and the assumption set enumerated
-in \S\ref{sec:deployment}. The division of labor is deliberate: the
-cryptographic layer makes the operator's claims \emph{exact, immutable, and
-attributable}; the deductive layer is what makes them \emph{true}.
-Table~\ref{tab:claims} decomposes the end-to-end chain: each consumer
-conclusion, the mechanism that establishes it, and the assumption that
-remains. The architecture does not pretend to eliminate trust; it
-decomposes trust into independently visible components---including two
-rows it deliberately does \emph{not} establish.
+\subsection{Scope of the deployed consistency claim}
 
-\begin{table}[t]
-\centering\small
-\begin{tabular}{@{}p{0.31\textwidth}p{0.28\textwidth}p{0.33\textwidth}@{}}
-\toprule
-consumer conclusion & established by & remaining assumption \\
-\midrule
-leaf bytes sit at index $m$ under head $h$ & inclusion proof (Thm~\ref{thm:sound}) & SHA-256 collision resistance; authentic head \\
-head was authorized under the log key & Ed25519 verification & correct key pin; EUF-CMA \\
-new local head extends the old one & consistency proof (Thm~\ref{thm:consistency}) & SHA-256 collision resistance \\
-equal-size heads conflict: equivocation & two valid signatures, unequal roots (Prop~\ref{prop:pin}) & correct key pin \\
-observed cone matches local policy & set equality (Prop~\ref{prop:verdict}) & semantic identity of the named declarations at the pinned commit \\
-the kernel produced the observation & operator replay attestation & replay-pipeline honesty, or independent replay (\S\ref{sec:model:residual}) \\
-deployed binary matches verified source & \emph{not established} & reproducible build / binary attestation \\
-signing binary is the claimed implementation & \emph{not established} & execution provenance (\S\ref{sec:selfref}) \\
-\bottomrule
-\end{tabular}
-\caption{The end-to-end claim matrix. Every consumer conclusion, what
-establishes it, and what remains assumed. The last two rows are
-deliberate non-claims (\S\ref{sec:intro}, \S\ref{sec:limitations}).}
-\label{tab:claims}
-\end{table}
+The Lean theorem covers the recursive predicate above. The deployed iterative
+verifier follows the familiar RFC bit-navigation algorithm. Differential
+testing discovered that the iterative verifier accepts a strict superset on
+malformed size claims: for example, a valid proof for a $2\to3$ transition can
+be accepted under the false old-size claim $1\to3$ when paired with the size-2
+root. The mechanism is elementary: the iterative algorithm seeds its
+reconstruction with the supplied old root and consults the size claims only as
+bit-navigation state, so several distinct old-size claims navigate one proof
+identically. In 73,573 lied-size boundary cases, 3,867 divergences were
+observed; all were one-sided (deployed accepts, recursive model rejects).
 
-\section{The self-referential signing loop}\label{sec:selfref}
+The intended consumer flow binds $(n_0,r_0)$ in local persistent state and
+binds $(n_1,r_1)$ together in a signed head. The present corpus does not prove
+a refinement theorem from that operational invariant to the recursive
+predicate. Consequently the public attestation says exactly this: the model is
+proved; deployment correspondence is finite-tested and relies on an
+unmechanized authentic-size/root invariant.
 
-Tree heads are Ed25519 signatures, and this creates an opportunity for
-coherence: the log contains correctness certificates for an Ed25519
-implementation. The LTL's heads are therefore signed by a binary built from
-the pinned source tree of exactly the implementation attested in the log
-(serial backend pinned, matching the verified extraction), and---before
-signing---the operator runs the same Merkle inclusion verification a
-consumer runs, on the newest leaf attesting the signing implementation,
-against the tree about to be signed. The verdict is embedded in the
-signature block:
-\begin{quote}\ttfamily\small
-signing\_backend: verified-dalek-serial\\
-signing\_library\_source\_commit: aa0f6ab...\\
-signing\_library\_leaf\_index: 8\\
-signing\_library\_certificates\_proven: 16/16\\
-self\_inclusion: verified
-\end{quote}
-(These provenance fields ride alongside the signature as operator-provided
-context; they are not part of the signed payload, and a consumer relies on
-none of them---the acyclic chain below rests only on the signature and the
-leaf's inclusion.)
-The signature vouches for the tree; the tree vouches for the code that
-produced the signature; and the two vouchings are different proof modalities
-(cryptographic and deductive), so the loop is self-referential without being
-circular. Concretely, a consumer's verification order is a directed acyclic
-chain, no step trusting its own output: pin the operator key (assumed, once)
-$\to$ check the head signature (EUF-CMA) $\to$ verify the signing library's
-leaf is included in that head (hashes only, no signature) $\to$ optionally
-rebuild that library from its pinned commit and re-check its certificates
-(Lean kernel). The self-reference is only that the code producing signatures
-also \emph{appears as a subject} in the log; no check consumes the result it
-is establishing. The self-check always references the \emph{newest} leaf
-attesting the signing library: after the re-attestation of
-\S\ref{sec:deployment}, the referenced index advanced from~4 to~8
-automatically, the loop re-anchoring itself to the fresh attestation
-without operator intervention.
+\section{Lean and Ed25519 instantiation}\label{sec:instantiation}
 
-\paragraph{The honest extent of this claim.} The Lean certificates cover
-the \emph{verification} path of the library (the theorems' subject is the
-extraction image of that path); the \emph{signing} path is not covered by
-any certificate and is declared trusted base. The deployed operator
-\emph{enforces and records} the invariant that the signing binary is
-built from the attested artifact rather than an unrelated third
-implementation; a consumer can check that the claimed source is attested
-in the signed tree, but---an Ed25519 signature reveals nothing about the
-program that produced it---cannot independently establish that this
-binary produced a given signature. Establishing that would require
-reproducible builds or execution attestation
-(\S\ref{sec:limitations}). Signature verification
-on consumer machines can optionally run through the same certified-source
-binary, with the backend that actually ran recorded in every result and a
-fail-closed policy flag available. First-append bootstrapping is handled
-honestly: heads signed before the signing library's attestation enters the
-log record \texttt{self\_inclusion: library\_not\_in\_log}.
+\subsection{Proof corpus}
 
-\section{Deployment and evidence}\label{sec:deployment}
+The initial subjects are upstream \code{curve25519-dalek}/\code{ed25519-dalek}
+and three deployed forks: Solana/Anza, RISC~Zero, and Betrusted --- all
+implementations of Ed25519~\cite{eddsa,rfc8032}. Aeneas
+provides a functional translation route from Rust to theorem-prover models;
+its design uses Rust ownership information to avoid explicit memory reasoning
+for a large class of safe Rust programs~\cite{aeneas}. Recent independent
+experience reports likewise show increasing use of Rust-to-Lean pipelines for
+cryptographic code~\cite{klaus2026}.
 
-The LTL is deployed\footnote{Service: \url{https://ltl.zkdefi.org}
-(read-only HTTP API and documentation). Mirror:
-\url{https://github.com/saymrwulf/lean-transparency-log}. Operator and
-consumer tooling: \url{https://github.com/saymrwulf/proof-aware-crypto-tooling-agent}.
-The underlying proof corpora are in the
-\texttt{saymrwulf/*-ed25519-verified} repositories; every claim in this
-paper is re-checkable from these artifacts.} with twelve leaves,
-produced by three full replay runs (one attestation per fork per run;
-58--64 Lean files and ${\approx}1{,}800$\,s per fork, under hard memory
-caps and core pinning; the per-fork duration is corroborated by the
-inter-leaf \texttt{issued\_at} spacing in the published log, whose
-uninterrupted within-run gaps fall between 29m35s and 30m40s). Each
-successful run reports 16/16 certificates
-proven with boundary-exact cones, pinned to exact commits. The three runs
-correspond to three states of the world, and their coexistence in one
-append-only ledger is the point of the system:
-
-\begin{itemize}[itemsep=2pt]
-\item \textbf{Leaves 0--3 (failed run).} The first run's audit step failed
-  on two defects in the operator tooling (a path issue and a parser that
-  mishandled Lean's line-wrapped axiom lists for the eleven-axiom cones).
-  The operator signed attestations \emph{recording the failure} rather
-  than suppressing the run. Both defects were fail-closed: valid proofs
-  were rejected, invalid ones never accepted.
-\item \textbf{Leaves 4--7 (clean run).} After the fix, all four forks
-  attested 16/16 boundary-exact at that day's commits.
-\item \textbf{Leaves 8--11 (clean run, new commits).} A subsequent
-  documentation-only rewrite of the subject repositories' histories
-  changed their commit hashes. Because a leaf pins an exact commit
-  (\S\ref{sec:leaves}), the operator re-ran the full corpus and appended
-  fresh attestations at the new commits rather than editing leaves 4--7.
-  That the proof \emph{files} survived the rewrite unchanged is
-  corroborated from the log itself: leaves 4--7 and 8--11 carry identical
-  certificate lists and identical observed axiom cones, re-checked by the
-  kernel at both commit generations. (The pre-rewrite trees themselves are
-  no longer distributed, so a direct tree diff is not among the public
-  artifacts.)
+Each fork's corpus contains sixteen reviewed certificates covering:
+\begin{itemize}[leftmargin=1.6em,itemsep=2pt]
+\item five-limb field arithmetic over $\Fp$ with value and bound preservation;
+\item complete twisted-Edwards group operations~\cite{edwards,twisted};
+\item scalar arithmetic modulo the Ed25519 group order;
+\item encoding, decoding, and constructive point decompression;
+\item a four-stage lifting ladder from byte-level verifier acceptance to a
+mathematical point equation.
 \end{itemize}
 
-\noindent This last event is a live exercise of the append-only
-discipline (G2): a change that a naive operator would have hidden by
-overwriting is instead absorbed by \emph{addition}, leaving a permanent,
-publicly verifiable record that the subject histories changed and that
-the mathematics survived the change. The ledger---four failure leaves and
-eight success leaves across two commit generations---is a feature of the
-trust model, not clutter to be pruned (Figure~\ref{fig:tree}).
+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
+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$;
+\item[T2:] those recomputed bytes are the canonical encoding of
+$[k](-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$.
+\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{Replay attestation}
+
+For every certificate the operator records:
+\begin{lstlisting}
+name
+status
+observed_axioms
+expected_axioms          # audit trail; consumer policy is local
+axiom_status
+diagnostics
+\end{lstlisting}
+The attestation also records repository URL and commit, Lean and Lake versions,
+replay diagnostics, and resource controls. Missing cones are
+\code{unverifiable}; they are never interpreted as empty.
+
+\subsection{Operational self-reference}
+
+The service reports that tree heads are generated using a binary built from the
+same Ed25519 source family whose verification-path certificates appear in the
+log. Before signing, the operator recomputes inclusion of the newest signing-
+library leaf in the tree. This is useful operational coherence, but not proof
+of execution provenance. The signature authenticates the tree-head payload; it
+does not reveal the program that produced it. Reproducible builds or execution
+attestation would be required to establish that stronger claim.
+
+\section{Deployment and evaluation}\label{sec:deployment}
+
+The evaluation asks four questions: (E1) can substantial proof-replay evidence
+be consumed without deploying Lean; (E2) does the public history retain failed
+and superseded observations rather than silently replacing them; (E3) can the
+accumulator's own arguments be placed under the same attestation discipline;
+and (E4) does mechanization expose mismatches between the proved model and the
+deployed verifier?
+
+\subsection{Public state}
+
+As of 16 July 2026, the public log contains thirteen leaves and current root
+\begin{center}
+\path{3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d}.
+\end{center}
+Every signed head issued since public mirroring began is retained --- six
+heads, at tree sizes 8 through 13 --- 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
+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 (the thirteenth entry) attests the accumulator corpus at commit
+\begin{center}\small\ttfamily
+172a1d0653f489d5b7cb73ac7942a57cbb496532
+\end{center}
+It records 61/61 reviewed
+certificates as proven with exact expected/observed cones. The corpus audit
+also inventories 222 compiled environment constants and permits exactly one
+boundary axiom, \code{LTLAcc.sha256}.
 
 \begin{figure}[t]
 \centering
 \begin{tikzpicture}[
-  every node/.style={font=\footnotesize},
-  leaf/.style={draw, minimum width=0.62cm, minimum height=0.42cm, inner sep=1pt},
-  fail/.style={leaf, draw=black!45, text=black!55, fill=black!7},
-  ok/.style={leaf, draw=black!85, fill=black!3},
-  node/.style={draw, circle, minimum size=0.34cm, inner sep=0pt, fill=black!4},
-  edge/.style={draw=black!55}, xscale=0.92]
-  % leaves 0..11
-  \foreach \i in {0,...,3} \node[fail] (l\i) at (\i,0) {\i};
-  \foreach \i in {4,...,11} \node[ok] (l\i) at (\i,0) {\i};
-  % exact RFC 9162 shape for n = 12: root splits 8 | 4
-  \foreach \i/\a/\b in {0/0/1, 1/2/3, 2/4/5, 3/6/7, 4/8/9, 5/10/11}
-    \node[node] (m\i) at ({(\a+\b)/2},1.0) {};
-  \node[node] (q0) at (1.5,1.95) {};   % leaves 0-3
-  \node[node] (q1) at (5.5,1.95) {};   % leaves 4-7
-  \node[node] (q2) at (9.5,1.95) {};   % leaves 8-11
-  \node[node] (o0) at (3.5,2.9)  {};   % leaves 0-7
-  \node[node, minimum size=0.4cm] (root) at (6.5,3.85) {};
-  \node[right=1pt of root, font=\small] {\ signed tree head $\;\sigma = \mathrm{Sig}(sk,(12,r,t))$};
-  % edges
-  \foreach \i/\a/\b in {0/0/1, 1/2/3, 2/4/5, 3/6/7, 4/8/9, 5/10/11}
-    { \draw[edge] (l\a)--(m\i); \draw[edge] (l\b)--(m\i); }
-  \draw[edge] (m0)--(q0); \draw[edge] (m1)--(q0);
-  \draw[edge] (m2)--(q1); \draw[edge] (m3)--(q1);
-  \draw[edge] (m4)--(q2); \draw[edge] (m5)--(q2);
-  \draw[edge] (q0)--(o0); \draw[edge] (q1)--(o0);
-  \draw[edge] (o0)--(root); \draw[edge] (q2)--(root);
-  % brackets under leaf ranges
-  \draw[decorate,decoration={brace,mirror,raise=3pt}, black!45]
-    (l0.south west) -- (l3.south east)
-    node[midway,below=7pt, black!55]{run 1: failed audit};
-  \draw[decorate,decoration={brace,mirror,raise=3pt}, black!70]
-    (l4.south west) -- (l7.south east)
-    node[midway,below=7pt]{run 2: clean, commits $g_1$};
-  \draw[decorate,decoration={brace,mirror,raise=3pt}, black!70]
-    (l8.south west) -- (l11.south east)
-    node[midway,below=7pt]{run 3: clean, commits $g_2$};
+  >=Latex,
+  box/.style={draw,rounded corners=2pt,minimum width=1.03cm,minimum height=.52cm,font=\scriptsize,align=center},
+  fail/.style={box,fill=black!6,draw=black!45,text=black!60},
+  ok/.style={box,fill=green!7!white,draw=deepgreen,text=deepgreen!80!black},
+  acc/.style={box,fill=blue!7!white,draw=deepblue,text=deepblue},
+  arrow/.style={->,draw=black!55}
+]
+\foreach \i in {0,...,3} {\node[fail] (l\i) at (1.08*\i,0) {\i\\failed};}
+\foreach \i in {4,...,7} {\node[ok] (l\i) at (1.08*\i,0) {\i\\clean};}
+\foreach \i in {8,...,11} {\node[ok] (l\i) at (1.08*\i,0) {\i\\clean};}
+\node[acc,minimum width=1.3cm] (l12) at (1.08*12,0) {12\\accumulator};
+\draw[decorate,decoration={brace,mirror,raise=5pt},black!45]
+  ($(l0.south west)+(-.05,0)$)--($(l3.south east)+(.05,0)$)
+  node[midway,below=11pt,font=\scriptsize]{run 1};
+\draw[decorate,decoration={brace,mirror,raise=5pt},deepgreen]
+  ($(l4.south west)+(-.05,0)$)--($(l7.south east)+(.05,0)$)
+  node[midway,below=11pt,font=\scriptsize]{run 2};
+\draw[decorate,decoration={brace,mirror,raise=5pt},deepgreen]
+  ($(l8.south west)+(-.05,0)$)--($(l11.south east)+(.05,0)$)
+  node[midway,below=11pt,font=\scriptsize]{run 3};
+\node[draw,rounded corners,fill=softgray,minimum width=4.3cm,minimum height=.7cm,font=\small] (sth) at (6.7,1.65)
+  {signed head: size 13, root \code{3488a2d0...}};
+\draw[arrow] (l12.north) -- (sth.south east);
+\draw[arrow] (l6.north) -- (sth.south west);
 \end{tikzpicture}
-\caption{The deployed twelve-leaf log. Grey leaves 0--3 record the first
-run's audit failure (retained, not erased); leaves 4--7 and 8--11 are two
-clean runs, at commit generations $g_1$ and $g_2$ across a subject-history
-rewrite. The interior is the exact RFC~9162 shape of \S\ref{sec:tree} for
-$n = 12$ (root split $8 \mid 4$; $r$ denotes the root value). Every value
-in the figure is recomputable from the public leaves.}
-\label{fig:tree}
+\caption{The public 13-leaf deployment. Failure leaves are retained; entry 13
+attests the accumulator corpus itself, scoped to the recursive model.}
+\label{fig:deployment}
 \end{figure}
 
-\begin{table}[t]
-\centering\small
+\subsection{Mechanization coverage}
+
+Entry 13 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
+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
+refinement from the deployed iterative consistency verifier remain outside the
+corpus.
+
+\begin{center}\small
+\begin{tabularx}{\textwidth}{@{}lXX@{}}
+\toprule
+Layer & Mechanized evidence & Explicit boundary \\
+\midrule
+Merkle definitions & MTH, Root, Path, recursive ConsRec & single SHA-256 boundary axiom \\
+Inclusion & completeness and named collision extractor & collision resistance interpreted externally \\
+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 \\
+\bottomrule
+\end{tabularx}
+\end{center}
+
+\subsection{Cost and reproducibility}
+
+A replay of one Ed25519 fork requires approximately 30 minutes of Lean kernel
+time under the pinned environment. Receipt verification requires one Ed25519
+signature and a logarithmic number of SHA-256 node computations. 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.
+
+The fidelity harness compares the Lean-definition transliteration with the
+deployed Python algorithms over pinned finite families:
+\begin{center}\small
 \begin{tabular}{@{}lrrl@{}}
 \toprule
-fork & Lean files & apex cone (axioms, total) & SHA-512 in the boundary \\
+Family & Cases & Divergences & Interpretation \\
 \midrule
-upstream \texttt{dalek} & 64 & 11 & 3-call streaming (\texttt{new/update/finalize}) \\
-Solana (\texttt{anza})  & 58 & \phantom{0}7 & one \texttt{ed\_sigs.sha512\_hash3} \\
-RISC~Zero               & 63 & \phantom{0}8 & one \texttt{verifying.sha512\_hash3} \\
-Betrusted               & 63 & \phantom{0}8 & one \texttt{verifying.sha512\_hash3} \\
+Inclusion & 230,271 & 0 & baseline and out-of-range families \\
+Consistency baseline & 230,016 & 0 & honest and mutation families \\
+Lied-size consistency & 73,573 & 3,867 & all deployed-accepts-only \\
 \bottomrule
 \end{tabular}
-\caption{The four subject implementations. Each replay re-checks 16
-certificates in ${\approx}1{,}800$\,s under memory caps and core pinning.
-The apex-cone count is the full allowed axiom set at the signature
-tiers---Lean's three standard axioms plus the fork's enumerated oracle
-boundary (Appendix~\ref{app:axioms}); it differs by fork because the
-SHA-512 surface and the byte-accessor shape differ. Proof-script
-divergence across forks is quantified in the portability paragraph below;
-the pure-mathematics files are byte-identical across all four.}
-\label{tab:forks}
-\end{table}
+\end{center}
+Finite testing is not a proof of extensional equality. Here it served a more
+valuable purpose: it falsified an overbroad equivalence claim and supplied a
+stable regression boundary.
 
-\paragraph{What a verified receipt establishes.} Under the assumptions
-enumerated below, a consumer who verifies a receipt knows: \emph{the
-operator whose key I pinned attests that the Lean certificates of repository
-$X$ at commit $Y$ re-check, with per-certificate observed axiom cones as
-included---and this statement is part of the log presented to every other
-consumer.} Combined with local verdict re-derivation
-(Proposition~\ref{prop:verdict}), this yields source-level assurance for the
-pinned commit. It deliberately does \emph{not} establish: correctness of any
-binary (consumers build from the pinned source; compilers are trusted base),
-correctness of SHA-512 (an opaque oracle in the theorems), correctness of
-the wire-format parsers (their outcomes are hypotheses of the signature
-tiers), signing-side correctness, or side-channel properties.
+\begin{remark}[Model/deployment seam]
+For malformed size claims, the deployed iterative verifier accepts a strict
+superset of the recursive model. In all 3,867 observed divergences the deployed
+verifier accepted and the model rejected; the reverse direction did not occur.
+The public attestation therefore scopes soundness to the recursive model and
+states the additional operational assumption: roots and sizes must be bound by
+the authenticated pin-store and signed-head flow. This invariant is not
+mechanized in the present corpus.
+\end{remark}
 
-\paragraph{The assumption set, in full.} The Lean kernel and its three
-axioms plus mathlib; faithfulness of the Charon/Aeneas
-extraction~\cite{aeneas}; each fork's documented oracle boundary; operator
-key custody and trust-on-first-use key distribution (mitigated by publishing
-the key in two independent locations); collision resistance of SHA-256 for
-the log (Theorems~\ref{thm:sound}, \ref{thm:consistency}); unforgeability
-of Ed25519 for the heads (Proposition~\ref{prop:pin}); and the consumer's
-own ${\approx}25$-line verifier (Appendix~\ref{app:verifier}).
+\subsection{Consumers}
 
-\paragraph{An observational by-product: proof portability.} Because the
-four corpora prove the same theorems against four independent extractions,
-the diff between proof files measures how portable proofs are across real
-forks. Pure-mathematics files (e.g., a carry-telescope lemma file) are
-byte-identical across all four; extraction-facing proof scripts diverge
-sharply where the forks' code or the extractor's naming differs (e.g., 215
-changed lines for the byte-parser proofs on the two forks whose extraction
-produces a closure-based loader; 121 lines for the signature-glue proofs on
-the same-crate fork; 27 lines between the two structurally closest forks,
-tracking one fork's \texttt{black\_box} optimization barrier and the
-operation reordering it induces). Per-target
-verification, in other words, is doing
-measurable work exactly where the targets actually differ.
+The deployed internal consumer is a quorum-custody signing service: its
+inbound boundary accepts a log-derived statement only when independently
+attested verifier backends agree, and its policy consumes recorded
+observations, never operator labels. A prospective external case study
+examined the Swiss Post e-voting system, whose vendored Ed25519 dependency
+matches an attested subject at family level but not at the attested version.
+The model treats that as a useful negative: attestations are version-exact by
+construction, and a family-level match confers nothing.
 
-\section{Limitations}\label{sec:limitations}
+\subsection{Proof portability across forks}
 
-The deployment is small (one operator, twelve leaves, four subject
-repositories) and the operator is a single party; split-view defense
-currently rests on consumer-side pinning (Proposition~\ref{prop:pin}) plus
-the public git mirror rather than an independent witness network. Key
-distribution is trust-on-first-use. The signing path of the dogfood binary
-is unverified (declared, not proven). The residual trust of
-\S\ref{sec:model:residual}---honesty of the operator's kernel
-observations---is mitigated only by targeted independent replay, and
-replayability presupposes retrievability: a leaf whose pinned commit is
-no longer distributed (leaves 0--7 after the subject-history rewrite,
-\S\ref{sec:deployment}) decays from a replayable claim to a historical
-record, and consumers act on the newest, retrievable attestations. The corpus
-itself stops at source-level assurance: reproducible builds and side-channel
-evidence remain open, and ML-DSA slots in the head format are deliberately
-recorded as unavailable rather than backed by an unverified implementation.
+Pure mathematical lemmas are largely reusable, while extraction-facing scripts
+diverge where code structure and generated names diverge. In the deployed
+corpora, selected parser and signature-glue files show tens to hundreds of
+changed lines across forks, whereas pure carry and field lemmas can remain
+byte-identical. This supports a practical conclusion: verification is portable
+above the representation boundary and target-specific where implementation
+structure actually differs.
 
-\section{Next step: verifying the accumulator itself}\label{sec:next}
+\section{Related work}\label{sec:related}
 
-The natural continuation applies the corpus's own discipline to the log's
-cryptographic half. Theorems~\ref{thm:complete}--\ref{thm:consistency} and
-Proposition~\ref{prop:pin} were stated so as to make their mechanization
-direct; we expect the principal work to be specification alignment and
-proof engineering rather than new cryptographic argument: (i) inclusion completeness
-(Theorem~\ref{thm:complete}) is assumption-free; (ii) inclusion soundness
-becomes the explicit extractor of Theorem~\ref{thm:sound}, with SHA-256
-collision resistance a documented boundary axiom audited exactly like the
-SHA-512 oracle in the Ed25519 tiers; (iii) likewise consistency
-(Theorem~\ref{thm:consistency}); (iv) domain separation
-(Lemma~\ref{lem:domsep}) is a one-line lemma; and (v) total correctness of
-the consumer's pin-store state machine (Proposition~\ref{prop:pin}).
-Verified Merkle implementations in F*~\cite{evercrypt} and machine-checked
-transparency-protocol analyses~\cite{cheval} show these proofs are well
-within reach; the LTL-specific closure is where the certificates go:
-\emph{into the log they defend, checked by the certified checker they
-specify}, alongside a consumer policy flag requiring the certified verifier.
-At that point both proving traditions in the composition run on certified
-code, and the remaining trusted base is two hash assumptions, a compiler, an
-extraction pipeline, and one key.
+\paragraph{Transparency.}
+Certificate Transparency introduced publicly auditable append-only logs for
+certificate issuance~\cite{ct1,ct2}; Crosby and Wallach developed efficient
+tamper-evident history trees~\cite{crosby}; Dowling et al. formalized security
+notions for secure logging and CT~\cite{dghs}. CONIKS applies transparency to
+key directories~\cite{coniks}. LTL reuses the authenticated data structure but
+changes the payload and trust semantics: a leaf is an observation of a proof
+replay, not an issuance event or key binding.
+
+\paragraph{Software supply-chain attestations.}
+In-toto expresses supply-chain steps and link metadata~\cite{intoto}. Sigstore
+combines ephemeral signing, identity, and transparency to reduce software-
+signing adoption barriers~\cite{sigstore}. LTL is complementary: it concerns
+what a theorem prover reportedly accepted and which assumptions remained, not
+who built or signed a binary. A complete assurance chain should eventually
+combine both.
+
+\paragraph{Proof transport and verified cryptography.}
+Proof-carrying code ships a proof to a consumer-side checker~\cite{pcc}. LTL
+serves consumers that cannot deploy that checker and therefore accepts a
+different trust trade. HACL*, EverCrypt, and Fiat-Crypto demonstrate verified
+cryptographic implementation pipelines~\cite{hacl,evercrypt,fiatcrypto};
+Computer-aided frameworks such as EasyCrypt address scheme-level security
+proofs~\cite{easycrypt}; Aeneas targets functional verification of Rust
+through translation~\cite{aeneas}.
+LTL does not compete with those systems: it distributes accountable statements
+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
+mechanizes accumulator arguments and then logs that replay result. The
+remaining refinement from the deployed state machine to the recursive model is
+explicitly open.
+
+\paragraph{Optimistic accountability.}
+Architecturally the model is closest to optimistic designs that substitute
+accountability for validity: a claim is accepted by default, and safety rests
+on any observer's ability to produce compact transferable evidence of a
+specific fault. The extractors of Section~\ref{sec:security} play the role of
+fraud proofs --- a false inclusion or consistency opening does not merely fail
+verification, it yields a concrete SHA-256 collision attributable to the log.
+LTL occupies the same design point for verification evidence, with targeted
+independent replay as the challenge mechanism.
+
+\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.
+
+\paragraph{Operator observation trust.}
+A malicious operator can fabricate a replay report. Signatures and Merkle
+proofs make the lie attributable and persistent; they do not make it true.
+Targeted independent replay is the corrective mechanism.
+
+\paragraph{Theorem identity.}
+Names and repository commits are not canonical semantic identifiers. A future
+schema should commit to elaborated theorem-type digests, axiom declaration-type
+digests, and an environment or replay-manifest digest.
+
+\paragraph{Source-to-binary gap.}
+The evidence concerns source models at pinned commits. Reproducible builds,
+compiler validation, binary measurement, and side-channel evidence are outside
+the present result.
+
+\paragraph{Witnessing and key distribution.}
+The deployment has one operator and trust-on-first-use key distribution. A Git
+mirror gives retaining observers a common public view, but does not force all
+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 has a larger malformed-
+input acceptance set. 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.
+
+\paragraph{Signed provenance.}
+Signing-backend metadata is operator-provided context and should be committed
+inside the signed tree-head payload. Even then it would remain an assertion,
+not execution proof.
+
+\paragraph{From accountable replay to cryptographic proof of replay.}
+A longer-term direction is a succinct proof that a fixed proof-checker binary
+accepted a fixed corpus. Such a system could reduce operator-observation trust,
+but would introduce a new verified-execution stack. LTL supplies an
+intermediate accountability layer and a public corpus against which that future
+system can be evaluated.
+
+\section{Conclusion}
+
+Formal verification solves the production of correctness evidence; it does not
+by itself solve distribution to consumers that cannot execute the verifier.
+This paper isolates that second problem and gives a cryptographic answer based
+on accountable replay attestation. The operator's observation remains trusted,
+but its content is structured, its history is signed and append-only, its
+assumption boundary is subject to consumer-local policy, and incompatible views
+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
+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
+useful scientific work.
+
+The next step is not to claim trustlessness. It is to close specific boundaries:
+canonical theorem-type commitments, reproducible source-to-binary linkage,
+independent witnesses, signed provenance commitments, and a proved refinement
+between the deployed signed-head flow and the recursive model. Accountable
+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
+\begin{center}\small\ttfamily
+8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a
+\end{center}
+and is included in the size-13 head with root
+\begin{center}\small\ttfamily
+3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d
+\end{center}
+The public artifacts are available at:
+\begin{itemize}[leftmargin=1.5em,itemsep=1pt]
+\item append-only mirror: \href{https://github.com/saymrwulf/lean-transparency-log}{\texttt{saymrwulf/lean-transparency-log}};
+\item accumulator mechanization: \href{https://github.com/saymrwulf/ltl-accumulator-verified}{\texttt{saymrwulf/ltl-accumulator-verified}};
+\item provider and consumer tooling: \href{https://github.com/saymrwulf/proof-aware-crypto-tooling-agent}{\texttt{saymrwulf/proof-aware-crypto-tooling-agent}}.
+\end{itemize}
+A clone of the mirror re-verifies every head, leaf, and receipt offline via
+\code{python3 verify.py --all} (Python standard library plus an \code{openssl}
+binary; the verifier fails closed if signature checking is unavailable).
 
 \section*{Acknowledgments}
+The author designed the system and is responsible for every claim. Claude
+(Anthropic) and GPT (OpenAI) were used as critical assistants in proof-corpus,
+tooling, and manuscript review. Their output was not accepted as evidence;
+claims were retained only after human review or reproducible artifact checks.
 
-The author designed the system, directed the verification effort, and is
-solely accountable for every claim in this paper. Claude (Anthropic) was
-used as an assistant in developing the proof corpora, tooling, and text,
-and adversarial reviews by both Claude and GPT (OpenAI) shaped the final
-manuscript; all
-proofs, measurements, and claims have been reviewed by the author and are
-independently re-checkable from the public artifacts and the referenced
-check scripts.
-% \authortodo{The sentence above must be true before you submit it.
-% Review every proof in Section 6 line by line and re-run every number in
-% Section 8 yourself.}
-
-\begin{thebibliography}{20}
+\begin{thebibliography}{22}
 \itemsep2pt
-
 \bibitem{ct1} B. Laurie, A. Langley, E. K\"asper. Certificate Transparency.
 RFC 6962, 2013.
 
@@ -1166,179 +988,103 @@ C. Peters. Twisted Edwards curves. AFRICACRYPT, LNCS 5023, pp. 389--405,
 \bibitem{pnueli} A. Pnueli. The temporal logic of programs. IEEE FOCS, pp.
 46--57, 1977.
 
+
+\bibitem{klaus2026} N. Klaus, J. Conejero, P. Tolmach. A Rust-to-Lean
+Verification Pipeline with AI Provers: An Experience Report. arXiv:2605.30106,
+2026.
+
 \end{thebibliography}
 
 \appendix
 
-\section{Leaf schema}\label{app:leaf}
-
-Each leaf is the canonical JSON serialization (sorted keys, no
-insignificant whitespace, UTF-8) of an attestation. Below is leaf~8 of
-the deployed log---the re-attestation of the upstream fork. The
-16-certificate array is elided to its first (foundational) and last
-(apex) entries; long values (hashes, timestamps, version strings,
-paths) are shortened, and omitted fields are marked, with ellipses; and
-fields are shown in logical rather than canonical (sorted-key) order
-for readability. The
-field names and values shown, and the axiom lists, are verbatim, and the
-unelided leaf is one \texttt{jq} invocation away in the public mirror.
-\begin{quote}\ttfamily\scriptsize
-\{ "type": "pacta.attestation", "schema\_version": 1,\\
-\hspace*{0.6em}"attestation": \{\\
-\hspace*{1.2em}"provider": "local-pacta-provider",\\
-\hspace*{1.2em}"issued\_at": "2026-07-07T...Z",\\
-\hspace*{1.2em}"subject": \{ "component": "dalek-ed25519-verified",\\
-\hspace*{2.4em}"repo\_commit": "33fb8bb2311c70ead2e83c0...",\\
-\hspace*{2.4em}"repo\_url": ..., "verified\_backend": "serial/u64",\\
-\hspace*{2.4em}... \},\\
-\hspace*{1.2em}"environment": \{\\
-\hspace*{2.4em}"lean\_version": "Lean (version 4.30.0-rc2, ...)",\\
-\hspace*{2.4em}"lake\_version": ..., "env\_script": ...,\\
-\hspace*{2.4em}"lean\_project\_dir": ... \},\\
-\hspace*{1.2em}"machine\_protection": \{ "lean\_guard": ...,\\
-\hspace*{2.4em}"note": "All Lean compiles route through the\\
-\hspace*{2.4em}repo's lean-guard (memory cap, core pinning,\\
-\hspace*{2.4em}timeout, single-flight lock) ..." \},\\
-\hspace*{1.2em}"replay": \{ "checked\_files": 64, "failed\_files": [],\\
-\hspace*{2.4em}"check\_ok": true, "axiom\_ok": true, ... \},\\
-\hspace*{1.2em}"certificates": [\\
-\hspace*{2.4em}\{ "name": "CurveFieldProofs.fieldImplementation",\\
-\hspace*{3.0em}"status": "proven", "axiom\_status": "clean",\\
-\hspace*{3.0em}"observed\_axioms": ["propext",\\
-\hspace*{3.6em}"Classical.choice","Quot.sound"],\\
-\hspace*{3.0em}"expected\_axioms": [...], ... \},\\
-\hspace*{2.4em}... \; \emph{(14 certificates elided)} \; ...\\
-\hspace*{2.4em}\{ "name":\\
-\hspace*{3.0em}"CurveFieldProofs.verify\_accepts\_iff\_decompress",\\
-\hspace*{3.0em}"status": "proven", "axiom\_status": "clean",\\
-\hspace*{3.0em}"observed\_axioms": ["propext","Classical.choice",\\
-\hspace*{3.6em}"Quot.sound","ed25519.Signature","sha2.Sha512",\\
-\hspace*{3.6em}"verifying.sha512\_finalize\_bytes",\\
-\hspace*{3.6em}"verifying.sha512\_new","verifying.sha512\_update",\\
-\hspace*{3.6em}"ed25519.Signature.to\_bytes",\\
-\hspace*{3.6em}"signature.error.Error",\\
-\hspace*{3.6em}"signature.error.Error.new"], ... \} ],\\
-\hspace*{1.2em}"signature": \{ "scheme": "openssl-ed25519", ... \},\\
-\hspace*{1.2em}... \} \}
-\end{quote}
-The \texttt{observed\_axioms} field is the exact output of
-\texttt{\#print axioms} for that theorem. Operator labels
-(\texttt{replay.check\_ok}, per-certificate \texttt{status} and
-\texttt{axiom\_status}) are recorded for the audit trail, but the
-cleanliness verdict is $\obs = \allowed$ computed against the consumer's
-own table in every case, with a missing cone mapped to
-\textsf{unverifiable} (Proposition~\ref{prop:verdict}). The
-\texttt{status} label is consulted only \emph{negatively}: a certificate
-the operator itself does not mark proven can never count toward
-acceptance, so labels can deny but never grant.
-
-\section{The consumer verifier}\label{app:verifier}
-
-The consumer-side inclusion check, in full (Python, standard library only);
-this is the recursive form proved in \S\ref{sec:security} and is equivalent
-to the iterative algorithm of RFC~9162 \S2.1.3.2.
-
-\begin{quote}\ttfamily\small
-import hashlib\\[2pt]
-def H(b): return hashlib.sha256(b).digest()\\
-def h\_leaf(d): return H(b'\textbackslash x00' + d)\\
-def h\_node(x, y): return H(b'\textbackslash x01' + x + y)\\[2pt]
-def largest\_pow2\_below(n):\\
-\hspace*{1em}k = 1\\
-\hspace*{1em}while 2 * k < n: k *= 2\\
-\hspace*{1em}return k\\[2pt]
-def root(v, m, n, path):\\
-\hspace*{1em}if n == 1:\\
-\hspace*{2em}if path: raise ValueError\\
-\hspace*{2em}return v\\
-\hspace*{1em}if not path: raise ValueError\\
-\hspace*{1em}*rest, s = path\\
-\hspace*{1em}k = largest\_pow2\_below(n)\\
-\hspace*{1em}if m < k:\\
-\hspace*{2em}return h\_node(root(v, m, k, rest), s)\\
-\hspace*{1em}return h\_node(s, root(v, m - k, n - k, rest))\\[2pt]
-def verify\_inclusion(leaf, m, n, path, head\_root):\\
-\hspace*{1em}return m < n and root(h\_leaf(leaf), m, n, path) == head\_root
-\end{quote}
-Signature verification of the head (Ed25519) and the pin-store logic of
-\S\ref{sec:pinstore} complete the consumer; the deployed
-${\approx}150$-line standalone verifier in the mirror additionally checks
-consistency proofs and recomputes prefix roots from the public leaves.
-
-\section{Allowed axiom sets}\label{app:axioms}
-
-Foundational certificates (12 of 16) must carry exactly Lean's three
-standard axioms:
-\begin{quote}\ttfamily\small
-propext \quad Classical.choice \quad Quot.sound
-\end{quote}
-The four signature-tier certificates additionally carry a per-fork
-enumerated boundary: an opaque SHA-512 oracle and opaque wire-format
-types (the signature type, its byte accessors, and---where the fork's
-API surfaces it---the error type). The
-boundary is not identical across forks---it reflects each fork's actual
-extracted surface---and auditing is exact against the fork's own set. The
-three distinct boundaries in the deployed corpus, verbatim from the
-repositories' check scripts, are as follows (the three standard axioms
-above, plus):
-
-\smallskip
-\noindent\textbf{Upstream \texttt{curve25519-dalek}} (11 axioms total;
-this fork exposes SHA-512 as three streaming operations):
-\begin{quote}\ttfamily\scriptsize
-ed25519.Signature \quad sha2.Sha512\\
-verifying.sha512\_finalize\_bytes\\
-verifying.sha512\_new \quad verifying.sha512\_update\\
-ed25519.Signature.to\_bytes\\
-signature.error.Error \quad signature.error.Error.new
-\end{quote}
-
-\noindent\textbf{RISC~Zero and Betrusted forks} (8 axioms total;
-identical to each other---SHA-512 is a single \texttt{hash3} oracle):
-\begin{quote}\ttfamily\scriptsize
-ed25519.Signature \quad verifying.sha512\_hash3\\
-ed25519.Signature.to\_bytes\\
-signature.error.Error \quad signature.error.Error.new
-\end{quote}
-
-\noindent\textbf{Solana (anza) fork} (7 axioms total; its own
-\texttt{ed\_sigs} namespace, and \texttt{R}/\texttt{s} byte accessors
-rather than a whole-signature encoder):
-\begin{quote}\ttfamily\scriptsize
-ed25519.Signature \quad ed\_sigs.sha512\_hash3\\
-ed25519.Signature.r\_bytes \quad ed25519.Signature.s\_bytes
-\end{quote}
-
-A consumer's local table (\S\ref{sec:auditing}) contains exactly these
-sets. That a boundary differs by fork is itself audited: an
-upstream-shaped cone appearing under the anza label, or vice versa, fails
-$\clean$ in the ``unexpected axiom'' direction.
-
-\section{The four verification tiers: Lean theorem names}\label{app:tiers}
-
-The lifting ladder T1--T4 and the mathematical facts it turns on are
-stated in \S\ref{sec:corpus}. For reproducibility we record here the
-verbatim Lean theorem name backing each tier in the upstream corpus
-(namespace \texttt{CurveFieldProofs} elided; the forks use the same names
-against their own extractions); a reader can
-\texttt{\#print axioms} any of these to reproduce the cones of
-Appendix~\ref{app:axioms}.
+\section{End-to-end claim matrix}\label{app:matrix}
 \begin{center}\small
-\begin{tabular}{@{}ll@{}}
+\begin{tabularx}{\textwidth}{@{}XXX@{}}
 \toprule
-tier (\S\ref{sec:corpus}) & Lean theorem \\
+Consumer conclusion & Established by & Remaining assumption \\
 \midrule
-T1 \enspace byte apex          & \texttt{verify\_accepts\_iff} \\
-T2 \enspace canonical half-lift & \texttt{verify\_accepts\_iff\_point} \\
-T3 \enspace injectivity / point eq. & \texttt{verify\_accepts\_iff\_point\_eq} \\
-T4 \enspace constructive full lift & \texttt{verify\_accepts\_iff\_decompress} \\
+Leaf occupies index $m$ under head $h$ & inclusion proof and signed head & SHA-256 collision resistance; correct public key \\
+Head was authorized by the log identity & Ed25519 verification & correct key acquisition; EUF-CMA \\
+New pinned head extends old pinned head & consistency proof & recursive-model soundness; authentic size/root pairing for deployment \\
+Equal-size unequal roots conflict & two valid signatures & both heads compared by a retaining observer \\
+Observed cone matches local boundary policy & exact set equality & semantic identity of named declarations \\
+Kernel produced the recorded observation & replay attestation & operator/replay-pipeline honesty or independent replay \\
+Source corresponds to deployed binary & not established & reproducible build and compiler assurance \\
+Claimed signer implementation produced STH & not established & execution provenance \\
+\bottomrule
+\end{tabularx}
+\end{center}
+
+\section{Deployed entry-13 scope}\label{app:entry13}
+The thirteenth public leaf 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
+mechanized recursive accumulator model. Correspondence with the deployed
+inclusion verifier is supported by finite differential testing over the pinned
+families. The deployed consistency verifier is not extensionally equal to the
+model; applying the mechanized soundness result to the deployed consumer flow
+additionally relies on an unmechanized authentic-size/root invariant
+(KNOWN-GAPS 14/15).
+\end{quote}
+Its exclusions name SHA-256 collision resistance, deployed-verifier extensional
+equality, the signature/STH layer, and asymptotic cost claims.
+
+\section{Compact receipt-verification core}\label{app:verifier}
+The following code is only the Merkle inclusion core. A complete receipt
+verifier must additionally validate the signed tree head, log identifier,
+tree-size binding, public-key fingerprint or pinned key, leaf hash, and receipt
+schema. The published log-repository verifier implements that full binding
+list and fails closed when signature checking is unavailable.
+\begin{lstlisting}[language=Python]
+import hashlib
+
+def H(data):
+    return hashlib.sha256(data).digest()
+
+def h_leaf(data):
+    return H(b"\x00" + data)
+
+def h_node(left, right):
+    return H(b"\x01" + left + right)
+
+def split_below(n):
+    return 1 << ((n - 1).bit_length() - 1)
+
+def root(value, index, size, path, used=0):
+    if size == 1:
+        return value, used
+    k = split_below(size)
+    if used >= len(path):
+        raise ValueError("proof exhausted")
+    if index < k:
+        left, used = root(value, index, k, path, used)
+        return h_node(left, path[used]), used + 1
+    right, used = root(value, index-k, size-k, path, used)
+    return h_node(path[used], right), used + 1
+
+def verify_inclusion(leaf, index, size, path, expected_root):
+    if size <= 0 or index < 0 or index >= size:
+        return False
+    try:
+        result, used = root(h_leaf(leaf), index, size, path)
+    except ValueError:
+        return False
+    return used == len(path) and result == expected_root
+\end{lstlisting}
+
+\section{Four Ed25519 verification tiers}\label{app:tiers}
+\begin{center}\small
+\begin{tabular}{@{}lll@{}}
+\toprule
+Tier & Meaning & Upstream Lean declaration \\
+\midrule
+T1 & byte-level acceptance equation & \code{verify_accepts_iff} \\
+T2 & canonical encoding lift & \code{verify_accepts_iff_point} \\
+T3 & injectivity / point equation & \code{verify_accepts_iff_point_eq} \\
+T4 & constructive decompression lift & \code{verify_accepts_iff_decompress} \\
 \bottomrule
 \end{tabular}
 \end{center}
-All four are proven under the wire-format hypotheses $\mathcal{W}$ of
-\S\ref{sec:corpus}; a consumer reasoning about the underlying group
-element relies on their conjunction (the ladder up to T4), and all four
-cones are audited against the same per-fork boundary of
-Appendix~\ref{app:axioms}.
 
 \end{document}
diff --git a/provider/src/pacta_provider/web.py b/provider/src/pacta_provider/web.py
index 4839412..301f241 100644
--- a/provider/src/pacta_provider/web.py
+++ b/provider/src/pacta_provider/web.py
@@ -46,12 +46,15 @@ def make_handler(log: TransparencyLog, base_path: str, docs_html: str, paper_pdf
             if route in ("/", "/docs"):
                 self._send_html(docs_html)
             elif route in ("/paper", "/paper/ltl.pdf",
-                           "/paper/v0.1", "/paper/v0.1/ltl.pdf"):
-                # /paper is the current (revised) paper; /paper/v0.1 the prior
-                # version - preserved for citability, linked from the docs page.
+                           "/paper/v0.1", "/paper/v0.1/ltl.pdf",
+                           "/paper/v0.2", "/paper/v0.2/ltl.pdf"):
+                # /paper is the current paper; /paper/v0.N are prior versions,
+                # preserved for citability, linked from the docs page.
                 variant = "current"
                 if route.startswith("/paper/v0.1"):
                     variant = "v0.1"
+                elif route.startswith("/paper/v0.2"):
+                    variant = "v0.2"
                 body = paper_pdfs.get(variant)
                 if body is None:
                     self._send(404, {"error": f"paper ({variant}) not available on this deployment"})
@@ -226,8 +229,9 @@ def serve(
         docs_html = render_docs(log, base_path)
     paper_dir = Path(__file__).resolve().parents[3] / "paper"
     variants = {
-        "current": paper_dir / "ltl.pdf",       # revised paper, the live one
+        "current": paper_dir / "ltl.pdf",       # v0.3 reinvention, the live one
         "v0.1": paper_dir / "ltl-v0.1.pdf",     # prior 4-page version
+        "v0.2": paper_dir / "ltl-v0.2.pdf",     # prior 19-page system report
     }
     paper_pdfs = {name: p.read_bytes() for name, p in variants.items() if p.is_file()}
     handler = make_handler(log, base_path, docs_html, paper_pdfs)
diff --git a/provider/src/pacta_provider/webdocs.py b/provider/src/pacta_provider/webdocs.py
index 66e97e5..df18590 100644
--- a/provider/src/pacta_provider/webdocs.py
+++ b/provider/src/pacta_provider/webdocs.py
@@ -290,15 +290,17 @@ our roadmap.</strong> (The full walk-through is lecture&nbsp;11 in the
 <a href="https://github.com/saymrwulf/proof-aware-crypto-tooling-agent">course</a>.)</div>
 
 <h2>The paper</h2>
-<div class="card"><a href="{base}/paper"><strong>The Lean Transparency Log: Distributing
-Kernel-Checked Correctness Evidence for Deployed Ed25519 Implementations</strong></a>
-(PDF, 19 pages, revised) — the trust model with an explicit malicious-operator adversary,
-security proofs for every consumer-facing claim (inclusion soundness as an explicit
-SHA-256-collision extractor, pin-store safety with transferable equivocation evidence,
-verdict integrity), the self-referential signing loop, the live deployment with
-its retained failure leaves, and appendices with the leaf schema, the full ~25-line
-consumer verifier, and the verbatim per-fork axiom boundaries.
-<span class="muted">Previous version: <a href="{base}/paper/v0.1">v0.1</a> (4 pages).</span></div>
+<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, 16 pages, v0.3) — 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, the policy
+boundary where operator labels can veto but never grant acceptance, the live thirteen-leaf
+deployment whose entry 13 attests the accumulator's own mechanized model, and the measured
+model/deployment seam (3,867 one-sided lied-size divergences) reported as a result rather
+than hidden.
+<span class="muted">Previous versions: <a href="{base}/paper/v0.2">v0.2</a> (19 pages, the
+system report) · <a href="{base}/paper/v0.1">v0.1</a> (4 pages).</span></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 course (12 Jupyter