Mathematical Physics

Motivation

This mission is a statement about ordinary differential equations and nothing else. It is motivated by the scaling analysis in the Shape Zero derivation (00_START_HERE/MODEL_SPEC.md §1b), which found that the golden ratio in an on-site quadratic well is a coordinate choice. The statements below do not depend on that motivation.

Result. For any $a \neq 0$ and any two distinct real roots $r_1 \neq r_2$, the equation

$$x'' = -a\,(x - r_1)(x - r_2)$$

becomes exactly

$$z'' = -(z^2 - 1)$$

under one fixed shift and scaling of the value and one fixed rescaling of time. So every oscillator with a quadratic restoring force and two real roots is the same oscillator, described in different units. In particular, the golden-ratio well $x'' = -(x^2 - x - 1)$, whose roots are $\varphi$ and $-1/\varphi$, is the normal form in disguise: its $\varphi$ is a choice of coordinates.

What this mission does NOT prove.

• Nothing about any lattice or model. It concerns a single oscillator. It does not treat coupling terms, and it says nothing about which dimensionless combinations survive in a coupled system.
• Not that $\varphi$ has no meaning anywhere. It shows only that $\varphi$ in this equation is a coordinate choice.
• Only solutions defined on all of $\mathbb{R}$. Some solutions of this equation escape to infinity in finite time; the theorem concerns twice continuously differentiable functions on the whole real line. The same transformation works on intervals, but that is not formalized.
• Not uniqueness of the transformation. It proves one exists.

Setting

Solutions are functions $x : \mathbb{R} \to \mathbb{R}$ that are twice continuously differentiable on all of $\mathbb{R}$ (ContDiff ℝ 2 x), with $x''$ written deriv (deriv x). The transformation is

$$z(\tau) = \frac{x(\tau/\omega) - m}{d},$$

a shift by $m$, a scaling by $d \neq 0$ of the value, and a rescaling $t = \tau/\omega$ of time with $\omega > 0$.

Formalization targets

Goal: one transformation for every solution

Let $a \neq 0$ and $r_1 \neq r_2$. There are real numbers $m$, $d$, $\omega$ with $d \neq 0$ and $\omega > 0$, chosen once, before any solution is considered, such that for every twice continuously differentiable $x : \mathbb{R} \to \mathbb{R}$:

$$\bigl(\forall t,\; x''(t) = -a\,(x(t) - r_1)(x(t) - r_2)\bigr) \iff \bigl(\forall \tau,\; z''(\tau) = -(z(\tau)^2 - 1)\bigr).$$

This is QuadraticWell.quadratic_well_equiv. Explicitly $m = (r_1 + r_2)/2$, $d = \pm(r_1 - r_2)/2$ with the sign chosen so that $a d > 0$, and $\omega = \sqrt{a d}$.

Milestones

1. M1 (the force in shifted, scaled form). If $r_1 \neq r_2$ and $d = \pm(r_1 - r_2)/2$ (either sign), then for every real $y$: $-a(y - r_1)(y - r_2) = -a\,d^2\bigl(((y - m)/d)^2 - 1\bigr)$ with $m = (r_1 + r_2)/2$.
2. M2 (the sign can be chosen). If $a \neq 0$ and $r_1 \neq r_2$, then $a (r_1 - r_2)/2 > 0$ or $a (r_2 - r_1)/2 > 0$ — so $\omega = \sqrt{a d}$ is real and positive for one choice of $d$.
3. M3 (chain rule for the rescaling). For $x$ twice continuously differentiable, $\omega \neq 0$ and $d \neq 0$, the second derivative of $\tau \mapsto (x(\tau/\omega) - m)/d$ at $\tau$ is $x''(\tau/\omega)/(\omega^2 d)$.

The goal combines them: by M1 the equation reads $x'' = -a d^2 (y^2 - 1)$ with $y = (x - m)/d$; by M3 this becomes $z'' = -(a d/\omega^2)(z^2 - 1)$; and $\omega^2 = a d$, available by M2, gives $z'' = -(z^2 - 1)$. The converse uses $\tau = \omega t$.

Corollary: the golden-ratio well

For every twice continuously differentiable $x : \mathbb{R} \to \mathbb{R}$, $x'' = -(x^2 - x - 1)$ everywhere if and only if

$$z(\tau) = \frac{x(\tau/\omega) - \tfrac12}{\sqrt5/2}, \qquad \omega = \sqrt{\sqrt5/2},$$

satisfies $z'' = -(z^2 - 1)$ everywhere. This is the explicit instance with roots $\varphi$ and $-1/\varphi$: $m = \tfrac12$, $d = \sqrt5/2$.

Significance

The result itself. It shows that the only content of a quadratic restoring force with two real roots, for a single oscillator, is the normal form $z'' = -(z^2 - 1)$; the roots and the stiffness are units.

Formalizing it. The equivalence had been checked numerically only.

Cross-check (independent code)

check	result
M1 identity, both signs of $d$ (sympy)	exact
golden-ratio well: $m$, $d$, $\omega$	$\tfrac12$, $\sqrt5/2$, $(\sqrt5/2)^{1/2} = 1.057371$
$z(\tau) = (x(\tau/\omega) - m)/d$ against a direct solution of $z'' = -(z^2 - 1)$, 400 points	max difference $6.9\times10^{-13}$
a case needing the sign flip ($a = -2$, roots $3$ and $-1$)	$a h = -4 < 0$, so $d = -h$ gives $a d = 4 > 0$

These agree with the repository's shape_zero_tests/scale_invariance.py (runs at four unit choices agreeing to $1.3\times10^{-14}$).

Difficulty

Low–moderate. M1 and M2 are short. M3 is the only fiddly part: Mathlib's chain rule for a composition with $\tau \mapsto \tau/\omega$, applied twice, needs the differentiability of $x$ and of $x'$ that ContDiff ℝ 2 supplies. The goal and corollary then follow by rewriting.

Formalization scope

• Solutions are functions on all of $\mathbb{R}$, twice continuously differentiable; the derivative is Mathlib's deriv.
• $m$, $d$ and $\omega$ are existentially chosen before the solution $x$, so one transformation serves every solution.
• The hypotheses of the goal are exactly $a \neq 0$ and $r_1 \neq r_2$.

Selected references

• Wikipedia, Nondimensionalization. https://en.wikipedia.org/wiki/Nondimensionalization
• Wikipedia, Golden ratio. https://en.wikipedia.org/wiki/Golden_ratio
• Shape Zero repository (motivation only). https://github.com/ShapeZeroSZ/shape-zero

Motivation

The Shape Zero model reaches the Fano plane — the seven-point, seven-line configuration behind the seven imaginary units of the octonions — by a combinatorial route: C1 Formal Proofs, §3, Theorem 3.6 ("Roles Force Fano") states that any Steiner triple system admitting a role colouring is the Fano plane. Its proof derives only that there are $7$ points, and takes the last step on trust: C1 §3 asserts "the unique STS(7) (the Fano plane PG(2, 2))" in Theorem 3.3 and justifies it with one sentence, "Uniqueness of STS(7) is classical."

The companion mission The role postulates force exactly seven points proved the point count and deliberately stopped there. This mission supplies the missing step and completes the chain:

1. Goal: every Steiner triple system on $7$ points is the Fano plane, up to a relabelling of its points.
2. Capstone: every nonempty Steiner triple system that admits a role colouring is the Fano plane, up to relabelling — C1 Theorem 3.6 in full.

The attack path is the standard textbook proof of the uniqueness of STS(7), supplying the step C1 §3 calls classical. The proof goes through three milestones: a normal form around one point, exactly two completions of it, and an explicit relabelling of each completion onto the Fano plane. The line count (seven lines, three through each point) and the meeting property (any two lines meet in exactly one point) then follow as corollaries of the goal. C1 gives no argument for this step; the milestones below are that classical argument, not C1's.

What this mission does NOT prove.

• Not the premise. Why lines have three points and why there are three roles is an input of the model, not derived here.
• Not the octonions. The Fano plane is the incidence structure behind the octonion multiplication table, but choosing an orientation and building the multiplication (C1 §4–5: the 16 valid orientations, the 48 role colourings) is a separate step, not covered here.
• Up to relabelling only. "Is the Fano plane" means: some bijection of points carries the system's lines exactly onto the Fano plane's lines.

