The Axiom You Can’t See

The previous post answered a fair question about a Mathlib-free library that proves things over an opaque Real: are those axioms even consistent? The answer was a soundness witness — Mathlib’s genuine ℝ modelling every MachLib axiom, each #print axioms bottoming out in Lean’s three foundations. It was done by hand, one small file at a time.

By hand is where the real problem starts. A witness written once is a photograph: true the day it was taken, silently stale the day after. Rename a Mathlib lemma, add an axiom in a late-night session, tighten a hypothesis — and the photograph still smiles back at you, witnessing a boundary that has since moved. What a proof deserves is not a photograph but a smoke detector: something wired into the build that goes off, loudly, the moment the trust boundary drifts.

This post is about building that detector. It turned out to have teeth — and the first thing it bit was an axiom that was actually false.

The number was wrong

Before you can guard a boundary you have to know where it is, and here the honest first finding was that we didn’t. The working mental model was “a few dozen interface axioms.” We enumerated them from the kernel instead of from memory — walking the environment, pulling every axiom under the namespace by its canonical name — and the count came back 252.

Not 252 load-bearing assumptions. Of those, 61 appear in the footprint of a shipped headline theorem (what #print axioms actually traverses); the other 193 are declared-but-dormant — scaffolding, alternate formulations, obligations nothing yet stands on. But the gap between “a few dozen” and “252 declared, 61 live” is exactly the gap a trust story cannot afford to guess about. The first job of the ledger is to make that number a fact the build re-derives, not a sentence in a README that was true last quarter.

No grep anywhere in the trust path

The tempting way to check “is this axiom witnessed?” is to search: does a file mention add_comm, is there a lemma whose name looks right. We banned that, on principle, from the entire trust path — and the ban is the whole point.

A name is not a claim. grep finding the string rolle tells you a symbol exists; it tells you nothing about whether the thing that symbol asserts is true. So the boundary is checked two ways, both reading the Lean kernel and never the source text:

That second rule is the one that earns its keep, because it can say no.

The false axiom the detector caught

MachLib’s analytic layer needs Rolle’s theorem. The version it had postulated stated its hypotheses on an open interval — and stated that way, Rolle’s theorem is false.

The counterexample is a one-liner once you look: take f equal to the identity on (0,1) but pinned to 0 at the two endpoints. On the open interval it has equal “boundary” values and a derivative of 1 everywhere — no interior point where f' = 0. The missing hypothesis is the closed-interval continuity that glues the endpoints on; drop it and Rolle collapses. We didn’t just delete the bad axiom, we tombstoned it — a machine-checked proof that the open-interval form is false over ℝ, so it can never quietly return:

theorem not_oldOpenRolle : ¬ OldOpenRolle := by
  -- f = fun x => if x = 0 ∨ x = 1 then 0 else x, then HasDerivAt.unique forces 0 = 1
  ...

Here is the part that matters for the method. A grep-and-name audit would have seen an axiom called rolle, seen that Mathlib has exists_deriv_eq_zero, matched the names, and stamped it witnessed — forever. The typecheck audit did the opposite: it interpreted the axiom’s actual open-interval statement into ℝ, went looking for a Mathlib term that inhabits that type, and found none, because none exists. The check failed exactly where it should. The axiom was retired and replaced with the correct closed-interval form (rolle_ct), which a Mathlib witness does inhabit — and the footprint of every downstream Khovanskii bound was re-checked to rest only on the sound version.

An audit that can only ever say “looks fine” is decoration. This one said no, about something that was really wrong.

Fail loud in both directions

A guard you only test with a synthetic tripwire is a guard you don’t yet trust. Both invariants are diffs, and both drew blood on real drift, not just on canaries:

Each gate ships with a canary that deliberately registers a wrong witness and confirms the gate goes red — so we know the teeth are attached, not just drawn on.

Honest scope

The boundary is enforced, not asserted, and the honest shape of it is:

Fifty-six of sixty-one, and we say which five and why. That sentence is generated from the kernel output, not typed by a human, so the prose cannot drift away from the gate underneath it.

A note from the workshop: the axiom that made me build a library

One of those 61 is an algebraic-dependence fact — the reason an iterated-exponential chain of N-plus-something functions in N variables must satisfy a polynomial relation. To witness it against ℝ I needed transcendence-degree machinery: a finite bound saying an algebraically independent family can’t outnumber a spanning one. At our pinned Mathlib revision, that machinery wasn’t there. So I built it — the exchange lemma (a pleasingly short contrapositive once you swap two coordinates of an independent family), and the piece that turned out to be the real bottleneck: an instance identifying the fraction field of a polynomial subring with the corresponding intermediate field, IsFractionRing ↥(Algebra.adjoin F X) ↥(IntermediateField.adjoin F X). Rings adjoin without inverses; fields adjoin with them; the whole argument stalls until you bridge the two, and that bridge had to be constructed from scratch.

The coda is the honest part. Current Mathlib — newer than the revision we pin — has since grown exactly this: a real transcendence-degree API, the matroid fact that all transcendence bases are equinumerous (which subsumes the finite bound), and an instance, instIsFractionRingSubtypeMemSubalgebraAdjoinAdjoin, that is the fraction-field bridge I wrote. Independent convergence on the same lemma, down to the shape of the hard instance. That’s not a gap we filled — the library’s authors were building it in parallel — but it is a quiet form of validation: two roads, forced by the same obstruction, arriving at the same crossing. The right move now isn’t to submit what Mathlib already has; it’s to say so plainly and let the boundary stand on what’s genuinely ours.

The model post answered are the axioms consistent? once. This one answers and how do you keep knowing? — continuously, from the kernel, failing loud in both directions. The measure of it isn’t the fifty-six green witnesses. It’s the one axiom it turned red, that a lesser check would have called fine forever.

A photograph goes stale. A smoke detector goes off. The trust boundary has the second kind now.

React