An Abuse of Notation

The natural numbers are built from two primitives following the Peano axioms:

• Zero — the number 0
• AddOne<N> — the successor of N, written S(N) in mathematical notation (i.e. N + 1)

Throughout this tutorial, S(N) denotes the successor function: S(0) = 1, S(1) = 2, S(2) = 3, and so on. In Swift, S(N) is the type AddOne<N>.

Every natural number is a unique nesting of AddOne around Zero:

The assertEqual function has an empty body. Its signature requires both arguments to have the same type:

If the two types differ, the compiler rejects the call. If they match, it compiles — and that successful compilation is the assertion. This is the Curry–Howard correspondence in action: types are propositions, and a compiling program is a proof.

A witness is a type whose existence proves a mathematical fact. The NaturalSum protocol declares three associated types — Left, Right, and Total — representing the operands and result of an addition. Each conforming type provides concrete type aliases for them:

• PlusZero<N> — a witness that N + 0 = N. It sets Left = N, Right = Zero, Total = N.
• PlusSucc<P> — given a witness P that A + B = C, a witness that A + S(B) = S(C). It sets Left = P.Left, Right = AddOne<P.Right>, Total = AddOne<P.Total>.

When you write PlusZero<N5>.Total, Swift resolves the type alias: Total = N, and N is N5, so .Total is N5. For PlusSucc<PlusZero<N5>>.Total, it resolves Total = AddOne<P.Total>, where P is PlusZero<N5>, so P.Total is N5 and .Total is AddOne<N5> = N6. Every associated type in this project — .Shifted, .Commuted, .Distributed, and the rest — works the same way: it's a type alias that the compiler resolves by following the chain of definitions.

A continued fraction (CF) is a nested expression of the form a₀ + 1/(a₁ + 1/(a₂ + ...)). The integers a₀, a₁, a₂, ... are called coefficients. The shorthand [a₀; a₁, a₂, ...] lists them in order — for example, [1; 2, 2, ...] means 1 + 1/(2 + 1/(2 + ...)). Truncating the CF at depth n gives a rational approximation called the n-th convergent. A partial sum is the analogous concept for a series: the sum of its first n terms.

Two classical formulas approximate pi: Brouncker's CF for 4/pi and the Leibniz series for pi/4. At each depth, the CF convergent equals the reciprocal of a Leibniz partial sum. Throughout this project, .P denotes the numerator and .Q the denominator of a type-level fraction.

In section 2, we built witness chains by hand: PlusSucc<PlusSucc<PlusZero<N2>>> for 2 + 3 = 5. For simple arithmetic this is manageable, but proving that a convergent equals a partial sum requires witness chains dozens of types deep, with exact numerical values that must be computed first. We need something to do that computation and emit the right types.

A Swift macro is a compiler plugin that generates code at compile time. In this project, macros perform arbitrary integer arithmetic — the kind of computation the type system can't do — and emit witness type chains that the type system can verify. This division of labor is the key idea: the macro is the proof search (finding the right witness chain), and the type checker is the proof verifier (confirming that the chain satisfies every protocol constraint). The search is unchecked computation; the verification is structural and cannot be fooled.

The Wallis product for pi/2. Each step multiplies the numerator by (2k)² and the denominator by (2k-1)(2k+1). The structural fingerprint: the numerator exceeds the denominator by 1 at each step — the difference-of-squares identity (2k)² = (2k-1)(2k+1) + 1.

WallisStep advances the partial product by one step. Its type parameters are multiplication witnesses for the four factors involved: the numerator is multiplied by 2k twice (squaring), while the denominator is multiplied by 2k-1 then 2k+1. The macro supplies these witnesses using two universal theorems that are formally proved in section 10:

• N.OneTimesProof — a witness that 1 * N = N, available on every natural number.
• .Distributed — given a proof that a * b = c, produces a proof that (a+1) * b = c + b. Chaining .Distributed repeatedly builds up the left operand: N2.OneTimesProof witnesses 1 * 2 = 2, then .Distributed produces 2 * 2 = 4, another .Distributed gives 3 * 2 = 6, and so on.