Setting

A Steiner triple system on the points $\{0, \dots, n-1\}$ is a family of $3$-point subsets, called lines, such that every pair of distinct points lies on exactly one line. A role colouring gives each point of each line one of three roles so that the three points of a line get different roles and every point takes every role exactly once.

The Fano plane is the Steiner triple system on $\{0, \dots, 6\}$ with lines $\{i, i+1, i+3\}$ modulo $7$:

$$\{0,1,3\},\ \{1,2,4\},\ \{2,3,5\},\ \{3,4,6\},\ \{0,4,5\},\ \{1,5,6\},\ \{0,2,6\}.$$

This is the companion mission's published definition RolesForceSeven.fano, labelled $0, \dots, 6$. (C1 §5 writes the same lines on $e_1, \dots, e_7$; this mission uses the companion mission's labelling.)

The definitions RolesForceSeven.STS, RolesForceSeven.RoleColouring and RolesForceSeven.fano are imported from the companion mission, not restated, so both missions refer to the same objects. The one new definition is FanoUnique.IsFano S: there is a bijection $e$ from the points of $S$ to $\{0, \dots, 6\}$ with $\{ e(\ell) : \ell \text{ a line of } S \} =$ the Fano lines.

Formalization targets

Goal: every STS(7) is the Fano plane

$$S \text{ a Steiner triple system on } 7 \text{ points} \;\Longrightarrow\; \exists\, e \text{ bijective},\quad e(\text{lines of } S) = \text{Fano lines}.$$

This is FanoUnique.sts7_is_fano.

Milestones — the attack path

1. M1 (normal form). Every STS on $7$ points can be relabelled so that the lines through point $0$ are $\{0,1,2\}$, $\{0,3,4\}$ and $\{0,5,6\}$.
2. M2 (two completions). If an STS on $7$ points contains $\{0,1,2\}$, $\{0,3,4\}$, $\{0,5,6\}$, its lines are exactly one of
   • A: those three and $\{1,3,6\}, \{1,4,5\}, \{2,3,5\}, \{2,4,6\}$;
   • B: those three and $\{1,3,5\}, \{1,4,6\}, \{2,3,6\}, \{2,4,5\}$.
3. M3 (both completions are the Fano plane). Explicit relabellings carry A and B onto the Fano lines.

The goal follows from M1, M2 and M3. (These are M3, M4 and M5 in the draft's original numbering.)

Corollaries of the goal

• A — seven lines, three through each point. An STS on $7$ points has exactly $7$ lines, and every point lies on exactly $3$ of them.
• B — two lines meet once. Any two distinct lines share exactly one point.

Both hold in the Fano plane and are preserved by relabelling, so they follow from the goal.

Capstone

For $n \ge 1$, a Steiner triple system on $n$ points with a role colouring is the Fano plane up to relabelling (FanoUnique.roles_force_fano). The companion mission's goal gives $n = 7$; the goal of this mission does the rest. The hypothesis $n \ge 1$ is kept, following the erratum to C1 §3: the empty system satisfies every other condition and is not the Fano plane.

Significance

The result itself. Together with the companion mission, it makes C1 Theorem 3.6 fully machine-verified: the role postulates force not only seven points but the Fano plane itself, up to relabelling.

Formalizing it. C1 cites the uniqueness of STS(7) as classical. It was checked numerically — exhaustively over labelled systems — but never proved in the C1 package; this mission proves it.

Numerical cross-check (exhaustive)

check	result
Steiner triple systems on 7 labelled points	30 (classical count $7!/168 = 30$)
of those, isomorphic to the Fano plane	30 of 30
any two distinct lines meet in exactly one point	true in all 30
completions of $\{0,1,2\}, \{0,3,4\}, \{0,5,6\}$	exactly 2 (A and B)
swapping points 1 and 2 carries A to B	true

Difficulty

Moderate. M3 is a finite computation. The work is in M1 — building the relabelling bijection from the three lines through a point — and M2, the case analysis on the line through points $1$ and $3$, which forces the remaining lines. Corollaries A and B follow from the goal by relabelling. Exhaustive search over all line families ($2^{35}$) is not feasible, so the structured proof is needed.

Formalization scope

• Points are Fin n; lines are Finset (Fin n); the definitions are the companion mission's, imported unchanged.
• "Is the Fano plane" is an equality of line families after relabelling by an equivalence Fin n ≃ Fin 7; it forces $n = 7$ and exactly $7$ lines.
• The capstone keeps $0 < n$ and the companion mission's role colouring unchanged.

Selected references

• Shape Zero LLC, Formal Proofs of the C1 Verification Package (August 2026), §3 (Theorem 3.3 and Theorem 3.6). https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ShapeZero_C1_Formal_Proofs.pdf
• Errata — C1 Formal Proofs, Section 3 (Theorem 3.6 needs a nonempty point set). https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ERRATUM_Theorem_6.1.md
• Wikipedia, Fano plane. https://en.wikipedia.org/wiki/Fano_plane
• Wikipedia, Steiner system. https://en.wikipedia.org/wiki/Steiner_system

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) predicts a propagation asymmetry: with a gyroscopic coupling of strength $\beta$, a wave travelling one way oscillates at a slightly different frequency from the same wave travelling the other way, and the difference, $2\beta c \sin k_0$, does not depend on the on-site stiffness $K$. The companion mission The propagation asymmetry does not depend on the on-site stiffness proves this on a one-dimensional uniform lattice. The model's base is three-dimensional, where a wave also carries transverse wavenumbers. This mission extends the result to a uniform lattice with any number q ≥ 1 of axes, and shows that the asymmetry is independent of both the stiffness and every transverse wavenumber.

What this mission does NOT prove.

• Only the linear, small-amplitude asymmetry, as in the companion mission; the nonlinear coefficient $\kappa$ is not protected.
• Only a uniform lattice.
• The gauge term acts along one axis (axis 0, the propagation axis, as in the model's q = 3 implementation). If it acted along several axes, each would add its own term to the asymmetry.

Setting

Fix real numbers $K$ (on-site stiffness), $c$ (neighbour coupling) and $\beta$ (gyroscopic strength), and a wavevector $k = (k_0, k_1, \dots, k_{q-1}) \in \mathbb{R}^q$. The upper-branch frequency is

$$\omega(k) = \beta c \sin k_0 + \sqrt{\bigl(\beta c \sin k_0\bigr)^2 + K + 2c \sum_{a=0}^{q-1} (1 - \cos k_a)},$$

with the sum over all axes. Reversing the wave along axis 0 gives $\bar k = (-k_0, k_1, \dots, k_{q-1})$. In Lean these are PinnedAsymmetryQ.omega q K c β k (with Real.sqrt) and flip0 q k. The formula has been checked against the eigenvalues of the actual q = 3 lattice generator to $1.8\times10^{-14}$ across 216 wavevectors and three parameter sets.

Formalization targets

Goal: the asymmetry is $2\beta c \sin k_0$

$$\omega(k) - \omega(\bar k) = 2\beta c \sin k_0 \qquad \text{for all real } K, c, \beta \text{ and every } k.$$

This is PinnedAsymmetryQ.asymmetry. Neither $K$ nor any transverse wavenumber appears on the right.

Milestones

1. M1 (branch frequency). When the quantity under the square root is non-negative, $\omega(k)$ solves $\omega^2 - 2\beta c\sin k_0\,\omega - \bigl(K + 2c\sum_a (1-\cos k_a)\bigr) = 0$.
2. M2 (the radicand is unchanged by reversing axis 0).

Corollaries (the statements in the title)

• A — independent of stiffness: for any $K_1, K_2$, the asymmetry $\omega(k) - \omega(\bar k)$ is the same.
• B — independent of transverse motion: for any two wavevectors with the same $k_0$, the asymmetry is the same.

Significance

The result itself. The goal isolates the part of the frequency that is exactly independent of the stiffness and of the transverse wavenumbers on a lattice of any dimension. At q = 3 it is the statement relevant to the model's actual base; at q = 1 it reduces to the companion mission.

Formalizing it. The q-dimensional statement had been checked numerically only (3,000 random parameter sets at q = 3: goal to $8.9\times10^{-16}$). A proof covers every $q$, every wavevector and all real parameters.

Difficulty

Low. The asymmetry is a difference of two expressions whose square-root parts depend on $K$ and on every $k_a$; the point is that reversing axis 0 leaves the radicand unchanged, so the square roots cancel. M1 needs the radicand non-negative in order to square the square root.

Formalization scope

• $q \ge 1$ ([NeZero q]), so axis 0 exists. All parameters are arbitrary reals, with no sign conditions in the goal.
• Lean's Real.sqrt returns $0$ on negative inputs. The goal still holds there, because the two radicands are equal, so the two square roots are equal whatever value they take.
• Only the upper branch (the $+$ sign) is treated; the gauge term enters through $\sin k_0$ only.

Selected references

• Wikipedia, Dispersion relation. https://en.wikipedia.org/wiki/Dispersion_relation
• Wikipedia, Gyrator (gyroscopic, non-reciprocal coupling). https://en.wikipedia.org/wiki/Gyrator
• Mathlib, Mathlib.Analysis.Real.Sqrt (Real.sqrt, returning $0$ on negative inputs). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Real/Sqrt.html

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) couples neighbouring nodes through a velocity-dependent force, one coupling matrix per link. The companion mission Zero net power forces every link coupling to be symmetric (rings of ≥ 3 sites) proves that a coupling doing no net work (a passive coupling) must have every link matrix symmetric — but only on a one-dimensional ring. The model's base is three-dimensional. This mission extends the result to a periodic cubic lattice with any number q of spatial axes, so it covers q = 3 directly and reduces exactly to the ring result at q = 1.

