Glossary

Aeneas and Charon

say: ee-NEE-as, SHAR-on

Tools that turn Rust code into Lean, so the actual Rust can be proved correct.

Charon reads the compiled form of a Rust program. Aeneas rewrites it as plain Lean definitions, one per function. A proof about the Lean version is a proof about the Rust.

See Lean 4, Refinement.

• Aeneas
• Charon
• Ho and Protzenko, 2022

Application, f x

say: f of x

Writing two things side by side means: give the second to the first. f x is “f given x”.

Like a machine f with a slot: put x in the slot. Several in a row are given one at a time, left to right: f a b means give f the thing a, then give the result b. Brackets change the order: f (g x) gives x to g first, then the answer to f.

In the tree pictures, every fork is one application: left branch given right branch.

See Combinator.

Attention

The part of a transformer that looks back at every earlier word to decide the next one.

For each new word, attention compares it with every stored earlier word and takes a weighted mix. So it must keep all of them (the key-value cache), and the work per word grows with the length of the text (Vaswani et al., 2017).

See State space model, Linear attention.

• Vaswani et al., 2017

Automatic differentiation

Getting a program to compute exact slopes of its own output, by carrying slopes alongside values.

Forward mode runs the program on dual numbers: each value carries its slope in the ε slot, and the rules of arithmetic keep the slopes right. Reverse mode, used to train neural networks, runs backwards from the output instead.

See Dual numbers, Derivative, C′.

• Wikipedia: Automatic differentiation

Cayley-Dickson doubling

say: KAY-lee DIK-son

A doubling construction: given an algebra, pair each element with itself under a conjugation twist to build one of twice the dimension. Iterating from the reals gives the complex numbers (dim 2), quaternions (dim 4), octonions (dim 8), sedenions (dim 16). Dickson (1919).

Rafael Bombelli (1572) first used imaginary numbers; Carl Friedrich Gauss (1831) interpreted the complex numbers as ordered pairs of reals. Arthur Cayley and Leonard Dickson systematized the doubling: each step pairs (a, b) with the conjugation rule. Division totality holds up to dimension 8 (Hurwitz, 1898); the 16-dimensional sedenions have zero divisors. In Apeiron: Doubling/CayleyDickson.lean.

See Quaternions, Octonions, Sedenions, Normed division algebra.

• Dickson, 1919
• Cayley-Dickson construction (Wikipedia)

Combinator

A rule for rearranging whatever it is given. It contains no numbers, only a pattern of what goes where.

K keeps its first input and drops its second. S hands its third input to its first two and combines the results. From just these two rewriting rules you can build any computation a computer can do (Schönfinkel, 1924; Curry, 1930).

Combinators are the smallest known way to compute. There is no memory, no loop and no number: only giving things to things and rewriting.

See K, keep, S, share, Iota, ι.

• Schönfinkel, 1924

Compiler fixpoint

Compile a compiler with itself until the output stops changing.

It shows the build is repeatable. It does not show the compiler is correct: a bug that copies itself survives it (Thompson, 1984).

See Trusted computing base.

• Thompson, Reflections on Trusting Trust

Complex numbers, ℂ

say: complex numbers

The algebra with x·x = −1, usually written with i. Multiplying by a size-1 number turns the plane.

The elliptic face, σ = −1. Usually the letter i is used instead of x, so i·i = −1.

Multiplying by cos t + i·sin t turns every point of the plane around the centre by angle t. No squashing, no stretching. Every non-zero number can be divided by, so this is a field, like the ordinary numbers.

Complex numbers run most of physics and signal processing: anything that repeats (waves, spins, orbits) is a turning.

See The three faces, Cosine and sine, Field.

• Wikipedia: Complex number

Contraction

A system is contracting if any two of its runs get closer every step, so it forgets where it started.

Lohmiller and Slotine (1998): if every step shrinks the distance between any two states, then all runs converge, and small disturbances die out. In the plane, multiplying by an element of norm below 1 does exactly that: distances shrink by the same factor every step.

See The norm, N, State space model.

• Lohmiller and Slotine, 1998

Coordinates

Two numbers that find a point: how far across, and how far up.

Cross two number lines at their zeros. To reach a point, go a across (right if positive, left if negative), then b up (down if negative). The pair (a, b) is the point's coordinates. René Descartes made this the standard in 1637.

On this site the pair is written a + b·x: a in the first slot, b in the second, and x marks the second slot.

See The plane, The pair.

Cosine and sine

say: cos, sine

Walk around a circle of radius 1 by distance t. cos t is how far right you are; sin t is how far up.

