Aether-Lang

What it is

Iterative numerical procedures almost always stop on a scalar. A residual is watched until it falls below a tolerance, and then the loop ends. The rule works, and it has two failure modes that anyone who has trained a model has met. A loss that oscillates in its third decimal forces a patience parameter or a moving average, and both are further hyperparameters. And a scalar compresses the whole state into one number before it thresholds it, so two residual fields with identical norms but different structure look the same to it. A float also wobbles in its last digits for reasons that have nothing to do with the data, and a program that decides with floats cannot tell a real change from rounding.

Aether is the research language I wrote to try a different rule. Persistent homology is built into it. topology.ph computes a persistence diagram exactly over $\mathbb{F}_2$, in homology dimensions 0, 1 and 2, from a Vietoris–Rips filtration or from a lazy witness complex. topology.betti reads the Betti numbers at a radius: the number of pieces, loops and enclosed voids. Those are integers, and the loop keyword seal (also spelled 🦭) can end when they stop changing. The README puts the idea in one line: “A loss that goes from 0.0341 to 0.0339 is noise, but a loop count that falls from 3 to 1 is an event.”

The mathematics sits in a no_std Rust core against libm. The same engine that answers topology.ph in a terminal builds for a Cortex-M3 (thumbv7m-none-eabi) and for bare x86_64, and links into a kernel that owns its own allocator and scheduler. A tree-walking interpreter is the reference implementation; a bytecode VM sits behind it on coverage. Around the persistence engine there is a certified library: a linking number, a top-$k$, an argmin, a threshold and more, each of which returns its answer with the bound that proves it, or a typed refusal.

topological-ml-toolkit is built on top of Aether-Lang.

The premise is narrow, and I want to state it before anything else: some loops should end when the shape of the data stops changing, not when a float becomes small. Whether that beats a well-tuned scalar criterion on real problems has not been measured. The repository calls it “the most important missing number”, and this essay does not supply it.

Here is the mechanism, in the five steps the README uses:

1. A time series is delay-embedded into a cloud of points: each point pairs a sample with the samples a fixed lag behind it.
2. Each point grows a ball. As the radius grows, touching points are joined and triangles fill in. This is the Vietoris–Rips filtration.
3. Features are born and die. Pieces merge; loops appear and are filled. Each lifetime is a bar.
4. The bars alive at a radius give integer Betti numbers.
5. A seal until loop reads those integers as its stopping condition.

The README’s tour program does exactly this to eighteen samples of a sine. The part that matters is four lines:

let r = 0~
🦭 until topology.betti(shape, radius=r)[0] == 1 {
    r = r + 0.25~
}

It prints [one piece at radius, 1, betti, [1, 1, 0]]: at radius 1 the thirteen-point cloud is one piece with one loop. The program never asks whether the signal is periodic. It asks for the shape. The loop is born at radius 0.93 and filled at 2.05, and the seal loop stopped inside that bar. Note what this loop is: it stops on an ordinary Boolean condition over a Betti number, not on stability. The stability form comes later, and it has a weakness the figure below makes visible.

What it can do

Three ways a loop can end

A seal loop has one syntax, seal until expr { body }, and three behaviours depending on what the condition is. The README lists them side by side:

🦭 until n >= 3 { ... }                               // a condition
🦭 until convergence(1e-6) { ... }                    // a tolerance
🦭 until stable(topology.betti(d, radius=r)) { ... }  // an invariant

A plain condition is evaluated before each pass, and the loop stops when it is true. stable(expr) evaluates the watched expression before each pass and stops at the first pass that left it unchanged, by exact structural equality over numbers, Booleans, strings, lists and records. convergence(ε) is the scalar rule, written so it can be compared with the other two. Newton’s iteration for $\sqrt 2$ is the repository’s example:

let x = 1~
let n = 0~
🦭 until convergence(1e-6) {
    n = n + 1~
    x = (x + 2 / x) / 2~
    x~
}
print([n, x])~