What this mission does NOT prove. As with the companion missions, commuting with the complex structure $J$ is not derived here; it remains a modelling premise. This mission shows only that passivity forces symmetry on every link in every direction.

Setting

Fix natural numbers $q$ (number of axes), $L$ (sites along each axis) and $d$. A site is a point $x \in (\mathbb{Z}/L\mathbb{Z})^q$ of the periodic cubic lattice; $x \pm e_a$ is the site one step forward or back along axis $a$, wrapping around. Each link — a site $x$ together with an axis $a$ — carries its own real $d\times d$ matrix $W(x,a)$, and each site carries a velocity $v(x) \in \mathbb{R}^d$. The force on site $x$ is

$$F(x) = \sum_{a} \Bigl( W(x,a)\, v(x+e_a) - W(x-e_a,a)\, v(x-e_a) \Bigr),$$

where the second term uses the matrix of the link behind $x$. The total power is

$$P_W(v) = \sum_{x} v(x) \cdot F(x).$$

In Lean, sites are Site q L = Fin q → Fin L, the step is shift x a s (update coordinate $a$ by $s$ in Fin L), and the power is PassivityTorus.power q L d W v. The coupling is passive when $P_W(v) = 0$ for every $v$.

Formalization targets

Goal: passive if and only if every link is symmetric ($L \ge 3$)

$$L \ge 3 \;\Longrightarrow\; \Bigl(\forall v,\; P_W(v) = 0\Bigr) \iff \Bigl(\forall x, a,\; W(x,a)^{\mathsf T} = W(x,a)\Bigr).$$

This is PassivityTorus.passive_iff_symm, for every $q$ and $d$.

Milestones

1. M1. Stepping back then forward along an axis returns to the start.
2. M2 (power identity, every $q$, $L$). $P_W(v) = \sum_x \sum_a v(x) \cdot \bigl((W(x,a) - W(x,a)^{\mathsf T})\, v(x+e_a)\bigr)$.
3. M3 (symmetric links are passive, every $L$).
4. M4 (passive forces symmetric, $L \ge 3$).

Significance

The result itself. It is the dimension-independent form of the passivity theorem: whatever the number of spatial axes, a per-link coupling does no net work for every motion exactly when every link matrix is symmetric. It removes the one-dimensional restriction from the step that justifies restricting the model's coupling class to symmetric matrices.

Formalizing it. The ring result has been machine-checked; the lattice extension had been checked numerically only (identity error $\le 3.6\times10^{-14}$ at $(q,L) = (1,3), (2,3), (3,3), (3,4)$). A proof covers every $q$, $L \ge 3$ and $d$.

Difficulty

The algebra is the ring argument; the difficulty is bookkeeping. The incoming term must be reindexed by the one-step shift, which is a bijection of the torus, and the converse needs a test motion supported on two neighbouring sites $x$ and $x+e_a$ together with a proof that no other link joins them.

The hypothesis $L \ge 3$ is necessary. At $L = 2$ the step forward and the step back along an axis reach the same site. This is proved (in Lean, locally): for every $q \ge 1$, putting the same non-symmetric matrix $\begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}$ on every link of the $L = 2$ lattice gives exactly zero power for every velocity field, so passivity does not force symmetry there. Weakening the hypothesis makes the goal false.

Formalization scope

• The lattice is periodic in every axis, with the same $L$ along each; [NeZero L] is needed for the literal $1$ in Fin L and is implied by $L \ge 3$ in the goal.
• There is one matrix per site per axis, with no relation assumed between links.
• Passivity is quantified over all velocity fields; everything is real.
• $q = 0$ (a single site, no links) and $d = 0$ are included; both sides of the goal hold trivially there, and this is not a trivialization since the statement is quantified over all $q$ and $d$.

Selected references

• Wikipedia, Symmetric matrix. https://en.wikipedia.org/wiki/Symmetric_matrix
• Wikipedia, Passivity (engineering). https://en.wikipedia.org/wiki/Passivity_(engineering)
• Mathlib, Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.html

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) makes one experimentally testable prediction: a propagation asymmetry. In a ring of oscillators with a gyroscopic coupling of strength $\beta$, a wave travelling one way oscillates at a slightly different frequency from the same wave travelling the other way. The predicted difference is

$$\Delta\omega = 2\beta c \sin q,$$

where $c$ is the neighbour coupling and $q$ the wavenumber. The claim is that this difference is pinned: it does not depend on the on-site stiffness $K$, even though each of the two frequencies does. Simulations of the model measured the linear asymmetry at $1.000038$, $1.000033$ and $1.000026$ times the predicted value at stiffness $0.90$, $1.00$ and $1.10$, i.e. protected to about $10^{-5}$. This mission proves the exact statement for a uniform lattice.

What this mission does NOT prove.

• Only the linear, small-amplitude asymmetry. At larger amplitude there is a nonlinear correction whose coefficient $\kappa$ does change with the stiffness; in simulation it swings by about 35% over a ±10% stiffness change. That coefficient is not protected, and this mission says nothing about it.
• Only a uniform lattice, with every site at the same stiffness $K$. When the stiffness varies from site to site, the asymmetry does shift (measured in simulation). This mission covers the uniform case only.

Setting

Fix real numbers $K$ (on-site stiffness), $c$ (neighbour coupling), $\beta$ (gyroscopic strength) and a wavenumber $q$. Write

$$b(q) = \beta c \sin q, \qquad R(q) = \bigl(\beta c \sin q\bigr)^2 + K + 2c\,(1 - \cos q).$$

The upper-branch frequency on a uniform ring is

$$\omega(q) = \beta c \sin q + \sqrt{\bigl(\beta c \sin q\bigr)^2 + K + 2c\,(1 - \cos q)} = b(q) + \sqrt{R(q)}.$$

In the Lean development this is PinnedAsymmetry.omega K c β q, with Real.sqrt for the square root. When $R(q) \ge 0$, $\omega(q)$ is a root of the dispersion relation

$$\omega^2 - 2\beta c \sin q\,\omega - \bigl(K + 2c\,(1 - \cos q)\bigr) = 0 .$$

Formalization targets

Goal: the asymmetry is $2\beta c \sin q$, independent of $K$

$$\omega(q) - \omega(-q) = 2\beta c \sin q \qquad \text{for all real } K, c, \beta, q .$$