Start at the rightmost point of a circle of radius 1 and walk anticlockwise a distance t along it. Your position is (cos t, sin t). After t = 2π ≈ 6.283 you are back where you started. This is the elliptic flow(σ, t).

See The flow, flow(σ, t), Complex numbers, ℂ.

CSS matrix()

How a web page describes a linear map: matrix(a, b, c, d, e, f) moves (x, y) to (a·x + c·y + e, b·x + d·y + f).

Every rotate, skewX and scale in CSS is a special case. This site writes every one as matrix(C, σS, S, C, 0, 0), which is multiplication by (C, S) in the algebra.

See Matrix.

• MDN: matrix()

Decidable

A yes-or-no question is decidable if some step-by-step procedure always finishes and always gives the right answer.

“Is 91 a prime number?” is decidable: try dividing by every number from 2 to 90. The list has an end, so the procedure always finishes. (The answer is no: 91 = 7·13.)

“Does this program ever stop?” is not decidable in general. Some questions of this kind have answers nobody can compute, no matter how clever the method. See halting problem.

Decidable does not mean easy or fast. It means an answer is guaranteed to come.

See The halting problem, Total.

Derivative, C′

say: C prime

How fast something changes. C′ ("C prime") is the rate at which C changes as time moves on.

If a car's position is C, then C′ is its speed. The flow is defined by two rates:

Said plainly: the first slot changes at σ times the second, and the second changes at the first. Start at (1, 0) and let it run.

See The flow, flow(σ, t).

Determinant

The number that says how much a matrix scales areas. Rows (p, q) and (r, s) give p·s − q·r.

A square of area 1 becomes a slanted box. The box's area is the determinant. Negative means the picture is also flipped.

For the multiplication-by-z matrix, rows (a, σb) and (b, a): a·a − σb·b = a² − σb², which is the norm. So the norm is the area scale.

See The norm, N, Matrix.

Dual numbers

say: dual numbers

The algebra with x·x = 0, usually written with ε. Multiplying by a size-1 number slides the plane sideways.

The parabolic face, σ = 0. Usually written with ε (Greek e, "epsilon"), so ε·ε = 0 even though ε is not 0.

Multiplying by 1 + t·ε sends (a, b) to (a, b + t·a): every point slides up by an amount that depends on how far right it is. That is a shear.

A useful trick. Because ε² = 0, putting a + ε into a formula gives the formula's value and its slope: f(a + ε) = f(a) + f′(a)·ε. Example with f(y) = y²: (3 + ε)² = 9 + 6ε + ε² = 9 + 6ε, and 6 is the slope of y² at 3. That is forward-mode automatic differentiation. Clifford introduced these numbers in 1873.

See Shear, Automatic differentiation, Derivative, C′.

• Wikipedia: Dual number

Exponential, eᵗ

say: e to the t

Growth where the speed of growth equals the current size. e ≈ 2.718.

e¹ ≈ 2.718, e² ≈ 7.389, e⁰ = 1, and e⁻ᵗ = 1/eᵗ shrinks towards 0. The squeeze stretches one diagonal by eᵗ and shrinks the other by e⁻ᵗ; the product is 1, so area is kept.

Field

A number system where you can add, subtract, multiply, and divide by anything except zero.

The ordinary real numbers are a field. So are the complex numbers. The dual and split-complex numbers are not: they have zero divisors, and you cannot divide by those.

See Zero divisor.

GGUF

say: G G U F

The single-file format llama.cpp uses to store a language model's weights and settings.

A header of settings, then named tables of numbers (tensors), usually quantised.

See Quantisation, llama.cpp.

• GGUF specification

Group

A collection of moves you can combine, undo, and that includes doing nothing.

Think of turning a picture: any two turns combine into one turn; every turn can be undone by turning back; and "no turn" is one of them. Anything with those three properties is a group. The elements with norm 1 form a group: multiply two and the norm is still 1, and the z̄ undoes each one.

See One-parameter group.

Holographic bound

The most information a region of space can hold grows with its surface area, not its volume.

Pack more and more bits into a ball and eventually it collapses into a black hole. The limit is set by the area of the ball's surface: about one bit per 4·ln 2 Planck areas (l_P ≈ 1.6×10⁻³⁵ m). Bekenstein (1981) found the bound for ordinary matter; 't Hooft (1993) and Susskind (1995) turned it into the holographic principle. For the region inside the cosmological horizon it comes to about 10¹²² bits.

See Turing machine, Ryu–Takayanagi formula.

• Bekenstein, 1981
• Bousso, The holographic principle (2002)

Hyperbolic cosine and sine

say: cosh, shine

