proof-aware-crypto-tooling-agent/paper/reinvention-outline.md

Paper reinvention — working outline (post second ePrint rejection)

Status: approved direction (operator order 2026-07-16: "entry 13 and paper reinvention"); this outline is the committed starting point for the full rewrite. Diagnosis it responds to: both external analyses (GPT-5.6 rejection post-mortem; round-6 reviewer aside) converge on POSITIONING, not correctness — five papers compressed into one, the novelty (trust decomposition) occupying less space than its supporting machinery, and the honest "components unchanged" refrain reading as "nothing new" in a thirty-second editorial skim.

0. The one sentence (everything else exists to support it)

We define and instantiate a cryptographic distribution model for machine-checked correctness evidence, enabling lightweight consumers to obtain accountable assurance without executing the original verifier — and demonstrate it end to end with a deployed log that carries kernel-checked proofs of its own accountability machinery as an entry in itself.

The second clause is the only-this-paper claim; it becomes literally true at entry 13 and the paper should be finalized AFTER that append so the abstract can cite the live leaf.

1. Title candidates (working)

• "Accountable Distribution of Machine-Checked Correctness Evidence"
• "Transparency for Theorem Provers: Distributing Formal Verification to Consumers Who Cannot Replay It"
• (subtitle either way): "…with a deployed log that notarizes the proofs of its own machinery"

"The Lean Transparency Log" becomes the system's name, not the paper's identity.

2. Inverted structure

1. Problem. Theorem provers solve the PRODUCTION of correctness evidence; nothing standard solves scalable DISTRIBUTION and CONSUMPTION by clients that cannot run the prover (no toolchain, no hours of replay, no trust in the operator's word). State it as the gap between "verified" and "verifiable by you."
2. Model. The trust decomposition, presented abstractly: (a) producer performs expensive deterministic verification once; (b) the result becomes a precise attestation object (subject commit, toolchain, certificates with exact assumption cones, scope); (c) a transparency structure supplies persistence, consistency, and equivocation-evidence; (d) consumers apply policy locally without executing the verifier; (e) the residual trust is enumerated, not waved at. Define the accountability property: misbehavior manufactures transferable evidence.
3. Design space (the section the old paper lacked). Position against: reproducible replay services; succinct proofs of proof checking (SNARKed kernels); checkpoint/cosigning committees; witness cosigning; downloadable proof artifacts; proof-carrying code; cached prover environments/containers. Axis of comparison: consumer cost, operator trust, accountability (evidence on misbehavior), incrementality, and what happens when the operator disappears. The log wins on accountability-per-consumer-cost; be honest where SNARKed checking would win (validity vs accountability) and why it is not yet practical for a full kernel.
4. Instantiation: the LTL. Lean 4 + Aeneas corpora as producers; Ed25519 heads signed by the dogfooded verified signer (self_inclusion); RFC 9162 accumulator; pin-store consumers. Compressed from old §4–5; the four ed25519 subject corpora become a TABLE + pointer to project documentation, not sections.
5. Security of the instantiation. The mechanized model (61 certificates, single opaque-SHA-256 axiom, environment-derived audit surface); Theorems 1–3 + Prop 1 in one page each of STATEMENT (the proofs live in the repo; the paper sells the statements). Present gap 14/15 as a RESULT, not a confession: the model/deployment seam located, measured (3,867 one-sided divergences), fenced by pinned tests, and bridged by an explicitly stated operational invariant — this is what honest mechanization boundaries look like.
6. Exhibit A: the log attests itself. Entry 13 as the paper's demonstration: the accountability machinery's own proofs, carried by the machinery, verifiable end to end by one command from a stock toolchain. Include the leaf hash + head root; a reader can check inclusion in seconds.
7. Deployment & consumers. Live service; warden (quorum custody wallet) as the internal consumer; Swiss Post e-voting PoC as the prospective external consumer (dalek-family transport). Replay economics (measured ~1,800 s/fork) as the cost the model amortizes.
8. Related work. CT lineage (RFC 6962/9162, CONIKS, sigstore); optimistic-rollup analogy (accountability-over-validity; the fraud-proof reading of Theorem 3 — from ltl-accumulator-verified/docs/optimistic-accountability.md); proof-carrying code; reproducible builds/SLSA; in-toto.
9. Limitations = the 15-gap ledger, grouped (assumption base / scope lines / unmechanized bridge), each one sentence, pointer to the repo ledger.

3. What moves OUT of the paper

• Ed25519 corpus construction details → project docs / possible separate implementation report ("Paper C" in the GPT taxonomy).
• Curriculum, wallet internals, agent-native surfaces → out entirely.
• Appendix A/B verbatim-leaf material → shrink to one leaf excerpt (entry 13 itself, naturally).
• The §8 operational-history narrative → compress to the retrievability-decay paragraph + one table.

4. Sequencing & venues

1. Entry 13 lands (prerequisite for the abstract's second clause).
2. Rewrite per this outline (fresh tex, new title; old ltl.tex remains hosted as the system report at /paper — versioned, not erased).
3. arXiv (cs.CR) immediately for timestamp + citability.
4. Venue: CPP/ITP (mechanization framing) or SCORED/SecDev (supply-chain framing) or RWC talk (deployment framing) — decide after the rewrite settles which face leads.
5. All queued wording fixes (Lemma-2 specializations, fidelity = pinned families, §10(i)/(v), Remark 1, pinned-pair side condition) are ABSORBED by the rewrite rather than patched into the old text.

5. Success criterion

A hurried editor can answer "what is the contribution?" from the title

• first paragraph alone, and the thought-experiment inversion holds: remove any single supporting component (Lean, Ed25519, RFC 9162) and the CLAIM survives; remove the trust-decomposition model and nothing is left. That is the opposite polarity of the rejected manuscript.