This is PinnedAsymmetry.asymmetry. The right-hand side contains no $K$. As an immediate consequence, for any two stiffnesses $K_1$ and $K_2$ the asymmetry is identical.

Milestones

1. M1 (the formula is a branch frequency). If $R(q) \ge 0$, then $\omega(q)$ solves the dispersion relation above.
2. M2 (the radicand is even in $q$). $R(-q) = R(q)$, because $\sin^2(-q) = \sin^2 q$ and $\cos(-q) = \cos q$.

Significance

The result itself. The goal isolates the one quantity in the model's prediction that is exactly independent of the on-site stiffness: the direction-dependent part of the frequency. Each branch frequency depends on $K$ through the square root, but the difference between the two directions does not. M1 is what makes this a statement about the physical frequency rather than about an arbitrary expression, by showing the formula solves the model's dispersion relation.

Formalizing it. The algebra is elementary; the content is that the stiffness provably drops out, for every value of the parameters rather than at the sampled stiffnesses of a simulation. The formal statement also records precisely what is covered (the linear asymmetry on a uniform lattice) and what is not (the nonlinear coefficient $\kappa$ and non-uniform stiffness).

Difficulty

The difficulty is low. The asymmetry is a difference of two expressions that each contain a square root depending on $K$; the point to establish is that the two square roots coincide, so that no stiffness dependence survives the subtraction. M1 requires squaring the square root, which is valid only when the radicand is non-negative.

Formalization scope

• All parameters $K, c, \beta, q$ are arbitrary reals; no sign conditions are imposed in the goal.
• Lean's Real.sqrt returns $0$ on negative inputs. The goal still holds in that regime, because the two radicands $R(q)$ and $R(-q)$ are equal, so the two square roots are equal whatever value they take. For physical parameters ($K \ge 0$, $c \ge 0$) the radicand is always non-negative.
• M1 carries the hypothesis $R(q) \ge 0$, since only then is $\omega(q)$ a genuine root of the dispersion relation.
• The frequency is the upper branch only (the $+$ sign in front of the square root).

The development needs only Mathlib's real trigonometric functions and Real.sqrt.

Selected references

• Wikipedia, Dispersion relation. https://en.wikipedia.org/wiki/Dispersion_relation
• Wikipedia, Gyrator (gyroscopic, non-reciprocal coupling). https://en.wikipedia.org/wiki/Gyrator
• Mathlib, Mathlib.Analysis.Real.Sqrt (Real.sqrt, returning $0$ on negative inputs; Real.sq_sqrt). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Real/Sqrt.html

Motivation

The Shape Zero model (Shape Zero LLC, unpublished) couples neighbouring nodes on a ring through a velocity-dependent force, with one coupling matrix per link. A companion mission, The passivity-admissible couplings have dimension n² = dim u(n), shows that real matrices which are symmetric and commute with a complex structure $J$ form a space of dimension $n^2 = \dim \mathfrak{u}(n)$. That mission deliberately takes symmetry as given. This mission supplies the reason for it: a coupling that never does net work (a passive coupling) must have every link matrix symmetric, provided the ring has at least three sites.

Together the two missions give the chain

$$\text{passive} \;\Longrightarrow\; \text{every } W_i \text{ symmetric} \qquad\text{(this mission)},$$ $$\text{symmetric} + \text{commutes with } J \;\Longrightarrow\; \dim = n^2 \qquad\text{(companion mission)}.$$

What these two missions do NOT prove. Commuting with $J$ is not derived here. It is the requirement that the coupling respect each node's complex structure, and in the model it is imposed, not forced by passivity. After both missions the proved content is: passivity forces symmetry, and symmetric $J$-compatible couplings have the dimension of $\mathfrak{u}(n)$. The $J$-compatibility step remains a modelling premise. In addition, the coupling space consists of the Hermitian matrices, which match $\mathfrak{u}(n)$ in dimension; the Lie algebra $\mathfrak{u}(n)$ itself appears only after multiplying by $i$ (Unitary group).

Setting

Let $N$ and $d$ be natural numbers with $N \ge 1$. A ring has $N$ sites labelled by $\mathbb{Z}/N\mathbb{Z} = \{0, \dots, N-1\}$, so site $N-1$ is next to site $0$; indices $i + 1$ and $i - 1$ are taken modulo $N$. Each site carries a velocity vector $v_i \in \mathbb{R}^d$, and each link $i \to i+1$ carries a real $d \times d$ link matrix $W_i$. The force on site $i$ is

$$F_i = W_i\, v_{i+1} - W_{i-1}\, v_{i-1},$$

where the second term uses the previous link's matrix $W_{i-1}$. The total power delivered by the coupling is

$$P_W(v) = \sum_{i \in \mathbb{Z}/N\mathbb{Z}} v_i \cdot \bigl( W_i\, v_{i+1} - W_{i-1}\, v_{i-1} \bigr).$$

In the Lean development this is PassivityRing.power N d W v, with sites indexed by Fin N (whose addition and subtraction wrap around modulo $N$), vectors in Fin d → ℝ, and $\cdot$ the dot product ⬝ᵥ. The coupling is passive when $P_W(v) = 0$ for every choice of velocities $v$.

Formalization targets

Goal: passive if and only if every link is symmetric (rings of at least 3 sites)

$$N \ge 3 \;\Longrightarrow\; \Bigl( \forall v,\; P_W(v) = 0 \Bigr) \iff \Bigl( \forall i,\; W_i^{\mathsf T} = W_i \Bigr).$$

This is PassivityRing.passive_iff_symm. It holds for every $d$ and every family of link matrices, with no assumption relating different links.

Milestones

1. M1 (power identity, every $N$). $P_W(v) = \sum_i v_i \cdot \bigl((W_i - W_i^{\mathsf T})\, v_{i+1}\bigr)$.
2. M2 (symmetric links are passive, every $N$). If every $W_i$ is symmetric, then $P_W(v) = 0$ for all $v$.
3. M3 (passive forces symmetric, $N \ge 3$). If $P_W(v) = 0$ for all $v$, then every $W_i$ is symmetric.

Significance

The result itself. The goal turns a physical requirement — no net work for any motion — into an exact algebraic condition on each link separately. It is the step that justifies restricting the companion mission's coupling class to symmetric matrices, so that the dimension count $n^2$ applies to the passive couplings of the model rather than to an assumed class.

Formalizing it. The model's claim has so far been checked numerically at ring sizes $1, 2, 3, 4, 7$. A machine-checked proof covers every $N \ge 3$ and every $d$, makes the role of the hypothesis $N \ge 3$ explicit, and separates what is proved (passivity forces symmetry) from what remains a modelling premise ($J$-compatibility).

Difficulty

The forward direction and the power identity are finite-sum bookkeeping. The central difficulty is the converse: the hypothesis constrains a single scalar quantity summed around the ring, and it must be shown to constrain each link matrix individually. On small rings this fails because distinct terms of the sum coincide, so the argument depends on the ring being large enough that neighbouring sites are genuinely distinct, and in Lean that is modular arithmetic on Fin N.

The hypothesis $N \ge 3$ is necessary, not a convenience:

• $N = 1$: the site is its own neighbour on both sides, so the force is $W_0 v_0 - W_0 v_0 = 0$ and the power vanishes for every $W_0$, symmetric or not.
• $N = 2$: the power reduces to $v_0 \cdot (D - D^{\mathsf T})\, v_1$ with $D = W_0 - W_1$, so it depends only on the difference of the two link matrices. Taking both links equal to the same non-symmetric matrix, for example $\begin{pmatrix} 0 & 1 \\ 0 & 0 \end{pmatrix}$, gives zero power for all velocities.

Weakening the hypothesis to $2 \le N$, or dropping it, makes the goal false.

Formalization scope

• Sites are Fin N with its wrap-around arithmetic, so $i + 1$ and $i - 1$ go around the ring; [NeZero N] is required for the literal $1$ in Fin N and is implied by $N \ge 3$ in the goal.
• There is one matrix per link, W : Fin N → Matrix (Fin d) (Fin d) ℝ, not a single shared matrix, and no relation between different links is assumed.
• Passivity is quantified over all velocity configurations v : Fin N → (Fin d → ℝ).
• Everything is real (ℝ); symmetry is (W i)ᵀ = W i.
• $d = 0$ is included; there both sides of the goal hold trivially. This is not a trivialization, since the statement is quantified over all $d$.