The hyperbola's version of cos and sin: cosh t = (eᵗ + e⁻ᵗ)/2, sinh t = (eᵗ − e⁻ᵗ)/2.

Instead of a circle, walk along the hyperbola a² − b² = 1. Your position is (cosh t, sinh t). Unlike the circle you never come back: both keep growing. This is the hyperbolic flow(σ, t).

See The flow, flow(σ, t), Exponential, eᵗ.

I, do nothing

say: I

I x → x. I hands back exactly what it was given.

The identity: it changes nothing. It does not need its own rule, because S K K x → K x (K x) → x does the same thing.

See Combinator.

iff

say: if and only if

Short for "if and only if": both statements are true together or false together.

"A iff B" means A and B always go together: whenever one is true, so is the other. Example: a whole number is even iff its last digit is 0, 2, 4, 6 or 8.

insert_with

say: insert with

Put a value in a table. If something is already there, combine the two with a chosen rule.

The rule picks what the table is: keep the old value (a set), keep the new one (a map), add them (a counter), or join them into a list (a graph).

Iota, ι

say: eye-OH-tuh

ι x → x S K. The one rule that hands S and K to whatever it is given. S, K and I can all be made from ι alone.

Found by Chris Barker (2001). Give ι to itself and watch:

• ι ι behaves as I (do nothing)
• ι (ι (ι ι)) behaves as K (keep)
• ι (ι (ι (ι ι))) behaves as S (share)

So one symbol and one rule are enough for all computation. ι is also a pair: the pair that holds S and K. In Apeiron's Lean corpus these are iota_is_I, iota_is_K, iota_is_S and iota_eq_pack.

See Combinator, The pair.

• Barker, Iota and Jot (2001)

Isomorphic

The same structure with different labels: a perfect translation that keeps every sum and product.

Two number systems are isomorphic if you can rename every element of one as an element of the other so that all sums and products still come out right. Roman numerals and Arabic numerals describe isomorphic arithmetic: the numbers are the same, only the writing differs.

K, keep

say: K

K a b → a. K keeps the first thing and throws the second away.

Given a then b, answer a. Example: K 3 7 → 3. Paired with K I, which answers the second instead, it is a yes-or-no choice.

See Combinator, S, share.

Lean 4

A programming language that checks mathematical proofs. A theorem is accepted only if the proof checks.

You write a statement and a proof. A small program (the kernel) checks every step. If one step is wrong, the whole thing is rejected. Mathlib is its shared library of mathematics.

• lean-lang.org

Letters for numbers

A letter like a or b stands for a number we have not chosen yet.

In maths a letter is a box that holds a number. a + b means: take whatever number is in a, add whatever is in b.

Why bother? Because then one sentence covers every number at once. a·b = b·a says 3·4 = 4·3, and 7·2 = 2·7, and every other pair, in one line.

On this site a, b, c, d are ordinary numbers, and x is special: see ℝ[x]/(x² − σ).

See The dot, ·.

Level set

All the points where some quantity has the same value, like a contour line on a map.

On a hiking map, a contour line joins every point at the same height. A level set of the norm joins every point with the same N. Multiplying by an element with N = 1 never moves a point off its level set, which is why the dots in the figures ride along the gold curves.

See The norm, N.

Linear attention

A version of attention rewritten so everything seen so far is folded into one fixed-size summary.

Katharopoulos et al. (2020) showed that removing one step (the softmax) lets attention be computed as a running sum: a fixed-size state updated once per word. The model becomes a recurrent network.

See Attention, State space model.

• Katharopoulos et al., 2020

Linear integer arithmetic decider

A program that answers, with proof either way, whether some whole-number equations and inequalities can all be true at once.

Only adding, multiplying by fixed numbers, = and ≤, with no "for all". Such questions always have an answer that can be computed. Song's decider returns either a solution or a proof that none exists, and a separate checker re-checks the proof.

See Compiler fixpoint.

Linear map

A way of moving every point of the plane that keeps straight lines straight and keeps the centre fixed.

Stretch, squash, turn, slide, flip, or any mix of these. Grid lines stay straight and evenly spaced, and the centre stays put. Multiplying every point by a fixed z is a linear map, and every linear map of the plane is written as a 2×2 matrix.

See Matrix, Determinant.

llama.cpp

say: llama C P P

The most widely used open-source program for running language models on ordinary computers.

Written in C and C++. It defines GGUF and is the usual speed baseline for local models.

• llama.cpp

Lorentz boost

say: LO-rents

A transformation between inertial frames at constant relative velocity. In the split-complex plane, multiplication by cosh(t) + x times sinh(t), which has norm 1 and maps hyperbolas to themselves. Lorentz (1904).

