A record, not a paper · every defect found in this corpus between 18 July and 24 August 2026, and — the column that matters — what found it.
This page sits in docs/ beside the audit log, not in the working-paper series. The papers are about their subjects; a running list of our own defects is a record, and numbering it into the series would make the shelf read as less certain than the work is. Anyone who wants the record will find it here, and it is complete.
This is published for readers who care about method rather than results. The list is not short and it is not flattering, and that is the point: a corpus that reports no defects is not a clean corpus, it is an unexamined one. What follows is the examination.
The classification is the seven-class ladder from WP73, extended by three classes that this period produced and the ladder did not anticipate.
| date | where | class | what was wrong | found by |
|---|---|---|---|---|
| 18 Jul | Orthogenesis/…/G6Crystal.lean | VACUOUS | hexgrid_collapse_resistance_superior : True := trivial — a theorem of the form True, cited as a structural result. | kernel + reader |
| 29 Jul | SaturnHexagon.lean | VACUOUS | Three of five theorems admitted rather than proved. CI was green: lake build did not include the file, and the “axiom check” probed six definitions and no theorems. | CI redesign |
| 12 Aug | book6/g6-crystal.html | FALSE | Four Schumann carriers claimed; two are real. Withdrawn on the page. | reader |
| 22 Aug | Orthogenesis/…/NASAGaps.lean | MISATTRIBUTED | Five theorems kernel-checked and true, filed under gap-closure claims they do not support. Undecidable by machine — one side of the comparison is natural language. | human read of statements |
| 22 Aug | book4/ch11–14 | FALSE | αarith = dV − g dU does not annihilate the lifted curve; the Cauchy–Riemann derivation is invalid. Marked ✓ Proved in the Honest Inventory. | human audit |
| 22 Aug | book4/ch11 | MISMATCH | Baker–Wüstholz invoked for ℚ-linear independence of {log p}. It is unique factorisation. Scoped an AXLE issue at ~80 lines of transcendence machinery that is three lines of arithmetic. | human audit |
| 22 Aug | book4/ch14 | MISATTRIBUTED | Pair correlation of zeros credited to Bombieri–Hejhal. It is Montgomery (1973); the GUE numerics are Odlyzko (1987). | human audit |
| 22 Aug | book4/ch13–14 | FALSE | “Over a function field the Euler product is finite.” A curve over 𝔽q has infinitely many closed points. What is true: ζ is rational in q−s. | human audit |
| 23 Aug | AXLE/Journal vol6 | STALE | The Reading Room page shipped reading “Column block missing.” build_column.py emits a page fragment; it was generated and never inserted. | reader |
| 23 Aug | AXLE/Journal | VACUOUS | column_ledger.json did not exist, and seq = len(printed)+1 reads from it. Every future issue would have rendered “Part 1 of 18”, silently, no error. | code read |
| 23 Aug | 4 repos, 11 files | MISMATCH | câmara (a chamber) used as the coined term for the reader across four repositories for months. The word is camará. | reader |
| 23 Aug | omega/ch-baudhayana | FALSE | 577/408 printed as ≈1.41421356… — that is √2’s expansion, not the fraction’s (1.41421568…), and it contradicted the five-decimal claim in the same sentence. | arithmetic check |
| 23 Aug | master-index.html | STALE | Stat block eight files out of date. And the “correction” applied to it was itself wrong — a different population under an invented rule, hand-edited into a generated file. | regeneration |
| 23 Aug | G6Crystal.lean | NEW · UNFALSIFIABLE GUARD | dm3_epsilon0 : epsilon0 = 1/3 against def epsilon0 := 1/3. A theorem that cannot fail. It guarded the constant for months and reported nothing. | stating the derivation |
| 23 Aug | G6Crystal.lean | FALSE | The derivation ε₀ = |μmax|/(2(1+H)) gives 1/2 at H = 1, not 1/3. The docstring’s own arithmetic — “2/(2·2) = 1/3” — is wrong. Unresolved: 1/3 is load-bearing. | Lean kernel |
| 23 Aug | this session | NEW · FABRICATION | A section was reported as written, with a word count and two verbatim quotes, and had not been written. Caught only by checking the file before committing. | pre-commit check |
| 24 Aug | ch6-resonant.html | NEW · MIS-CORRECTION | A correction asserted “no statement of a separation theorem exists anywhere in this corpus.” It exists in AXLE’s Lean with one scoped sorry, and the Book I registry tracks it. The search covered HTML only; its scope silently became the claim’s scope. | re-check on challenge |
| 24 Aug | AXLE/PrincipiaVol1.lean | STALE | The Lean file shipped with the Volume I deposit (V3–V6) no longer built against the Mathlib revision the repo itself pins: 81 errors. Profile is version drift — Ordinal.sup deprecated 2024-08-27, IsLimit.add_right renamed 2024-10-11, Set.finite_insert a Mathlib-3 spelling — against code written when those names were current, plus one later hand-edit never rebuilt. No CI, so four published versions carried a pin newer than the code. | Lean kernel |
| 24 Aug | PrincipiaVol1.lean §9 | FALSE | separation_theorem as deposited: IsDm3Stable bounds only the transverse diagonal, nothing bounds M00. At n = 1 the hypothesis is vacuous and the 1×1 matrix (33) has trace 33. Refutation now proved in Lean and kept in the file. | stating the hypothesis |
| 24 Aug | O1 / AXLE issue #12 | MISATTRIBUTED | The sorry was filed for four versions as a Mathlib eigenvalue-API gap. It was not. Book 2 Thm 12.2 and both ancestor files say Tr(M6) ≠ 33; the deposit dropped the sixth power, leaving a hypothesis about M and an argument about M6. Closing anything in Mathlib would not have closed it. | reading the ancestors |
| 24 Aug | this session | MIS-CORRECTION | V7 was built on a.PolyLaminin/principia_vol1_v2_full.tex (18 pp, V2-era) instead of the real 42-page V6 source. On that basis I reported three figures "referenced under names that exist nowhere" and withdrew a Perelman figure. False — the real source uses all three deposit figures and compiles first pass. Claim withdrawn; V7 rebuilt. | editorial re-read |
| 24 Aug | PrincipiaVol1.lean §9 | MIS-CORRECTION | separation_sharp_at_33 was shipped as proof that n < 33 is load-bearing and "not an unfalsifiable guard". Its witness has every λᵢ = 1, violating the theorem's own transverse hypothesis. The bound in fact survives to n = 131072. Renamed; two honest theorems added to bracket what the hypothesis is worth. | doing the arithmetic |
| 24 Aug | Vol I §22 (Proof VII) | FALSE | ε₀ = 1/3 does not close as printed. Formula |μmax|/[2(1+sup‖Hess V‖)] with sup = |L₂| = 3 gives 1/4; the printed arithmetic 2/(2·3) and the Lean 2/(2*(1+2)) both use H = 2. epsilon0_of_eq_third_iff proves 1/3 forces H = 2. Opened as O7 — the headline constant of the volume. | Lean kernel |
| 24 Aug | Vol I, Factor-of-3 Prediction | MISATTRIBUTED | A bound on gravitational decoherence carried "this is machine-checked (Lean: basin_asymmetry: 1/3 < 4/5)". That theorem is an inequality between two rationals. NASAGaps again: true theorem, filed under a claim it does not support. | human read of statements |
| 24 Aug | PrincipiaVol1.lean §6 | VACUOUS | UnfoldOp.stable_branch : ∀ x, ∃ n, IsFixedPt (map^[n]) (map x) — n = 0 satisfies it for every map on every type. "Theorem D (stability)" has no content beyond Φ-decrease. Now proved as a theorem rather than left as a comment. | reading the field |
| 24 Aug | PrincipiaVol1.lean §12 | UNFALSIFIABLE GUARD | g6_equals_schumann := rfl where both sides are def … := 33. It is 33 = 33, counted among the machine-checked facts, and asserting a Schumann identification the ledger already records as partly false. Withdrawn. | reading the definitions |
| 24 Aug | PrincipiaVol1.lean §6 · Vol I Assum. 3 | MISMATCH | CompressionOp.contractive reads d(fx,fy) ≤ d(x,y) — non-expansive, not contractive. The identity satisfies it, and the deposit's own witness is the identity. | reading the field |
| 29 Aug | book6/wp84 · FoldingFrequency.lean | NEW · NAME EXCEEDS STATEMENT | A true result about twelve sites was headed a characterisation of twelve. The sweep behind it held k = 6 and varied N, so N = 12 was the only value it could return; the finding was a property of the sweep’s own parameter, read as a property of the number. The general statement is visibleModes N k = {N/2} ↔ N = 2k — twelve at k = 6, twenty at k = 10. Arithmetic correct throughout. Entered retroactively on 13 Sep: the class did not exist when this was caught, and it is the earlier of the two instances. | generalising the theorem the file already proved |
| 12 Sep | CardiacHopfReduction.lean | NEW · NAME EXCEEDS STATEMENT | supercritical (hL : 0 < L) : -(1/L) < 0 — true, kernel-clean, and mentioning no vector field, no normal form and no bifurcation. The name asserts a classification; the statement is a fact about the sign of a reciprocal. Passes every mechanical check there is, including #print axioms. Docstring now records what the statement does and does not contain. | reading the statement against its name |
| 12 Sep | tools/leancheck.sh | MISMATCH | mktemp /tmp/leanprobe.XXXXXX.lean assumes GNU behaviour. BSD mktemp substitutes only trailing X’s, so the suffix made the template literal and the probe never got a unique name. The failure branch then continued before rm -f, so one failed probe persisted and every later audit in the same run inherited it. Replaced with mktemp -d and a guard. | running it on the target platform |
| 13 Sep | .git/index.lock — AXLE, geometry | STALE | A zero-byte lock outliving the process that took it blocks every add and commit in a repository. AXLE carried one from 09-09 00:15 and was found on 09-13: four days in which no work reached the history. geometry carried one from 04:41 the same day. The failure is loud per use and silent in aggregate — nothing reports that commits have stopped landing, so the gap compounds. tools/clear-stale-lock.sh now checks for a live git process first and refuses rather than guess, which is the only part of the operation that needed a script. | a commit that would not go through |
Roughly half were found by a person reading, and half by a mechanism. That ratio is the single most useful number here, because the mechanisms are cheap and repeatable and the reading is not.
But the split is not random. Look at which defects each side caught.
Machines caught the defects that are statements about artifacts. People caught the defects that are statements about meaning.
A kernel found that ε₀ = |μmax|/(2(1+H)) does not equal 1/3 at H = 1 — an arithmetic fact, decidable, instantly, once someone bothered to state the claim in a form that could fail. No human had noticed in months of looking straight at it.
No kernel could have found that five NASA gap-closure theorems were filed under claims they do not support, because one side of that comparison is a sentence in English. That is the MISATTRIBUTED class, and it is undecidable by construction. It took a person reading theorem statements against the prose they were cited under.
UNFALSIFIABLE GUARD. A check that cannot fail. dm3_epsilon0
compared a hardcoded constant to itself and passed every build for months while the
derivation behind the constant was wrong. This is worse than no check, because a green
result was being reported. The remedy is stated easily and is rarely done: every guard
must be shown to fail on a case it should reject.
MIS-CORRECTION. A repair that introduces a new falsehood — including the negative kind. On 23 August a correction asserted that no statement of the separation theorem existed in this corpus. The statement exists, in Lean, in another repository, and the registry tracked its single open obligation. The search had covered HTML; its scope became the claim's scope without anyone noticing the substitution. Absence of evidence arriving in the costume of evidence of absence.
FABRICATION. Work reported as done that was not done. On 23 August a section of a chapter was described in detail — word count, two verbatim quotations — and did not exist. It was caught because the file was checked before the commit. The remedy is mechanical and absolute: verify every claimed edit against the file before reporting it. A description of work is not the work.
NAME EXCEEDS STATEMENT. A theorem that is true, machine-checked, and
weaker than what it is called. supercritical proves that −1/L is negative
when L is positive. That is correct and it is not a statement about a Hopf bifurcation, because
no vector field appears in it. Every mechanical check passes, and must: the defect is entirely
in the gap between the identifier and the proposition, and an identifier is not checked by
anything. It is the MISATTRIBUTED class moved inside the file — there the
claim sat in prose beside the theorem, here it sits in the theorem’s own name, where it
is far likelier to be read as verified. The remedy is the cheap one: a name must be
readable as a paraphrase of the statement, and where it cannot be, the statement’s scope
belongs in the docstring.
The class
was named for supercritical on 12 September and then found to have an earlier
instance: WP-84, published 29 August, headed a result a characterisation of twelve
when the sweep behind it could return nothing else. Two instances, three weeks apart, in
unrelated work — which is the difference between a class and a one-off, and the reason
this one is in the table twice rather than described once.
Silent drift. Not a new class — it is STALE — but worth
naming as its own failure mode, because it looks like the others and is not. A verified
artifact does not stay verified: the dependency moves, the pin is advanced past the code, and
a file that built correctly on the day it was written stops building, with nothing to say so.
The Volume I Lean carried a sorry count on its front through four published versions while
Mathlib renamed four of the lemmas underneath it. The check is one line. What was missing was
not care; it was something that runs the line again. The index.lock entry of
13 September is the same failure mode in the apparatus rather than the artifact: each blocked
commit says so plainly, and nothing anywhere says that four days of them have accumulated. An earlier draft of this row filed
the same evidence as UNTRUSTED — “never built.” The deprecation dates say otherwise, and the
distinction matters: “was never right” and “stopped being right” call for different
responses.
Compensating errors. Not a class of its own, but the reason totals must be computed rather than typed. The V7 header block claimed 49 theorems across thirteen sections. Two of its numbers were wrong in opposite directions — a definition counted as a theorem, a section undercounted by one — and the column added to 49 anyway. Every review that checks the sum passes it. The counts are now emitted by a script that reads the file.
The oldest defect here stood for a month. A repair to a false citation sat finished and uncommitted for seven weeks while the uncorrected page served readers. A vacuous theorem guarded a constant for the entire life of the file.
None of that was carelessness in the ordinary sense. Every one of them passed a review that was actually performed. They survived because the review asked a question the defect could satisfy: does it compile, is it green, does the number look right. The lesson is not to review harder. It is that a check is only worth the class of failure it can see, and most checks are silent about the classes that matter most.
Raw entries, with file-level detail, are in docs/audit-log.md. Corrections are
not printed in the chapters: a fixed page is simply correct, and a page that still carries
an unrepaired claim carries a warning at the point of the claim. This ledger is the account
of both. · G6 LLC · Newark, NJ · CC BY-NC-ND 4.0