The Fibonacci sequence encoded as type-level state transitions. Each state has three associated types: .Prev, .Current, and .Next. These are type aliases, resolved the same way as .Total (section 2). Fibonacci0 sets them directly: Prev = N1, Current = Zero, Next = N1.

FibonacciStep<S, W> advances the state by one position. It takes a previous state S and an addition witness W proving that S.Current + S.Next = W.Total — the Fibonacci recurrence. Its type aliases shift forward: Prev = S.Current, Current = S.Next, Next = W.Total. So each .Current resolves through the chain: FibonacciStep<S, W>.Current is S.Next, which is the previous step's W.Total.

The golden ratio φ has CF [1; 1, 1, ...] — the Fibonacci recurrence. Convergents satisfy h_n = F(n+2), k_n = F(n+1).

The CF for √2 is [1; 2, 2, ...]. The recurrence h_n = 2h_n-1 + h_n-2 is equivalently left-multiplication by M = [[2,1],[1,0]]. The macro constructs both and proves they match.

Sections 3–7 proved specific numerical facts: this convergent equals that value. Universal theorems prove statements for all natural numbers at once, via structural induction: a base case on Zero/PlusZero and an inductive step on AddOne/PlusSucc.

The generic functions below prove universality. When the compiler accepts useLeftZero(N0.self), useLeftZero(N5.self), and useLeftZero(N9.self), it's not just checking three cases — the generic constraint <N: AddLeftZero> means it accepts any natural number. If there were a natural number that didn't satisfy the theorem, the conditional conformance chain would break and the generic call would fail to compile.

Each theorem defines an associated type that transforms one proof into another, following the same type-alias-resolution mechanism as .Total (section 2).

.Shifted (Theorem 2) takes a proof that a + b = c and produces a proof that S(a) + b = S(c). The base case: PlusZero<N>.Shifted = PlusZero<AddOne<N>> — bump N to S(N). The inductive step: PlusSucc<P>.Shifted = PlusSucc<P.Shifted> — shift the inner proof, then re-wrap. So PlusSucc<PlusZero<N2>>.Shifted resolves to PlusSucc<PlusZero<N3>> — a proof that 3 + 1 = 4.

.Commuted (Theorem 3) takes a proof that a + b = c and produces a proof that b + a = c. The base case: PlusZero<N>.Commuted = N.ZeroPlusProof — flip N + 0 to 0 + N using Theorem 1. The inductive step: PlusSucc<P>.Commuted = P.Commuted.Shifted — commute the inner proof, then shift. Commutativity is built from the first two theorems.

(a + b) + c = a + (b + c) requires reasoning about two addition proofs simultaneously: one for a + b and another for the result plus c. But Swift's conditional conformance can only do induction on one type parameter at a time.

The seed technique solves this. ProofSeed<P> is a wrapper type that conforms to Natural while carrying a NaturalSum proof P inside. Its .AssociativeProof type alias is just P itself — the unwrapped proof. Each AddOne layer adds one PlusSucc: AddOne<X>.AssociativeProof = PlusSucc<X.AssociativeProof>. So AddOne<AddOne<ProofSeed<P>>>.AssociativeProof resolves to PlusSucc<PlusSucc<P>> — the original proof extended by two successor steps. The seed freezes the first parameter (the proof of a + b) so the second parameter (c) can vary freely.

This pattern recurs: ProductSeed (section 12) wraps a NaturalProduct proof for distributivity. Any time you need induction over two parameters, you can wrap one as a seed and induct over the other.

An earlier encoding, TimesSucc, composed a product witness with a sum witness using where clauses. This works for individual proofs, but when used inside inductive protocols, each layer compounds the constraints the type checker must solve simultaneously. Swift's type checker uses a rewrite system to resolve associated types, and the exponentially growing constraint set overwhelms it — compilation fails. The flat encoding (TimesTick/TimesGroup) decomposes multiplication into where-clause-free primitives, sidestepping the problem entirely and enabling universal theorems.

