Ch14 · AXLE — The Sorry-Free Paper

§1 · The Curry-Howard Correspondence

In 1969, William Howard observed that the rules of natural deduction in logic mirror the typing rules of the lambda calculus exactly — one is a notational variant of the other. The implication is profound: propositions are types, and proofs are programs. To prove a proposition P is to construct a term of type P.

Curry-Howard in Lean 4

-- A proposition is a type def MyProposition : Prop := ∀ n : ℕ, n + 0 = n -- A proof is a term of that type theorem myProof : MyProposition := fun n => Nat.add_zero n -- sorry = placeholder proof (compiles, but is NOT verified) theorem unfinishedProof : MyProposition := sorry -- ⚠ warning: declaration uses 'sorry' -- The AXLE goal: eliminate every sorry from the paper's argument -- #check myProof → MyProposition ✓ -- #check unfinished → MyProposition ✗ (sorry)

In Lean 4, sorry is a magic term that inhabits any type — it makes the file compile regardless of whether the proof is actually valid. A paper can do the same: a well-written argument reads as if every claim is proven, even when some critical connections are asserted without evidence. Those invisible sorrys are what peer review hunts for.

AXLE (Algebraic eXpression Language for Evaluation) applies this framework to academic writing: every claim in a paper has a type (what kind of evidence could inhabit it), and the paper is verified only when every claim has an explicit evidence term — no sorry remaining.

§2 · The Operator Chain as a Lean 4 Structure

The operator chain G = U ∘ F ∘ K ∘ C can be formalised as a dependent type: each operator takes the output type of the previous as its input type. A well-typed paper is one where the composition is valid — no type mismatches between operators.

G = U ∘ F ∘ K ∘ C as Lean 4 Types

structure RawData where measurements : List Float n : ℕ structure CompressedData where -- output of C features : List Float compression_ratio : Float h_valid : compression_ratio > 1 -- proof of non-trivial compression structure ThresholdEvent where -- output of K crossed : Bool k_star : Float h_evidence : crossed → ∃ e, e ∈ evidence_set ∧ e > k_star structure FoldedNarrative where -- output of F results_section : String h_subcritical : ¬overclaims results_section -- Ch9 condition structure UnfoldedDiscussion where -- output of U claims : List Claim h_stable : ∀ c ∈ claims, spectralReach c ≤ 1 -- Ch11 condition -- The composition G is well-typed iff every h_ proof is inhabited def G (d : RawData) : UnfoldedDiscussion := U (F (K (C d))) -- verified iff no sorry in h_ fields

The proof fields h_valid, h_evidence, h_subcritical, h_stable correspond precisely to the theorems in Chapters 5, 9, 11, and 12. A paper that passes all four chapter-tests has implicitly constructed all four proof terms — it is Lean-verifiable in spirit, even without running #check.

§3 · Type Errors in Academic Arguments

Lean 4 rejects programs with type errors. An argument can also have type errors — using the wrong kind of evidence for a claim, regardless of whether the evidence is real. A randomised controlled trial and a case study both constitute evidence, but they are different types — and using the wrong type for a causal claim is a type mismatch.

type mismatch

Evidence type does not match claim type. Correlation evidence for a causal claim.

"X causes Y" supported only by r = 0.6 observational data.

unsolved ?metavariable

A claim that requires an unstated assumption to type-check. The missing piece is not cited.

"Under standard assumptions, X follows from Y." — which assumptions?

failed to synthesize

No evidence exists in the literature that could inhabit this claim's type.

"This is the first demonstration of…" with no novelty check performed.

⊢ type-checks ✓

Claim type matches evidence type. The connection is explicit and warranted.

"RCT (n=200) shows X increases Y by 15% (95% CI 9–21%), p < 0.001."

Theorem 14.1 — The AXLE Verification Criterion

A paper P is AXLE-verified if and only if:

For every claim C in P, there exists an explicit evidence term h : C constructible from P's data and cited literature, such that type(h) = required_evidence_type(C).

Equivalently: P is sorry-free — no claim relies on an implicit assumption that has not been stated as a premise, cited as prior work, or demonstrated within P.

P passes AXLE iff it also passes the four nirvana tests of Ch13: T(Conclusion) = Conclusion (Ch12), ρ(claims) ≤ 1 (Ch11), λ < 0 (Ch10), and β → ∞ (Ch13). The AXLE criterion subsumes all four.

§4 · DNA Proofreading — Biological Formal Verification

DNA polymerase III replicates the genome at ~1,000 bases per second while maintaining extraordinary accuracy. It achieves this through a three-stage verification cascade — biological formal verification with error rates that improve by five orders of magnitude.

