Didactic mentorship revision: the ratchet rule, stated and honored

The owner's requirement, now the book's explicit contract (new "ratchet
rule" box in chapter 1): every load-bearing idea is worked at least
twice - once at napkin scale (mod 13, inverses by scanning) and once at
REAL scale, the actual 77-digit Ed25519 constants printed in full with
no digits hidden and no artificial zeros; where raw size genuinely
exceeds paper (a 77-digit square root), the book says so and teaches
witness-auditing instead of pretending.

Socratic audit result: chapters 1-11 already honor the rule (verified
rung by rung - e.g. ch6 pairs the Z/12 clock with 19^-1 mod the real p;
ch7 pairs Pratt-for-97 with costing the real certificate; ch8 runs the
extracted model at the real envelope edge). The gaps were ch12's three
summit rungs, which had NO numeric examples at all. Filled:

- Group law: "running the addition law by hand - napkin curve, then the
  real one". Doubling (2,4)->(10,11) mod 13 in full; then the real base
  point with x1, y1 printed in 5-digit groups, the first machine step
  certified as x1*y1 = q*p + u with the 77-digit witness q printed, and
  the student auditing it by casting out nines AND elevens (both clocks
  close: 3=3, 1=1). Lands on the real 2B coordinates.
- Scalars: the cycle felt on the napkin curve first (order 16, so
  21P = 5P) before the real prime ell.
- Apex: "decompression, run twice". Encode/decode (10,11) as "(11,
  even)" mod 13 - x^2 = 3/9 = 9, roots {3,10}, parity picks 10; then
  the real compressed base point: all 32 bytes printed (58 66...66),
  byte 31 = 0x66 sign-bit read, y_B printed in full, and the
  no-shortcuts full-size hand verification 5*y_B - 4 = 4*p, both
  78-digit sides printed for digit-by-digit comparison. The square
  root honestly declared machine territory, with the witness-checked
  certificate named.
- New paper exercise 12.4 (+pathway/solution): encode & decompress
  3P = (6,10) solo - the wrong root lands on -3P, one bit doing real
  cryptographic work.

Every printed constant machine-verified before typesetting (base point
on-curve, q*p+u exact, 5y-4 = 4p exact, 2B on-curve, toy order 16).
PDF rebuilt: 109 pages, zero errors. Honesty ledger records the
revision.

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

README.md

@@ -5,18 +5,18 @@ background** — from `1 + 1 = 2` to reading (and extending) real,
 machine-checked proofs that production elliptic-curve code is correct.
 
 This is the educational companion to a family of verification projects in