M1 and M2 hold for every $N \ge 1$ and carry no ring-size hypothesis; M3 and the goal require $N \ge 3$. The development needs only Mathlib's finite sums, dot products, matrix–vector products and Fin arithmetic.

Selected references

• B. C. Hall, Lie Groups, Lie Algebras, and Representations: An Elementary Introduction, 2nd ed., Graduate Texts in Mathematics 222, Springer, 2015. https://doi.org/10.1007/978-3-319-13467-3
• Wikipedia, Unitary group. https://en.wikipedia.org/wiki/Unitary_group
• Wikipedia, Symmetric matrix. https://en.wikipedia.org/wiki/Symmetric_matrix
• Mathlib, Mathlib.Data.Matrix.Mul (dot product ⬝ᵥ, matrix–vector product *ᵥ). https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Matrix/Mul.html

Motivation

An integer winding label is discrete, but its exponential readout lies on a continuous circle. This mission makes that relationship exact. For a nonzero real algebraic angle $\alpha$, the map

$$n\longmapsto e^{i n\alpha}$$

is simultaneously a group character, a faithful encoding of $\mathbb Z$, and a countable dense orbit in the unit circle. Its complex values also form a linearly independent family over the algebraic complex numbers $\overline{\mathbb Q}$.

The result welds three previously completed interfaces. Circle covering theory produces canonical integer winding. Irrational-rotation theory classifies when an integer orbit is dense. Lindemann–Weierstrass gives the arithmetic rigidity that excludes resonance and algebraic linear relations. The point is not that topology alone proves transcendence, or that transcendence constructs winding: the theorem records the precise composition of the three layers.

The foundations are the completed private missions Winding Dynamics I, Lindemann–Weierstrass I, and Winding Arithmetic II. The transcendence layer is an attributed Lean 4.30-compatible port of Yuyang Zhao's mathlib PR #28013.

Setting

Write $S^1\subset\mathbb C$ for the complex unit circle. For a real angle $\alpha$ and integer $n$, define

$$\operatorname{phase}_\alpha(n)=e^{i n\alpha}\in S^1.$$

This is an additive-to-multiplicative character: phase at $0$ is $1$, and phase at $m+n$ is the product of the phases at $m$ and $n$.

A based Circle loop $\gamma$ has a canonical integer $\operatorname{wind}(\gamma)$, obtained from the endpoint of its zero-based lift through the exponential cover. Its real phase readout is $\operatorname{phase}_\alpha(\operatorname{wind}(\gamma))$.

The orbit is dense when every nonempty open subset of $S^1$ contains some $\operatorname{phase}_\alpha(n)$. It is faithful when distinct integers have distinct phases. These properties are compatible: a countable subset may be dense without being all of the circle.

Formalization targets

Irrational rotation criterion

For every real $\alpha$,

$$\operatorname{DenseRange}(n\mapsto e^{i n\alpha}) \quad\Longleftrightarrow\quad \frac{\alpha}{2\pi}\notin\mathbb Q.$$

The proof identifies the phase orbit with integer multiples in $\mathbb R/(2\pi\mathbb Z)$ and transports Mathlib's irrational-rotation theorem through the standard homeomorphism with the complex unit circle.

Algebraic angles are nonresonant

If $\alpha\in\mathbb R$ is nonzero and algebraic over $\mathbb Q$, then $\alpha/(2\pi)$ is irrational. Otherwise $\pi$ would be algebraic, contradicting the proved transcendence of $\pi$. Consequently the real phase character has dense range.

Faithfulness and arithmetic rigidity

For the same nonzero algebraic $\alpha$, the character is injective and

$$\bigl(e^{i n\alpha}\bigr)_{n\in\mathbb Z}$$

is linearly independent over $\overline{\mathbb Q}$. The first conclusion says no two winding integers alias. The second says no nontrivial finite algebraic-coefficient linear relation exists among the phase values.

Actual Circle-loop consumer

For based Circle loops $\gamma$ and $\delta$,

$$e^{i\alpha\operatorname{wind}(\gamma)} =e^{i\alpha\operatorname{wind}(\delta)} \quad\Longleftrightarrow\quad \operatorname{wind}(\gamma)=\operatorname{wind}(\delta).$$

This consumes the canonical covering-space winding rather than an arbitrary externally supplied integer.

Resonance control

At the full-turn angle $\alpha=2\pi$, every integer phase is $1$, so the character is not injective. This negative control is outside the algebraic-angle regime because $\pi$ is transcendental. It records exactly why a nonresonance hypothesis is load-bearing.

Significance

The capstone exhibits one object with three complementary properties:

1. topological discreteness — values are indexed by integer winding;
2. dynamical density — the countable orbit visits every Circle neighborhood;
3. arithmetic rigidity — distinct values are faithful and linearly independent over $\overline{\mathbb Q}$.

This is a precise version of the intuitive claim that winding creates an integer coordinate whose phase representation explores a continuum. The continuum statement is density, not surjectivity: the image remains countable. The arithmetic statement is linear independence, not algebraic independence of the separate phase variables; the character law itself supplies multiplicative relations.

Together with Winding Arithmetic II, continuous homotopy preserves these readouts and a registered reset ledger factorizes their changes. This mission isolates the extra fact that the resulting character is both faithful and dense for every nonzero real algebraic angle.

Difficulty

No single layer implies the capstone by itself. The Circle exponential is periodic, so injectivity requires a genuine nonresonance argument. Density requires the exact normalization by $2\pi$ and transport through the AddCircle–Circle homeomorphism in both directions. Linear independence requires the completed Lindemann–Weierstrass theorem, not merely irrationality or transcendence of $\pi$.

The coercion bridge between the real Circle phase and the complex exponential character is also orientation-sensitive: the formal phase is exactly $\exp(i n\alpha)$. Reversing the sign would still define a dense faithful character, but it would not be the registered convention used by the prior winding arithmetic mission.

Formalization scope

All artifacts use Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. Circle density is stated only for real $\alpha$. The arithmetic conclusions require both IsAlgebraic ℚ α and $\alpha\ne0$.

The actual-loop theorem proves equality of phase values if and only if equality of canonical winding integers. It does not claim that the loops themselves are equal, and it does not add a new classification of homotopy classes. That classification remains the responsibility of the Circle covering-space layer.

The theorem proves a faithful representation of winding values, not the existence of winding in an arbitrary physical model. A Kuramoto, XY, or Lohe consumer must still provide a jointly continuous Circle field or a preserved non-simply-connected carrier and readout. No particle–wave or quantum-mechanical interpretation is asserted.

Selected references

• Yuyang Zhao, The Lindemann–Weierstrass theorem, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
• Nathan Jacobson, Basic Algebra I, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
• Lean mathematical library, Dense subgroups of the additive circle. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Instances/AddCircle/DenseSubgroup.html
• Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002, Chapter 1. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf

Motivation

In F-theory, the non-abelian gauge algebra of an elliptic fibration is read off from the Kodaira/Tate type of the singular fibres over the discriminant locus, via the fibre--gauge-algebra dictionary (T. Weigand, TASI Lectures on F-theory, arXiv:1806.01854). For a locally minimal short Weierstrass model $y^2 = x^3 + f x + g$, each potentially good additive Kodaira type has a fixed discriminant vanishing order $\operatorname{ord}\Delta$ — the entries of Tate's table — and the exceptional types $\mathrm{IV}^*, \mathrm{III}^*, \mathrm{II}^*$ have Dynkin types $E_6, E_7, E_8$ (the gauge algebra in the split/geometric setting; a nonsplit $\mathrm{IV}^*$ instead gives $F_4$). On an elliptically fibered K3 the global discriminant divisor has degree $24 = e(\mathrm{K3}) = 12\,\chi(\mathcal{O}_{\mathrm{K3}})$ (the topological Euler characteristic; the formalized affine statement is $\deg\Delta \le 24$), so the total discriminant charge of the singular fibres is capped. This mission formalizes the potentially good additive rows of the Tate table and the resulting 7-brane budget.