Hendrik Lorentz (1904) and Henri Poincare (1905) formulated the boost as a linear map mixing space and time coordinates. In the split-complex algebra (sigma = +1), the norm-1 element cosh(t) + x sinh(t) acts as a squeeze: it stretches one null axis by e^t and compresses the other by e^(-t), preserving all hyperbolas. The parameter t is the rapidity; velocities do not add, but rapidities do.

See Split-complex numbers, Rapidity, Squeeze.

• Lorentz, 1904

Madelung equations

say: MAH-deh-loong

The hydrodynamic form of the Schrodinger equation: writing psi = sqrt(rho) times exp(iS/hbar) splits it into a continuity equation for density rho and a Hamilton-Jacobi equation for phase S. Madelung (1927).

Erwin Madelung (1927) showed that any solution of the Schrodinger equation can be written in polar form, where the imaginary part carries a quantum potential Q = -hbar^2 times the Laplacian of sqrt(rho), divided by 2m times sqrt(rho). Within the quadratic window (Hamiltonians at most quadratic in position and momentum), Q vanishes and the Madelung equations reduce exactly to classical Hamilton-Jacobi theory.

See Wick rotation, The flow, flow(σ, t).

• Madelung, 1927

Matrix

A small table of numbers that says how a linear map moves points: where the right-pointing and up-pointing arrows go.

A 2×2 matrix has two rows of two numbers. Its two columns say where the arrow (1, 0) and the arrow (0, 1) land. Every other point follows, because every point is a mix of those two.

Multiplying by z = a + b·x sends (1, 0) to (a, b) and (0, 1) to (σb, a), so its matrix has rows (a, σb) and (b, a).

See Linear map, Determinant, CSS matrix().

Normed division algebra

An algebra where every non-zero element is invertible and the norm satisfies N(ab) = N(a)N(b). Over the reals, exactly four exist: the reals (dim 1), complex numbers (dim 2), quaternions (dim 4), octonions (dim 8). Hurwitz (1898).

Adolf Hurwitz proved in 1898 that the only finite-dimensional normed division algebras over the real numbers are the reals, complex numbers, quaternions, and octonions. The proof uses the composition property N(ab) = N(a)N(b) to restrict possible dimensions to powers of two and then to exactly 1, 2, 4, and 8. This is the Hurwitz theorem, formalized in Apeiron as HurwitzTraversal.lean.

See Cayley-Dickson doubling, Quaternions, Octonions, Sedenions.

• Hurwitz, 1898

Numbers as repetition (Church numerals)

say: church numeral

The number n is the rule “given f and x, apply f to x n times”. 2 f x → f (f x).

• 0 f x → x (do it no times)
• 1 f x → f x
• 2 f x → f (f x)
• 3 f x → f (f (f x))

Built from S and K: 0 = K I, and “one more” is S (S (K S) K). Alonzo Church introduced numbers this way in the 1930s.

See Combinator.

Octonions

say: ok-TOH-nee-onz

The eight-dimensional normed division algebra: non-commutative and non-associative; the last division algebra over the reals. Graves (1843), Cayley (1845), Hurwitz (1898).

John T. Graves discovered the octonions in December 1843; Arthur Cayley published them independently in 1845. Adolf Hurwitz proved in 1898 that the reals, complex numbers, quaternions, and octonions are the only normed division algebras over the reals. The automorphism group of the octonions is the exceptional Lie group G2. In Apeiron: Doubling/Octonion.lean.

See Cayley-Dickson doubling, Quaternions, Sedenions, Normed division algebra.

• Hurwitz, 1898

One-parameter group

A family of moves, one for each number t, where doing t then s is the same as doing t + s.

Turning by 10° then 20° is turning by 30°. Turning by 0° is doing nothing. That makes "turn by t" a one-parameter group. The flow(σ, t) is one on every face.

See The flow, flow(σ, t), Group.

Palmieri obstruction

say: pal-mee-EH-ree

The theorem that no commutative, associative binary operation can produce a discarding combinator K. Proved in Apeiron as no_K_of_comm_assoc in Implicative.lean.

John H. Palmieri proved in 2026 (arXiv:2603.27007) that finite extensional magmas cannot combine a classifier and retraction pair under associativity. In Apeiron, no_K_of_comm_assoc and idem_no_K in Implicative.lean prove that no commutative, associative algebra operation can act as a discarding combinator K. Bilinearity also forces (K·a)·0 = 0, so combinatory application must operate in an autonomous term calculus rather than as linear algebra multiplication.

