Respecting Equality: Complete Inference, Deterministic and Step-Optimal

Definition 0.1 (type, function, dependent pair). A type is a collection of values, written a : A. A function f : A → B maps values to values. For a family P — one type P a for each a : A — the dependent pair Σ[ a ∈ A ] P a holds pairs (a , w) with w : P a.

Definition 0.2 (identity type). Equality is a type: x ≡ y is the type of proofs that x equals y, with refl : x ≡ x. A proof is a value you keep.

Definition 0.3 (the interval). 𝕀 has two endpoints 0 and 1, a meet ∧, a join ∨, and an operation ~ that exchanges the endpoints and reverses order. The laws are: ∧ and ∨ are associative, commutative and idempotent, absorb one another (x ∧ (x ∨ y) = x) and distribute over one another, with 0 the unit of ∨ and 1 of ∧; and ~ 0 = 1, ~ 1 = 0, ~ ~ x = x, ~(x ∧ y) = ~x ∨ ~y. The unit interval [0,1] with min, max and 1 − x satisfies all of this and is a usable picture; what is used below is only these laws, never any property of the real numbers. "Free De Morgan algebra on one generator" is the exact name for that restriction: the elements are the expressions built from one symbol i by ~, ∧ and ∨, and two are equal only where the laws just listed force it. It is built, not assumed.

Definition 0.4 (path). A proof of x ≡ y is a map p : 𝕀 → A with p 0 = x and p 1 = y. refl is the constant map.

Definition 0.5 (contractible). A is contractible when some point of it exists and every element is equal to that point — the whole type collapses onto it.

Definition 0.6 (transport). For a family P, a proof p : x ≡ y gives transport p : P x → P y.

Proposition 0.7 (reversibility of transport). transport is reversible and loses nothing: it runs backward along the reversed path λ i → p (~ i), and transport refl x ≡ x — moving nowhere changes nothing.

Proof. Reversal is ~ from the interval (0.3) applied to the map of paths (0.4). For the second, note what is and is not being claimed: transport refl x is not the same term as x — Agda rejects refl as a proof of it, since transp (λ i → refl i) i0 x has still to be computed — but it is path-equal to x, which is what ≡ asserts and all that is used below. The path is built by filling the constant line (transportRefl in the library). ∎

Theorem 0.8 (the one fact). Σ[ y ∈ A ] (x ≡ y) — the values equal to x, each with its proof — is contractible, with centre (x , refl).

Proof. The path from the centre to any (y , p) slides along p itself: at stage t sit at the point p t, holding as its proof the piece of p from x up to t, which shows x ≡ p t. At t = 0 that is (x , refl); at t = 1 it is (y , p). The piece of p up to t is λ j → p (t ∧ j) — the i ∧ j of the term below. Its two ends follow from 0.3 alone: at j = 0 it is p (t ∧ 0) = p 0 = x, and at j = 1 it is p (t ∧ 1) = p t. So it is a path from x to p t, which is the proof the pair at stage t must carry. That is the whole use of ∧ here: it cuts a path off at a point. ∎

Corollary 0.9 (path induction, J). To act on every (y , p : x ≡ y) it suffices to give the value at (x , refl).

Proof. Transport the value at the centre forward along the contraction path of the one fact (0.8). This is the eliminator of ≡. ∎

Definition 1.1 (the inputs over an output). For f : A → B and b : B, write

f⁻¹(b)  =  Σ[ a ∈ A ] (f a ≡ b)

— the inputs that land on b, each kept with its proof that it does.

Theorem 1.2 (partition by output). A ≃ Σ[ b ∈ B ] f⁻¹(b).

Proof. Forward a ↦ (f a , (a , refl)); backward (b , (a , p)) ↦ a. Both round trips are refl, the return using the kept proof p : f a ≡ b. Nothing is lost, only regrouped. ∎

Definition 1.3 (completion). A completion of f is a family T assigning a type T(b) to each b, together with an equivalence A ≃ Σ[ b ∈ B ] T(b) that respects the output map — an input's b is unchanged.

Theorem 1.4 (the partition is the only one). Every completion of f is f⁻¹.

Proof. Respecting the output map means the equivalence carries the piece over each b to the piece over that same b; by the partition (1.2) the inputs over b on the right are exactly T(b), so it carries f⁻¹(b) onto T(b). A completion is therefore a choice, at each b, of a type equivalent to f⁻¹(b). The types equivalent to a fixed one form a contractible type (2.4), and a per-b choice among contractible options is again contractible (2.5). So T = f⁻¹: the decomposition is forced, not a chosen encoding. ∎

Definition 2.1 (equivalence). A ≃ B is maps both ways with proofs that they cancel: runnable in both directions, nothing lost either way. This is the lossless match the partition (1.2) asserts.

Proposition 2.2 (two sides of one thing). f has a two-sided inverse if and only if f⁻¹(b) is contractible for every b.

Proof. An inverse g centres f⁻¹(b) at (g b , ·), and the cancellation laws contract every (a , p : f a ≡ b) onto that centre (0.5). Conversely, choosing the centre of each f⁻¹(b) is an inverse. ∎

Theorem 2.4 (univalence). ua : (A ≃ B) → (A ≡ B), and it computes: transportua(e) = e. Hence Σ[ X ] (X ≃ Y) is contractible.

