A formalization has a boundary, and the useful question is never how large the formalized part is. It is which single statement, if it were proved, would move the boundary furthest. In the zeta files at this desk that statement had a name and had been admitted since 30 August. It is now a theorem.
The file is book4/ZetaReflection.lean. It now holds eighteen theorems, every one of them resting on Lean’s three standard axioms — propext, Classical.choice, Quot.sound — and none on sorryAx. The report saying so was written by the gate run and not transcribed.
“Mathlib has nothing on ζ′/ζ” is a sentence one could write from the wrong page, and it would be false. Mathlib has ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div — the von Mangoldt series is −ζ′/ζ for ℜ s > 1 — which lives in LSeries.Dirichlet and not in RiemannZeta. The PNT+ project has more: an entire subsection of bounds, ZetaUpperBnd, ZetaDerivUpperBnd, ZetaInvBnd, LogDerivZetaBnd, LogDerivZetaBndAlt, all formalized.
The gap is narrow, which is the only kind worth naming. The Dirichlet identity holds where the series converges, ℜ s > 1, and says nothing inside the strip. Bounds are inequalities and carry no identity across σ ↦ 1 − σ. The three functional equations are about ζ and not about its logarithmic derivative, and differentiating one is not a rewrite. The missing statement sits exactly where those three stop.
The whole of it is that Λ(1−s) = Λ(s) holds as a function identity, so it can be differentiated. That gives −Λ′(1−s) = Λ′(s), and dividing by Λ(s) = Λ(1−s) turns it into a statement about logarithmic derivatives: they sum to zero. Then Λ = Γℝ·ζ splits that sum into an archimedean part and a ζ part, and the archimedean part is computed directly. The two halves of −½ log π add to the +log π of the gamma-factor defect, and the identity falls out.
One piece is worth separating from the rest, because it is reusable and mentions nothing this desk invented:
That is a statement about Gammaℝ and digamma alone, both of them Mathlib’s, and it is what one needs any time an archimedean factor is differentiated. It is the piece that goes to the library first.
The statement carries four side conditions: s and 1−s off the poles of the two Γ factors, and ζ non-vanishing at both. Without them the identity would assert an equality of junk values at the zeros, and whether it held would depend on where those zeros are — which is the thing nobody knows.
They are also enough, which was not obvious when they were written. At n = 0 the first gives s ≠ 0 and the second gives s ≠ 1 — precisely the two points where ζ and Λ fail to be differentiable. So the differentiability conditions the proof needs were already inside the four as stated, and nothing further had to be assumed. Whoever wrote them picked the right ones.
The file no longer contains an admitted statement. That is a fact about the file and not about the problem, and the paper’s status table now says so in as many words. Every row of that table concerns the coefficients of the arithmetic contact form and how they transform under the functional equation; not one of them bounds anything, and the last row — global positivity, and the Riemann Hypothesis itself — is unchanged. Two rows moved on 8 September, and they moved between kinds, from numerically verified to machine-checked. Nothing moved from open to closed. A reader who takes “no sorryAx anywhere” as movement on the last row has read a taxonomy as a scoreboard.
The log-derivative form of the functional equation is in current Mathlib, as logDeriv_riemannZeta_one_sub. It is not in the v4.32.0 tree this work is pinned to, which is where the search was run, and that is the only claim the search supported. Reported on the Lean Zulip within a day of the claim being made there. The proof on this page is an independent derivation of an existing result; what it establishes is that the statement holds under this toolchain with an axiom report behind it, not that it was first.
On priority the claim is equally narrow. The statement is missing from the library everything here builds on, and from the project nearest to needing it; the PNT+ blueprint was read before this page was set, which is why the paragraphs above name lemmas instead of gesturing at a project. Whether it exists in some third place is not asserted either way, and the value of contributing it does not depend on being first.
Elsewhere in this issue: Page 2 sets out what the library has and has not, line by line. Page 3 reports a field that turns out not to exist, and what was found by checking whether it should. Page 4 is about a table of nine numbers that agreed with a formula published in a journal this desk had not read.
ZetaReflection.lean, and how many trust sorryAx. Every one on propext, Classical.choice, Quot.sound; the control fixture on none at allLSeries.Dirichlet, bounds in PNT+ § 3.4. The reflection is the third, and it is in current Mathlib as logDeriv_riemannZeta_one_sub — see the note at the footWhere a boundary should be drawn. An admitted statement earns its place only if it is stated with the side conditions that make it true, isolated so nothing proves itself through it twice, and small enough that a reader can see what would close it. This one met all three, which is why closing it was four steps and not a programme.
NumberTheory.LSeries.RiemannZeta and cross-checked against the 2025 survey of zeta and L-function formalization. A boundary is only useful when it is printedThe reason to publish a table like this is that a boundary nobody prints gets re-discovered by everyone who approaches it, each at their own cost. Below is what a Lean development can currently reach for, and what it has to prove itself.
| Statement about ζ | in Mathlib |
|---|---|
| Definition, analytic continuation, differentiability | yes |
| Euler product | yes |
| Functional equation, completed form Λ₀(1−s) = Λ₀(s) | yes |
| Functional equation, completed form Λ(1−s) = Λ(s) | yes |
| Functional equation, asymmetric form for ζ | yes |
| Non-vanishing on the closed half-plane ℜ s ≥ 1 | yes |
| Residue at s = 1; special values; Dirichlet series | yes |
| Statement of the Riemann Hypothesis | yes |
logDeriv as a general operation | yes |
−ζ′/ζ as the von Mangoldt Dirichlet series, ℜ s > 1LSeries_vonMangoldt_eq_deriv_riemannZeta_div, in LSeries.Dirichlet — not on the RiemannZeta page | yes |
| Bounds on ζ, ζ′, 1/ζ and ζ′/ζ PNT+ § 3.4 — formalized, and not Mathlib | elsewhere |
| Log-derivative form of the functional equation | no |
| Hadamard factorization | no |
| Zero-free regions beyond ℜ s ≥ 1 | no |
| The explicit formula | no |
Rows marked no should be read as dated rather than permanent — libraries move, and PNT+ is working next door. The row marked elsewhere is why the table has three values and not two: a statement can be formalized, correct, and still not reachable from Mathlib, and a table that hides that difference is the kind that sends somebody off to prove what already exists.
One declaration in the same file does the work that makes the rest mean anything: lseries_vonMangoldt_eq_neg_Zlog, which says that for ℜ s > 1 the von Mangoldt Dirichlet series is −ζ′/ζ. That is what ties the two coefficients of Chapter 12 — the cosine one and the sine one — to the primes rather than to a definition invented to suit them.
The file carries an instruction about it that is worth quoting as a general rule: if that declaration ever shows up in the audit report as resting on sorryAx, the bridge has broken and nothing above it means anything. An audit expectation written into the file, moving in the same edit as the declarations it counts. An expectation that lags the artifact is not a check; it is a second claim to audit.
The Lean docstring records the numerical verification as 30 digits at three interior points. The file’s own header block, forty lines above it, records 30 digits at eight points — and lists them: σ = 0.3, 0.5, 0.8, 1.1, 1.5, 2.3, with t from 0.7 to 25, maximum deviation 8.8×10⁻¹⁶. The status table of the accompanying preprint records seven. Three figures, one measurement, two of them in the same file. Reconciled on 8 September to the eight-point line, which is the only one that carried its inputs; the docstring and the paper now agree with it. Neither is load-bearing — the statement is admitted either way, and numerical agreement is not proof at three points or at seven — but a corpus that lets three figures for one measurement stand in three places has, by that fact, stopped being able to tell which of them came from a run. The eight-point line is the only one that carries its inputs and its residual, which is the reason to believe it and also the reason the other two should not have been written.
Recorded here rather than quietly corrected, because the correction is cheap and the habit that produces the discrepancy is not. The rule this desk works to: print the convention beside the number, or do not print the number.
Between 2024 and the end of 2025, Luis Crespo and Álvaro Pelayo built p-adic symplectic geometry from almost nothing: a p-adic Jaynes–Cummings model, integrable systems and Weierstrass–Williamson theory, Darboux’s theorem, and group actions. Across all of it there is no contact structure, no Reeb field, no Legendrian submanifold, and no odd dimension. The programme is even-dimensional and is carried out that way.
An empty shelf invites two mistakes: assuming it is empty because the objects do not exist, and assuming it is empty because nobody got round to it. Here it is the second. The interesting part is where the arithmetic turns out to live once one looks.
The contact condition α ∧ (dα)n ≠ 0 is an open algebraic condition, so a form that satisfies it over ℚ satisfies it over every completion. No place is excluded. And the Reeb field is a linear solve, which no field cares about: for the prototype form dz − r²dθ it returns ∂/∂z over every ℚp, the same answer the smooth computation gives.
What does not survive is the question one asks next. Over ℝ the Reeb field integrates to a flow and the subject is closed orbits — Weinstein’s conjecture, Taubes’ theorem in dimension three. ℚp has no ℝ acting on it, and a p-adic analytic vector field integrates only on a ball of bounded radius. “Closed Reeb orbit” has no p-adic meaning as stated. That is a gap in a vocabulary, which is weaker than a theorem, and it is reported as the weaker thing.
The natural hope is that a contact structure over ℚp splits into arithmetic classes the way a quadratic form does. Quadratic forms over ℚp genuinely do: the square classes are four for odd p and eight for p= 2, and they separate ⟨1,1⟩ from ⟨1,u⟩. That is why p-adic orthogonal geometry is rich.
Alternating forms carry no such invariant, and the failure is explicit rather than an absence of proof. A contact structure puts a symplectic form up to scale on ker α, so the question is whether the scale is an invariant. It is not: the similitude diag(λ,…,λ,1,…,1) realises every multiplier, and one writes it down. Checked for n = 1, 2, 3 against every square class at p = 2, 3, 5, 7 — sixty cases, all solved.
The arithmetic appears one level up, on the ℤp-lattice model. There dα restricted to ker α is an alternating form over ℤp, and alternating forms over ℤp have elementary divisors — Shimura, 1963. Coordinate changes have unit Jacobian and cannot move them; rescaling α shifts them all together. The coarse shadow is one integer per place, δp(α) = vp(α ∧ (dα)n) mod (n+1).
Run against this desk’s own prototype it returns 1 at p = 2 and 0 at 3, 5, 7, 11. The prototype is ℤp-isomorphic to the standard contact model at every odd place and is not at p = 2. The invariant is not what convinces; the witness is: over ℝ the substitution z′ = z + xy, x′ = 2x standardises the form, and it has determinant 2 — invertible over ℤp for odd p and not over ℤ2.
The 2 comes from writing r²dθ antisymmetrically. There is no hidden content in it, and a form written the other way would return 0. That is a fact about a chart, which is precisely why the number is an invariant of a model and never of a manifold — and saying so is the difference between an invariant and a coincidence with a name.
None of it applies to the adele class space, which is not a p-adic analytic manifold but the non-Hausdorff quotient that motivated the noncommutative treatment in the first place. And it points against the hope it was checked for: if the contact analogue of Crespo and Pelayo’s global classification holds — every second-countable p-adic symplectic manifold is a union of balls determined by volume alone — then there is no tight/overtwisted dichotomy over ℚp, and “the arithmetic contact form is tight” has no content at the finite places. A question answered in the negative is still answered, and it is better than a question left in a form that cannot come back either way.
The n-bonacci characteristic polynomials qn(x) = xn − xn−1 − … − 1 collapse under multiplication by (x − 1) to a single one-parameter family, xn+1 − 2xn + 1, and the 2 in the middle is not chosen — it is what the telescoping leaves. A working note of 23 August recorded that, together with an exact identity: if rn is the root in (1, 2), then 2 − rn = rn−n, not asymptotically but exactly. The note also printed nine discriminants, computed.
Luca, in The Fibonacci Quarterly 62:3 (2024), gives those discriminants in closed form for every k. The formula reproduces all nine entries. The table was computed before the formula was known to the note, so the agreement is a cross-check running in both directions rather than one source restating another — which is the only kind of agreement worth printing.
On the same page of the same journal sits a citation to Martin, The Galois group of xn − xn−1 − … − 1 (2004) — a paper about exactly this family’s Galois group. The August note had a section on that group: rigorous through n = 7 by Jordan’s theorem, and sampling evidence at 8, 9 and 10, with the transposition at n = 8 first appearing at the prime 17,921 after two thousand failed primes.
The status column read “evidence, not proof”. It now reads “not proved here”, and here is doing real work in that sentence. It records what one computation established. It is not a report on the state of knowledge, and it was never entitled to be one.
The note had printed its code and shipped no runnable companion, which fails this desk’s own rule that a published number must be regenerable by a tool. Writing the tool found two faults, both in the tool:
The ladder root was being taken as the last entry of a root-finding call, which does not order its output. For several n that returns a different root, and it made a check pass for the wrong reason: the note’s deliberately flagged near-miss at n = 5, where h = 17.000510 and the whole point is that it is not 17, was being confirmed against a number near 2.13. A check that passes for the wrong reason is worse than one that fails, because nothing draws attention to it. The root is now selected by the property that defines it, 1 < r < 2, and asserted unique.
The second was a perfect-square test calling a library method that does not exist — which at least fails loudly, and is the kind of defect one is glad to have.
Everything above is reproducible: book4/ladder-polynomials-verify.py regenerates the collapse, the exact identity to fifty digits, the Pisot check, the ADE threshold, the single coincidence below n = 40, the discriminants, the Galois orders for n = 2…6, both transposition witnesses, and the cross-check against the closed form.
WP-106 · The Arithmetic Is in the Lattice — contact geometry over ℚp, the subject of Page 3. Novelty is claimed in one section and nowhere else, and “unwritten” is recorded as a literature search rather than a difficulty. Companion script, exact arithmetic, all checks pass.
The Ladder Polynomials — § 7 added, placing the note against Luca (2024) and Martin (2004), with a companion script it should have had in August. Page 4.
The Riemann Hypothesis as Non-Integrability of an Arithmetic Contact Structure — § 4.6 updated: two rows move from numerically verified to machine-checked, a row is added for logDeriv_Gammaℝ, and two paragraphs are added against reading the closure as movement on § 6. Generated from its manuscript by a tool that exits non-zero when the two disagree.
Upstreaming logDeriv_Gammaℝ. Page 1. Proved here against a pinned toolchain, mentions only Gammaℝ and digamma, and is not in Mathlib. The next step is a thread on the Lean Zulip, not a pull request — that order is the community’s, and it is the right one.
Contact Darboux over ℚp. The tool exists — a p-adic Moser method with a strengthened vanishing hypothesis — and the classical proof of contact Darboux should transfer under it. Until it does, the lattice classification of Page 3 covers models and not germs.
The global question. Whether every second-countable p-adic contact manifold is standard. That is the statement that would settle what Page 3 ends on, and it is the one worth the effort.
Print the convention beside the number, or do not print the number. Two figures computed on different denominators can both be correct and still describe a corpus that does not exist.
The gate is the axiom report, not a clean compile. A file that compiles has said nothing about what it rests on.
An instrument must not count its own echo. A file carrying its own audit block gets probed twice by the tool that probes it.
Superseded work is evidence. Retired drafts, wrong turns and replaced files are kept and filed, not discarded. A corpus that deletes its mistakes cannot later say how it learned anything, and the record of how a result was reached is part of the result.
Member of Technical Staff, Axiom Math, Palo Alto, full-time — machine learning and AI for mathematical discovery and reasoning: deep learning, neuro-symbolic methods, automated theorem proving, and pure and applied mathematics. The posting asks for advanced Python and a modern ML framework; large-scale training, reinforcement learning and program synthesis; a foundation in algebra, analysis and combinatorics and in formal proof systems — Lean, Coq, Isabelle; and a record of peer-reviewed publication. It is reproduced nowhere here. It is at axiommath.ai/careers, and the exercise is to read it as a specification and then ask what would count as evidence.
The exercise. Take each line of that specification and try to resolve it at an address. Not a claim that the skill is held — a file, a script, a report, something a stranger can run. This desk has spent eleven issues insisting that is the only kind of evidence that counts, so it would be poor form to exempt itself. Worked, on this corpus, it comes out as follows.
Resolves. Formal proof systems. Lean 4
daily, with an axiom gate rather than a clean compile as the verdict: tools/axiom_gate.py
reads #print axioms and fails on sorryAx or on anything outside
[propext, Classical.choice, Quot.sound], with fixtures including the CI run that once
failed for the right theorem and printed the wrong reason. No. 8 put numbers on the corpus:
2,234 declarations written, 1,984 free of sorry, 173 audited — three different
denominators, printed together rather than reconciled into one flattering figure.
Higher mathematics. This issue: a reflection formula for ζ′/ζ that is not in the
library, sixty similitude cases in exact arithmetic. Elsewhere, with addresses rather than adjectives: the index of the shift computed from actual kernels and cokernels, geometry/book28, and the classification of planar linear systems, geometry/book21, which was used to falsify a claim this desk had itself published on eleven pages.
Reproducible pipelines, experiment design, rigorous analysis. Every chapter carries a
verify script that exits non-zero when the page and the data disagree, and the audit log keeps
the failures with dates on them.
Machine learning and computer science — as the subject, not the method. A rule set
2026-09-01 requires that a paper whose finding is about machine-assisted production carry
#Machine Learning, and three do.
All three are working papers: not peer-reviewed, not deposited — which is the other
box's point and is repeated here so the two cannot be read against each other. What is claimed
is that the work exists and is addressable, not that it has been refereed.
WP-80 · The Theorem and the Reader
takes the comprehension bottleneck as its object: machine-assisted mathematics produces
statements faster than anyone can judge them, with this corpus as the specimen.
WP-81 · The Conviction and the Kernel
reports the failure mode found by auditing many assistant sessions — machine-assisted
mathematics overstates most reliably when the author is right.
WP-91 · A Theorem Twenty-Seven
Characters Long is the worked defect: a registry publishing
collatz_converges with a proved badge
over an axiom that states Collatz, counted twice from two files distinguishable only by case,
neither of which compiles. The artefacts are kept rather than cleaned:
docs/ml-evidence
is a git-tracked archive of superseded copies, on the principle that a finding about production
needs the thing it corrected. The distinction that governs all of it is stated in WP-96:
assistance used is not the test; assistance as the subject is.
Does not resolve. Large-scale training, reinforcement learning, program synthesis at scale — as a method. There is no training run in this corpus, no PyTorch or JAX pipeline, no GPU budget and no learned model of any size. This is about method and not about subject: the corpus's machine-learning and computer-science work is in the box above, where it studies machine-assisted production rather than performing it. An earlier printing of this page omitted that distinction and so reported as absent three papers that exist. A track record of peer-reviewed publication at top AI venues. Preprints and a Zenodo community are not that, and calling them that would be the exact move No. 3 was written to catch. Successors to PatternBoost. Nothing here searches a space for latent structure with a learned proposer; the discovery in this corpus is done by hand and checked by a kernel.
And the reason, stated rather than implied. That second box is not a list of things this desk is uninterested in. It is the aim, and it is the part that is bought rather than written. A proposer that searches a space and a kernel that checks the results are not equally priced: the check costs seconds, and the search costs a budget. At present the models that could stand in for the proposer are metered at a rate that assumes a funded laboratory, and a great deal of what such a search spends its compute on is menial — enumerating, discarding, re-enumerating — work nobody would pay a person to do and which this desk therefore pays for out of pocket or does not do at all. So the discovery here is done by hand and checked by a kernel, which is the affordable half of the method rather than the preferred one. That is a fact about the meter, not about the mathematics, and it is printed here because the alternative is to let a reader infer the wrong reason from a blank.
What the exercise is for. Half a specification met, at an address, is a more useful thing to know than a whole one asserted. A reader who does this with a posting in their own field will find the same shape: the lines that resolve, the lines that do not, and the third category that matters most — the lines they had assumed they met until they went looking for the file. That third category is the reason to run the exercise at all, and it is the same reason every number in this issue carries the script that produced it.
Checked against a source. Mathlib’s declaration list for ζ and the 2025 formalization survey (Page 1–2). The four hypotheses, the definition of the gamma-factor defect, and the one-of-twelve count, read from the Lean file itself. Crespo and Pelayo’s four papers and their publication list (Page 3). Luca’s closed form and its citation of Martin (Page 4).
Computed here. The sixty similitude cases, the elementary-divisor valuations, δp at five primes, and everything on Page 4 — all in exact arithmetic, all reproducible from committed scripts.
Not claimed. That nobody anywhere has formalized any part of ζ′/ζ — Mathlib holds its Dirichlet series and PNT+ § 3.4 holds bounds on it, both named on Pages 1–2. What is claimed missing is the reflection, and only from those two places. That Martin’s theorem says any particular thing — the paper is cited, not summarised. That anything in No. 10 bears on the Riemann Hypothesis. It does not, and no page here says otherwise.
The physician's name was Duval, and he had kept Fermat's confidences for eleven years without once betraying them, which was either a testament to his loyalty or to how carefully Fermat had always calculated what to tell him and what to leave out. This time he told him almost everything, because this time he needed more than silence. He needed a body.
"There is one," Duval said, on the second night, without being asked twice. "A carter. No family left in the parish — his wife took the fever in the spring, his boy the week after. He died an hour ago, in the pest-house on the Bordeaux road, and no one there will come near enough to note the particulars of his face. They haven't come near enough to note anyone's face in a month."
That, Fermat understood, was the entire mechanism. Not deception — deception implied someone was looking closely enough to be deceived. This was simpler and darker than deception. This was the absence of anyone willing to look at all.
The carriage that came for him that night was shuttered on every side, the driver's face wrapped to the eyes, a physician's mark chalked crudely on the door — the universal, terrible symbol that meant do not stop this, do not ask about this, let it pass. Toulouse had learned, over the preceding month, exactly what that mark required of its citizens, which was nothing. No questions. No lingered glances. A door shut quickly, a child pulled back from a window, a whole street's worth of collective, practiced looking-away.
Fermat watched from an upper room as the carter's body — wrapped, weighted at the shoulders in the manner Duval swore was standard practice for a plague death, no different from any of the eleven such bodies that street had already surrendered that month — was carried down and laid inside. He did not know the man's face. He had made a point, in the last hour, of never learning it, on the theory that a stranger's death should not be permitted to feel like anything other than what it was: a terrible, useful accident that he was about to make use of.
"You understand," Duval said quietly, "once this leaves the house, there is no version of events where you are still alive in France. I cannot call it back."
"I am aware of what an irreversible operation looks like, Duval. I have spent my life proving which ones exist."
The carriage did not go to the burial ground outside the city walls, where the recent dead were laid in unmarked ground too fast and too shallow for any grieving family's comfort. It went, instead, the long way, down toward the river and the barge that would carry it to the coast, because Duval — practical in exactly the way eleven years of trust had taught Fermat to expect of him — had arranged for the body to be received not by a gravedigger but by a ship's crew paid to understand only one instruction: a plague death, sealed, to be committed properly to the sea, well clear of any port, in the manner ships had used for a hundred years to keep contagion from following them into harbor.
No grave, then. No stone, no plot that some later, more careful hand might think to open. A death that existed everywhere in report and nowhere in fact — witnessed at a distance by an entire terrified street, verified up close by no one at all, and finally given to an ocean wide enough to keep any question from ever finding an answer.
The carter — whose name Fermat did not know, and would spend a strange, quiet portion of his remaining years wishing he had asked for, so that some prayer might be said for him that used the right word — went into the water not two hundred yards from where, three days later, a commissioned ship would take on a magistrate everyone in France now agreed was dead, standing at the rail beside a boy no one on board had any reason to look at twice.
Duval had arranged it that way on purpose, though he never said so outright, and Fermat only understood the full shape of it once he was standing at that same rail himself, watching La Rochelle's harbor fall away. A death and a departure sharing one port, three days apart, drew less suspicion than two events pulled carefully apart across half of France — the same reasoning, applied once more, that had let a plague-marked carriage pass unquestioned through a street that wanted nothing to do with it. The safest place to hide two things was never far apart. It was in plain sight of each other, where no one thought to compare them at all.
Part 5 of 18 · Fiction, drawn from the documented record; what is invented and what is not is set out in the series’ own note on fact and fiction. © 2026 Pablo Nogueira Grossi · G6 LLC.
Rights notice. Pierre et Mademoiselle is not covered by this issue’s CC BY 4.0 licence. The serial and the work it belongs to — a limited series in development — are © 2026 Pablo Nogueira Grossi / G6 LLC, all rights reserved. No licence to reproduce, adapt, translate or perform it is granted here.
Documented. In May 1653 Fermat caught bubonic plague at Toulouse and survived, weaker afterwards. Bernard Medon, a judicial colleague, wrote to Nicolas Heinsius the Elder announcing his death — then withdrew it in the next letter, reporting that Fermat was alive and no longer feared for, “even though we had counted him among the dead a short time ago.” Europe believed a false report of this man’s death once, on the record, twelve years before he died. That accident is the seed of the premise and it belongs to this instalment and no earlier one. Fermat died at Castres on 12 January 1665. The route the next chapters use — La Rochelle to Tortuga and French Hispaniola, down the Guiana coast toward Cayenne and on to Maranhão — was a working French Atlantic corridor in exactly those years; Bertrand d’Ogeron took up the Tortuga governorship in June 1665.
Invented. The arrangement. The death itself is real and dated; the staging of it is the fiction, and so is everything in this instalment that makes it work — the physician Duval, the carter, the shuttered carriage, the barge, the burial at sea. Duval is not Medon, and the two are never merged: Medon’s report was an accident in 1653 that a second letter undid; Duval is what it looks like when somebody reads that accident as a method. No story of this kind attaches to Fermat’s remains. He was buried at Castres, the family tomb is at the couvent des Augustins in Toulouse, and a bust by François Lucas went into the church choir in 1782.
Each issue, when it goes out. No list bought, harvested, or lifted from a conference roster. Unsubscribe by replying with the word stop.
book4/ladder-polynomials-verify.py — the companion the August note shipped without. Two defects in it found and fixed before it shipped, one of which had a check passing for the wrong reason.