See K, keep, Combinator, Cayley-Dickson doubling.

• Palmieri, 2026 (arXiv:2603.27007)

Peirce decomposition

say: PURSE deh-kom-poh-ZI-shun

The splitting of an algebra by two orthogonal idempotents: e+ times e- equals 0 and e+ plus e- equals 1. Each idempotent projects onto one independent channel. Benjamin Peirce (1870).

Benjamin Peirce introduced the decomposition of a linear associative algebra into orthogonal idempotent summands in his 1870 memoir (lithographed 1870; published with addenda by Charles Sanders Peirce in 1881). In the hyperbolic face (sigma > 0), the two projectors e+ = (1 + x/sqrt(sigma))/2 and e- = (1 - x/sqrt(sigma))/2 satisfy e+^2 = e+, e-^2 = e-, e+e- = 0, and e+ + e- = 1. In Apeiron: complementary_idemPlus and the_razor in DotToTorus.lean.

See Unchanged by itself: x·x = x, Split-complex numbers, Zero divisor.

• Peirce, 1870

Polynomial

A sum of powers of a letter with numbers in front, like 3 + 2x + 5x².

Built only from adding and multiplying: no dividing by the letter, no square roots. λ² − qλ − p is a polynomial in λ.

See Root.

Power series, Σ

say: sum

Σ (capital sigma) means add up a list. A power series is an endless sum like 1 + t + t²/2 + t³/6 + …

Σ is a capital Greek S, for Sum. k! ("k factorial") is 1·2·3·…·k, so 3! = 6. The flow can be written as endless sums:

Put σ = −1 and you get cos and sin; σ = +1 gives cosh and sinh; σ = 0 leaves 1 and t. One formula, three faces, and it changes smoothly as σ passes through zero.

See The flow, flow(σ, t).

Quantisation

Storing a model's numbers with fewer bits each, for example 4 instead of 16, plus a shared scale per block.

Running a model reads every weight once per word it writes, so memory speed usually limits it. Fewer bits per weight means less to read, at some cost in accuracy.

See GGUF.

Quaternions

say: kwah-TER-nee-onz

The four-dimensional normed division algebra: elements a + bi + cj + dk with i squared = j squared = k squared = ijk = minus 1. Non-commutative but associative. Hamilton (1843).

William Rowan Hamilton discovered quaternions on 16 October 1843. Every non-zero quaternion has a multiplicative inverse; the norm satisfies N(pq) = N(p)N(q). They appear in 3-D rotation, Clifford algebras, and the Cayley-Dickson tower as the second doubling step. In Apeiron: Doubling/Quaternion.lean.

See Cayley-Dickson doubling, Octonions, Normed division algebra.

• Hamilton, 1843

Rapidity

say: ruh-PID-ih-tee

The additive parameter of a Lorentz boost: tanh(t) = v/c gives the velocity, but rapidities add directly where velocities do not. Robb (1911).

Alfred Robb introduced rapidity in 1911 as the natural parameter for composition of boosts. If two frames move with rapidities t1 and t2, their combined rapidity is t1 + t2. In the split-complex plane, the boost by rapidity t is multiplication by cosh(t) + x sinh(t), and the group law flow(sigma, s) times flow(sigma, t) = flow(sigma, s+t) is exactly additivity of rapidity, proven as flow_add in Apeiron.

See Lorentz boost, Split-complex numbers, The flow, flow(σ, t).

• Robb, 1911

Refinement

A proof that fast, complicated code gives the same answers as a short, obviously-right definition.

Example: word_mul_denote proves the 64-bit Rust multiplication in Apeiron equals the canonical ringMul, computed in 64-bit wrap-around arithmetic, on every input.

See Aeneas and Charon, Lean 4.

Return address

Where a function jumps back to when it finishes, stored in memory right next to its local data.

When a C function runs, its local buffers and the address to return to sit side by side on the stack. Write past the end of a buffer and you overwrite the return address. When the function finishes, the machine jumps wherever the attacker's bytes say. That is a stack buffer overflow (Aleph One, 1996).

• Aleph One, Smashing the Stack for Fun and Profit (1996)

Root

A number that makes a polynomial equal zero. λ² − 4 has roots 2 and −2.

Draw the polynomial as a curve. The roots are where the curve crosses the flat axis. A curve like λ² − σ crosses twice if σ is above 0, touches once if σ is 0, and misses entirely if σ is below 0. That count is the face.

See Polynomial, Why there are only three.

Rotary position embedding (RoPE)

Tell a model where a word is by turning pairs of its numbers by an angle that grows with position.