Proof. The primitive is the interval (0.3): a path is a map out of the interval (0.4), and paths can be joined end-to-end and pushed along one another — Kan composition, which is what runs transport. The second ingredient is Glue, a type former whose defining property is exactly what is wanted: given a type B, and on part of the boundary a type A with an equivalence A ≃ B, it yields a type that is A on that part of the boundary and B elsewhere. Apply it along one interval coordinate with A and e at the 0 end: the result is a map 𝕀 → Type sending 0 to A and 1 to B, which by 0.4 is a path A ≡ B, and transport along it is e. Contractibility is then the one fact (0.8) read at the universe, with ≡ between types supplied by ua. Voevodsky's axiom, built from the interval and Glue (Cohen–Coquand–Huber–Mörtberg 2018). ∎

Corollary 2.5 (function extensionality). Functions that agree at every argument are equal.

Proof. Given h : (x : A) → f x ≡ g x, the map λ i x → h x i is a path f ≡ g by paths (0.4) — the interval is pulled out of the argument. ∎

Definition 3.1 (reversible). A step is reversible when some map sends its output back to its input, so it runs backward as well as forward, losing nothing (2.1). By reversibility of transport (0.7), transport and every equivalence are of this kind.

Theorem 3.2 (every reversible operation is a transport). A reversible operation is transport along a path, namely the one its own reversibility names, and that path is the only one inducing it.

Proof. Maps both ways whose round trips are the identity are an equivalence (2.1, 2.2), which ua turns into a path A ≡ B (2.4). Transport along that path is the operation, by univalence (2.4)'s computation rule. Uniqueness is ua being an equivalence, again univalence (2.4). ∎

Definition 3.3 (effect-cost). A step is irreversible when several inputs share one output b: then which of them the input was is gone. That forgotten "which one" is the only thing a step can ever destroy. Its effect-cost is the entropy of the input given the output: log₂ of the number of inputs mapping to b when those are equally likely (2ᵏ inputs give k bits), and less when they are not — the count is the most it can be. This is one of the two axes; the other is the number of steps taken (5.7).