Setting

Fix a field $k$; work with $y^2 = x^3 + f x + g$, $f, g \in k[X]$, discriminant $\Delta = 4f^3 + 27g^2$ (up to the unit $-16$). Write $\operatorname{ord}_{t_0}(p)$ for the multiplicity of $t_0$ as a root of $p$; for the $\mathrm{I}_0^*$ row, whenever $(X - t_0)^2 \mid f$ and $(X - t_0)^3 \mid g$, write $f = (X - t_0)^2 F$ and $g = (X - t_0)^3 G$ and set the reduced coefficients $c_2 = F(t_0)$, $d_3 = G(t_0)$ (equivalently the order-$2$ and order-$3$ Taylor coefficients of $f$ and $g$ at $t_0$). The K3 degree data is $\deg f \le 8$, $\deg g \le 12$, $\Delta \ne 0$. The seven potentially good additive types ($\mathrm{II}, \mathrm{III}, \mathrm{IV}, \mathrm{I}_0^*, \mathrm{IV}^*, \mathrm{III}^*, \mathrm{II}^*$) are encoded by their $(\operatorname{ord} f, \operatorname{ord} g)$ signatures (HasKodaira), with lower bounds written as divisibility $(X - t_0)^n \mid \cdot$ and exact orders as rootMultiplicity.

Formalization targets

Goal — the 7-brane budget

For $k$ of characteristic zero and $(f,g)$ satisfying the K3 degree data, any finite set $S$ of base points, and any assignment $\tau$ of a Kodaira type each point genuinely carries,

$$\sum_{t \in S} \operatorname{discOrder}(\tau(t)) \le 24.$$

Milestones — the Tate table (each entry: fibre signature $\Rightarrow$ exact $\operatorname{ord}\Delta$)

1. $\deg\Delta \le 24$ under $\deg f \le 8$, $\deg g \le 12$.
2. Local orders are bounded by the degree: $\sum_{t \in S}\operatorname{ord}_t\Delta \le \deg\Delta$ ($\Delta \ne 0$, $S$ finite).
3. Type $\mathrm{II}$: $(\operatorname{ord} f \ge 1, \operatorname{ord} g = 1) \Rightarrow \operatorname{ord}\Delta = 2$.
4. Type $\mathrm{III}$: $(\operatorname{ord} f = 1, \operatorname{ord} g \ge 2) \Rightarrow \operatorname{ord}\Delta = 3$.
5. Type $\mathrm{IV}$: $(\operatorname{ord} f \ge 2, \operatorname{ord} g = 2) \Rightarrow \operatorname{ord}\Delta = 4$.
6. Type $\mathrm{I}_0^*$ (full row): $(\operatorname{ord} f \ge 2, \operatorname{ord} g \ge 3,\ 4c_2^3+27d_3^2 \ne 0) \Rightarrow \operatorname{ord}\Delta = 6$.
7. Type $\mathrm{IV}^*$ ($E_6$): $(\operatorname{ord} f \ge 3, \operatorname{ord} g = 4) \Rightarrow \operatorname{ord}\Delta = 8$.
8. Type $\mathrm{III}^*$ ($E_7$): $(\operatorname{ord} f = 3, \operatorname{ord} g \ge 5) \Rightarrow \operatorname{ord}\Delta = 9$.
9. Type $\mathrm{II}^*$ ($E_8$): $(\operatorname{ord} f \ge 4, \operatorname{ord} g = 5) \Rightarrow \operatorname{ord}\Delta = 10$.

Corollaries (also milestones)

10. Exceptional-fibre budget: $8 N_{\mathrm{IV}^*} + 9 N_{\mathrm{III}^*} + 10 N_{\mathrm{II}^*} \le 24$ (pairwise-disjoint IV*/III*/II* loci).
11. At most three type $\mathrm{IV}^*$ ($E_6$) points ($4 \times 8 = 32 > 24$).
12. At most two type $\mathrm{III}^*$ ($E_7$) points ($3 \times 9 = 27 > 24$).
13. At most two type $\mathrm{II}^*$ ($E_8$) points ($3 \times 10 = 30 > 24$).
14. Residual budget: for any finite set $E$ of $\mathrm{II}^*$ ($E_8$) points and any finite $S$ disjoint from $E$, $10\,|E| + \sum_{t \in S}\operatorname{ord}_t\Delta \le 24$ (two $E_8$ points leave at most $4$; note $S$ need not be classified by the seven types).

Significance

Every entry of the table is load-bearing for the budget: the goal converts each $\operatorname{discOrder}(\tau(t))$ into the true local order $\operatorname{ord}_t\Delta$ (milestones 3--9), then bounds the sum by $\deg\Delta \le 24$ (milestones 1--2). Corollaries recover the physics: at most two $\mathrm{II}^*$, at most two $\mathrm{III}^*$, and at most three $\mathrm{IV}^*$ fibres (the $E_8, E_7, E_6$ loci in the split/geometric setting -- a nonsplit $\mathrm{IV}^*$ gives $F_4$); the exceptional budget $8 N_{\mathrm{IV}^*} + 9 N_{\mathrm{III}^*} + 10 N_{\mathrm{II}^*} \le 24$; and the residual budget $10\,\#E + \sum_{t \in S} \operatorname{ord}_t\Delta \le 24$, so two $\mathrm{II}^*$ points leave at most $4$ for the other fibres. Mathlib has a single-curve WeierstrassCurve/EllipticCurve library but no elliptic-fibration theory: this mission builds a machine-checked slice of the Kodaira/Tate fibre-order table over Mathlib's Polynomial API. The results are classical (Kodaira; Tate's algorithm; Schuett--Shioda, arXiv:0907.0298), so the work is the formalization.

Difficulty

The six "clean" rows ($\mathrm{II}, \mathrm{III}, \mathrm{IV}, \mathrm{IV}^*, \mathrm{III}^*, \mathrm{II}^*$) sit at unequal orders $3\operatorname{ord} f \ne 2\operatorname{ord} g$, so the order of the sum is the smaller summand's order — an order-of-a-sum computation, valid in characteristic zero where $4, 27$ are units. The genuinely hard row is $\mathrm{I}_0^*$, which needs finer data than the raw orders. Writing $f = (X - t_0)^2 F$, $g = (X - t_0)^3 G$ with $c_2 = F(t_0)$, $d_3 = G(t_0)$, both terms of $\Delta = 4f^3 + 27g^2$ have order at least $6$, and the coefficient of $(X - t_0)^6$ is $4c_2^3 + 27 d_3^2$; its nonvanishing gives $\operatorname{ord}_{t_0}\Delta = 6$. This covers the three branches $(\operatorname{ord} f, \operatorname{ord} g) = (2,3),\ (2, {\ge} 4),\ ({\ge} 3, 3)$ uniformly — only in the $(2,3)$ branch, where $3\operatorname{ord} f = 2\operatorname{ord} g = 6$, can two nonzero order-$6$ contributions cancel. The nonvanishing is the distinct-roots criterion for the reduced cubic $x^3 + c_2 x + d_3$ and, under $\operatorname{ord} f \ge 2$ and $\operatorname{ord} g \ge 3$, characterizes the $\mathrm{I}_0^*$ row; when it vanishes, further valuation data distinguish the $\mathrm{I}_n^*$ series, the higher potentially good types, and nonminimal cases. The budget itself then needs the local-to-global degree bound (milestones 1--2).

Formalization scope