Each pair of numbers is treated as a point in the plane and turned by angle θ·position: multiplication by flow(−1, θ·position), the elliptic flow. Because turns add, the angle between two words depends only on how far apart they are (Su et al., 2021).

See The flow, flow(σ, t), Complex numbers, ℂ.

• Su et al., 2021

Ryu–Takayanagi formula

In holography, how entangled a region of the boundary is equals the size of the shortest surface hanging into the interior.

In a space with a boundary (like the rim of the Poincaré disc), pick a stretch of the rim. The shortest path through the inside that joins its two ends has a length, and that length gives the stretch's entanglement entropy (Ryu and Takayanagi, 2006). Geometry inside, information on the edge.

See Holographic bound.

• Ryu and Takayanagi, 2006

S, share

say: S

S f g x → f x (g x). S hands x to both f and g, then hands g's answer to f's.

S is how one input is used twice. Written out: first work out f x and g x, then give the second to the first. With K it can build every other combinator.

See Combinator, K, keep.

Sedenions

say: seh-DEE-nee-onz

The 16-dimensional Cayley-Dickson algebra: contains zero divisors, so it is not a division algebra. The first step past the Hurwitz barrier. Dickson (1919).

Applying the Cayley-Dickson doubling to the octonions produces the sedenions. They lose the division property: non-zero elements exist whose product is zero. The zero-divisor set forms a 9-dimensional manifold. Despite the loss of division totality, the sedenions retain a norm satisfying N(ab) = N(a)N(b) on the zero-divisor complement. In Apeiron: Doubling/Sedenion.lean.

See Cayley-Dickson doubling, Octonions, Zero divisor, Normed division algebra.

• Dickson, 1919

Shear

Slide each row sideways by an amount proportional to its height, like pushing the top of a deck of cards.

Areas stay the same and flat lines stay flat. On this site's panels, flow(0, −0.24) is a shear, which is what makes them lean. CSS calls it skewX.

See Dual numbers, CSS matrix().

SPIR-V

say: spur-V

A vendor-neutral instruction format for GPU programs, used by Vulkan.

Instead of writing for one company's GPUs (CUDA is NVIDIA's), a SPIR-V program runs on any GPU with a Vulkan driver.

• Khronos: SPIR-V

Split-complex numbers

say: split complex

The algebra with x·x = +1, often written with j. Multiplying by a size-1 number squeezes the plane.

The hyperbolic face, σ = +1, often written j, with j·j = 1 but j ≠ 1 and j ≠ −1.

Multiplying by cosh t + j·sinh t stretches the plane along one diagonal and squashes it along the other by the same factor. That is a squeeze, and in physics it is how speed mixes space and time (a Lorentz boost).

Something odd happens here: (1 + j)(1 − j) = 1 − j² = 0. Two things that are not zero multiply to zero. See zero divisor. James Cockle described these in 1848–49.

See Squeeze, Zero divisor, Hyperbolic cosine and sine.

• Wikipedia: Split-complex number

Squared, x²

say: x squared

x² ("x squared") means x·x, a number times itself. 3² = 9.

The small raised 2 means: multiply the number by itself.

• 3² = 3·3 = 9
• (−3)² = (−3)·(−3) = 9. A minus times a minus is a plus, so a square of an ordinary number is never below zero.
• 0² = 0

That last fact is the whole reason this site's algebra is interesting. An ordinary number squared cannot be −1. So we invent a new thing, x, and simply declare what x² is. See σ.

See σ (sigma), The algebra ℝ[x]/(x² − σ).

Squeeze

Stretch along one diagonal and squash along the other by the same factor, so area is kept.

Multiply by cosh t + x·sinh t at σ = +1: one diagonal grows by eᵗ, the other shrinks by e⁻ᵗ. In special relativity, with one space direction, this is a Lorentz boost, and t is the rapidity: rapidities add, speeds do not.

See Split-complex numbers, Exponential, eᵗ.

• Wikipedia: Rapidity

State space model

A model that keeps a fixed-size state and updates it once per input: new state = A·old state + B·input.

Borrowed from control theory. Memory does not grow with the length of the input, and the next step costs the same no matter how much came before. S4 (Gu, Goel and Ré, 2021), Mamba (Gu and Dao, 2023), Mamba-2 (Dao and Gu, 2024), DeltaNet (Yang et al., 2024) and Mamba-3 (Lahoti et al., 2026) are the line of work.

See Attention, Contraction, Rotary position embedding (RoPE).

• S4
• Mamba
• Mamba-2
• Mamba-3

The algebra ℝ[x]/(x² − σ)

say: R x mod x squared minus sigma

