Paper v2: author, the mathematics, and a figure that survives being looked at

Review feedback applied:

- Author: Olaf Horvath.
- New "What the certificates state" block in the introduction - the
  actual mathematics the Lean proving is about, kept compact: the
  radix-51 denotation, a representative two-clause specification
  (value + invariant preservation for mul), the complete twisted
  Edwards addition law with the d-non-square completeness fact, and
  both apex tiers as single-line equivalences
  (accept <=> compress([s]B-[k]A) = R; accept <=> decompress(R) =
  [k](-A)+[s]B) with the hash oracle's role stated inline.
- The figure was genuinely broken (leaf boxes overlapped - box width
  exceeded spacing - and the annotation collided with a node); this
  time it was inspected VISUALLY, not just for build warnings.
  Redrawn as a full-width figure*: generous spacing, grey failed-run
  leaves labeled "retained forever", bold leaf 4, the dashed
  self-certification loop routed through clear space, and the float
  relocated in source so it lands on page 3 beside the deployment
  section instead of drifting to the references page.
- Held the 4-page line through prose trims (intro paragraphs, related
  work, deployment opening) and a compact accept() notation; zero
  build errors, one 0.66pt overfull in a bibliography line.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

paper/ltl.tex

@@ -1,5 +1,5 @@
 \documentclass[10pt,twocolumn]{article}
-\usepackage[margin=1.9cm,bottom=2.2cm]{geometry}
+\usepackage[margin=1.7cm,bottom=2.1cm]{geometry}
 \usepackage[T1]{fontenc}
 \usepackage{lmodern}
 \usepackage{microtype}