Proposition 3.4 (Landauer's principle). Destroying k bits dissipates at least k · k_B T ln 2 of heat, with k_B Boltzmann's constant and T the temperature; a reversible step dissipates 0.

Proof. Landauer in units (5.9), which derives it from reversibility (3.1) and effect-cost (3.3). ∎

Theorem 3.5 (reversibility costs nothing, for any measure). Let ℓ be any ℕ-valued measure that adds under composition with ℓ e = 0. Then ℓ g = 0 wherever g has a right inverse — no group laws are used.

Proof. A sum of naturals is 0 only when each summand is. ∎

Corollary 3.6 (§§1–2 destroy nothing). transport and every equivalence destroy nothing: every construction in §§1–2 runs backward and dissipates no heat.

Proof. Reversibility (3.1) and the vanishing grading (3.5), or reversibility (3.1) and Landauer (3.4) for the bit count alone. ∎

Definition 4.1 (point-surjective). Picture e : A → (A → B) as a table whose row a is the function e a; reading row a at its own index gives e a a, the diagonal. Call e point-surjective when every h : A → B appears as some row, with the row index produced:

onto e  =  (h : A → B) → Σ[ a ∈ A ] (e a ≡ h)

The Σ is untruncated, which is why the fixed point below comes out as a value you can hold.

Theorem 4.2 (Lawvere 1969). If e : A → (A → B) is point-surjective then every g : B → B has a fixed point.

Proof. Put h a := g (e a a), the twist of e by g. Point-surjectivity gives a₀ with e a₀ ≡ h, so

and e a₀ a₀ is a fixed point of g. ∎

The proof reads e at one argument only, so the hypothesis can be weakened to exactly what it uses: it is enough that e hits the single function h. That weaker form, lawvere-one-row in the box, is what the diagonal lemma (4.6) and halting (4.10) supply, where only the definable or computable functions are rows.

Corollary 4.3 (contrapositive). If some g : B → B has no fixed point, no e : A → (A → B) is point-surjective.

Corollary 4.4 (Cantor). No e : A → (A → 2) is point-surjective.

Proof. The contrapositive (4.3) with B = 2, g = ¬: negation swaps true and false, so it has no fixed point. (A → 2) is the decidable subsets of A by characteristic functions — not every subset, which would be maps into propositions. ∎

Lemma 4.5 (representability). Work in a theory with sentences, a derivability predicate ⊢, negation, and a provability formula Prov — the box names these Sent, Pf, neg, prov. Code each one-variable formula by a number and let sub(m , n) be the code of formula m with the numeral n̄ substituted for its variable. Then sub is represented by a formula.

Proof. sub is primitive recursive, and every primitive-recursive function is represented by a formula: induct on how it is built — the base functions (zero, successor, projection) are formulas, and composition and primitive recursion stay first-order by quantifying, boundedly, over the finite run that computes the value. A base as weak as Robinson's Q suffices. ∎

Theorem 4.6 (the diagonal lemma). For every formula ψ there is a sentence G with ⊢ G ↔ ψ(⌜G⌝).

Proof. Lawvere (4.2) in the one-row form, at the table e(m)(n) = sub(m , n): row m is the formula coded by m, and reading row m at its own index is sub(m , m). The row 4.2 needs is the twist's, and that it is a row is representability (4.5), nothing more — the full notion of 4.1 is false here, most families of formulas being cut out by no formula, which is why the one-row form is the one that fires. Concretely, for g = ψ the twist δ(x) := ψ(sub(x , x)) is a formula, has a code d, and the fixed point G := δ(d̄) has code sub(d , d). The B this fires over is the sentences up to provable equivalence, where ↔ is equality, so g b = b read there is exactly ⊢ G ↔ ψ(⌜G⌝). The box records formulas, their application, and the fixed point just built as the interface HasDiagonal, and reads it in the ¬Prov form as diagonalGivesGoedelFix. ∎

Corollary 4.7 (Gödel, first conjunct). Take ψ = ¬Prov, so 4.6 gives G with ⊢ G ↔ ¬Prov(⌜G⌝) — G says I am unprovable. If the theory is consistent and satisfies D1 (⊢ s ⇒ ⊢ Prov⌜s⌝), then ⊬ G, and by soundness G is true.

Proof. goedelHalfOne in the box. If ⊢ G then D1 gives ⊢ Prov⌜G⌝, and the forward half of the fixed point (4.6) gives ⊢ ¬Prov⌜G⌝, contradicting consistency. Prov(⌜G⌝) is the formula a proof of G exists — one unbounded existential over a decidable proof-check, which is what Σ₁ names — so G's unprovability is its truth. ∎

Proposition 4.8 (the second conjunct is a further hypothesis). Consistency, D1 and the fixed point do not give ⊬ ¬G.

Proof. noHalfTwo runs any claimed derivation of ⊬ ¬G against the four-sentence model Wit in the box — ⊤, ⊥, g, ¬g with Prov constantly ⊤. It is consistent, satisfies D1, and carries the fixed point at g — whose two arrows are both vacuous, not by accident but in every model of these hypotheses: those already force ⊬ g (fixIsAlwaysVacuous, from 4.7) and ⊬ ¬Prov⌜g⌝ (provNegEmpty), so neither arrow ever receives an input. What Wit alone adds is that ¬g is provable — so no such derivation exists. Wit fails exactly where it must: OmegaBad, proving Prov⌜g⌝ yet not g — consistent but ω-inconsistent. (In a real arithmetic that gap is consistency surviving because the asserted proof is a nonstandard one no numeral names; Wit is the same separation stripped to four points and no arithmetic.) ∎

Theorem 4.9 (Gödel's first incompleteness theorem). If the theory is also ω-consistent, and its logic carries contraposition, double-negation elimination and transitivity internally, then G is independent: ⊬ G and ⊬ ¬G.

Proof. independenceFromRepresentability in the box. The first conjunct is 4.7. For the second, the backward half of the fixed point (4.6), ¬Prov⌜G⌝ → G, contraposed and cleared of its double negation (internalFix), gives ¬G → Prov⌜G⌝; so ⊢ ¬G would force ⊢ Prov⌜G⌝ alongside ⊬ G (4.7) — the OmegaBad that 4.8 exhibits and ω-consistency forbids. ∎ (Rosser 1936 lowers ω-consistency to plain consistency by changing the fixed point.)

Corollary 4.10 (halting). No total H decides, of an arbitrary machine and input, whether it halts.

Proof. Running code a on input x is partial, so it is no table of total functions; a total halting-decider H makes it one, since φ(a)(x) := if H(a,x) then run(a,x) else 0 is then total. Every total computable h : A → 2 is a row of it: take any program for h; it halts everywhere, so H never diverts it. Now Lawvere (4.2) at g = ¬, in the one-row form: the twist δ(a) := ¬ φ(a)(a) is total and computable, hence a row, so δ ≡ φ(d) for some code d, and reading row d at its own index gives φ(d)(d) = ¬ φ(d)(d), which ¬, having no fixed point, forbids. ∎

Corollary 4.11 (Russell, Tarski). The non-self-members are no set's membership, and no truth predicate is definable.

Proof. The contrapositive (4.3) twice. Russell: B the propositions, g = ¬ on x ∈ x — the non-self-members are the diagonal row, and ¬ fixes nothing. Tarski: B the truth values, g = ¬ — a truth predicate would make the liar a fixed point of negation. ∎

Theorem 4.12 (Kleene's recursion theorem — the positive reading). Where e has a section — e being the interpreter, sending a code to the function it runs, and the section the compiler, sending a function to a code for it — Lawvere (4.2) hands every g a fixed point: a program equal to its own transform, the quine.

Proof. Lawvere (4.2) unchanged. The fixed-point-free instances — Cantor (4.4), halting (4.10), Russell–Tarski (4.11) — read it where g has no fixed point and conclude against e; here e is given and the conclusion is kept. ∎

Corollary 4.13 (Rice). No decider exists for a nontrivial semantic property of programs.

Proof. Suppose one, and take programs a that has the property and b that lacks it. By the recursion theorem (4.12) build a program which reads its own code, runs the decider on it, and then behaves like b if the verdict is yes and like a if no. Either verdict is wrong about it. ∎

Definition 5.1 (the correspondence). Each connective is read as a type former:

For the first four rows — the propositional part, with sums and the empty type — the connectives and the type formers are one structure: the free bicartesian closed category (Curry 1934; Howard 1969; Lambek 1980). The two quantifier rows go past it, since their types depend on a value; the setting for those is a locally cartesian closed category, which is what §0 has been building.

Definition 5.2 (question, answer). A computation is a term of a value type, a decision a term of Dec P = P ⊎ ¬ P, an answer a term of the type the question asks for. The answer to a question is the normal form of that term.

Proposition 5.3 (one operation). Proving, deciding, computing and answering are one operation: build the term, normalize it.

Proof. Immediate from the correspondence (5.1) and questions and answers (5.2): the four differ only in which type the term inhabits. ∎

Definition 5.4 (net). A cell has one distinguished principal port and finitely many auxiliary ports. A net is a finite set of cells with a partial matching of their ports by wires. The distance between two cells is the number of wires on a shortest path between them.

Definition 5.5 (interaction step). An active pair is two cells whose principal ports are wired to each other. For each pair of cell kinds a rule gives a net R on exactly the auxiliary wires of those two cells:

Every other cell and wire of N is unchanged. Write Step s t for one such step.

Definition 5.6 (trace, length, normal form).

data Trace : ℕ → S → S → Type where
  done      : {s : S} → Trace zero s s
  stepTrace : {n : ℕ} {s u t : S} → Step s u → Trace n u t → Trace (suc n) s t

Normal : S → Type
Normal t = (u : S) → Step t u → ⊥

The length of a trace is its index n.

Definition 5.7 (the two axes). The length of a reduction is the number of steps it takes (5.6). Its effect-cost is the quantity defined in 3.3: the entropy of its input given its output.

Proposition 5.8 (the two costs of a step). A reversible step has effect-cost 0 and length 1. A step merging 2ᵏ inputs into one output has effect-cost k and length 1.

Proof. A step whose input can be recovered is a bijection (3.1), so one input shares each output and log₂ 1 = 0; a 2ᵏ-fold merge gives log₂ 2ᵏ = k. Neither touches the step count. ∎

Proposition 5.9 (Landauer's bound, in units). A step of effect-cost k dissipates k · k_B T ln 2 of heat, and a reversible step dissipates 0.

Proof. Reversibility (3.1) and effect-cost (3.3) read twice — once on the datum, once on the dynamics carrying it. A 2 → 1 merge of microstates is an entropy drop of ln 2 nats, k_B ln 2 once k_B converts nats to thermodynamic entropy. Reversibility (3.1) splits the ambient dynamics into two cases. Injective: the two microstates the step merged stay distinct in it, so the distinction the datum lost is now in the surroundings, as heat T ΔS, with T the conversion of entropy to energy that defines temperature. Non-injective: it is a merging step itself, and effect-cost (3.3) charges it the same k one level down. Both cases pay k bits; k_B and T convert that to joules. By the two costs (5.8) a reversible step has k = 0, so the drop is 0 and the heat is 0. ∎ (Landauer 1961; Bennett 1973, 1982 named it.)

Lemma 5.11 (one-step diamond). If Step s a and Step s b then a ≡ b, or there is c with Step a c and Step b c.

Proof. Two distinct active pairs are disjoint: distinct principal-port pairs cannot share a cell. By interaction (5.5) each step leaves everything outside its own pair untouched, so doing one leaves the other available and untouched, and the two converge in one further step each. This is structural to interaction nets (Lafont 1990), not an assumption. It is also why the machine is nets and not terms: β-reduction is confluent but has no one-step diamond — two overlapping β-redexes need several steps to reconverge, which is why the classical proof goes through parallel reduction — so the equal-length result below is false for it. A rule firing on an active pair cannot overlap another, by the disjointness just shown, and that is the whole difference. ∎

Lemma 5.12 (peel). Step s u → Trace (suc n) s t → Normal t → Trace n u t.

Proof. Induction on the trace's length. Apply the diamond (5.11) to the given step and the trace's first step: either they merge, and the tail is the required trace, or they reach a common term, from which the inductive hypothesis peels the shorter tail. At a normal form no step is left to carry, so the given step is absorbed exactly once. ∎

Theorem 5.13 (equal length). Trace n s t → Trace m s t → Normal t → n ≡ m.

Proof. Induction on the first trace, peeling its first step through the second by peel (5.12). ∎

Corollary 5.14 (the length is fixed by the endpoints). Every reduction of a term to its normal form has the same length, so each is the minimum: the step-count is fixed by the endpoints, never by the strategy, and the cost is as deterministic as the answer.

Proof. Equal length (5.13) with ≤-refl, as normalization-is-geodesic in the box. ∎

Theorem 5.15 (Bellman). In the reduction graph — vertices terms, edges steps of cost c(u→v) — call Φ a potential when Φ(normal form) = 0 and Φ(u) ≤ c(u→v) + Φ(v) on every edge. Then every potential is a lower bound on every finishing path, and where a normal form is reachable the geodesic distance is the greatest potential, satisfying

Proof. Adding the edge inequality along any path to a normal form, where Φ = 0, gives Φ(u) ≤ the path's total cost. The geodesic distance satisfies both conditions, so it is a potential, and it meets the bound with equality at the cheapest edge (Bellman 1957). By minimality (5.14) it is attained by every reduction, so there is nothing to minimise over. ∎

Theorem 5.16 (unit lookahead). An output that must read input at distance n from it cannot be produced in fewer than n steps — a bound on every reduction, not on one chosen strategy.

Proof. By interaction (5.5) one step changes the datum only where its two cells sat, so its output at a position depends on that position and its one wired neighbour. Composing k steps, the output depends only on input within distance k of it in the net one started from: one step reaches a wired neighbour, so each widens the reach by exactly one. The rewriting does not let that slip — a rule replaces two cells by a net on their own auxiliary wires, and the cells it puts there can carry only what those two already held, so no interaction moves information further than one wire, however the distances in the rewritten net come out. ∎

Read from the other end, the same k is an information demand. Write x ≡ₙ y for agreement through observational depth n: the bound says x ≡ₙ₊ₖ y ⇒ w(x) ≡ₙ w(y) for every k-step w, so an output determined to depth n requires source read to depth n + k. One number, two orientations — elapsed interaction depth read dynamically, source information required read observationally — and both are the length axis (5.7), not a third cost: the effect-cost (3.3) counts what collides under an observation, this counts what must be read to produce it. In the observational orientation the criterion of 8.11 reads as a radius, since one step widens the source a position can consult by exactly one wire.

Corollary 5.17 (step-optimality). The native evolution attains the geodesic: no reduction is shorter than the one it takes.

Proof. Minimality (5.14). ∎

Theorem 5.18 (unique normal form). A term has at most one normal form.

Proof. The diamond (5.11), tiled. Take two reductions of one term; the diamond closes their first steps to a common term, and filling the grid step by step reconverges them. If both end at a normal form — nothing left to rewrite — that common reduct can only be each endpoint, so the two are equal. (Church–Rosser, here the diamond filled in.) ∎

Corollary 5.19 (the dichotomy). For every question there are two cases and no third. Either a normal form exists, and by minimality (5.14) and unique normal form (5.18) every reduction reaches that one answer in the one step-count the endpoints fix; or §4 proves there is none — a decider for one's own halting is among these, since asking for one asks for the fixed point the diagonal forbids — and the question had no answer to find, which the system establishes rather than running out of time looking.

Proposition 5.21 (the building route is the size of the answer). Take a rule set in which each interaction emits at most one constructor — true of the standard encodings, and a property of the rules rather than of interaction (5.5). The normal form is then a complete proof-carrying witness — the answer with its certificate — and the steps that build it number exactly its constructors.

Proof. Each building step emits exactly one constructor — one piece of the answer, a successor, a pair, a tag — so the building route's length equals the witness's size; building sucⁿ takes one successor per step. A term carrying extra redexes — spots still waiting to reduce, like (λx.x) t — clears those first, administrative steps building nothing, so its total length is its own geodesic by minimality (5.14) while the witness's size counts only the constructors built. Reading the finished term off is a fold that copies it, adding no step. ∎

Theorem 5.27 (complete inference). Let a declaration be any type — anything rationally stateable (the correspondence (5.1), 5.2). Pose it together with the identities available, which by uniqueness of the partition (1.4) is forced rather than a choice of encoding, and normalize. Then exactly one of two cases holds, and the reduction itself decides which:

(a) the declaration is inhabitable, and the normal form is an inhabitant of it — a proof, carrying its own acceptance as refl (decide = verify (8.6)) — reached in a number of steps fixed by where the reduction starts and ends (equal length (5.13)), which no order of applying the identities can beat (5.14, 5.17), and with no step repeating work (sharing (5.24));

(b) it is not inhabitable, and §4 names the obstruction: the system establishes that no inhabitant exists, rather than failing to find one (the dichotomy (5.19)). Case (b) is a statement about the declared type and never a term of a negation one level inside it — where the declaration is a theory’s provability of a sentence, establishing it empty is ⊬ G, not ⊢ ¬G (4.7, 4.8).

By no outer layer (5.26) this holds of declarations about the system itself.

Proof. One operation (5.3) makes proving, deciding, computing and answering the same act, so the four are this one statement. Unique normal form (5.18) makes the inhabitant unique; 5.13 makes every reduction to it the same length and 5.14 makes each one minimal; unit lookahead (5.16) is the matching lower bound; 5.19 supplies the two cases and no third. ∎

Definition 6.1 (counting). To count a finite set is to forget which element is which. Any two n-element sets differ only by a relabelling, so all of them are one thing; what the forgetting throws away is exactly the relabellings, the n! permutations of n things. To count is to keep the class and discard Sₙ:

Greek arithmetic states this construction outright. Euclid VII Def. 1–2 define the unit as "that by virtue of which each of the things that exist is called one" and a number as "a multitude composed of units" — so the unit is defined separately and is not itself among the numbers, which is identity's standing here too (0.2): it generates the sequence without being a term of it. And the units are athetos, without position: a monad is a position-less substance where a point is one having position (Aristotle, Metaphysics 1016b; Posterior Analytics 87a36). Position-less is the whole content of this definition. Units with no position have nothing to tell one from another, so a multitude of them carries nothing beyond how many there are, and every relabelling of it is the same multitude. That is Sₙ discarded, given as a definition rather than derived.

Proposition 6.2 (card). card is the bijection between iso-classes of finite sets and ℕ, with inverse n ↦ {1,…,n}.

Being a bijection and not a measurement, the number is the iso-class rather than a label attached to it. Aristotle marks exactly this as the Pythagorean position against the Platonic one (Metaphysics 1090a): number is not separated from the things.

Proposition 6.3 (arithmetic). Addition is disjoint union and multiplication is product:

|A ⊎ B| = |A| + |B|        |A × B| = |A| · |B|

Written in base b, adding two digit strings is this disjoint union done place by place, carrying whatever overflows a place into the next.

Proposition 6.4 (divisibility is a distributive lattice). d ∣ n iff each prime's exponent in d is ≤ its exponent in n. So gcd is the meet (minimum exponents) and lcm the join (maximum), and unique factorization sends n to its exponent vector, making ℕ the product of one chain per prime, where minimum and maximum distribute componentwise.

Theorem 6.5 (number theory and logic are one lattice). The divisor lattice carries the operations of propositional logic: gcd/lcm are ∧/∨, coprimality is disjointness, the divisibility order is entailment, and d ↦ n/d is an order-reversing involution satisfying De Morgan. So divisibility and the propositional connectives are one algebra — the same distributive lattice with involution, whether the elements are divisors or truth values — and 6.6 says when it is the Boolean one.

Proof. The product decomposition of the divisor lattice (6.4) matches the Chinese remainder theorem ℤ/mn ≅ ℤ/m × ℤ/n by x ↦ (x mod m, x mod n): injective, since coprime m, n both dividing x − y force mn ∣ (x − y), hence bijective by count. ∎

Proposition 6.6 (Boolean exactly on the squarefree). Being finite and distributive, the divisor lattice of every n is a Heyting algebra. It is Boolean iff n is squarefree.

Proof. What varies is whether the involution of 6.5 is the Heyting negation. On squarefree n it is: a divisor is a subset of the primes and n/d its complement. A repeated prime breaks it — on n = p² the divisors are the chain 1 < p < p², where the Heyting negation of p is 1 and ¬¬p = p² ≠ p, while the involution sends p to n/p = p. So the lattice is Boolean on squarefree n and properly intuitionistic otherwise. ∎

Definition 7.1 (the quarter-turn). σ(x , y) = (−y , x), a length-preserving quarter-turn of the plane. Write i for σ: then σ(x,y) = (−y, x) is i·(x + iy) = −y + ix. It is reversible, so free on the effect axis by the vanishing grading (3.5).

Proposition 7.2 (σ² = −1). σ² = −1.

Proof. σ²(x,y) = σ(−y,x) = (−x,−y) = −(x,y). The identity needs no analysis and holds over any ring; the box checks it on the integer lattice, where it is exact arithmetic. ∎

Corollary 7.3 (ℂ, the phases, unitarity). The complex numbers, the four phases and unitarity are generated by this one reversible operation.

Proof. By σ² = −1 (7.2) the powers of σ cycle 1, σ, −1, −σ, the phases {1, i, −1, −i}; adjoining σ to the reals by those same two lines is ℝ[σ]/(σ²+1) = ℂ; and σ, a rotation, preserves length, so it is unitary. Unitary evolution is exactly the reversible side of 3.1; the physics that costs — measurement, erasure — is the irreversible side (3.3, 5.9). ∎

Theorem 7.4 (Riemann–Silberstein). With F = E + iB and units in which c = 1 — otherwise F = E + icB, and a c rides along on the right — Maxwell's two vacuum equations are one Schrödinger equation:

Proof. i ∂_t F = i ∂_t E − ∂_t B = i(∇×B) + ∇×E = ∇×(E + iB) = ∇×F, using the two Maxwell equations; splitting real and imaginary parts gives them back. Classical electromagnetism and single-particle quantum mechanics are the same equation. ∎

Lemma 7.5 (curl is self-adjoint). ∫ a·(∇×b) = ∫ (∇×a)·b.

Proof. Integrate ∇·(a×b) = b·(∇×a) − a·(∇×b) over a domain with no boundary — a torus, or fields decaying at infinity — where the left side integrates to zero. ∎

Theorem 7.6 (the flow is unitary). ‖F‖² is conserved, and the generator −i∇× is skew-adjoint.

Proof. ‖F‖² = ⟨E+iB, E+iB⟩ = ‖E‖² + ‖B‖², the Hermitian cross terms ±i⟨E,B⟩ cancelling. From ∂_t F = −i∇×F (7.4),

since curl is self-adjoint (7.5) at a = b = F makes ⟨F, ∇×F⟩ real, so its imaginary part vanishes. A length-preserving flow is unitary. ∎

Definition 8.1 (solutions). For F : assignments → {true, false}, the solutions are the fibre (1.1) at b = true:

Write S_F for this type, and Q_N for the 2^N assignments.

Theorem 8.2 (the cube splits). Q_N = S_F ⊎ ⋃α V_α, where V_α is the subcube of assignments breaking clause α. Deciding and solving are two observations of this one partition.

Proof. The partition (1.2) at F. For 3-SAT a clause forbids exactly one setting of its three literals, so the assignments that break it fill a subcube V_α — those three bits fixed to the forbidden setting, the other N−3 free, a codimension-3 face. Every assignment either satisfies all clauses, so lies in S_F, or lies in some V_α, and S_F is disjoint from ⋃ V_α. ∎

Theorem 8.3 (the count).

Proof. Inclusion–exclusion on the cube splits (8.2): #S_F = Σ_{T⊆C} (−1)^{|T|} |⋂_{α∈T} V_α|. When the clauses in T can be violated together, |⋂_{α∈T} V_α| = 2^{N−r(T)} with r(T) the coordinates they jointly fix; when two of them demand opposite values on a shared variable the intersection is empty and contributes 0. Regrouping per assignment by the j clauses it breaks, its weight is Σ_{i≤j} C(j,i)(−1)^i = (1−1)^j, which is 1 only at j = 0: each solution survives once, the rest cancel. ∎

Definition 8.4 (deciding, solving). Solving is S_F — a vertex with its membership proof. Deciding is ‖S_F‖, writing ‖·‖ for the proposition that this is inhabited: one bit, and when true a single point, every witness collapsed onto it. The truncation is τ : S_F → ‖S_F‖.

Theorem 8.5 (what the one bit discards). The pre-image of τ is S_F itself, and τ has no left inverse once |S_F| > 1.

Proof. τ sends every witness to the one point, so by the fibre (1.1) its pre-image is Σ[ w ∈ S_F ] (τ w ≡ pt). Since ‖S_F‖ has any two of its points equal, the equality component carries nothing, and the pre-image is S_F. The one-bit decision therefore discards exactly the which-witness pre-image. ∎

Theorem 8.6 (deciding and verifying are one equivalence). For the machine's step f, decide(a) = (f a , (a , refl)) and verify reads the witness's pre-image back out; the round trip is refl.

Proof. Deciding an input a completes it to an answer with a witness, and by the partition (1.2) that completion is the equivalence A ≃ Σ[ b ] f⁻¹(b), unique by uniqueness of the partition (1.4). The two directions are decide and verify. The decided witness carries its own acceptance as refl, so the lossless run produces the witness with the answer in one forward pass, and verifying is that pass reversed: no operation sits between them for a gap to live in. ∎

Proposition 8.8 (the moment tower). #SAT = Σ_{T compatible} (−1)^{|T|} 2^{N−r(T)} = Σ_r (−1)^r M_r, the alternating collapse of the clause-intersection (factorial-moment) tower M_r = Σ_{|T|=r} |⋂ V|. The scalar count is the extremely lossy projection (1,−1,1,…)·(M_r), and F is unsatisfiable iff it is 0.

Proof. Regroup the count (8.3) by |T|. ∎

Proposition 8.9 (eight clauses). An unsatisfiable formula whose every clause has exactly three literals needs m ≥ 8 clauses, and eight suffice.

Proof. Write ν(x) for the clauses assignment x violates. Each clause is violated by 2^{N−3} assignments, and unsatisfiability means every x violates at least one, so Σ_x ν(x) = m·2^{N−3} ≥ 2^N, that is m ≥ 8. Sharp: the eight clauses on three variables, one for each sign pattern, forbid all eight settings. ∎

Theorem 8.10 (no count bounds the length). None of the four counts proposed as lower bounds — assignments, satisfying vertices, clause-intersections, and the width of a fixed-order pass — bounds the length of the problem: each can be made small by factoring or a change of coordinates while the problem stays the same, so none can serve as the potential of Bellman (5.15) for the problem itself.

Proof. Each collapses under factoring or a change of coordinates. Disjoint triples: m clauses on disjoint variable-triples each kill 1 of 8 and leave 7, so #SAT = 7^m while the intersections number 2^m. Inner product ⟨x,y⟩ mod 2: read all of x first and the state reached must fix the map y ↦ ⟨x,y⟩ — distinct x ≠ x′ give different maps, disagreeing at y = e_i, the vector with a single 1 in place i, wherever x_i ≠ x′_i — so the 2ⁿ inputs force 2ⁿ distinct states, width 2ⁿ; read the pairs x_i, y_i interleaved and it is a running parity, remembering x_i and folding x_i y_i in, width ≤ 4. ∎

Definition 9.1 (sorting). To sort a finite set is to assign it indices matching its order — to compute the ordering, delivered as a sequence. The orderings of n elements number n!, and each comparison restricts which of them survive.

Theorem 9.2 (the fibre is the relabellings). The fibre of sort over a sorted sequence is the n! rearrangements of it: a list is a sorted list together with a permutation, and nothing besides.

Proof. The partition (1.2) at sort, whose fibre (1.1) over a sorted sequence is the inputs landing on it, and forced rather than chosen by 1.4. ∎

Counting (6.1) discards exactly these relabellings to reach the number; sorting recovers the one the order names. The two are one forgetting, run in opposite directions. Keep the permutation and the run destroys nothing (3.6); deliver the sorted sequence alone and the effect-cost (3.3) is log₂ n!, the size of the fibre.

Proposition 9.3 (a comparison is a restriction). A comparison leaves exactly the orderings consistent with its outcome. Comparing two elements about which nothing is known leaves half, since exchanging them is a bijection between the orderings answering one way and those answering the other (2.6). A comparison already implied leaves all of them and is never made: what is held is a partial order, so from a < b, b < c, b < d the relations a < c and a < d are there already, the n² pairs never stored.

Proposition 9.4 (which comparison). Naming any still-unordered pair is not enough: a supply offering (a,b), then (a,c), then (a,d) spends n−1 comparisons to learn only which element is least. The one that excludes most is wanted. Of the twenty-four orderings of four elements, a < b leaves twelve. Comparing c with d halves those to six; comparing a with c instead leaves eight when a wins — a least of three, one of three equally — so its worse outcome is worse than six. Fresh pairs are taken while any remain. With a < b and c < d the six survivors are the C(4,2) interleavings, and comparing the two least leaves three either way, where comparing b with c leaves five in one outcome, b < c forcing abcd alone. The least are compared, and the result is one component with a known least, below everything in both. Five comparisons in all, and ⌈log₂ 24⌉ = 5.

Theorem 9.5 (why the least halve). A comparison between two elements exchanged by a symmetry of what is already known splits the survivors exactly in half.

Proof. The exchange carries orderings consistent with what is known to orderings consistent with it and swaps the two outcomes, so it is a bijection between them (2.6), and two sets in bijection are equal halves of their union. Two runs of equal length are exchanged by the symmetry that interchanges them, which carries least to least. No symmetry of a < b, c < d exchanges b with c, which is why that comparison is lopsided. ∎

Each such comparison establishes a new least for the two components it joins; every relation already established stays, and the loser remains least of its own run. Two fresh elements are always so exchanged, so a fresh pair always yields one.

Definition 9.6 (merge). Sortedness unfolds into one recursion, and merge is that unfolding:

Sorted(x)  =  head x ≤ every element of tail x  and  Sorted(tail x)

merge(x, y)  =  head x ≤ head y  ?  head x ∷ merge(tail x, y)
                                 :  head y ∷ merge(x, tail y)

A single comparison is merge running on two one-element runs. Sorting is the composition of merges and nothing else, beginning from the elements as runs of length one.

Theorem 9.7 (every + is a merge). Writing n as a sum is choosing the merges. Each + is one merge of two runs and costs the sum it produces, so the cost of sorting is the sum of the intermediate sums — equivalently, each element pays once for every + above it.

(1+1)+(1+1)        2, 2, 4              cost  8  =  n log₂ n
1+(1+(1+1))        2, 3, 4              cost  9
n = 8, balanced    2,2,2,2, 4,4, 8      cost 24  =  n log₂ n
n = 8, chained     2,3,4,5,6,7,8        cost 35

Proof. A merge of runs of lengths a and b emits a + b elements, and under a rule set emitting one constructor per step (5.21) that is a + b steps: the sum it produces. Summing over the + signs counts each element once for each + standing above it, which is its depth. ∎

This counts steps, one per element emitted. The comparisons are fewer — a merge of a and b makes at most a + b − 1, since the last run empties without one — and they are bounded separately, below.

Theorem 9.8 (the information is fixed by the endpoints). A merge of runs of lengths a and b settles which of C(a+b, a) interleavings occurred, and along every way of writing n as a sum these binomials multiply to n! exactly.

Proof. An ordering of the whole is an ordering within each run together with the interleaving, so each merge contributes its binomial and the product telescopes to n! — info≡ in the box under 9.7. ∎

What is learned is fixed by where the sorting starts and ends, never by the shape — the pattern of equal length (5.13) on the other axis (5.7), reached here by a counting telescope rather than by the diamond. The shape decides only what each merge pays for what it settles: equal runs pay 2a for nearly 2a bits, a run against one element pays a+1 for log₂(a+1). That is the whole difference between the two sums of 9.7 — one quantity, distributed differently over the + signs.

Corollary 9.10 (the two smallest). Minimising the sum of the intermediate sums over the ways of writing n as a sum is solved by repeatedly adding the two smallest parts — Huffman 1952 — which for n units gives the balanced sum. This answers 9.4 from the cost side rather than the information side: the cheapest merge available is the one between the two smallest runs, and two fresh elements are the smallest there are.

Theorem 9.11 (the shape is the numeral). The balanced sum is the binary representation of n, and the chain is the tally.

Proof. For n = 2ᵏ each element has a k-bit index, and the path from the root of the sum down to it spells that index: the first layer of merges joins indices differing in the last bit, the next those differing in the second-to-last. Resolving the ordering one layer at a time is resolving it one bit of the index at a time. For general n the runs are the 1-bits: 13 = 8 + 4 + 1. Counting is merging — add elements one at a time, keep runs matching the binary form of the count, and each carry merges two equal runs into one twice the size, which is 6.3's carrying read at its cost. The chain 1+(1+(1+⋯)) is the same number in tally marks: no carries, one growing run. ∎

The gap between the two costs is the gap between a tally and a numeral. Succession gives a line; place value gives a log₂ n-dimensional cube, which is what a base system has always been. A set indexed by the naturals already carries that structure, so there is no reason to prefer succession unless the input arrives as a line.

Proposition 9.12 (the same factorisation from the other end). Read downward, that product of binomials is a partition rather than a composition: at the top, which half of the set lies below and which above — C(n, n/2) ways — then the same within each half, down to single elements. Every element is sent toward its own index, as though searching for its own position one bit at a time. Merge splits by position and builds from the leaves; this splits by value and descends from the root. Splitting by value is partition by output (1.2), the output being where the element lands, so the two directions are that one partition taken at the two ends of the same factorisation, and inverting the permutation exchanges them.

Proposition 9.13 (the space of orderings). Take the orderings as points, joining two when they differ by swapping neighbours in the sequence. For three elements the six close into a hexagon:

            abc
          /     \
       bac       acb
        |         |
       bca       cab
          \     /
            cba

The distance from an ordering to the sorted one is its number of out-of-order pairs, since each swap of an out-of-order neighbouring pair fixes exactly one. Every route that only fixes out-of-order pairs therefore has the same length whatever order the swaps are taken in — not by the diamond (5.11), which fails here, but by Bellman (5.15): the out-of-order count is a potential that every such swap meets with equality — the swap costs one and lowers the count by exactly one — and a potential met with equality on every edge of the reduction makes every route a geodesic. (A swap of an in-order pair raises the count instead; it is not a step of the reduction, and a route using one is longer.) Two swaps at disjoint positions do commute and their routes close a square, the diamond where it holds; three sharing an element close the hexagon above, where it does not — those two reconverge only after two further swaps on each side, not one — and both sides are still the same length. So the picture reaches 5.13’s conclusion through 5.15, and shows the diamond failing on the way. A comparison is a cut through this space, and one already implied is a cut that misses what remains.

Proposition 9.14 (comparisons and swaps). Comparisons count cuts and swaps count distance, and the counts differ: about log₂ n! comparisons are needed (9.9), while the swaps are the out-of-order pairs (9.13), of which there are at most the n(n−1)/2 pairs. One comparison can authorise several swaps, and that is the whole of the gap — the two axes (5.7), with both numbers in hand.

Proof. In the set there are no swaps at all — comparisons add knowledge and the order is learned, not moved; swaps belong to the sequence presentation. At a single pair the two coincide: one comparison, one swap, one edge of 9.13. Above that they part. Merging [a,b] with [c,d] and learning c < a gives c < b free from the a < b already held, so one comparison authorises both swaps. Every swap is backed by a comparison made or inherited, and in a sorting that wastes nothing most are inherited. ∎