Pairs of numbers a + b·x, added slot by slot and multiplied using one rule: x·x = σ.

An element is a pair of real numbers written a + b·x. The x is a label that marks the second slot, like the i in complex numbers.

Adding is slot by slot: (1 + 2x) + (3 + 4x) = 4 + 6x.

Multiplying is what you learned at school (multiply everything by everything), plus one rule: wherever x·x appears, write σ instead. Worked, with σ = −1:

In general:

The name ℝ[x]/(x² − σ) says how it is built: ℝ[x] is all expressions in x with real numbers in front, and "/ (x² − σ)" means we treat x² − σ as zero, which is the same as x² = σ.

See σ (sigma), The norm, N, The three faces, The dot, ·.

The arrow, →

say: becomes

“Becomes”. The left side is replaced by the right side, one step at a time.

K a b → a means: wherever you see K a b, you may replace it with a. Computation, for combinators, is nothing more than doing these replacements until none are left.

The conjugate, z̄

say: z bar

Flip the sign of the second slot: the conjugate of a + b·x is a − b·x.

Written with a bar on top, said "z bar". Multiply an element by its conjugate and the x part cancels, leaving one plain number, the norm:

Example, σ = −1: (3 + 4x)(3 − 4x) = 9 + 16 = 25.

See The norm, N.

The dot, ·

say: times

A raised dot means multiply. 3·4 means 3 times 4, which is 12.

A raised dot means multiply. It is the same as ×, written smaller so it does not look like the letter x.

• 3·4 = 12
• 2·5·10 = 100

When letters stand for numbers, the dot is often left out: ab means a·b, and 2x means 2·x.

See Letters for numbers.

The flow, flow(σ, t)

say: flow of sigma at t

Start at 1 and move steadily along the curve of norm-1 points. Where you are at time t is flow(σ, t).

Two facts at every σ. It never leaves the curve: N(flow(σ, t)) = 1. And flowing for s then for t equals flowing for s + t. Physically, t is twice the area swept by the line from the centre to the moving point, so the second fact says swept areas add.

See One-parameter group, The norm, N, Derivative, C′.

The halting problem

The question “does this program ever stop?” No program can answer it correctly for every program (Turing, 1936).

Suppose a perfect checker existed. Build a program that asks the checker about itself and then does the opposite: loops forever if the checker says it stops, stops if the checker says it loops. The checker is wrong either way, so it cannot exist.

This is why careful systems either restrict themselves to programs that must stop (bounded loops), or give a checker a step budget and let it say “ran out” instead of guessing.

See Decidable, Turing machine.

• Turing, 1936

The norm, N

say: norm

N(a + b·x) = a² − σb². It says how much multiplying by an element grows or shrinks areas.

Every element gets one number:

Example with σ = −1: N(3 + 4x) = 9 − (−1)·16 = 25.

What it means, physically. Multiply every point of the plane by z. A square of area 1 becomes a slanted box of area N(z). If N(z) is negative the picture is also flipped like a mirror. If N(z) = 0 the plane is squashed flat onto a line.

Why it matters. Doing z and then w scales area by N(z) and then by N(w), so N(z·w) = N(z)·N(w). Elements with N = 1 keep every area the same. They only move things around, and that is why they are used for motion.

See Determinant, The conjugate, z̄, Zero divisor.

The pair

Something that holds two things, a then b, and hands both to whatever it meets: pair(a, b) given m becomes m a b.

Built only from S and K. Reading it back is a choice: give it K and you get a (keep the first); give it K I and you get b (keep the second).

The same two-slot shape appears again when we hold two numbers: a point on the the plane, written a + b·x.

See K, keep, Coordinates.

The plane

A flat sheet where each point is a pair of numbers: how far right, and how far up.

Take two rulers and cross them. A point is found by two numbers: a (how far right, negative means left) and b (how far up, negative means down). So a pair of numbers is a point, and a point is a pair.

In every figure on this site, a runs left and right and b runs up and down. That is why an element a + b·x can be drawn as a dot.

See The algebra ℝ[x]/(x² − σ), The real numbers, ℝ.

The real numbers, ℝ

say: R, the reals

All the ordinary numbers on a line: whole numbers, fractions, negatives, and ones like π.

Picture a ruler that goes on forever both ways. Every point on it is a real number: 0, 1, −2, 0.5, π = 3.14159…. The blackboard-bold ℝ is the name for all of them together.

"a and b over ℝ" means a and b are real numbers.

See The plane.

The three faces

The three kinds of this algebra: σ below zero (elliptic), zero (parabolic), above zero (hyperbolic).