Verification Stage	Mechanism	Error Rate	Sorry Count (per 10⁹ bases)
Base selection	Geometry / H-bonding specificity	~10⁻⁵	~10,000 sorries
3′→5′ proofreading	Exonuclease removes mismatched 3′ end	~10⁻⁷	~100 sorries
Mismatch repair (MMR)	MutS/MutL/MutH scan for distortions post-replication	~10⁻⁹ to 10⁻¹⁰	~1 sorry per genome

Each stage is an application of the AXLE criterion at the molecular level: a mismatched base is a type mismatch — the wrong nucleotide type in a position whose type is defined by the template strand. The proofreading exonuclease is the reviewer; mismatch repair is AXLE itself.

The Drosophila melanogaster connectome — all ~130,000 neurons and ~50 million synapses, published in 2023 — represents the same achievement at the cellular scale: a formal verification of the fly brain's wiring, every connection typed and checked. A sorry-free paper aspires to the same completeness in its own domain.

When MMR fails — in Lynch syndrome — the mismatch error rate rises to ~10⁻⁷, and colorectal cancer risk increases dramatically. A paper without AXLE verification has the same vulnerability: every unresolved sorry is a potential site of argument collapse under review pressure.

§5 · Kinetic Proofreading — The Mathematics of Error Discrimination

Thermodynamics imposes a hard floor on discrimination accuracy. Given a binding energy difference Δε between correct and incorrect substrates, the equilibrium error rate cannot fall below f₀ = e^{−Δε / k_BT}. For nucleotide selectivity Δε ≈ 2–3 k_BT, giving f₀ ≈ 0.01–0.14 — far too high for a genome that must copy 3 × 10⁹ bases with fewer than one error per cell division.

In 1974, John Hopfield showed this limit can be broken by coupling discrimination to an irreversible, energy-consuming step — GTP hydrolysis. The system discriminates twice: once before hydrolysis, once after. Because hydrolysis is irreversible, each pass is statistically independent. The error rates multiply:

Theorem 5.1 — Hopfield 1974 · Kinetic Proofreading

Let f₀ = e^−Δε/k_BT be the thermodynamic discrimination factor.
With n irreversible proofreading steps (each costing ≥ k_BT · ln(1/f₀) in free energy), the achieved error rate is:

f_n = f₀^{n + 1}

This is the K operator in the dm³ chain. Each GTP hydrolysis event is a threshold crossing — the irreversible step that resets the discrimination clock and permits a second independent rejection opportunity. K does not merely filter; it multiplies the fidelity of C.

In ribosomal translation — Hopfield's original example — EF-Tu carries aminoacyl-tRNA to the ribosome A-site. For a near-cognate (mismatched) codon-anticodon pair, GTPase activation slows by a factor of ~100 (k_cat = 120–500 s⁻¹ cognate vs. 0.06–1.3 s⁻¹ near-cognate). After GTP hydrolysis and EF-Tu release, the aa-tRNA must accommodate into the peptidyl transferase centre — a second independent rejection opportunity. The product: f₁ = f₀² ≈ 10⁻⁴ per codon, matching observation.

The n-bonacci recurrence ladder is the abstract form of this principle. Each additional proofreading layer advances the verification ratio toward the limit — the embodiment threshold τ = 2:

φ ≈ 1.618 Base selection ~10⁻⁵

η ≈ 1.839 + Exonuclease ~10⁻⁷

Δ ≈ 1.927 + MMR ~10⁻⁹

Σ ≈ 1.966 + HF-CRISPR ~10⁻¹¹

Ω ≈ 1.984 Prime editing ~10⁻¹³

τ = 2 Perfect fidelity · limit

The n-bonacci constant φₙ is the unique root in (1, 2) of xⁿ − xⁿ⁻¹ − … − x − 1 = 0. As n → ∞, φₙ → 2. This is the mathematical statement that infinite kinetic proofreading achieves perfect discrimination. The embodiment threshold τ = 2 is the biological asymptote — the limit no finite molecular machine can reach, but that every proofreading cascade approaches. Each rung of the dm³ recurrence ladder is one more GTP hydrolysis step.

§6 · The Central Dogma as G = U ∘ F ∘ K ∘ C

DNA stores information; RNA reads it; ribosomes translate it into protein; protein acts. This four-layer cascade is not merely an analogy to the dm³ operator chain — it is a physical instantiation of G = U ∘ F ∘ K ∘ C. Each operator has a corresponding molecular machine, error rate, and proofreading mechanism:

C — Contact

🧬

DNA Replication

