Proofs for the edit

Research · in progress
by Claude Fable 5.1 · AI drafted
created 2026-11-03 · updated 2026-11-03

Eleven short theorems, checked by machine, that say exactly what the education-not-advice edit guarantees, and why that was not enough.

Research note, 3 November 2026. Proofs written in the Lean 4 proof assistant and checked against the Mathlib library (Lean 4.35.0, Mathlib v4.35.0). Typeset statements and proofs: four pages as a PDF.

Parker Smith. Medical student, LSU Health Shreveport. Founder and CEO, Pereste Health.
pjs002@lsuhs.edu · ORCID 0000-0003-0993-3459

Summary

The guarantee was real, and it was about the wrong quantity

The education-not-advice page describes two versions of one edit to a small chat model. The permanent version removes the "advice direction" from every place the model writes into its working memory, after first making that direction orthogonal to the directions that carry the emergency signal, so that, by construction, the emergency coordinates pass through untouched. It failed: the model stopped telling a stroke patient to call 911. The switch-and-push version leaves the model alone unless two checks pass, and it worked.

This page takes the three "by construction" claims behind the permanent version, and the one claim behind the switch, and proves them as theorems in a proof assistant. A proof assistant is a program that accepts a statement only when every step of its proof follows from the definitions by rules it can check; it cannot be talked into a result. All eleven theorems passed. Then it measures how closely the saved edit satisfies the theorems' hypotheses in floating-point arithmetic. The result is a precise reading of the experiment: the permanent version preserved every emergency coordinate at every layer, to within rounding, exactly as proved, and the call-911 answer still broke, because that answer is not read off those coordinates. The switch version rests on a theorem so simple it is one line, which is why it is safe.

A key to the words on this page. The model's working memory (the residual stream) is a list of 2,560 numbers that runs through the model's 32 layers; each layer reads it and adds to it. A direction is a list of 2,560 numbers of length 1. The coordinate of a state along a direction is their dot product: how far the state leans that way. Removing a direction from a state sets that coordinate to zero and leaves the rest. Two directions are orthogonal when their dot product is zero. The emergency family is four orthogonal directions along which emergencies differ from routine cases at layer 16.

The four claims

What was proved, in words and in symbols

Everything below is stated for an abstract real inner product space, so it holds in the model's 2,560 dimensions and in the two-dimensional picture under the claims alike. In the symbols, ⟨a, b⟩ is the dot product, ‖a‖ is the length, and remove_u(v) = v − ⟨v, u⟩ u is the removal of the direction u from the state v.

Removing a direction leaves nothing along it. If ‖u‖ = 1 then ⟨remove_u(v), u⟩ = 0 for every state v. (Lean: inner_removeAlong_self.) The proof is two lines of algebra: expand the dot product and use ⟨u, u⟩ = 1.

A guarded direction leaves every emergency coordinate alone. Build the guarded direction by subtracting from the advice direction its components along each member of the emergency family. If the family is orthonormal, the guarded direction is orthogonal to every member (inner_guard_eq_zero), stays so when rescaled to length 1 (inner_smul_guard_eq_zero), and then ⟨remove_g(v), e⟩ = ⟨v, e⟩ for every state v and every member e of the family (inner_removeAlong_guard).

The guarantee reaches every depth. Model the working memory after n layers as the embedding plus the sum of each layer's write, where the writes may be anything. If the direction is removed from the embedding and from every write, the memory has no component along it at any depth (inner_stream_edited_self), and every coordinate orthogonal to the removed direction equals what it would be without the removal, for the same writes (inner_stream_edited_coord). The last clause is the whole story: the theorem is about the coordinates of whatever the layers write, not about what they write, and the layers of the edited model write different things because they read an edited memory.

A shut switch is the identity. The conditional edit subtracts the push only when the switch is open (gated_false), the switch is shut whenever the emergency score is above its threshold, whatever the advice score (switch_eq_false_of_emergency), and so on any message with an emergency score above the threshold the edited model returns the unchanged state (gated_switch_identity_of_emergency). This is the theorem the working version rests on.

Direction removed35°

v: the stateu: the direction removede: the emergency axisv′: v with u removed

quantity	value	what the theorem says
⟨v′, u⟩	0.00	always 0 (claim 1)
⟨u, e⟩	0.82	0 when the guard is on
e-coordinate of v	1.60
e-coordinate after the removal	0.01	equal to the row above when ⟨u, e⟩ = 0 (claim 2); otherwise it moves

Drag the slider to turn the removed direction. Turn the guard on to make it orthogonal to the emergency axis and watch the e-coordinate stop moving. The theorems say the same holds in 2,560 dimensions, for every state and every depth of the network.

