Research period: September 2–3, 2026 and later formal hardening
Historical anchors: #196, #199, #200, #252
The hypersphere experiments generated several possible explanations for what normalization might be doing: removing an unnecessary magnitude channel, changing optimization, suppressing shortcuts, preserving some directions while contracting others, or changing the long-term dynamics of recurrence. At this point, simply training another model for every plausible explanation was becoming a bad research strategy.
Some of these questions had mathematical answers that could be established before running another experiment. If a proposed mechanism depended on normalization behaving a particular way, I could derive that behavior first and use the result to decide which empirical questions were still meaningful.
That became the beginning of a proof-first layer in the research program: derive what can be derived, keep the assumptions and boundaries explicit, then spend compute on the parts the mathematics cannot decide.
Formal checkpoint: for a nonzero vector
x, normalization isN(x) = x / ||x||. Ifu = x / ||x||, its derivative is
DN_x = (1 / ||x||)(I - uuᵀ)The checked version is available in the public Theorem Library normalization proof.
Radial and tangent directions
The expression I - uuᵀ is a projection: it removes the part of a small change that points in the same direction as u.
That gives normalization two different local behaviors. If I perturb x only by changing its magnitude, the normalized direction doesn't change to first order, so the derivative of that radial perturbation is zero. If I perturb x perpendicular to its radius, the change lies along the surface of the sphere and survives, scaled by 1 / ||x||. At unit radius, that tangent perturbation is preserved to first order.
Sticky note — tangent direction: at a point on a sphere, a tangent direction is perpendicular to the radius through that point. Locally, these are the directions in which you can move along the surface rather than toward or away from its center.
This gave me an exact version of something the earlier experiments had only suggested. Normalization really does remove infinitesimal changes that affect only overall scale while allowing changes in direction to survive locally.
The useful part was the boundary around that statement. The mathematics says what normalization does to perturbations; it doesn't say what those perturbations mean to a language model.
Illustrative example
This two-dimensional calculation illustrates the derivative. The linked Lean sources carry the formal result; this numerical example is not a proof.
Saved output is included so you can inspect the example without starting a kernel. Running it in Lab executes this example only.
import numpy as np
x = np.array([3., 4.]); r=np.linalg.norm(x); u=x/r
DN = (np.eye(2)-np.outer(u,u))/r
radial = u
tangent = np.array([-u[1], u[0]])
print('radial derivative:', DN @ radial)
print('tangent gain:', np.linalg.norm(DN @ tangent))
radial derivative: [-8.39328607e-18 -1.45217172e-17] tangent gain: 0.2
What this changed
That distinction became a template for the next stage of the project.
Suppose an experiment suggests that normalization helps because magnitude contains nuisance variation while direction carries useful information. The derivative above can prove that normalization removes radial variation locally. It cannot prove that radial variation is nuisance information, or that tangent variation contains semantics. Those are properties of the task, representation, and trained model, so they still require measurement.
Separating those two kinds of claims prevents an appealing geometric interpretation from quietly turning into an empirical conclusion.
This also changed how I thought about experiment design. A proposed architecture can depend on assumptions that are already mathematically true, mathematically false, or true only under specific conditions. Deriving those boundaries first can eliminate experiments whose premises are impossible, simplify experiments whose mechanisms are already known, and leave training for questions that genuinely depend on learned behavior.
The resulting workflow became:
hypothesis → derivation / theorem boundary → surviving empirical question → experiment
rather than treating training as the default way to answer every question.
Research context
This proof-first turn also brought the project closer to a broader body of geometric machine-learning research. Work such as nGPT had already shown that Transformer computation could be formulated around normalized states on a hypersphere, so normalization and hyperspherical optimization themselves weren't new ideas. The useful question for this project was narrower: what could the exact mathematics tell me about the mechanism behind the behavior I had already measured?
The literature provided established constructions and mathematical neighborhoods to compare against; the theorem work gave me a way to separate those established facts from claims that were still specific to this representation and task.
What this does not show
The derivative does not establish that radial directions are useless, that tangent directions encode semantics, or that normalization must improve a model. “Useful,” “nuisance,” and “semantic” are task-dependent descriptions; they don't appear anywhere in the normalization theorem.
It also describes a local, first-order effect. Repeated nonlinear updates can behave very differently from one infinitesimal perturbation, so this calculation doesn't identify the long-term dynamics of a recurrent model by itself.
What it does provide is a hard boundary for later explanations: any mechanism story involving normalization has to agree with the mathematics before it earns an experiment.
Public formal sources
These pinned sources state the mathematical assumptions and checked conclusions. They do not establish the empirical interpretation of a model’s learned directions.