It prints [5, 1.414213562373095]. The fourth pass moves $x$ by about $2.1\times10^{-6}$ and the fifth by about $1.6\times10^{-12}$. With $\varepsilon=0$ the loop waits for an exact repeat, which floating point reaches one ulp below the correctly rounded $\sqrt2$. The rule, writing $v_i$ for the body’s value after pass $i$ and $d$ for the max norm, is

The repository is blunt about the middle form: “A tolerance loop is a scalar stopping rule.” Only stable over a topological value is a topological stop. The cleanest example in the tree watches a certified face count of a planar drawing while spokes are added to a square, one per pass (examples/planar_faces.aegis):

let growing = [[[0, 0], [2, 0]], [[2, 0], [2, 2]], [[2, 2], [0, 2]], [[0, 2], [0, 0]], [[0, 0], [1, 1]]]~
let k = 1~
🦭 until stable(euler(growing).faces) {
    if k < 4 {
        growing.push(spokes[k])~
        k = k + 1~
    }
}

The program’s own comment says the face count goes 1, 2, 3, 4, 4, and the loop seals with all four spokes in and four faces.

Proof, or a typed refusal

The second thing the language does is decide things without trusting a float. “A confident wrong answer is worse than no answer.” Every decision in the certified library comes with the bound that proves it, or with a refusal that names its reason. The README’s list of refusals is short enough to quote whole:

linking refused: Intersecting { segment_a: 0, segment_b: 0 }
certify refused: BoundaryUndetermined { .. straddling: [1, 2] }
arrangement refused: EdgesCross { first: 0, second: 1, count: 1 }
persistent homology failed: TooManySimplices { max: 4096 }

“None of these ever becomes a zero, a default, or a best guess.” The persistence engine follows the same discipline: when a filtration would exceed its simplex budget, it refuses before building it rather than truncating it.

A certified top-$k$ is the simplest case. Each score $D_i$ carries a forward error radius $R_i$, built from $\gamma_n = nu/(1-nu)$ with $u$ the unit roundoff, and the code refuses outright when $nu > 0.5$. A set $T$ of $k$ indices is returned only if

and otherwise the answer is BoundaryUndetermined. The tour makes this a stopping rule. It asks whether 1.0 is below 1.5 when the score may be off by a radius, and halves the radius until the answer is proven:

let radius = 2~
🦭 until certified_threshold([1.0], radius, 1.5)[0] == "below" {
    print(["radius", radius, "verdict", certified_threshold([1.0], radius, 1.5)[0]])~
    radius = radius / 2~
}
print(["proven at radius", radius])~

It prints undetermined at radius 2, 1 and 0.5, then [proven at radius, 0.25]. At 0.5 the interval’s upper end is exactly 1.5, which is not strictly below it.

The linking number works the same way, and it is the second program in the tour: a square and a hoop threaded through it.

What the engine has measured

The persistence engine is exact and slow, and the repository measures how slow. This is scale_probe on a regular circle with no radius cap, single core, --release, Windows 11:

Every pair count equals its closed form ($n$, $\binom n2+1$, $\binom n3+n$). Against the simplex count $m$, the local exponent in each of the seven intervals lies between 1.41 and 1.56, so running time is close to $m^{1.5}$ in all three dimensions. These are single runs on one machine with no confidence intervals; the repository says to read them as orders of magnitude. One ratio is robust to that, because it compares identical assertions on the same machine in one session:

Where it went upstream

merged into triton-lang/kernels #22 · 2026-07-28

Add topology-derived sparse attention kernel

3.48× Triton sparse vs dense-CSR at seq 4096 (80.9% block reduction); 1.04× at seq 1024. RTX 4060 Laptop GPU, 50 timing rounds, as stated in the PR.

Aether-Lang led to my triton-lang/kernels#22 kernel.

triton-lang/kernels #22teerth.dev/triton-kernels-22