Over a characteristic-zero field $k$ (intended $k = \mathbb{C}$), Mathlib-native Polynomial API only (natDegree, rootMultiplicity, roots, taylor). Lower-bound orders use divisibility $(X - t_0)^n \mid \cdot$, which faithfully includes the $f = 0$ / $g = 0$ ($\operatorname{ord} = +\infty$) corner that a rootMultiplicity-only encoding drops; exact orders use rootMultiplicity. No global minimality predicate is assumed; at every point classified by HasKodaira, the stated signature implies local minimality (one of $\operatorname{ord} f$, $\operatorname{ord} g$ lies below the non-minimal threshold $\operatorname{ord} f \ge 4 \wedge \operatorname{ord} g \ge 6$). The potentially multiplicative $\mathrm{I}_n$ and $\mathrm{I}_n^*$ series are excluded by design (their discriminant orders form unbounded families, not fixed by $(\operatorname{ord} f, \operatorname{ord} g)$). The budget goal is an upper bound over the fibres one classifies — it assumes a valid type assignment on $S$ but neither constructs it nor proves the existence and uniqueness of the complete Kodaira classification, and $S$ need not exhaust the singular locus. A full exhaustive classification, the $\mathrm{I}_n^*$ series, and the literal $\mathbb{P}^1$ statement (fibre at infinity via homogeneous forms) are natural future extensions. Characteristic zero is assumed for uniformity, not necessity: the degree bound is characteristic-free and the local order lemmas only need $4, 27 \ne 0$ (characteristic $\ne 2, 3$). Over a non-closed field the classification counts $k$-rational affine points; base-change to $\bar{k}$ recovers the geometric statement. Counts are over the affine chart $\mathbb{A}^1 \subset \mathbb{P}^1$.

Selected references

• J. Tate, Algorithm for determining the type of a singular fiber in an elliptic pencil, in Modular Functions of One Variable IV, LNM 476 (1975), 33--52.
• M. Schuett, T. Shioda, Elliptic Surfaces, Adv. Stud. Pure Math. 60 (2010), 51--160. https://arxiv.org/abs/0907.0298
• T. Weigand, TASI Lectures on F-theory, arXiv:1806.01854 (2018). https://arxiv.org/abs/1806.01854

Motivation

Winding number is a topological integer: continuous deformation preserves it, while crossing a branch cut or registering a reset can change it by an integer amount. Transcendence theory gives a different kind of rigidity. For a nonzero algebraic coupling $\alpha$, the phases $e^{i\alpha n}$ attached to distinct integers $n$ are linearly independent over the field $\overline{\mathbb Q}$ of algebraic complex numbers. This mission joins those statements at their exact formal interfaces.

The result is useful wherever a model first produces an integer winding label and then represents that label by a complex phase. Topology supplies the discrete coordinate, dynamics determines when it is conserved or reset, and Lindemann–Weierstrass supplies arithmetic distinguishability. None of those layers is asked to manufacture the others.

The foundation comes from three completed private missions: Winding Dynamics I: Homotopy Conservation and Reset Balance, Integer Winding Transcendence I: Exponential Phase Independence, and Lindemann–Weierstrass I: Exponential Independence. The transcendence proof is an attributed Lean 4.30-compatible port of Yuyang Zhao's mathlib PR #28013.

Setting

Let $S^1$ be the complex unit circle. A based Circle loop is a continuous path in $S^1$ that starts and ends at $1$. Its canonical real lift through the exponential covering starts at $0$; the lift endpoint determines an integer $\operatorname{wind}(\gamma)$.

For $\beta\in\mathbb C$ and $n\in\mathbb Z$, define the integer exponential character

$$\chi_\beta(n)=\exp(n\beta).$$

The arithmetic consumer uses $\beta=i\alpha$, where $\alpha$ is nonzero and algebraic over $\mathbb Q$. Thus a loop $\gamma$ carries the phase $\chi_{i\alpha}(\operatorname{wind}(\gamma))$.

A closed Circle field is a jointly continuous map on the time/spatial square $I\times I$ whose two spatial endpoints agree at every time. Each spatial slice is normalized by its moving basepoint, producing a based loop. A carrier/readout segment generalizes this: an ambient trajectory remains in a registered carrier subspace and is observed through a continuous map from that carrier to $S^1$.

The discontinuous branch is represented separately by a finite reset ledger. It stores successive integer edge-turn cochains. Pairing those cochains with a certified closed edge cycle produces integer winding values and reset periods.

Formalization targets

Circle winding separates algebraic phases

For a family of loops $(\gamma_j)_{j\in J}$ with pairwise-distinct windings,

$$\left(e^{i\alpha\operatorname{wind}(\gamma_j)}\right)_{j\in J} \text{ is linearly independent over }\overline{\mathbb Q}.$$

Continuous evolution preserves the phase basis

If the initial windings of a family of closed Circle fields are distinct, then the initial phase family is linearly independent, every phase is unchanged between endpoint times, and the final phase family remains linearly independent. The same conclusion is exposed through the carrier/readout interface.

Reset balance becomes phase factorization

If a reset ledger has endpoint winding change $W_{\mathrm f}-W_{\mathrm i}$ and registered reset periods $\Delta W_j$, then

$$\chi_\beta(W_{\mathrm f}-W_{\mathrm i}) =\prod_j\chi_\beta(\Delta W_j).$$

This is the multiplicative image of the exact additive ledger balance.

The phase readout is faithful

For nonzero algebraic $\alpha$, the character $\chi_{i\alpha}$ is injective on $\mathbb Z$. Consequently, two actual Circle loops have equal algebraic phase readouts exactly when they have equal canonical winding. On the reset branch,

$$\prod_j\chi_{i\alpha}(\Delta W_j)=1 \quad\Longleftrightarrow\quad W_{\mathrm f}=W_{\mathrm i}.$$

Thus the multiplicative reset record detects zero net winding change without losing integer information.

Significance

The main theorem upgrades conservation of a single integer to conservation of an arithmetic basis. Distinct homotopy classes do not merely retain distinct integer labels: after the algebraic exponential readout, the corresponding phases admit no nontrivial finite linear relation with algebraic coefficients. This lets downstream consumers treat a family of winding sectors as a linearly independent family over $\overline{\mathbb Q}$.

The reset theorem provides the matching event law. Continuous evolution preserves the basis, whereas a registered reset multiplies phases according to the reset periods. The two branches share one character but retain different hypotheses, so a discontinuous ledger event is not misrepresented as a continuous homotopy.

The algebraic readout is also faithful: despite taking values on the complex exponential curve, it neither aliases two winding sectors nor hides a nonzero net reset behind total phase $1$ under the stated algebraic hypothesis.

This does not establish a particle–wave duality or a quantum-mechanical interpretation. It establishes a precise mathematical analogy: an integer topological label has a complex character representation whose distinct values enjoy a strong arithmetic independence theorem under an algebraic nonresonance condition.

Difficulty

The individual deductions are short only because three difficult interfaces have already been proved. Replacing an arbitrary integer map by actual Circle winding requires using the canonical covering lift rather than postulating labels. Preserving the phase basis requires transporting injectivity and linear independence through a jointly continuous moving-basepoint normalization. The reset branch requires respecting the sign convention and mapping a finite sum to a finite product, including the empty ledger.

Several tempting statements would be false. Duplicate winding labels cannot give a linearly independent family. The exponent $\alpha=0$ collapses every phase to $1$. Continuity of finitely many vertex phases does not by itself define a continuous spatial Circle field, and crossing the principal cut can change a discrete principal-turn winding. A global readout from a simply connected carrier such as all of $SU(2)$ cannot support nonzero loop winding without a separately registered non-simply-connected subcarrier or channel.

For a general complex coupling, exponential resonance can destroy injectivity. The nonzero algebraic hypothesis excludes that resonance here through the proved Lindemann--Weierstrass theorem; it is not merely a convenient side condition.

Formalization scope

All artifacts use Lean 4.30 and Mathlib revision c5ea00351c28e24afc9f0f84379aa41082b1188f. The Circle winding is the floor of the canonical zero-based lift endpoint divided by $2\pi$. Closed fields live on $I\times I$ and are normalized at spatial coordinate zero. The coupling $\alpha$ is an arbitrary complex algebraic number, not necessarily real, and must be nonzero.

The main carrier/readout theorem is conditional on an explicit continuous carrier-valued trajectory, closed spatial slices, and continuous Circle readout. It does not prove existence of a Kuramoto, XY, or Lohe solution, nor preservation of a particular carrier by such an ODE. Those are model-specific successors.

The reset factorization consumes the registered coherent ledger and certified closed cycle. It is an exact algebraic event law, not an energy estimate and not a claim that every physical trajectory realizes such a ledger. Its vertex and edge types retain the universe-zero scope of the existing reset interface.

