Triggered by the operator's hint (references flow into App A but a full
break sits between B and C). Full-document inspection found and fixed:
- ghost page 23 (~85% blank): the fossil \clearpage before Appendix C,
placed under an older pagination, removed; appendix policy now
DECLARED: the block starts on a fresh page, then flows with no
internal breaks
- claim matrix (the paper's honesty centerpiece): solid-set rows merged
visually and narrow justified columns gaped (badness-10000 in every
build log, never read) -- now ragged-right columns, 3pt row air,
EUF-CMA/SHA-256 unbreakable
- Figure 3 still drew the July 13-leaf snapshot in a v0.11 paper that
narrates 19 leaves -- extended: leaves 13-18, August-2026 brace,
dual-signed size-19 head box, pq-styled leaf 18
- ConsRec hyphenated as Con-sRec and set in serif vs sans elsewhere ->
math-face identifiers in the mechanization table
- 'tuple' stranded its last syllable as a whole line in Definition 1;
'timestamp' broke as times-tamp -> mbox + \hyphenation
- thesis box hyphenated its showcase slogan -> ragged-right no-hyphen
(first attempt justified+nohyphen was caught by the new gate itself)
- Appendix E header caps + layer-cell caps + continuation row cleanup;
related-work 3.4pt overfull removed
- NEW check-paper.sh: fails on overfull>10pt, any badness-10000, ghost
pages (<300 chars/page), missing version on title page, ?? refs;
4-check selftest; renders all pages for the mandatory eye pass
All 25 pages re-rendered and flipped by eye. Gate green. Tests green.
paper/ltl.tex + built PDF: "LTL: the Lean Transparency Log -
Distributing Machine-Checked Proof Evidence via an Authenticated Data
Structure Signed by Its Own Certified Artifact". Exactly four pages,
two-column, self-contained (embedded bibliography, TikZ figure of the
real 8-leaf log with the self-certifying signature loop).
Structure: intro (the consumption-economics argument), the LTL
(roles, replay-attestation leaves, boundary-exact auditing,
observation-not-verdict, pinning + git witness), the self-certifying
signature (with the honest verify-path/signing-path distinction),
deployment & evidence (the failure leaves as a feature; the full
assumption enumeration; the proof-portability observation with real
divergence numbers), related work (Rekor/CT/PCC/CONIKS/in-toto
engaged head-on; Cheval-Moreira-Ryan as the complementary direction -
"they verify the log; we log the verification"), limitations, and the
next-step agenda (Lean-verified RFC 9162 verifiers with SHA-256
collision resistance as a documented boundary axiom, certificates
entering the log they defend; EverCrypt/verified-Merkle prior art
credited).
Claim discipline verified on the rendered text: zero hype vocabulary,
explicit does-not-establish list, full trusted-base enumeration,
single-operator/TOFU/prototype-scale limitations stated, AI drafting
assistance acknowledged. References verified against the literature
(Sigstore CCS'22, Aeneas ICFP'22, HACL* CCS'17, Fiat-Crypto S&P'19,
EverCrypt S&P'20, in-toto USENIX'19, CONIKS USENIX'15, RFC
6962/9162/8032, Necula POPL'97, Lean 4 CADE-28, Bernstein et al.).
Footnote acknowledges the linear-temporal-logic acronym collision.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