@@ -11,12 +11,14 @@
 \usepackage[hidelinks]{hyperref}
 \usepackage{xcolor}
 \newcommand{\code}[1]{\texttt{\small #1}}
+% poor-man's semantic brackets (stmaryrd unavailable in minimal TeX trees)
+\newcommand{\den}[1]{[\![#1]\!]}
 \setlength{\columnsep}{0.8cm}
 
 \title{\textbf{LTL: the Lean Transparency Log}\\[2pt]
 \large Distributing Machine-Checked Proof Evidence via an Authenticated
 Data Structure Signed by Its Own Certified Artifact}
-\author{saymrwulf\\ \small zkdefi.org --- \url{https://zkdefi.org/lean-transparency-log}}
+\author{Olaf Horvath\\ \small zkdefi.org --- \url{https://zkdefi.org/lean-transparency-log}}
 \date{July 2026}
 
 \begin{document}
@@ -74,37 +76,111 @@ verification~\cite{ed25519,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$.
 
-The economics of \emph{consuming} such evidence are poor. Re-checking
+\paragraph{What the certificates state.} Concretely, the corpus is a
-one fork's certificates takes $\approx$30 minutes of Lean kernel time on
+stack of theorems about extracted code, each stated through a
-commodity hardware and requires a pinned toolchain. A wallet
+\emph{denotation} from machine representation to mathematics. Field
-application, a package manager, or an autonomous agent choosing a
+elements are five 51-bit limbs denoting
-cryptographic backend cannot pay this per decision---and should not have
+$\den{(a_0,\dots,a_4)}=\sum_i a_i2^{51i}\bmod p$, and every
-to: the result of a deterministic re-check is a fact that can be
+operation carries a two-clause specification---the value is right
-attested once and then distributed.
+\emph{and} the representation invariant is preserved, e.g.
+\begin{align*}
+\footnotesize
+\forall a\,b.\ &\mathrm{bnd}\,a \Rightarrow \mathrm{bnd}\,b \Rightarrow{}\\[-2pt]
+&\exists c.\ \code{mul}\,a\,b = \code{ok}\,c \,\wedge\, \mathrm{bnd}\,c
+\,\wedge\, \den{c} = \den{a}\cdot\den{b}.
+\end{align*}
+Point operations are proven to implement the complete twisted Edwards
+addition law on
+$E : -x^2+y^2 = 1+d\,x^2y^2$ over $\mathbb{F}_p$,
+\begin{equation*}
+\small
+(x_1,y_1)+(x_2,y_2)=
+\Bigl(\tfrac{x_1y_2+x_2y_1}{1+d\,x_1x_2y_1y_2},\;
+\tfrac{y_1y_2+x_1x_2}{1-d\,x_1x_2y_1y_2}\Bigr),
+\end{equation*}
+including the completeness fact that makes it branch-free ($d$ is a
+non-square, so the denominators never vanish~\cite{bernsteinlange}).
+At the apex, writing $\code{accept}(A,m,R,s)$ for ``the extracted
+verifier returns \code{ok}'', with $k$ the scalar produced by the hash
+oracle $H(R,A,m)$ and no properties assumed of $H$, the byte-level tier
+states
+\begin{equation*}
+\footnotesize
+\code{accept}(A,m,R,s) \;\Leftrightarrow\; \code{compress}([s]B-[k]A) = R,
+\end{equation*}
+and the strongest tier lifts byte equality to the group:
+\begin{equation*}
+\footnotesize
+\code{accept}(A,m,R,s) \;\Leftrightarrow\; \code{decompress}(R) = [k](-A)+[s]B,
+\end{equation*}
+with decompression itself proven (exact byte parsing, the
+$(p{+}3)/8$-power square root, sign-bit root selection). Each theorem's
+axiom cone is pinned exactly---the standard three below the apex, the
+enumerated oracle boundary at the apex tiers.
 
-This is the classic transparency-log trade. Certificate
+The economics of \emph{consuming} such evidence are poor: re-checking
-Transparency~\cite{rfc6962,rfc9162} made certificate issuance publicly
+one fork's certificates takes $\approx$30 minutes of Lean kernel time
-auditable; Sigstore's Rekor~\cite{sigstore} did the same for software
+and a pinned toolchain. A wallet, a package manager, or an autonomous
-signing events and supply-chain attestations~\cite{intoto}; key
+agent choosing a cryptographic backend cannot pay this per
-transparency systems~\cite{coniks} for identity bindings; Go's checksum
+decision---and need not: a deterministic re-check yields a fact that can
-database for module hashes. The LTL applies the same authenticated data
+be attested once and distributed.
-structure to a payload with different trust semantics: \emph{evidence of
-machine-checked mathematical truth, together with its exact assumption
-set}. We do not claim novelty for any component---the hash structure and
-proof algorithms are RFC~9162 verbatim; the contribution is the
-composition, its trust model, and a deployed, reproducible instance.
 
-Concretely, this paper describes: the attestation format and the
+This is the classic transparency-log trade---Certificate
-\emph{observation-not-verdict} trust model
+Transparency~\cite{rfc6962,rfc9162} for certificate issuance, Sigstore's
-(\S\ref{sec:log}); boundary-exact axiom auditing
+Rekor~\cite{sigstore} for signing events and supply-chain
-(\S\ref{sec:log}); the self-referential signing loop
+attestations~\cite{intoto}, key transparency~\cite{coniks}, checksum
-(\S\ref{sec:dogfood}); the deployment and what its evidence
+databases---applied to a payload with different trust semantics:
-establishes (\S\ref{sec:deploy}); and the verification agenda for
+\emph{evidence of machine-checked mathematical truth, together with its
-the log itself (\S\ref{sec:next}).
+exact assumption set}. We claim no novelty for any component (the hash
+structure and proof algorithms are RFC~9162 verbatim); the contribution
+is the composition, its trust model, and a deployed, reproducible
+instance.
+
+\S\ref{sec:log} describes the log and its trust model,
+\S\ref{sec:dogfood} the self-referential signing loop,
+\S\ref{sec:deploy} the deployment and what its evidence establishes,
+and \S\ref{sec:next} the verification agenda for the log itself.
 
 \section{The Lean Transparency Log}
 \label{sec:log}
 
+\begin{figure*}[t]
+\centering
+\begin{tikzpicture}[every node/.style={font=\small}]
+  \tikzset{box/.style={draw, rounded corners=2pt, minimum width=1.6cm, minimum height=0.56cm}}
+  % leaves: 0-3 failed run (gray), 4-7 verified (black)
+  \foreach \i/\c in {0/gray, 1/gray, 2/gray, 3/gray, 4/black, 5/black, 6/black, 7/black}
+    \node[box, draw=\c, text=\c] (l\i) at (\i*2.05,0) {leaf \i};
+  \node[box, draw=black, very thick, fill=black!6] at (4*2.05,0) {\textbf{leaf 4}};
+  \node[text=gray, font=\footnotesize] at (3*2.05/2 - 1.02,-0.62) {failed-audit run --- retained forever};
+  \node[font=\footnotesize] at (5.5*2.05 + 0.35,-0.62) {verified attestations (16/16, boundary-exact)};
+  % internal nodes
+  \foreach \i in {0,...,3}
+    \node[box] (m\i) at (\i*4.1+1.025,1.25) {node};
+  \foreach \i in {0,1}
+    \node[box] (n\i) at (\i*8.2+3.075,2.5) {node};
+  \node[box, thick] (root) at (7.175,3.75) {root};
+  \foreach \a/\b in {l0/m0, l1/m0, l2/m1, l3/m1, l4/m2, l5/m2, l6/m3, l7/m3,
+                     m0/n0, m1/n0, m2/n1, m3/n1, n0/root, n1/root}
+    \draw[gray!70] (\a) -- (\b);
+  % signature head
+  \node[box, thick, minimum width=5.2cm] (sig) at (7.175,4.95)
+    {signed tree head: $\mathrm{Ed25519}(\mathrm{root})$};
+  \draw[-{Stealth}] (root) -- (sig);
+  % the self-certification loop, routed through clear space on the right
+  \draw[-{Stealth}, thick, dashed]
+    (sig.east) .. controls (13.2,4.95) and (12.4,1.6) .. (l4.north east);
+  \node[align=left, font=\footnotesize, anchor=west] at (12.45,3.1)
+    {signed by the binary built\\ from the source attested at\\ leaf 4; the operator verifies\\ that leaf's inclusion first};
+\end{tikzpicture}
+\caption{The deployed 8-leaf log. Leaves 0--3 record an early replay whose
+audit step failed (two tooling defects, since fixed); an append-only ledger
+retains them. The tree head is signed by a binary built from the
+implementation attested at leaf 4, and each signature embeds the operator's
+own inclusion check of that leaf against the tree being signed.}
+\label{fig:loop}
+\end{figure*}
+
 \paragraph{Roles.} 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
@@ -199,44 +275,7 @@ First-append bootstrapping is handled honestly: heads signed before the
 signing library's attestation enters the log record
 \code{self\_inclusion:\ library\_not\_in\_log}.
 
-\begin{figure}[t]
+
-\centering
-\begin{tikzpicture}[scale=0.74, every node/.style={font=\scriptsize}]
-  \tikzset{leaf/.style={draw, rounded corners=1pt, minimum width=0.92cm, minimum height=0.42cm}}
-  % leaves
-  \foreach \i/\x/\c in {0/0/gray, 1/1.05/gray, 2/2.1/gray, 3/3.15/gray,
-                        4/4.2/black, 5/5.25/black, 6/6.3/black, 7/7.35/black}
-    \node[leaf, draw=\c, text=\c] (l\i) at (\x,0) {leaf \i};
-  % highlight leaf 4
-  \node[leaf, draw=black, very thick, fill=black!5] (l4) at (4.2,0) {\textbf{leaf 4}};
-  \node[anchor=north, text=gray] at (1.575,-0.30) {failed-audit run, retained};
-  \node[anchor=north] at (5.775,-0.30) {verified attestations};
-  % internal nodes
-  \foreach \i/\x in {0/0.525, 1/2.625, 2/4.725, 3/6.825}
-    \node[leaf] (m\i) at (\x,0.95) {node};
-  \foreach \i/\x in {0/1.575, 1/5.775}
-    \node[leaf] (n\i) at (\x,1.9) {node};
-  \node[leaf, thick] (root) at (3.675,2.85) {root};
-  \foreach \a/\b in {l0/m0, l1/m0, l2/m1, l3/m1, l4/m2, l5/m2, l6/m3, l7/m3,
-                     m0/n0, m1/n0, m2/n1, m3/n1, n0/root, n1/root}
-    \draw[gray!60] (\a) -- (\b);
-  % signature box
-  \node[leaf, thick, minimum width=3.4cm] (sig) at (3.675,3.75)
-    {signed head: $\mathrm{Ed25519}(\mathrm{root})$};
-  \draw[-{Stealth}] (root) -- (sig);
-  % the loop
-  \draw[-{Stealth}, thick, dashed] (sig.east) .. controls (8.15,3.4) and (8.15,0.6) ..
-    (l4.north east);
-  \node[align=left, anchor=west, font=\tiny] at (7.35,2.15)
-    {signed by the binary\\ built from the source\\ attested at leaf 4;\\ inclusion self-checked};
-\end{tikzpicture}
-\caption{The deployed 8-leaf log. Leaves 0--3 record an early replay
-whose audit step failed (two tooling defects, since fixed); an
-append-only ledger retains them. The head is signed by a binary built
-from the implementation attested at leaf 4, whose inclusion the
-operator verifies before signing.}
-\label{fig:loop}
-\end{figure}
 
 \section{Deployment and evidence}
 \label{sec:deploy}
@@ -249,11 +288,10 @@ Operator/consumer tooling and a twelve-lecture course:
 underlying proof corpora are in the \code{saymrwulf/*-ed25519-verified}
 repositories; every claim in this paper is re-checkable from these
 artifacts.} with eight leaves: one attestation per fork from each of two
-full replay runs. Each replay re-checked $\approx$64 Lean files per fork
+full replay runs ($\approx$64 Lean files and $\approx$1{,}800\,s per
-($\approx$1{,}800\,s per fork under hard memory caps and core pinning)
+fork, under hard memory caps and core pinning). In the second run all
-and audited all 16 certificates; in the second run all four forks
+four forks reported 16/16 certificates proven with boundary-exact cones,
-reported 16/16 proven with boundary-exact cones, pinned to exact
+pinned to exact commits. The first run is deliberately still in the log: its audit step
-commits. The first run is deliberately still in the log: its audit step
 failed due to two defects in the \emph{operator tooling} (a path issue
 and a parser that mishandled Lean's line-wrapped axiom lists for the
 eleven-axiom cones), and the operator signed attestations recording the
@@ -307,7 +345,7 @@ in-toto~\cite{intoto} link metadata; its payloads attest \emph{process}
 kernel-checked \emph{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 accumulator pattern with different payloads. Proof-carrying
+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
@@ -360,7 +398,8 @@ and this paper were produced with substantial assistance from Claude
 (Anthropic). All claims are enforced by the referenced check scripts and
 are independently re-checkable from the public artifacts.
 
-\begin{thebibliography}{19}\small
+\begin{thebibliography}{19}\footnotesize
+\setlength{\itemsep}{1pt}
 
 \bibitem{rfc6962} B.~Laurie, A.~Langley, E.~K\"asper.
 \emph{Certificate Transparency}. RFC 6962, 2013.