To prove a * b, you build b groups of a ticks each. TimesTick adds 1 to Total (one step within a copy of the left operand). TimesGroup adds 1 to Right without changing Total (marking that one complete copy has been accumulated). After a ticks followed by a group boundary, one copy of a has been added; repeating b times gives a * b.

.Distributed transforms a proof of a * b = c into a proof of S(a) * b = c + b. Each conformance defines a Distributed type alias: TimesZero<N>.Distributed = TimesZero<AddOne<N>> (bump Left), TimesTick<P>.Distributed = TimesTick<P.Distributed> (pass through), TimesGroup<P>.Distributed = TimesGroup<TimesTick<P.Distributed>> (each group gains one extra tick for the new successor). So FlatProduct2Times3.Distributed resolves through the chain to a proof of 3 * 3 = 9.

Commutativity pairs two proofs of the same product. .ForwardProof directly constructs A * b with a hardcoded number of ticks per group (e.g., AddOne<Seed>.ForwardProof = TimesGroup<TimesTick<TimesTick<Seed.ForwardProof>>> for A = 2). .ReverseProof builds b * A by chaining .Distributed: AddOne<X>.ReverseProof = X.ReverseProof.Distributed. Each .Distributed step increments the left operand by one, building up from 0 * A = 0.

The bounded proofs in sections 3–7 represent irrational numbers through finite convergent chains (macro-generated). Coinductive streams provide a complementary representation: the continued fraction coefficient sequence itself as a type. Where the convergent proofs compute specific rational approximations, the stream is the irrational number — an infinite object encoded in a finite type definition.

A CFStream has a Head (the current coefficient) and a Tail (the rest of the stream). For periodic CFs, self-referential types create productive fixed points — corecursion in the type system. Swift resolves the self-reference lazily, so .Tail.Tail...Head always terminates.

The stream coefficients match the values used by the macro-generated convergent proofs. For the golden ratio, PhiCF.Head = N1 matches the all-ones CF used in section 6. For √2, Sqrt2CF encodes [1; 2, 2, ...], the same CF computed by section 7. The streams encode the identity of the number; the convergent proofs compute its approximations.

a * (b + c) = a*b + a*c bridges sum and product witnesses. The product proof for a * (b + c) is built as c groups of a ticks on top of ProductSeed<Q>, where Q witnesses a * b. Each conformance defines a DistributiveSum type alias — a sum witness that rides along inside the product proof:

• ProductSeed<Q>.DistributiveSum = PlusZero<Q.Total> — the sum begins at a*b + 0 (no a*c contribution yet).
• TimesTick<P>.DistributiveSum = PlusSucc<P.DistributiveSum> — each tick adds 1 to the right side (the a*c portion grows by 1).
• TimesGroup<P>.DistributiveSum = P.DistributiveSum — group boundaries pass the sum through unchanged.

After c groups of a ticks, the right side of the sum has accumulated a*c, so DistributiveSum witnesses a*b + a*c = a*(b+c).

Distributivity and SuccessorLeftMultiplication explain why identities hold, not just that they hold. Both sides of each identity decompose via a shared base product, and the tools from sections 10 and 12 provide the witnesses.

Both sides share the base product n*(n+1). The right side is (n+1)² = n*(n+1) + (n+1) via SuccessorLeftMultiplication. The left side is n*(n+2) = n*((n+1)+1) = n*(n+1) + n via distributivity. The remainders differ by exactly 1.

FlatProduct1Times2 witnesses 1 * 2 = 2 (the shared base for n=1). Applying .Distributed gives 2 * 2 = 4. The left side DifferenceOfSquares1 witnesses 3 + 1 = 4 via PlusSucc<PlusZero<N3>>, and the type checker confirms both totals are 4.