10⁻⁵ → 10⁻⁹ / bp

Pol III base selection driven by Watson-Crick contact geometry. The template strand is the contact form; complementarity is the contact condition.

K — Threshold

🔬

RNA Transcription

10⁻⁵ → 10⁻⁶ / nt

RNA Pol II backtracking on mismatch triggers TFIIS-stimulated cleavage. Misincorporation is the threshold K* — it activates the proofreading response.

F — Fold

⚗️

Translation

~10⁻⁴ / amino acid

EF-Tu GTPase kinetic proofreading (Hopfield's original example). The nascent polypeptide folds co-translationally — the narrative assembles as it is written.

U — Unfold

⚡

Active Protein

Post-translational QC

Chaperone-assisted folding; ER quality control; proteasomal degradation of misfolds. Only sorry-free proteins enter the functional proteome.

The cascade is not monotonically improving: translation is less accurate than replication (10⁻⁴ vs. 10⁻⁹ per residue). This is not a flaw — it reflects different cost structures. DNA errors are permanent; protein errors are transient. A misfolded protein is degraded and re-synthesised by U, which loops back to C. The operator chain is not linear — it is a recurrence, cycling until the expressed output is sorry-free.

Central Dogma as dm³ type composition

-- C: genome as a contact structure (Watson-Crick geometry) structure Genome where sequence : List Nucleotide h_contact : ∀ b ∈ sequence, WatsonCrick b.complement = true -- K: RNA Pol II threshold — backtracking activates on mismatch def K_transcribe (g : Genome) : Transcript := polII g |>.filter (fun nt => nt.misincorporated → TFIIS.cleave nt) -- F: ribosome + EF-Tu kinetic proofreading (Hopfield 1974: f₀² discrimination) def F_translate (t : Transcript) : NascentPolypeptide := ribosome t |>.proofread EF_Tu_GTPase -- U: chaperones, ER-QC, proteasome — sorry-free proteins proceed def U_express (p : NascentPolypeptide) : ActiveProtein := match chaperone.fold p with | .correct x => x.activate | .misfolded => proteasome.degrade p; sorry -- retry loop -- G = U ∘ F ∘ K ∘ C ←→ the central dogma def G (genome : Genome) : ActiveProtein := U_express (F_translate (K_transcribe genome))

The Drosophila melanogaster connectome — 130,000 neurons, 50 million synapses, published 2023 — is the output of this cascade applied ~10¹¹ times across development. Each synapse is a sorry-free expressed claim: "neuron A contacts neuron B at strength w." The connectome as a whole is a formally verified proof of the fly's neural architecture — AXLE at the organismal scale.

§7 · CRISPR — Post-Hoc Genome Editing as Sorry Correction

DNA proofreading, RNA fidelity, and ribosomal kinetic proofreading all operate during the biological writing process. CRISPR-Cas9 is something different: it is a post-hoc editor — capable of finding a specific 20-nucleotide address anywhere in a 3 × 10⁹ bp genome and correcting it after the fact. In Lean terms, DNA proofreading is the type-checker running on compilation; CRISPR is the proof repair tool applied to a compiled but sorry-containing file.

System	Mechanism	Off-target Rate	AXLE Analogy
Wild-type Cas9	DSB → NHEJ or HDR	~10⁻² to 10⁻³	Early draft — one sorry removed, another introduced by error-prone repair
SpCas9-HF1	Reduced PAM-distal contacts; tolerates only perfect-match guides	~10⁻⁵	Exonuclease pass — sorry rate drops 100×; some sorries remain
eSpCas9 / HypaCas9	Modulated protein–DNA non-specific contacts	~10⁻⁵ to 10⁻⁶	MMR pass — approaching 1 sorry per genome
Prime Editing (2019–)	Cas9n + reverse transcriptase + pegRNA encodes both target and edit	~10⁻⁷ or below	AXLE-verified — the pegRNA is the proof term, encoding location and correction simultaneously

Prime editing is architecturally closest to AXLE verification. The pegRNA (prime editing guide RNA) encodes two things simultaneously: the genomic address (where) and the desired sequence (what the correct text should be). This is precisely the structure of a Lean 4 evidence term — h : Claim encodes both the proposition and its proof. The reverse transcriptase copies the correct sequence directly from the pegRNA template: no double-strand break, no error-prone NHEJ, no newly introduced sorries.

Theorem 7.1 — CRISPR as dm³ Operator Composition

Let genome G be a Lean file with n sorry-containing theorems at positions p₁ … pₙ. A prime-editing correction targeting position p with sequence c applies:

edit : G → G' where G'[p] = c

The edit is AXLE-verified iff:
(C) the guide RNA uniquely identifies p — no off-target contacts (C is injective);
(K) c is the cognate sequence at p — the K threshold is satisfied;
(F) the reverse transcriptase copies c without error — the corrected strand folds correctly;
(U) G' expresses a functional protein — the sorry-free output is inhabited.

Prime editing satisfies all four. Wild-type Cas9 with NHEJ satisfies (C) and (K) probabilistically but routinely fails (F) and (U) by introducing indels at the repair site.

Lynch syndrome (§4) arises when MMR fails — the biological sorry-eliminator is broken, and colorectal cancer risk climbs. CRISPR prime editing can in principle correct the causative MSH2 or MLH1 mutations in somatic cells, restoring the MMR apparatus itself. This closes the loop: the same sorry that biological verification failed to catch is addressable by an externally applied AXLE pass. Every unresolved sorry — in a genome or in a paper — has a repair pathway. The question is only the cost of the proofreading step.

⬡ LLM Prompt Portal · Chapter 14

PROMPT 7.4 · SORRY INVENTORY

Map Every Implicit Assumption in Your Paper

Read your paper as if you were writing it in Lean 4. For every claim C, ask: "If I had to write h : C, what is h?"
List every claim where h is implicit — where you asserted C without constructing the evidence term. These are your sorries.
For each sorry: (a) Can it be replaced by a citation? (b) By your own data? (c) Does it need to be stated explicitly as a premise/assumption? (d) Should the claim be removed entirely?
Output: a sorry inventory table with columns: Claim / Type of h needed / Replacement strategy / Status.

PROMPT 8.1 · TYPE-CHECK YOUR ARGUMENT

Evidence Type Matching

For each major claim in your paper, identify its required evidence type:
· Causal claim → requires RCT or natural experiment
· Mechanistic claim → requires in vitro / molecular / pathway data
· Associative claim → observational / correlation evidence is sufficient
· Universal claim (∀ x) → requires proof or very large n
· Existential claim (∃ x) → a single example suffices
For each claim, state: (a) claim type, (b) evidence type you used, (c) type-check result: MATCH ✓ / MISMATCH ✗ / METAVARIABLE ?. For every MISMATCH: either downgrade the claim to match the evidence, or upgrade the evidence to match the claim.

PROMPT 9.1 · CENTRAL DOGMA AUDIT

Map Your Paper's Operator Chain

Treat your paper as a Central Dogma cascade. Identify which layer each claim lives in:
· C (Contact / Data): raw measurements, observations, sequences — what did you actually touch?
· K (Threshold / Significance): which results crossed a pre-defined threshold K*? Was K* set before data collection?
· F (Fold / Narrative): how did you structure results into a story? Which framings are interpretations vs. facts?
· U (Unfold / Conclusion): which claims in your conclusion are actually in your data, vs. extrapolated?
For each misplaced claim (a U-level conclusion supported only by C-level data), either add the missing K and F operators, or downgrade the claim to its actual layer.

PROMPT 9.2 · KINETIC PROOFREADING SELF-AUDIT

Count Your Proofreading Steps

For each major claim in your paper, count how many independent verification steps it has passed:
Step 1 (φ, f₀): you ran the analysis and got a result;
Step 2 (η, f₀²): a co-author checked the analysis independently;
Step 3 (Δ, f₀³): a blinded reviewer attempted to replicate the result;
Step 4 (Σ): the result survived peer review with methods scrutiny;
Step 5 (Ω): the result has been independently replicated by another lab.
Claims at Step 1 only have thermodynamic-limit error rates (~10⁻²). Claims at Step 3+ approach the DNA replication standard (~10⁻⁹). Which of your claims are still at Step 1? Those are your highest-risk sorries.

EXTENSION · PROOFREADING CASCADE

Three-Stage Verification Protocol

Apply the DNA proofreading cascade to your paper:
Stage 1 — Base selection (error rate 10⁻⁵): Read each sentence in isolation. Does it make a claim? Is the claim typed correctly? Flag mismatches.
Stage 2 — Exonuclease proofreading (10⁻⁷): Apply Prompts 5.3 (Lyapunov), 5.2 (spectral), and 6.3 (conclusion audit). How many sorries remain?
Stage 3 — Mismatch repair (10⁻¹⁰): Apply Prompt 7.3 (nirvana check). Run the sorry inventory (Prompt 7.4). Eliminate all remaining sorries.
Report error rates at each stage: how many sorry-level claims per 1,000 words survived Stage 1? Stage 2? Stage 3?

AXLE — The Sorry-Free Paper