The repository describes crates/aether-core/src/scheduled.rs as a Rust port of that merged kernel: the same CSR block schedule from sink blocks, a local window and the top-$k$ blocks by an $H_0$ merge height. The port reproduces the schedule and matches dense masked attention to within $10^{-12}$ over four schedules and four block geometries, and its 16-block configuration visits 56 of 136 causal blocks, a 58.8% cut. That cut is cost. Whether the blocks it keeps are the right ones is a different question, and the repository’s answer is no: at sequence length 512 the topological selection captures 5.6% of the achievable gain over random at an equal budget, and with top-$k$ raised to 32 it recovers 0.7446 of the attention mass against random selection’s 0.8643. The upstream timings are the PR’s; the repository does not reproduce them.

How it was made

The object

The filtration is the clique complex of its 1-skeleton, so every simplex is determined by its edges. With no radius cap the number of pairs depends only on the number of points and the top dimension, which gives the engine a closed-form check. The scale_probe example prints the pair count so it can be compared against it; no test asserts it:

Boundaries, ranks and Betti numbers

Over $\mathbb{F}_2$ the boundary of a simplex is the sum of its faces, with no orientation signs. Each $(k-2)$-face of a $k$-simplex arises twice, and $1+1=0$, so a boundary has no boundary. The Betti numbers count the cycles that are not boundaries:

Here $c_k$ is the number of $k$-simplices: $\beta_0$ counts components, $\beta_1$ independent loops, $\beta_2$ enclosed voids. The Euler characteristic $\chi=\sum_k(-1)^k c_k=\sum_k(-1)^k\beta_k$ is a free cross-check.

Persistence as a column reduction

The barcode comes from one matrix. Order the simplices by filtration value, then dimension, then vertex list (faces always first). Put each simplex’s boundary in a column $D_j$. Let $\mathrm{low}(j)$ be the lowest nonzero row of column $j$. Then reduce, left to right:

After reduction $\mathrm{low}$ is injective on the non-zero columns, and the pairing lemma reads the barcode off it: $R_j=0$ exactly when $\sigma_j$ creates a class, and if $\mathrm{low}(j)=i$ then $\sigma_j$ kills the class $\sigma_i$ created, which is the bar $[f(\sigma_i), f(\sigma_j))$.

In the Rust engine (crates/aether-core/src/persistence.rs) the steps are, in order: validate the configuration (dimension at most 2, a radius that is neither NaN nor negative, non-empty input); enforce the point cap before any distance is computed; build the distance matrix; enumerate simplices up to dimension $K+1$ whose diameter is at most the radius cap, with no slack in the comparison; push each one through push_simplex, which returns TooManySimplices instead of truncating; sort with f64::total_cmp; reduce. The reduction is short enough to read whole:

    for j in 0..simplices.len() {
        let mut column = boundary_indices(simplices, &index, j);
        loop {
            let Some(&low) = column.last() else {
                break;
            };
            let Some(owner) = low_owner[low] else {
                break;
            };
            let owner_column: &[usize] = reduced_columns[owner].as_slice();
            column = xor_sorted(&column, owner_column);
        }

        if let Some(&low) = column.last() {
            low_owner[low] = Some(j);
            paired_birth[low] = true;
            let dimension = simplices[low].dimension;
            if dimension <= max_homology_dim {
                pairs.push(PersistencePair {
                    dimension,
                    birth: simplices[low].filtration,
                    death: Some(simplices[j].filtration),
                });
            }
        }
        reduced_columns.push(column);
    }

Unpaired columns of positive simplices become essential classes with death: None. The low-load path replaces Rips with a lazy witness complex: landmarks are chosen by farthest-point selection from the first point, and each candidate simplex takes the value $f_W(\sigma)=\min_{w}\max\bigl(0,\max_{v\in\sigma}d(w,v)-m_w\bigr)$, where $m_w$ is the witness’s distance to its nearest landmark. The code evaluates that on every simplex directly. topology.ph starts from that low-load preset (24 landmarks, 24 points, 4,096 simplices) unless the program overrides it.

Stability

The reason a long bar can be trusted is a theorem, not a property of this code. Cohen-Steiner, Edelsbrunner and Harer proved that $d_B(\mathrm{Dgm} f,\mathrm{Dgm} g)\le\lVert f-g\rVert_\infty$; in the Vietoris–Rips form, if no point moves more than $\varepsilon$ and there is no radius cap, then