Selected references

• Yuyang Zhao, The Lindemann–Weierstrass theorem, mathlib4 PR #28013, 2022–2026. https://github.com/leanprover-community/mathlib4/pull/28013
• Nathan Jacobson, Basic Algebra I, 2nd edition, W. H. Freeman, 1985, §4.12, Theorem 4.22.
• Allen Hatcher, Algebraic Topology, Cambridge University Press, 2002, Chapter 1. https://pi.math.cornell.edu/~hatcher/AT/AT.pdf

Motivation

F-theory geometrizes the strongly coupled regime of type IIB string theory by encoding the varying axio-dilaton as the complex structure of an elliptic curve fibered over a base. Non-abelian gauge symmetry is read off from the Kodaira/Tate type of the singular fibres over the discriminant locus, following the fibre--gauge-algebra dictionary of the classification of singular fibres (T. Weigand, TASI Lectures on F-theory, arXiv:1806.01854). The simplest compact example is an elliptically fibered K3 surface, the arena of 8d F-theory and its duality with the heterotic string on $T^2$; there the global discriminant divisor has degree $24$ ("24 seven-branes", equal to the topological Euler characteristic $e(\mathrm{K3}) = 12\,\chi(\mathcal{O}_{\mathrm{K3}})$; the formalized affine statement is $\deg\Delta \le 24$), and an elliptic K3 can contain at most two type II* fibres. A configuration with two such fibres realizes the $E_8 \oplus E_8$ enhancement familiar from eight-dimensional heterotic/F-theory duality.

Setting

Fix a field $k$ and work with the (short) Weierstrass model $y^2 = x^3 + f\,x + g$ whose coefficients are polynomials $f, g \in k[X]$ on the affine base line. Its discriminant is $\Delta = 4f^3 + 27g^2$ (the usual discriminant up to the unit $-16$). For $t_0 \in k$ write $\operatorname{ord}_{t_0}(p)$ for the multiplicity of $t_0$ as a root of $p \in k[X]$, and $\deg p$ for its degree. A base point $t_0$ is an $E_8$ point when $\operatorname{ord}_{t_0}(f) \ge 4$ and $\operatorname{ord}_{t_0}(g) = 5$ (the vanishing orders of a Kodaira type II*). The Calabi--Yau/K3 degree data condition is $\deg f \le 8$, $\deg g \le 12$, and $\Delta \ne 0$.

Formalization targets

Goal

$$\#\{\, t_0 \in k : \operatorname{ord}_{t_0}(f) \ge 4 \text{ and } \operatorname{ord}_{t_0}(g) = 5 \,\} \le 2$$

for $k$ of characteristic zero and $(f,g)$ satisfying the K3 degree data, together with finiteness of that set.

Milestones

1. $\deg\Delta \le 24$ under $\deg f \le 8$, $\deg g \le 12$.
2. $\operatorname{ord}_{t_0}(\Delta) = 10$ at an $E_8$ point (char $0$).
3. $\sum_{t_0 \in S} \operatorname{ord}_{t_0}(\Delta) \le \deg\Delta$ for finite $S$ and $\Delta \ne 0$.

Significance

The count of $E_8$ points controls the maximal non-abelian enhancement of an elliptic K3: two disjoint type II* fibres consume $20$ of the global discriminant budget of $24$ ($2 \times 10 = 20$), leaving at most $4$ units for the remaining singular fibres, and realize $E_8 \oplus E_8$; a third is obstructed ($3 \times 10 = 30 > 24$). This is the F-theory count underlying the two $E_8$ factors of the 8d heterotic string, and a prerequisite for classifying 8d gauge groups. (It bounds the number of $E_8$ factors; it is not by itself the full rank-$16$ statement, which additionally involves the Shioda--Tate/Neron--Severi lattice.)

On the formalization side, Mathlib has a substantial single-curve WeierstrassCurve/EllipticCurve library but no theory of elliptic surfaces or elliptic fibrations: discriminants as sections over a base, vanishing orders, and fibre counting are absent. This mission builds the first fibration-level results directly on top of Mathlib's Polynomial API. The results are established classically (Kodaira; Tate's algorithm; the Euler-number/discriminant-degree identity in M. Schuett and T. Shioda, Elliptic Surfaces, arXiv:0907.0298), so the work here is the machine-checked formalization, not new mathematics.

Difficulty

Two things are worth separating.

The cardinality bound itself is elementary. An $E_8$ point forces $\operatorname{ord}_{t_0}(g) = 5$, so distinct $E_8$ points contribute coprime factors $(X - t_0)^5$ of $g$; then $\deg g \le 12$ already caps their number at two ($3 \times 5 = 15 > 12$). This uses neither the discriminant, nor $f$, nor characteristic zero. The goal is stated in the finiteness-and-cardinality form precisely so it cannot be satisfied vacuously.

The fibration-level content is the milestones, which are the genuine Kodaira/Tate statements and are independently meaningful: that an $E_8$ point contributes exactly $10$ to the discriminant order (milestone 2 -- an order-of-a-sum computation valid because $3\operatorname{ord}(f) \ge 12 > 10 = 2\operatorname{ord}(g)$ and $4, 27$ are units in characteristic zero); the global degree bound $\deg\Delta \le 24$ (milestone 1); and the local-to-global inequality $\sum \operatorname{ord}_{t_0}\Delta \le \deg\Delta$ (milestone 3). These are the load-bearing steps for the stronger statements about $E_8$ points coexisting with other fibres -- e.g. that fixing two $E_8$ points leaves only degree $4$ of discriminant for all remaining singular fibres ($\sum_{t \in S}\operatorname{ord}_t\Delta \le 4$) -- which is the natural next goal and cannot be shortcut through $g$.

Formalization scope

Everything is stated over a characteristic-zero field $k$ (the intended model is $k = \mathbb{C}$) using only Mathlib's Polynomial API: natDegree, rootMultiplicity, roots. The discriminant is $\Delta = 4f^3+27g^2$ (up to the unit $-16$). An $E_8$ point is IsE8Point: $\operatorname{ord}_{t_0}(f) \ge 4$ and $\operatorname{ord}_{t_0}(g) = 5$. The predicate IsK3Data fixes $\deg f \le 8$, $\deg g \le 12$, $\Delta \ne 0$ -- the degree bound characterizing the maximal (K3) elliptic surface and below; it is not a full surface-theoretic K3 hypothesis. To rule out a trivializing reading: the goal asserts finiteness of the $E_8$-point set conjoined with the cardinality bound, so it cannot be satisfied vacuously through the convention that an infinite set has cardinality $0$; and $\Delta \ne 0$ is assumed wherever $\deg\Delta$ is used as a bound.

Convention note. Mathlib's rootMultiplicity is $0$ at the zero polynomial, so IsE8Point implicitly forces $f \ne 0$ and $g \ne 0$; in particular the degenerate $f \equiv 0$ type II* locus (where $\operatorname{ord} f = +\infty \ge 4$ morally holds) is excluded by this encoding. This only shrinks the $E_8$-point set, so it does not affect the bound; a faithful $f \equiv 0$-inclusive definition is a candidate refinement.

Characteristic zero is assumed for uniformity rather than necessity: the degree bound is characteristic-free, and the local order calculation only needs $4, 27 \ne 0$ (characteristic $\ne 2, 3$). Over a non-closed field the count is of $k$-rational affine points; base-change to $\bar{k}$ recovers the geometric statement. The count is taken over the affine chart $\mathbb{A}^1 \subset \mathbb{P}^1$; the literal $\mathbb{P}^1$ statement (adding the fibre at infinity via homogeneous forms) is a natural extension and a welcome future contribution, as are the remaining Kodaira/Tate fibre-order lemmas.

Selected references

• M. Schuett, T. Shioda, Elliptic Surfaces, Advanced Studies in Pure Mathematics 60 (2010), 51--160. https://arxiv.org/abs/0907.0298
• T. Weigand, TASI Lectures on F-theory, arXiv:1806.01854 (2018). https://arxiv.org/abs/1806.01854