The key step uses distributivity: F(n+1)*F(n-1) = (F(n)+F(n-1))*F(n-1) = F(n)*F(n-1) + F(n-1)². This relates the cross-product at step n to the square and cross-product at step n-1. At n=4: F(3)=2, F(4)=3, F(5)=5, so F(3)*F(5) = 2*5 = 10 and F(4)² + 1 = 9 + 1 = 10.

FlatProduct2Times5 witnesses 2 * 5 = 10 (built by extending FlatProduct2Times3 from section 10 with two more groups). CassiniIdentity4 witnesses 9 + 1 = 10 via PlusSucc<PlusZero<N9>>.

The convergent determinant h_nk_n-1 - h_n-1k_n = (-1)ⁿ⁺¹ connects CF matrices to number theory. For the golden ratio, this reduces to Cassini. For √2, with convergents h₀/k₀ = 1/1, h₁/k₁ = 3/2, h₂/k₂ = 7/5:

The products are built by chaining .Distributed from OneTimesProof. Each .Distributed increments the left operand by one: N1.OneTimesProof witnesses 1 * 1 = 1, the first .Distributed gives 2 * 1 = 2, and the second gives 3 * 1 = 3. Similarly, N5.OneTimesProof.Distributed.Distributed builds 1 * 5 = 5 → 2 * 5 = 10 → 3 * 5 = 15.

The codebase proves three representations of pi independently: Brouncker's CF (section 3), the Leibniz series (section 3), and the Wallis product (section 4). This section connects all three.

Brouncker–Leibniz (proved by the @PiConvergenceProof macro): at each depth k, the CF convergent numerator equals the Leibniz denominator and vice versa: CF_k.P = LS_k+1.Q. This was verified in section 3.

Wallis–Leibniz (proved here): each Wallis denominator is the product of two consecutive Leibniz denominators: WQ[k] = LQ[k+1] * LQ[k]. Leibniz denominators accumulate one odd factor per step (1, 3, 15, 105, ...), while Wallis denominators accumulate paired odd factors — the product telescopes.

Brouncker–Wallis (derived): combining the two, WQ[k] = CF_k.P * CF_k-1.P. Each Wallis denominator is the product of two consecutive CF numerators. This closes the triangle.

Section 13 proved the Cassini identity for the golden ratio CF by hand. Section 14 proved the convergent determinant for √2 by hand. Both follow the same pattern: at each step n, h_nk_n-1 - h_n-1k_n = (-1)ⁿ⁺¹. They were always the same theorem — applied to different coefficients.

The @CFDeterminantProof macro makes the unification explicit. Given any continued fraction's coefficients, it computes convergents internally, generates shared SuccessorLeftMultiplication chains grouped by right operand, and emits determinant sum witnesses at each step. The same macro, applied to [1, 1, 1, 1, 1] or [1, 2, 2, 2], recovers both identities.

This section ties together nearly every technique from the tutorial:

• Witness chains (section 2): the determinant sums are PlusSucc/PlusZero chains, exactly the addition witnesses introduced at the start.
• Macros as proof search (section 3): the macro computes convergents and products at compile time, then emits witness types for the type checker to verify — the same search/verify split that powers the pi and Fibonacci proofs.
• Universal multiplication theorems (section 10): the products h_n * k_n-1 and h_n-1 * k_n are built from OneTimesProof and chained .Distributed — the same universal theorems that eliminated per-factor product chains in the golden ratio and √2 macros.
• Distributivity and difference of squares (sections 12–13): the Cassini identity decomposes F(n+1) * F(n-1) via distributivity, and the factor correspondence uses the difference-of-squares identity — both are structural decompositions that the determinant identity generalizes.
• Cross-verification: the assertEqual calls below compare the macro's convergents against GoldenRatioProof (section 6) and Sqrt2ConvergenceProof (section 7). Two independently generated proofs — one from the constant-specific macro, one from the unified macro — must produce identical types.

Where earlier sections proved individual identities, this section shows them as instances of one parametric structure. The coefficients change; the proof shape doesn't.