The bottleneck distance matches bars one-to-one, or to the diagonal at cost $\tfrac12(d-b)$, and takes the worst match of the best matching. The test that the code obeys the theorem is the one the test file calls its most valuable assertion: a 12-point noisy circle, four seeds, three perturbation sizes, the $H_1$ diagrams compared.

The suite around it includes two negative controls: a Gaussian blob produces no long $H_1$ bars over four seeds, and dense sampling of a circle manufactures no extra loops. The circle’s $H_1$ death matches the closed form $2r\sin(\pi\lceil n/3\rceil/n)$ to $10^{-12}$ for eight values of $n$, and the $H_0$ deaths match an independent union-find minimum spanning tree to $10^{-9}$.

Linking, in closed form

The linking number of two closed curves is an integral that must be an integer:

For two polygons there is no quadrature. Each pair of straight segments contributes the signed area of a spherical quadrilateral, fanned into two triangles, each evaluated by the Van Oosterom–Strackee formula. The module header writes it out:

Omega(a, b, c) = 2 atan2( a . (b x c),  1 + a.b + a.c + b.c )
omega_ij       = -[ Omega(r13^, r14^, r24^) + Omega(r13^, r24^, r23^) ]
Lk             = 1/(4 pi) sum_i sum_j omega_ij

The evaluation returns a value and an error bound $B$ on its rounding. The rounding rule is one line, (self.value - n).abs() + self.error_bound < 0.5, and when it fails the verdict is Undetermined, carrying the estimate and the bound. When it holds with $n=0$ the verdict is ZeroLinking, never “unlinked”.

The linking module, like most of the certified library, is a port from another of my projects: its header names nerve (closed-form linking number and writhe) and tangle (the one-directional LINKED certificate), and says the error bound that licenses rounding appears in neither source and was derived for the port. The certified top-$k$ comes from separatrix, and the coupling operator from sigmoid.

The seal loop in the interpreter

The loop’s semantics live in one function, execute_seal in crates/aether-lang/src/interpreter.rs. The cap is a literal on line 1203, let max_iters = 1000;. After the tolerance branch, the stable and plain-condition branches and the body read:

            if let Some(expr) = watched {
                let now = self.evaluate_expr(expr)?;
                if let Some(prev) = &previous {
                    if integrated::same(prev, &now)? {
                        break;
                    }
                }
                previous = Some(now);
            } else if let Some(condition) = &stmt.until {
                if self.evaluate_condition(condition)? {
                    break;
                }
            }
            match self.execute_stmt_block(&stmt.body)? {
                RuntimeFlow::Value(value) => last_value = value,
                RuntimeFlow::Return(value) => return Ok(value),
                RuntimeFlow::Break => break,
                RuntimeFlow::Continue => continue,
            }
        }
        Ok(last_value)

Three things follow from these lines. The stable rule compares the watched value before a pass with its value before the previous pass, so it accepts the first repeat: a one-pass window. A plain condition must be a Boolean, or the program stops with an error. And when the for loop runs out of its 1,000 passes, the function falls through to Ok(last_value): hitting the cap is not an error.

The Lean tree

The repository has a Lean 4 tree, Aether/, of 11,637 lines on toolchain leanprover/lean4:4.31.0. It holds 48 theorem declarations, 47 in Core.lean and one in VM.lean, and a repo-wide grep finds no sorry. Two facts come first. CI does not build it, so nothing in the repository shows that it still compiles. And it is not connected to the Rust: there is no extraction, refinement proof or correspondence argument between Core.lean and the crates. It is a second implementation of the language in Lean (lexer, parser, static checker, pipeline, VM, with big-step relations and a fuel-bounded executor), exercised mostly by example blocks.

Forty-five of the 48 theorems have one shape. Here is one:

theorem evalExprWithFnsRel_binary_add_sound :
    EvalExprWithFnsRel [] [] (Expr.binary (Expr.num 2) BinOp.add (Expr.num 5)) (Value.num 7) ->
    evalExprWithFns 2 [] [] (Expr.binary (Expr.num 2) BinOp.add (Expr.num 5)) =
      some (Value.num 7) := by
  intro _
  native_decide

The statement reads as soundness: if the big-step relation says 2 + 5 evaluates to 7, the executor agrees. The proof does not use that. intro _ takes the relation hypothesis and discards it, and native_decide then evaluates the right-hand side by compiled computation. What the theorem establishes is the conclusion alone: the fuel-2 executor returns 7 on the single closed program 2 + 5. It does not show that the relation holds for that program, it says nothing about any other program, and native_decide adds Lean’s compiler to the trusted base. All 45 closed instances, including the nine seal-loop ones, begin with intro _. They are checks of specific runs, not general guarantees. The repository’s own account calls them closed instances discharged by native_decide; this essay adds only that the named hypothesis is never used.

The other three are general in their arguments.

theorem lookup_bind_same (env : Env) (name : Ident) (value : Value) :
    Env.lookup (Env.bind env name value) name = some value := by
  unfold Env.bind Env.lookup
  simp

For every environment, name and value, looking up a name just bound returns the bound value. That is a real universally quantified lemma about the Lean environment, proved by unfolding and simplification. It says nothing about the Rust interpreter’s variable table.

theorem eval_bound_var (env : Env) (name : Ident) (value : Value) :
    evalExpr (Env.bind env name value) (Expr.var name) = some value := by
  unfold evalExpr
  exact lookup_bind_same env name value

The Lean evaluator, on a variable that was just bound, returns its value, for all arguments. It covers one expression form of the Lean evaluator and nothing else.

theorem compileCheckedFrameProgram_static_ok
    {stmts : List Stmt}
    {result : SlotEnv × FrameFnEnv × List FrameOp}
    (h : compileCheckedFrameProgram stmts = some result) :
    ∃ checked, Static.checkProgramDetailed stmts = Except.ok checked := by
  unfold compileCheckedFrameProgram at h
  cases hs : Static.checkProgramDetailed stmts with
  | error found =>
      simp [hs] at h
  | ok checked =>
      exact ⟨checked, rfl⟩

For every program, if the checked frame compiler succeeds, the Lean static checker accepted the program. The compiler is defined as a match on the checker’s result, so this is close to its definition, and it is the only general theorem touching the VM. It does not say the compiled frame code is correct, or that the checker rejects anything bad.

There is also a mismatch between the two implementations that matters for seal loops. The Lean semantics decides a loop condition with truthy:

def truthy : Value -> Bool
  | Value.bool b => b
  | Value.num n => n != 0
  | Value.float intPart fracMicros => intPart != 0 || fracMicros != 0
  | Value.str value => value != ""
  | Value.list values => values != []
  | Value.unit => false

and the seal rules use it (truthy value = true -> StepStmt env (Stmt.seal (some condition) body) env (Flow.value Value.unit), Core.lean:770-778). In Lean, seal until 1 { ... } ends at once because 1 is truthy. The Rust interpreter rejects the same condition with condition must be boolean. The Lean seal rule also has no iteration cap, while the Rust loop stops at 1,000 passes. So even if the Lean tree were built and linked, it would describe a different language on these two points.

What’s new in it

The usual way to stop an iterative procedure is a scalar tolerance, and the usual way to make it robust is to add patience. Keras’s EarlyStopping is the standard form: watch one monitored number, ignore changes smaller than min_delta, and stop after patience epochs without improvement. One continuous knob and one integer knob, both on a single compressed number. Aether moves the watched quantity from a float to a vector of integers computed from the data’s shape, and moves the knob from a continuous threshold to a discrete window. The paper is careful about what that buys: “Topological convergence does not remove tuning. It moves it.” An integer window is easier to reason about than a tolerance that interacts with the scale of a loss, and that is the claim, nothing larger. Today the window is one pass.

