A type is a range. A vicious circle is a range that contains the thing quantifying over it. Stated that way it becomes a test a script can run, and this corpus has three instances in two days to show for it.
Volume XIII is rung 30 and it is where this corpus's Lean and Mathlib work lives, which is the reason the type theory belongs here rather than in the gallery. ch-whitehead-russell measures the position: “Lean” occurs in 470 tracked files and 405 chapters, and “theory of types” in none. Lean's kernel is a dependent type theory. Types were invented in Principia Mathematica, for one purpose, and that purpose is a problem this repository keeps having.
No object may be defined in terms of a totality that includes itself. The theory of logical types enforces it, and it enforces it by stratifying the range of a variable: a function may not take itself as argument, because its range is of lower type than the function is.
The operative clause is the last one. A statement is not in danger because of the words it uses; it is in danger when the set it quantifies over contains the statement. That distinction is the whole difference between a test that works and one that does not, and it is what the instrument below is built on.
The shape recurred three times in this corpus before it had a name:
| where | the circle | the patch |
|---|---|---|
| ch-van-der-pol block [6] | asserted “van der Pol” appears in no chapter. Publishing the chapter put the phrase into the Book 7 index and two generated index pages, so the count it asserted on included the act of asserting it. | a classify() returning 'self' |
| two verify scripts | shipped a literal control token meant to match nothing. Each file then contained it, so each found the other. | assemble the token at run time |
| WP-82's rung table | counts the paper that prints it — 12 of 12 rows in its second column, 0 of 12 in its first, because the paper is not in the tree at the commit the first column names. | exclude the ruler from the range, at both refs |
Each was fixed by hand, in the file where it appeared, and the class was never named. A hand-written self-exclusion, once per script, is the ramified-type dodge: stratify, and forbid the level from quantifying over itself. Naming it is what lets the dodge be checked rather than remembered.
tools/self_reference.py asks, for every *-verify.py in the
repository, what totality it counts over, and whether the counter is inside it:
It read 1 vicious on its first run, and the row was WP-82.
wp82-verify.py's files() now excludes the ruler at both refs, and
block [2] asserts the stratified and the unstratified column separately so the difference
is printed rather than absorbed. Stratified, rung 28 goes 2 → 17, rung 33 goes
31 → 56, and the inversion narrows to 3.3 : 1.
The eight GUARDED rows are the instructive ones. Every chapter written from
WP-82's gaps this week is corpus-wide, is inside its own range, and carries a stratification
— because each one's count block went red on its own commit and was patched then. The
tool turns eight separate acts of discipline into a property checkable in one command, and
--strict exits 1 on any vicious row, so it can gate CI rather than be remembered.
The range is inferred from string literals and call shapes, not
by running anything. A script that builds its pathspec at run time reads as
NARROW whether or not it is. A pattern assembled from pieces is invisible —
which is precisely the trick that fixes the control-token bug, so a clean report here
is consistent with a script that assembles a bad pattern.
Two findings about the tool's own design are worth printing, because
both are the failure it exists to catch. Testing vocabulary rather than range
over-reports: six scripts contain a word they count while the counted set is Mathlib's tree or
a single .tex file, and none of those is a circle. And resolving a script's page
by its stem alone mis-files book6/wp82-verify.py, whose page is
book6/wp82-the-missing-floor.html — a longer title than the script carries.
The tool reports what it examined, in four labelled buckets, rather than a bare verdict, so a
clean line can be checked instead of believed.
No type hierarchy is constructed here, and nothing about Lean's kernel is verified. The descent from Russell's ramified types through Church's simple types to Martin-Löf and to Lean's dependent type theory is a historical reading, stated to place the instrument, and it is not the subject of a check. What is established is narrower and is the part worth keeping: stated as a condition on ranges rather than on words, the vicious-circle principle is mechanically testable over this repository, and it found a live instance in the corpus's own flagship measurement.
| PM Vol I | A. N. Whitehead and B. Russell, Principia Mathematica, Volume I, 2nd edition, Cambridge University Press. Introduction ch. II, The Theory of Logical Types; ∗12, The Hierarchy of Types and the Axiom of Reducibility. |
| instrument | tools/self_reference.py — standard library only. --strict exits 1 on any VICIOUS row, so this can gate CI. |
| in-corpus | ch-whitehead-russell · ch-newton · WP-82 · ch-van-der-pol · tools/corpus_count.py |