-which the arithmetic core of Ed25519 (from
+which complete Ed25519 proof pyramids (from
 [curve25519-dalek](https://github.com/dalek-cryptography/curve25519-dalek)
-and three production forks) and the Pasta curves' field layer were
+and three production forks — field, group law, scalars, and the signature
-machine-checked in Lean 4 against models extracted from the actual Rust
+verifier itself) and the Pasta curves' field layer were machine-checked in
-sources:
+Lean 4 against models extracted from the actual Rust sources:
 
 | Companion project | What is verified there |
 |---|---|
-| [dalek-ed25519-verified](https://github.com/saymrwulf/dalek-ed25519-verified) | field 𝔽ₚ + Edwards group law + scalar foundations, upstream dalek |
+| [dalek-ed25519-verified](https://github.com/saymrwulf/dalek-ed25519-verified) | the complete pyramid, upstream dalek: field 𝔽ₚ + Edwards group law + scalar arithmetic mod ℓ + the four-tier signature apex (accept ⇔ decompress(R) = [k](−A)+[s]B, hash opaque) |
-| [anza-ed25519-verified](https://github.com/saymrwulf/anza-ed25519-verified) | same layers, Solana's fork, its own extraction |
+| [anza-ed25519-verified](https://github.com/saymrwulf/anza-ed25519-verified) | the complete pyramid, Solana's fork, its own extraction |
-| [risc0-ed25519-verified](https://github.com/saymrwulf/risc0-ed25519-verified) | same layers, RISC Zero's fork |
+| [risc0-ed25519-verified](https://github.com/saymrwulf/risc0-ed25519-verified) | the complete pyramid, RISC Zero's fork |
-| [betrusted-ed25519-verified](https://github.com/saymrwulf/betrusted-ed25519-verified) | same layers, Betrusted's fork |
+| [betrusted-ed25519-verified](https://github.com/saymrwulf/betrusted-ed25519-verified) | the complete pyramid, Betrusted's fork |
 | [pasta-pallas-verified](https://github.com/saymrwulf/pasta-pallas-verified) | Pallas modulus primality (Lucas/Pratt), Montgomery foundations |
 | [formal-verification-control](https://github.com/saymrwulf/formal-verification-control) | the method: invariants, terrain map, failure map, tooling |
 
@@ -103,6 +103,23 @@ In the spirit of Chapter 11:
 - The book's claims about the companion projects (what is proven, what is
   frontier) mirror those repos' own READMEs and TRUSTED-BASE ledgers at the
   time of writing; the repos, not this book, are the source of truth.
+  Re-audited 2026-07-06 after the signature apex reached its final
+  four-tier form (coherence pass 4): chapter 12's status diagram, apex
+  section, and audit-drill solution, chapter 11's boundary example,
+  chapter 8's extraction notes, the repo tour, and this table were
+  brought up to the proven state.
+- Didactic revision (2026-07-06, same day): the book now states and keeps
+  a "ratchet rule" (chapter 1) — every load-bearing idea worked at napkin
+  scale AND at real scale with the full 77-digit constants printed,
+  nothing elided. Chapter 12 gained the missing rungs: the addition law
+  run by hand on a mod-13 curve and then on the real base point (with a
+  machine-supplied quotient witness audited by casting out nines and
+  elevens), the scalar cycle felt on the napkin curve, decompression run
+  twice (mod-13 sign-bit walk, then the real compressed base point:
+  byte-31 sign bit, and the full-size hand verification 5·y_B − 4 = 4·p,
+  every digit printed), plus a new paper exercise (12.4). Every printed
+  constant was machine-verified before typesetting; the PDF (109 pages)
+  is rebuilt from these sources.
 - The PDF in the repo is built from the committed sources by the command
   above; rebuild it yourself if you don't trust binaries (good instinct).
 - The three named solution certificates were kernel-audited

chapters/appendix-repo-tour.tex

@@ -20,9 +20,9 @@ where Montgomery form demands it.
 the honest-boundary statements of Chapter~\ref{ch:honesty} \\
 \code{TRUSTED-BASE.md} & the ledger: every assumption, each with its
 reason --- read this \emph{before} being impressed by anything \\
-\code{verification/extract.sh} & extraction roots for the field layer
+\code{verification/extract.sh} & the extraction recipe (Charon $\to$
-(Charon $\to$ LLBC $\to$ Aeneas); \code{extract-scalar.sh} likewise for
+LLBC $\to$ Aeneas): ONE merged universe per repo --- field, curve,
-scalars \\
+scalar, and the verify path --- plus the signature glue \\
 \code{verification/gen/} & the extracted model. \textbf{Never
 hand-edited} (Chapter~\ref{ch:rust}); regenerated or left alone \\
 \code{verification/Proofs/} & the human-written theorems ---
@@ -58,10 +58,11 @@ you audited in Chapter~\ref{ch:field}'s worked example.
 (\code{fieldImplementation}) and its \lean{\#print axioms} line. This
 is the artifact all the marketing language ultimately refers to; note
 how unglamorous it looks.
-\item \textbf{The frontier} --- the scalar layer's in-progress files,
+\item \textbf{The apex} --- \code{verify\_accepts\_iff\_decompress}
-clearly marked. Read one open lemma statement and recognize its shape
+in \code{Proofs/DecompressMain.lean}, the top of the four-tier stack,
-(it is 9.B with bigger constants). This is where
+and the check script's boundary phase that guards its axiom cone. Note
-Chapter~\ref{ch:pyramid}'s invitation points.
+how short the capstone proof is: every hard fact was certified below it.
+This is where Chapter~\ref{ch:pyramid}'s invitation points.
 \end{enumerate}
 
 \section{Running the machinery}
@@ -91,7 +92,9 @@ mechanical half of the Chapter~\ref{ch:honesty} field guide, automated.
 unlike source text, cannot be hidden in comments. \emph{Phase 3 is the
 one-command audit}, run on every certificate, every time, so the
 axiom-clean property is continuously enforced rather than occasionally
-asserted.
+asserted. A fourth phase arrived with the signature layer: \emph{3b pins
+the apex tiers' cones to the documented hash/wire-format boundary
+EXACTLY} --- an unexpected addition \emph{or removal} fails the build.
 
 \section{The control repository}
 

chapters/ch01-why-verify.tex

@@ -167,7 +167,7 @@ one abstraction level and rests on the layer beneath it:
   \node[note] at (5.6,0)    {limbs, carries, multiplication};
   \node[note] at (5.6,1.15) {point addition is complete \& correct};
   \node[note] at (5.6,2.3)  {the group order $\ell$, reduction};
-  \node[note] at (5.6,3.45) {the equation $8sB = 8R + 8kA$};
+  \node[note] at (5.6,3.45) {the equation $sB = R + kA$,\\ checked from the raw bytes};
 \end{tikzpicture}
 \end{center}
 
@@ -187,6 +187,20 @@ proofs at every layer of this pyramid. The journey looks like this:
   ethics of axioms and honest boundaries, and the layers above.
 \end{itemize}
 
+\begin{bigidea}
+\textbf{The ratchet rule of this book.} Every load-bearing idea is worked
+at least twice: once at \emph{napkin scale} (a modulus like $13$, numbers
+you can invert by scanning), and once at \emph{real scale} --- the actual
+77-digit constants of Ed25519, printed in full, with no digits hidden and
+no artificial zeros. The napkin run teaches the moves; the real-size run
+proves the moves are the whole story, because they are \emph{identical} ---
+only the digits get longer, and wherever raw size genuinely exceeds paper
+(a 77-digit square root, say) the book says so explicitly and shows you
+how to audit the machine's work instead (witnesses, small clocks,
+certificates). If a step ever feels like a leap, back up one worked
+example: the missing rung is there, at the smaller size.
+\end{bigidea}
+
 \section{Proofs versus tests: the honest comparison}
 
 Formal verification is not magic, and this book will never pretend otherwise.

chapters/ch08-rust-to-lean.tex

@@ -178,13 +178,15 @@ companion projects:
 \begin{itemize}[leftmargin=1.4em]
 \item \textbf{Extract functions, not crates.} Charon accepts specific roots
   (individual functions and impls); the extraction scripts in each companion
-  repo (\code{extract.sh}, \code{extract-scalar.sh}) name exactly the
+  repo (\code{extract.sh}) name exactly the needed roots and get one
-  arithmetic functions and get a small, clean model --- 28 definitions
+  small, clean, merged model per repo --- dozens of definitions instead
-  instead of a thousand.
+  of a thousand.
-\item \textbf{Some code will not translate.} The dalek scalar-multiplication
+\item \textbf{Some code will not translate.} The dalek SIMD backends use
-  backends use CPU-specific SIMD intrinsics no translator models. The
+  CPU-specific intrinsics no translator models. The boundary is then
-  boundary is then \emph{documented}: those functions enter the trusted base,
+  \emph{engineered} rather than assumed: extraction pins the serial
-  stated as assumptions, visible in every audit. Honest boundaries beat
+  backend --- real, translatable code the campaign proved like everything
+  else --- and the SIMD alternatives are scoped out of the verified
+  claim, the scoping documented in the ledger. Honest boundaries beat
   heroic fictions (Chapter~\ref{ch:honesty} dwells on this).
 \item \textbf{Pin your tools.} The pipeline records exact versions of
   Charon, Aeneas, and Lean. A model regenerated with a different translator

chapters/ch11-honesty-and-axioms.tex

@@ -190,8 +190,13 @@ axiom sha512_spec : ∀ msg, Sha512.hash msg = SHA512_ideal msg
 \end{lstlisting}
 
 A signature-layer certificate honestly reads: \emph{EdDSA verification is
-correct, GIVEN the hash behaves ideally and GIVEN the documented backend
+correct, GIVEN the declared oracles} --- with every \emph{given}
-assumptions} --- with both \emph{given}s machine-visible. Compare the two
+machine-visible. The companion repos push the posture one step further
+than this example: their SHA-512 is opaque with \emph{no properties
+assumed at all} --- not even ``behaves ideally''; the apex theorems hold
+for whatever bytes it produces --- and the backend question was
+\emph{eliminated} rather than assumed (extraction pins the serial path,
+which is real translated code, proven like everything below it). Compare the two
 postures: ``everything verified!'' (and hope nobody checks) versus ``these
 two assumptions, this ledger, audit me'' --- the second is both humbler and
 \emph{stronger}, because its claim survives the audit.

chapters/ch12-the-pyramid.tex

@@ -20,8 +20,8 @@ and the keys.
   \node[lay,fill=codebg,minimum width=10.2cm]     (fld) at (0,0)    {\textbf{Field $\Fp$}};
   \node[st] at (5.7,0)    {\textbf{done}: certificates in 4 repos, axiom-clean};
   \node[st] at (5.7,1.25) {\textbf{done}: complete addition, all 4 forks};
-  \node[st] at (5.7,2.5)  {\textbf{in progress}: foundations proven,\\ mul at the kernel frontier};
+  \node[st] at (5.7,2.5)  {\textbf{done}: add, sub, Montgomery mul\\ certified, all 4 forks};
-  \node[st] at (5.7,3.75) {\textbf{ahead}: awaits scalars;\\ hash axiomatized by design};
+  \node[st] at (5.7,3.75) {\textbf{done}: accept $\Leftrightarrow$ decompress$(R) = [k](-A){+}[s]B$;\\ hash an opaque oracle by design};
 \end{tikzpicture}
 \end{center}
 
@@ -47,6 +47,79 @@ Bernstein and Lange, is a jewel of quiet algebra: if a denominator vanished,
 $d$ would have to be a square in $\Fp$ --- and it is not, which is a
 \lean{decide}-scale fact away from primality.)
 
+\begin{worked}{running the addition law by hand --- napkin curve, then the real one}
+Two runs of the same formula: first on numbers that fit a napkin, then on
+the real 77-digit constants with nothing hidden. \emph{The moves are
+identical; only the digits get longer.}
+
+\emph{Run 1 --- the napkin curve.} Work mod $13$ with $d = 2$ (a
+non-square mod $13$: the squares are $\{1,3,4,9,10,12\}$ --- so this toy
+inherits the real curve's completeness, as the worked example below
+derives). The point $P = (2,4)$ is on the curve: $-4 + 16 = 12$ and
+$1 + 2\cdot 4\cdot 16 = 129 \equiv 12$ \checkmark. Now double it. The
+shared product first: $d\,x^2 y^2 = 2 \cdot 4 \cdot 16 = 128 \equiv 11$.
+Then
+\[
+x_3 \;=\; \frac{2xy}{1 + 11} \;=\; \frac{16}{12} \;\equiv\; 3 \cdot 12^{-1}
+\;=\; 3\cdot 12 \;=\; 36 \;\equiv\; 10,
+\qquad
+y_3 \;=\; \frac{y^2\!+\!x^2}{1 - 11} \;=\; \frac{20}{3} \;\equiv\; 7\cdot 3^{-1}
+\;=\; 7 \cdot 9 \;=\; 63 \;\equiv\; 11
+\]
+(the inverses by scanning: $12\cdot 12 = 144 \equiv 1$, $3\cdot 9 = 27
+\equiv 1$). So $2P = (10, 11)$ --- and recheck it is on the curve:
+$-100+121 = 21 \equiv 8$; $1 + 2\cdot(100\cdot 121) \equiv 1 + 2\cdot(9
+\cdot 4) = 73 \equiv 8$ \checkmark. Keep $(10,11)$; the apex section will
+want it.
+
+\emph{Run 2 --- the real base point, full digits.} The same doubling, on
+Ed25519's base point $B = (x_1, y_1)$:
+\par\noindent{\footnotesize $x_1 \;=$}\\[-2pt]
+{\footnotesize\ttfamily\begin{tabular}{@{}l@{}}15\,11222\,13495\,35400\,77250\,11514\,09588\,53151\,14540\\
+12693\,04185\,72060\,46113\,28394\,98477\,62202\end{tabular}}\par\smallskip
+\par\noindent{\footnotesize $y_1 \;=$}\\[-2pt]
+{\footnotesize\ttfamily\begin{tabular}{@{}l@{}}46\,31683\,56949\,26478\,16942\,83940\,03475\,16314\,13079\\
+93866\,25622\,56157\,83033\,60316\,52518\,55960\end{tabular}}\par\smallskip
+The machine's first step is the product $u = x_1 y_1 \bmod p$. Nobody
+multiplies two 77-digit numbers by hand --- and nobody needs to, because
+the machine can hand you its homework for auditing: the quotient $q$ and
+remainder $u$ it claims, turning the step into one integer equation
+\[
+x_1 \cdot y_1 \;=\; q \cdot p + u ,
+\]
+\par\noindent{\footnotesize $q \;=$}\\[-2pt]
+{\footnotesize\ttfamily\begin{tabular}{@{}l@{}}12\,08977\,70796\,28320\,61800\,09211\,27670\,82520\,91632\\
+10154\,43348\,57648\,36890\,62715\,98782\,09761\end{tabular}}\par\smallskip
+\par\noindent{\footnotesize $u \;=$}\\[-2pt]
+{\footnotesize\ttfamily\begin{tabular}{@{}l@{}}46\,82740\,38508\,23179\,24507\,22166\,30277\,19756\,51442\\
+05554\,12565\,49766\,74165\,82953\,38171\,01731\end{tabular}}\par\smallskip
+which Chapter~\ref{ch:modular}'s shadow arithmetic audits on two
+independent small clocks. Digit sums (clock $9$): $x_1 \to 3$,
+$y_1 \to 1$, $q \to 0$, $p \to 7$, $u \to 3$; left side $3\cdot 1 = 3$,
+right side $0 \cdot 7 + 3 = 3$ \checkmark. Alternating digit sums (clock
+$11$, signs from the units digit up): $x_1 \to 5$, $y_1 \to 9$,
+$q \to 10$, $p \to 2$, $u \to 3$; left $5 \cdot 9 = 45 \equiv 1$, right
+$10 \cdot 2 + 3 = 23 \equiv 1$ \checkmark. Do the digit sums yourself ---
+each is two careful minutes over the blocks printed above; that labor
+\emph{is} the pen-and-paper content at this size. Five more certified
+steps of exactly this shape (square, multiply by $d$, the two inversions
+via Fermat chains) complete the doubling, landing on
+\par\noindent{\footnotesize $x_{2B} =$}\\[-2pt]
+{\footnotesize\ttfamily\begin{tabular}{@{}l@{}}24\,72741\,32351\,06541\,00255\,45745\,71675\,58883\,46227\\
+68167\,39763\,84567\,26423\,68252\,12336\,08206\end{tabular}}\par\smallskip
+\par\noindent{\footnotesize $y_{2B} =$}\\[-2pt]
+{\footnotesize\ttfamily\begin{tabular}{@{}l@{}}15\,54967\,55802\,80190\,17635\,26687\,10449\,54225\,15495\\
+72066\,44506\,05805\,07079\,59306\,26430\,49417\end{tabular}}\par\smallskip
+--- the coordinates of $2B$ that every Ed25519 stack on earth agrees on.
+Two honest footnotes. A passing two-clock audit is strong evidence, not
+proof (a wrong digit survives both clocks once in $99$ tries); the kernel
+checks the exact equation --- the audit is \emph{your} hand on the
+ladder, the kernel is the ratchet. And what you just did --- verify a
+giant computation through small residues plus a supplied witness --- is
+precisely the certificate method of Chapter~\ref{ch:prime} and the
+denotation method of Chapter~\ref{ch:denotation}, meeting at the summit.
+\end{worked}
+
 \begin{worked}{the completeness argument, derived to its hinge}
 The Bernstein--Lange proof rewards a full pen-and-paper walk --- symbols,
 not toy numbers, because the argument \emph{is} the real one at every
@@ -121,6 +194,16 @@ limbs, Montgomery multiplication) and its own denotation bridge. Nothing
 conceptually new --- which is itself the lesson: the method \emph{scales
 sideways} without new ideas.
 
+First feel the cycle on the napkin curve: the multiples of $P = (2,4)$
+from the group-law worked example repeat with period $16$ ($16P$ is the
+identity $(0,1)$ --- patient readers can verify with fourteen more
+doublings-and-additions of the kind already performed). So computing
+$21 \cdot P$ never takes $21$ additions: $21 \equiv 5 \pmod{16}$, hence
+$21P = 5P$. \emph{All exponent bookkeeping happens mod the cycle
+length.} For the real base point $B$ the cycle length is the prime
+$\ell$ below, and ``bookkeeping mod $\ell$'' is an entire second
+arithmetic world in the code --- this floor.
+
 \begin{worked}{sizing the group --- real constants, three-line audits}
 The scalar layer's constants invite the same pen-and-paper audits as the
 field's. The group order is $8\ell$ with
@@ -167,35 +250,119 @@ $sB = R + kA$ is not. Three multiplications by $8$, bought by exactly the
 three-line computation above.
 \end{worked}
 
-The engineering, however, has a frontier, and this book has told you enough
+The engineering met a wall here, and this book has told you enough truth
-truth to locate it precisely. Scalar Montgomery multiplication mixes
+to locate it precisely --- and to appreciate how it fell. Scalar Montgomery
-$2^{256}$-scale coefficients into single certificate steps; this is the
+multiplication mixes $2^{256}$-scale coefficients into single certificate
-kernel-capacity wall of Chapter~\ref{ch:field}, and it marks the current
+steps; this is the kernel-capacity wall of Chapter~\ref{ch:field}, and for
-working edge of the campaign: additions and the foundational constants are
+a while it marked the campaign's working edge. It was crossed the way the
-certified (including the pleasing theorem that the code's constant
+method file predicts: re-decompose until every heavy identity is an
-\code{L} \emph{is} $\ell$); the multiplication path is a construction site
+isolated, context-free lemma the kernel checks alone --- exact-division
-with scaffolding --- decomposed lemmas, isolated carry steps ---
+Montgomery rounds, a double round through $RR \equiv R^2$ --- and the
-mid-assembly, honestly labeled in-repo.
+layer is now \emph{complete on all four forks}: add, sub, and Montgomery
+multiplication certified (including the pleasing theorem that the code's
+constant \code{L} \emph{is} $\ell$, digit for digit).
 
-\section{The apex: what ``verified signature'' will say}
+\section{The apex: what ``verified signature'' says}
 
-EdDSA verification accepts $(R, s)$ on message $m$ under key $A$ iff
+EdDSA verification accepts $(R, s)$ on message $m$ under key $A$ when the
+verification equation holds --- and RFC~8032 admits two readings. The
+\emph{cofactored} form $8sB = 8R + 8kA$ (with $k = H(R,A,m)$; the $8$s
+absorb the torsion, as the exercises below explore) is what ZIP-215-style
+verifiers check. The dalek lineage this campaign verified checks the
+\emph{stricter, canonical} form: recompute $[k](-A) + [s]B$, encode it,
+and demand the signature's $R$ match \emph{byte for byte}. The apex
+certificates state, in four button-enforced tiers that climb from bytes
+to points, that the extracted verifier accepts exactly when:
+
+\begin{itemize}[leftmargin=1.4em]
+\item \textbf{byte apex}: $\code{compress}([s]B - [k]A) = R$ as bytes;
+\item \textbf{half-lift}: $R$ \emph{is the canonical encoding} of
+  $[k](-A) + [s]B$;
+\item \textbf{point equation}: any valid curve point canonically encoded
+  by $R$ \emph{equals} $[k](-A) + [s]B$ --- encodings are injective on
+  the curve, courtesy of $d$'s non-squareness doing a second job;
+\item \textbf{full lift}: $R$ \emph{decompresses} to a valid on-curve
+  point equal to $[k](-A) + [s]B$ --- decompression itself proven, square
+  root, sign bit, and all.
+\end{itemize}
+
+\begin{worked}{decompression, run twice --- napkin curve, then the real base point}
+The four tiers stand on one mechanism: a point is stored as \emph{$y$
+plus a single bit --- is $x$ odd or even?} Run it small, then real.
+
+\emph{Run 1 --- the napkin curve} (mod $13$, $d = 2$, the curve of the
+group-law worked example). Encode $2P = (10, 11)$: store $y = 11$ and the
+bit ``$x$ even.'' Now decompress $(11, \text{even})$ from scratch. The
+curve equation, solved for $x^2$:
 \[
-8 s B \;=\; 8 R + 8\,H(R, A, m)\,A
+x^2 \;=\; \frac{y^2 - 1}{1 + d\,y^2}
+\;=\; \frac{121 - 1}{1 + 2\cdot 121}
+\;\equiv\; \frac{3}{9}
+\;=\; 3 \cdot 9^{-1} \;=\; 3\cdot 3 \;=\; 9 \pmod{13}.
 \]
-in the curve group ($B$ the base point, $H$ = SHA-512, the $8$s absorbing
+The square roots of $9$ mod $13$: $3$ and $10$ --- \emph{one odd, one
-the cofactor). The apex certificate will state: \emph{the extracted
+even}, and that is no accident: the two roots are $x$ and $13 - x$, and
-verification routine returns true exactly when this equation holds} ---
+$13$ is odd, so their parities always differ (unless $x = 0$, where both
-given the two declared trusted-base entries you can already predict:
+roots coincide). The stored bit says ``even'': take $x = 10$. Recovered:
-SHA-512 as an ideal hash (axiomatized by design --- hash function
+$(10, 11)$, exactly the point we encoded --- and no \emph{other} curve
-correctness is a different mathematical universe), and the SIMD
+point could have produced $(11, \text{even})$, which is the entire
-point-multiplication backends (untranslatable, documented). Everything
+content of tier 3.
-between those declared boundaries and the field bedrock: kernel-checked,
-axiom-clean, per fork.
 
-Read that sentence again with Chapter~\ref{ch:honesty} eyes: it is a
+\emph{Run 2 --- the real thing.} The compressed base point of Ed25519 is
-\emph{smaller} claim than ``Ed25519 is verified!'' --- and that is exactly
+a 32-byte constant you can find in any implementation on earth (hex,
-why you can believe it.
+little-endian):
+\begin{center}
+\ttfamily 58 66 66 66 66 66 66 66 66 66 66 66 66 66 66 66\\
+66 66 66 66 66 66 66 66 66 66 66 66 66 66 66 66
+\end{center}
+\noindent (one \code{58}, then thirty-one \code{66}s --- all thirty-two
+bytes, nothing elided).
+Byte 31 is $\code{0x66} = 01100110_2$: its top bit is $0$, so the sign
+bit says ``$x$ even.'' The remaining 255 bits, read little-endian, are
+\par\noindent{\footnotesize $y_B \;=$}\\[-2pt]
+{\footnotesize\ttfamily\begin{tabular}{@{}l@{}}46\,31683\,56949\,26478\,16942\,83940\,03475\,16314\,13079\\
+93866\,25622\,56157\,83033\,60316\,52518\,55960\end{tabular}}\par\smallskip
+The design claim behind this constant: $y_B = 4/5$ in $\Fp$, i.e.\
+$5\,y_B \equiv 4 \pmod p$. At full size that is one integer equation,
+\[
+5 \cdot y_B - 4 \;=\; 4 \cdot p \quad\text{\emph{exactly}},
+\]
+and this one you can verify with \emph{no} shortcuts and \emph{no}
+witnesses: multiply $y_B$ by $5$ yourself (one right-to-left carry pass),
+multiply $p$ by $4$, subtract $4$, compare every digit:
+\par\noindent{\footnotesize $5\,y_B - 4 \;=$}\\[-2pt]
+{\footnotesize\ttfamily\begin{tabular}{@{}l@{}}231\,58417\,84746\,32390\,84714\,19700\,17375\,81570\,65399\\
+69331\,28112\,80789\,15168\,01582\,62592\,79796\end{tabular}}\par\smallskip
+\par\noindent{\footnotesize $4\,p \;=\;\;\;\;\;\;\;$}\\[-2pt]
+{\footnotesize\ttfamily\begin{tabular}{@{}l@{}}231\,58417\,84746\,32390\,84714\,19700\,17375\,81570\,65399\\
+69331\,28112\,80789\,15168\,01582\,62592\,79796\end{tabular}}\par\smallskip
+An honest fifteen minutes, and you have hand-checked a constant that
+every Ed25519 signature on the planet flows through. Then the sign bit
+earns its keep exactly as on the napkin: the real
+$x_B$ ends in $\ldots 202$ (even), and $p - x_B$ ends in $\ldots 747$
+(odd --- check it from the last six digits alone: $819949 - 762202 =
+57747$). One even root, one odd root; the bit picks $x_B$. The one thing
+paper cannot do at this size is the square root itself: the machine
+raises to the exponent $(p+3)/8$ --- about $252$ squarings of 77-digit
+numbers --- and the certificate \code{sqrt\_ratio\_i\_sq\_spec} pins its
+output with the same kind of witness-checked equation you audited in the
+group-law example, the kernel playing the role of your two clocks.
+\end{worked}
+
+The trusted base is \emph{smaller} than the one you might have predicted.
+SHA-512 enters as an opaque oracle with \textbf{no assumed properties at
+all} --- not even ``behaves like an ideal hash''; the theorems hold for
+whatever bytes it produces. The wire-format types stay opaque. And the
+point-multiplication backends are \emph{not} in the trusted base:
+extraction pins the serial path, which is real translated code, proven
+like everything below it. Each repo's check script has a dedicated phase
+that \lean{\#print axioms} all four tiers and fails the build if any
+cone deviates from that documented boundary by a single axiom.
+
+Read that again with Chapter~\ref{ch:honesty} eyes: it is a
+\emph{smaller} claim than ``Ed25519 is verified!'' --- nothing about the
+hash, nothing about signing, nothing about side channels --- and that is
+exactly why you can believe it.
 
 \section{What you now know, and where to take it}
 
@@ -213,10 +380,13 @@ Where to go from here, in increasing order of ambition:
 \item \textbf{Read a real proof end-to-end.} \code{FieldSpec.lean} in
   \code{dalek-ed25519-verified}, top to bottom, with this book as the
   decoder ring. Budget an afternoon; expect the odd hour of humility.
-\item \textbf{Extend the pyramid.} The scalar layer's open lemmas are
+\item \textbf{Extend the pyramid.} The ed25519 pyramids are capped, but
-  decomposed, labeled, and waiting; the repos' \code{CONTRIBUTING} notes
+  the Pasta curve layer (Pallas group law and scalar multiplication) is
-  state exactly what a finished brick looks like (spec shape, axiom
+  paused with its field foundations proven and the route mapped --- the
-  audit, check-script entry). Frontier work, undergraduate-accessible.
+  scalar layer's kernel-frontier crossing is the template, and the
+  control repo's \code{METHOD.md}/\code{TIERS.md} state exactly what a
+  finished brick looks like (spec shape, axiom audit, check-script
+  entry). Frontier work, undergraduate-accessible.
 \item \textbf{Verify something of yours.} Pick a 200-line pure function you
   actually use --- a parser, a checksum, a data structure --- write its
   denotation (what does it \emph{mean}?), state the square, prove it.
@@ -300,11 +470,17 @@ prime and $> 8$? (c) Conclude what an attacker who adds a small-order
 point to a public key changes, and what they provably cannot change.}
 
 \exercise{(Audit drill) Write down, from memory, the complete list of
-what the apex certificate will \emph{assume} (its trusted base) and what
+what the apex certificates \emph{assume} (their trusted base) and what
-it will \emph{establish}, then check yourself against this chapter's
+they \emph{establish}, then check yourself against this chapter's
 apex section. Anything you forgot is the thing to reread before you
 audit a real system.}
 
+\exercise{(Paper) The point $3P = (6, 10)$ lives on the napkin curve
+(mod $13$, $d = 2$). Encode it (which bit?), then decompress your own
+encoding from scratch --- compute $x^2$ from $y$, find both square
+roots by scanning, and let the bit choose. Confirm you recover $(6,10)$
+and not the other root.}
+
 \section*{Solutions and pathways}
 \solutionsintro
 
@@ -349,25 +525,44 @@ invertible on the $\Z_\ell$ part.'' (c) The attacker changes the point
 $X$ (so: byte-level equality checks, hashes of the key, uniqueness
 assumptions \emph{can} be affected --- real protocols have been bitten)
 but provably cannot change $8X$, hence cannot affect the truth value of
-any cofactored verification equation. The formal apex certificate
+any cofactored verification equation. Note carefully which verifiers
-inherits exactly this robustness, and the ``$8$'' in its statement is
+inherit this robustness: the \emph{cofactored} (ZIP-215) lineage. The
-this exercise, immortalized.
+verified dalek-lineage verifier deliberately checks the stricter
+canonical byte-equality criterion instead --- knowing \emph{which}
+equation a library actually checks is this exercise's real teeth, and
+the anza repo's ledger pins exactly that distinction for Solana's
+verifier.
 
 \solhead{12.3}
 \pathway Close the book. Write two columns: \emph{assumes} /
 \emph{establishes}. Then open the apex section and diff.
 \answer The list your memory should reproduce --- \emph{assumes}:
-(1) SHA-512 behaves as an ideal hash (axiomatized by design, in the
+(1) SHA-512 as an opaque oracle, with \emph{no} properties assumed ---
-trusted-base ledger); (2) the untranslatable SIMD point-multiplication
+not even ideality; the theorems hold for whatever bytes it produces;
-backends meet their stated specs (documented, per fork); (3) the three
+(2) the opaque wire-format types (the signature struct and error type,
-standard Lean axioms; (4) the extraction pipeline preserves meaning
+per fork); (3) the three standard Lean axioms; (4) the extraction
-(one tool, pinned versions). \emph{Establishes}: for every input in the
+pipeline preserves meaning (one tool, pinned versions). Notably ABSENT:
-bounds discipline, the extracted verification routine returns true
+any backend assumption --- the serial path is pinned at extraction and
-\emph{iff} $8sB = 8R + 8\,H(R,A,m)\,A$ in the curve group --- with
+proven as real code. \emph{Establishes}, in four tiers each pinned to
-field arithmetic, group law, scalar arithmetic, and encoding each
+exactly that boundary by the check script: the extracted verifier
-carried by its own kernel-checked layer below. If your two columns
+returns true \emph{iff} the signature's $R$ decompresses to a valid
-match this, you can audit a verification paper's abstract in ninety
+on-curve point equal to $[k](-A) + [s]B$ --- with field arithmetic,
-seconds --- which was the promise on the book's cover, kept.
+group law, scalar arithmetic, encoding, and decompression each carried
+by its own kernel-checked layer below. If your two columns match this,
+you can audit a verification paper's abstract in ninety seconds ---
+which was the promise on the book's cover, kept.
+
+\solhead{12.4}
+\pathway Mirror the worked example's run 1 with $y = 10$.
+\answer Encode: $x = 6$ is even $\Rightarrow$ store $(10, \text{even})$.
+Decompress: $y^2 = 100 \equiv 9$, so
+$x^2 = (9-1)/(1 + 2\cdot 9) = 8/19 \equiv 8 \cdot 6^{-1}$; scanning gives
+$6^{-1} = 11$ ($6 \cdot 11 = 66 \equiv 1$), so $x^2 = 88 \equiv 10$. The
+roots of $10$: scan the squares --- $6^2 = 36 \equiv 10$ and
+$7^2 = 49 \equiv 10$, so $\{6, 7\}$, one even, one odd (they sum to
+$13$). The bit says even: $x = 6$ \checkmark. Choosing $7$ instead would
+put you on the curve at the WRONG point $(7,10) = -3P$ --- the sign bit
+is one bit of information doing real cryptographic work.
 
 \begin{checkpoint}
 The book's ending is a beginning, so the final checkpoint is prospective:

chapters/glossary.tex

@@ -31,7 +31,9 @@ translates LLBC into pure Lean definitions
 
 \gloss{Cofactor} The factor $8$ in the Ed25519 group order $8\ell$;
 multiplying by it annihilates the small-torsion component of any point,
-which is why the verification equation reads $8sB = 8R + 8kA$
+which is why \emph{cofactored} verifiers (the ZIP-215 lineage) check
+$8sB = 8R + 8kA$. The verified dalek-lineage path checks the stricter
+\emph{canonical} uncofactored equation byte-exactly
 (Chapter~\ref{ch:pyramid}).
 
 \gloss{Commuting square} The diagram --- machine operation along the