The usual place for persistent homology is after the fact. A program computes a point cloud, hands it to ripser or GUDHI from a notebook, and a person reads the barcode. The repository’s comparison table marks ripser, GUDHI, giotto-tda and Dionysus as “Topology as control flow: no”, which is a description of what they are for rather than a fault. In Aether the diagram is a value inside the running program, the Betti vector is something a loop condition can read, and the engine that produces it is the same no_std code that builds for a microcontroller and links into a kernel. The README’s phrase for the goal is topology that makes decisions inside a running program, not topology that describes data afterwards in a notebook.

The usual way a program decides “is this score below the threshold” or “are these curves linked” is a float comparison or a rounding. In Aether each such decision is a value that is either a certificate or a typed refusal, and refusals propagate as errors rather than as zeros. The persistence engine takes a budget in the same spirit: “The caps are a budget, not a correctness limit.” A filtration that would exceed its simplex cap is refused before it is built, never truncated.

The last difference is in how the repository treats its own claims. PAPER.md has a negative-results section, “what we got wrong”, that lists withdrawn claims with the numbers that killed them, and a status ledger that marks the Lean tree as ungated rather than counting it. I list those in Limitations below.

What no one else built

Most of what is in Aether exists elsewhere, and better. The parts below are named against the closest prior work I found, with the concrete difference.

Persistence engines. Ripser (Bauer 2021) computes Vietoris–Rips barcodes far faster than this engine, using cohomology, clearing and apparent pairs; the repository says plainly that ripser handles clouds of tens of thousands of points and this engine does not. GUDHI, Dionysus 2, PHAT and giotto-tda are libraries, in C++ with Python bindings or in Python, that return diagrams to a host program. Libraries in other general-purpose languages, such as Haskell’s Persistence and TDA4j, are the same shape. A Chalmers paper implements persistent homology in the array language Futhark, but there the language is the vehicle for the algorithm, not a language with homology in its semantics. Aether’s engine is the textbook reduction and claims nothing over any of these as an engine.

Stopping on topology. This is not new as an idea. Rieck et al. (ICLR 2019) derive an early-stopping criterion for neural network training from neural persistence, a scalar summary of the persistence of the weight graph, used with a patience-style rule. Melodia and Lenz stop an iterative Voronoi interpolation when bottleneck and Wasserstein distances between diagrams cross a heuristic threshold. Both build a topological criterion into one algorithm, and both reduce it to a scalar compared against a threshold.

What is left, and what I claim. In Aether the topological stop is not part of one algorithm. It is a loop form of the language: seal until stable(expr), where expr can be the integer Betti vector produced by the language’s own exact persistence engine, compared by exact equality, with no float in the stopping test. The same loop form takes a certified decision as its condition, as in the tour’s threshold loop, so “stop when this is proven” is also a loop a program can write. And the engine that answers the condition is no_std. In the libraries, papers and languages above I found no loop construct whose termination condition is a Betti vector computed by a built-in persistence engine. That is a statement about my search, not a proof of absence, and the construct’s value is exactly the unmeasured premise in the next section.

Not claimed. The Lean tree is not a contribution of this kind. CompCert and CakeML prove their implementations correct against their semantics; Aether’s Lean tree is not connected to its Rust at all. The certified decisions are ports from my other projects (nerve, tangle, separatrix, sigmoid and others), so they are not new to Aether either. What Aether adds to them is that they are language values with typed refusals that a loop can wait on.

Limitations

The core premise is unmeasured. No controlled experiment compares stopping on Betti stability with stopping on a tuned scalar residual on real problems. The repository lists it first among its open items and calls it the most important missing number. Until it exists, nothing here says topological stopping is better.

No external parity. The engine has not been checked against ripser, GUDHI, giotto-tda or Dionysus on shared fixtures. Every correctness statement in this essay is internal consistency: closed forms, negative controls, the stability bound, mutants.

seal until stable has a one-pass window. Exact equality accepts the first repeat. The repository names this as the standing objection to topological stopping without a window. Figure 1 shows the effect on the tour’s own cloud: with step 0.25 the stable rule stops at radius 0.5 on [9, 0, 0], nine pieces, long before the loop that is the point of the example. That stop is computed by the figure’s port of the engine, not printed by the repository; the window is the repository’s own caveat.