The names come from the shape you get when you draw all points with norm 1: an ellipse (here a circle), two straight lines (a flattened parabola), or a hyperbola. The same three words sort curves (conic sections) and equations of physics for the same reason: the sign of one number.

See Complex numbers, ℂ, Dual numbers, Split-complex numbers, The norm, N.

Theorem and proof

A theorem is a statement proved true for every case it covers. A proof is the step-by-step argument, and in Lean a program checks every step.

A test checks some cases: “N(zw) = N(z)·N(w) for these 25 pairs.” A proof covers all of them at once: multiply out both sides as formulas, with letters instead of numbers, and show they are the same formula. Then no case can fail, including cases nobody tried.

A proof assistant like Lean refuses any step that does not follow from the rules, so an accepted proof does not depend on anyone's say-so.

See Lean 4, Refinement.

Total

A procedure is total if it gives an answer for every possible input and always finishes.

“Add two whole numbers” is total. “Divide by b” is not, because b = 0 has no answer. A loop that counts to a fixed number is total; a loop that runs “until something happens” may not be. Building only from total pieces is one way to keep every question about a program decidable.

See Decidable.

Trusted computing base

The code that has to be right for everything else to be right, because nothing checks it.

Usually the kernel, the compiler, the loader and the proof checker. Every line in it is trusted, not proved, so smaller is better.

See Compiler fixpoint.

Turing machine

Alan Turing's 1936 model of a computer: a head reading and writing symbols on a tape that never runs out.

A head sits on one cell of a tape, reads its symbol, writes a new one, moves one cell left or right, and repeats, following a fixed table of rules. A universal one can imitate any other. The model assumes the tape is as long as it ever needs to be. No physical tape is.

See Holographic bound.

• Turing, 1936

Unchanged by itself: x·x = x

say: idempotent: EYE-dem-POH-tent

A thing that stays the same when combined with itself. Among ordinary numbers only 0 and 1 do.

Try it: 0·0 = 0 and 1·1 = 1, but 2·2 = 4 and ½·½ = ¼. Only 0 and 1 stay put.

George Boole (1847) used this as the rule of logic: "yes and yes" is just "yes", "no and no" is just "no". That is why computers are built from 0s and 1s, called bits.

In the algebra on this site, two more such things appear when σ is above zero: (1 + x)/2 and (1 − x)/2. They add up to 1 and multiply to 0: the one, split into two halves that do not overlap.

See The dot, ·, Split-complex numbers.

Why there are only three

Every two-slot number system with a 1 in it is one of the three faces, and which one is decided by a sign.

Take any such system and any element w that is not a plain number. Two slots means w² must be made of 1 and w: w² = p + q·w. Shift w by half of q: set x = w − q/2. Then

which is a plain number. Call it σ. Its sign picks the face. Classically due to Weierstrass and Wedderburn; in the Lean corpus, Apeiron.Trichotomy.classification.

See The three faces, Root.

Wick rotation

say: wick

Swapping time t for i·t turns the hyperbolic flow into the elliptic one: waves become circles.

Since cosh(i·t) = cos t, replacing t by i·t swaps the hyperbolic and elliptic flows. Physicists use it to turn time evolution into a heat-like weighting. The elliptic flow comes back after a fixed period; in that picture the period is 1/temperature (the KMS condition).

See The flow, flow(σ, t), The three faces.

• Wikipedia: Wick rotation
• Wikipedia: KMS state

Zero divisor

Something that is not zero but multiplies with something else that is not zero to give zero.

With ordinary numbers, if a·b = 0 then a or b must be 0. That rule breaks here when σ is 0 or above.

• σ = 0: x·x = 0, and x is not zero.
• σ = +1: (1 + x)(1 − x) = 1 − x² = 1 − 1 = 0.

Physically: multiplying by a zero divisor squashes the whole plane onto a line, so information is lost and cannot be undone. That is why you cannot divide by one. They are exactly the non-zero points with norm 0.

See The norm, N, Split-complex numbers.

σ (sigma)

say: SIG-muh

The number we declare x·x to be. Choose it once, then all the multiplying follows.

σ is the Greek letter s, said "sigma". Here it is one real number that we pick at the start, and it answers one question: **what is x·x?**

• Pick σ = −1: then x·x = −1. These are the complex numbers.
• Pick σ = 0: then x·x = 0.
• Pick σ = +1: then x·x = +1.

Any other σ behaves like one of these three. If σ is negative, stretch x by 1/√|σ| and it becomes −1; if positive, it becomes +1. So only the sign of σ matters: below zero, zero, or above zero. Those are the three faces.

See The algebra ℝ[x]/(x² − σ), The three faces.