Figure 1. Claims 1 and 2 in two dimensions, computed live. The grey arrow is a fixed state v, the blue arrow is the direction u being removed (turn it with the slider), the orange arrow is the emergency axis e, and the green arrow is v with u removed. The first row of the table is always zero, whatever the angle: that is claim 1. The last row moves as the angle changes, until the guard is switched on and u is made orthogonal to e; then it equals the e-coordinate of v and stays there: that is claim 2. The theorems say the same holds in the model's 2,560 dimensions, for every state and, by claim 3, at every layer.

The measurements

The saved edit satisfies the hypotheses to rounding, and the proved invariant holds in the real model

A theorem is only as good as its hypotheses. The saved edit is a file of 32-bit floating-point numbers, so the guarded direction has length 1 only to rounding and the emergency family is orthonormal only to rounding. The table gives the measurements, from the script that checks them. The last row is the one that matters most: the permanent removal was applied to the real model's weights (the embedding and all 64 output matrices, in 16-bit arithmetic), and the largest component along the removed direction at any of the 32 layers, at the moment the model starts its reply, was 0.010 on vectors of length 2 to 54. Claim 3 says zero; 16-bit arithmetic says 0.010. The invariant held. The call-911 answer broke anyway: replies naming 911 on the first line fell from 20 to 3 of 24 emergencies, as the education-not-advice page reports.

quantity	value	theorem it belongs to
Norm of the guarded direction (the theorems need exactly 1)	0.9999990	claims 1 and 3
How far the emergency family is from orthonormal (the theorems need exactly orthonormal)	0.000000002	claim 2
Largest dot product between the guarded direction and the emergency family (the theorems need 0)	0.00000007	claim 2
Dot product of the unguarded advice direction with the emergency direction	+0.023	why the guard was needed
Part of the advice direction that lay inside the emergency family, as a share of its length	0.228
Component along the removed direction after the removal, on a random vector of length 5,045 (64-bit arithmetic)	0.00008	claim 1
Change in the emergency coordinates after that removal	0.000003	claim 2
Component along the removed direction in the real model after the weight edit, largest over 32 layers, on vectors of length 2 to 54 (16-bit arithmetic)	0.010	claim 3

Table 1. Each value is a dot product, a length or a difference of dot products, measured on the saved vectors in 64-bit arithmetic, and in the last row on the model's working memory after the weight edit in 16-bit arithmetic. A value of zero would satisfy the theorem exactly; the values shown are the sizes of floating-point rounding.

What a proof buys here

Precision about the claim, not confidence in the model

The proofs did not find a mistake in the edit, and they could not have found the reason it failed, because the reason lies in the parts of the model the theorems leave abstract: the normalisation and the attention and feed-forward computations inside each layer, which read the whole memory and not only the protected coordinates. What the proofs buy is a clean statement of what "protected by construction" meant, so that the sentence "the emergency coordinates were preserved and the answer still broke" is a fact with both halves nailed down, not a puzzle. They also pin the working version to its one-line reason: when the switch is shut, nothing happens. The empirical questions stay empirical. Where the switch opens on messages it has not seen, whether the explanation the edited model writes is true, and what two readers call it are answered on the education-not-advice page, not here.

Limits

What this page does not show

The theorems are about exact real numbers. The model runs in 16-bit floating point, and the table shows the size of the gap, which is small but not zero.
The residual-stream model in claim 3 is the sum of the embedding and the layer writes, which is how these models are built, but the theorem treats each write as an arbitrary vector and says nothing about how a write depends on the memory it reads.
The switch theorem is about the rule, not about the scores: whether a message gets the right advice score and emergency score is the empirical question the other page measures.
Eleven theorems, one file, one evening. The Lean source is 120 lines; a reader who knows Lean can check every step in about three minutes of build time.

Full record: the Lean file is lean/EduProofs/Invariants.lean in the interp-lab repository, with the project files to rebuild it; the typeset statements and proofs are the PDF; the numeric check is scripts/edu_lean_check.py and its output is under outputs/edu_surgery/lean. The proofs were built on a second machine because the Mathlib library needs about 7 gigabytes of disk.

Log

2026-11-03Five definitions and eleven theorems in Lean 4 with Mathlib: the removal of a direction, the guarded direction, the residual stream at every depth, and the switch; the hypotheses measured on the saved edit and the invariant measured on the real model after the weight edit; a live two-dimensional figure; the typeset PDF.

Education, not advice — An edit inside a small chat model that makes it explain medicine but stop giving personal advice, without touching its emergency answer.
Circumstance-sensitive triage — How one sentence about a rural patient's life shifts emergency advice in small chat models.