A capped loop does not fail. A seal loop that reaches its 1,000th pass returns its last value with no error. The README says loops are capped; it does not say the cap is silent.

Topology is opt-in, and one predicate is dead. convergence(ε) is a scalar tolerance, ConvergenceCond::BettiStable is declared and never constructed, and the built-in regress statement stops on a sign pattern of its residuals, not on a filtration, with a tolerance of $10^{-6}$ whatever its until: field says. A seal loop is topological only when its author writes a topological condition. The paper’s limits section still says the convergence(ε) spelling fails at runtime (PAPER.md:2141), while its §4.6 says it now runs and is pinned by tests (PAPER.md:1079-1081); one of the two passages is stale.

Scale. $H_0$ at 4,000 points took 335 s and $H_1$ at 300 points 131 s. With every default in place, topology.ph refuses any cloud of 19 or more points, because the full 3-skeleton on $n$ points has more than 4,096 simplices from $n=19$:

The witness complex that topology.ph uses by default is not bounded as an approximation of the Rips diagram of the full cloud; no such bound is implemented or tested.

The kernel is not shown to boot. It compiles for x86_64-unknown-none; there are no QEMU logs, and seven kernel tests never execute.

The Lean tree. It is not built in CI and not linked to the Rust. Forty-five of its 48 theorems are closed instances whose proofs discard the relation they name. Its truthy accepts numbers and strings as loop conditions where the Rust interpreter rejects them, and its seal rule has no cap.

The headline stability test uses its own bottleneck. The 12-case stability check compares diagrams with a bottleneck function defined in the test file. The crate’s diagram::bottleneck_distance is cross-checked only in diagram_distance.rs. The paper describes the invariant check without that detail.

Evidence in the tree is not reproducible from the tree. crates/aether-core/test_results.txt records a failed run (manifold::tests::test_gatekeeper_branching), and output.txt shows a path from an earlier name of the project. No mutation result file is tracked: crates/aether-core/mutants.sh defines a 26-mutant harness, and the paper reports 26 caught in the core and 26 in the GPU crate (the README’s “52 of 52”), but no tally is in the repository. The README’s 428 passing tests are a reported figure; I did not run the suites. The paper gives the Rust line count as 53,228; wc -l over the tracked .rs files under crates/ at this commit gives 53,246 lines in 105 files.

Attention is synthetic, and the topological selection loses to random. All attention results use synthetic keys. Placement, the share of the achievable gain over random that a selector captures at an equal budget,

falls from 38.3% at sequence 128 to 5.6% at 512, and goes to −109% at top-$k$ 32. Block salience measures how isolated a block is, which is anti-correlated with attention mass by construction; selecting the lowest-salience blocks beats random. Every selector also allocates a dense [seq, seq] mask, so memory is quadratic.

Read more

• The project site, with every theorem and algorithm drawn: teerth.dev/Aether-Lang. Short link: teerth.dev/aether-lang.
• The repository: github.com/teerthsharma/Aether-Lang, read at commit 6d8d004.
• README.md: the tour program and the three loop forms.
• PAPER.md: the technical account, with 29 numbered results, the evaluation, “What we got wrong” and the limits.
• The Lean tree, Aether/, and its description in docs/FORMAL_CORE.md.
• The engine, crates/aether-core/src/persistence.rs, and the seal loop, crates/aether-lang/src/interpreter.rs.
• The upstream kernel: triton-lang/kernels#22 (teerth.dev/triton-kernels-22).
• Related essays: topological-ml-toolkit, which is built on Aether-Lang; Epsilon-Hollow; sigmoid, the source of the coupling module.

@misc{sharma2026aether-lang,
  author = {Teerth Sharma},
  title = {Aether-Lang},
  howpublished = {\url{https://teerth.blog/aether-lang}},
  year = {2026},
  note = {CC BY 4.0}
}