THE MOTTO
“i, the rotation; o, the point it turns about.”
Vol. Ω · No. 17
The Generative Science Journal
Newark, N.J.
Free · CC BY 4.0
← No. 16 · No. 17 →
Imaginary Origin
Saturday, November 14, 2026emblem: $g^{17}$Morning Edition
Duals and the Clock at the Fold
Chapter 10 of Book XXIV builds the dual space and uses it to explain why a quadrature rule is exact. A separate result bounds the time a flow takes to pass a fold, and a numerical check says the bound is close to sharp.

A linear functional takes a vector and returns a number. Given a basis, the functionals that read off one coordinate each form the dual basis, and when the basis changes by a matrix P they are the rows of P−1. Vectors change by P−1, functionals by P, and bilinear forms by PT(·)P. That last rule is why the trace of a form is not meaningful and its signature is. Page 2 lays out the counts and Page 4 the sources and limits.

The chapter's worked use is quadrature. A rule that integrates by evaluating at nodes is a functional written in the dual basis of the evaluation functionals, and its weights are the coordinates. Simpson's weights 1/3, 4/3, 1/3 on the nodes −1, 0, 1 are exact on 1 and t2 and miss t4. The weights 5/9, 8/9, 5/9 on the nodes ±√(3/5) and 0 are exact through t4 and miss t6. Both statements are exact rational arithmetic.

The checks count cases on small grids. They test the statements; the proofs are Lax's. The Lean file for the chapter has not been compiled.

Page 3 turns to the fold-flow files, where a lower bound on the passage time is proved, and the numerical check on how close that bound is to the real time.

The Reading Room, Page 6, carries Part 12 of the serial, set from its source.

The one number to carry

1.006. The measured passage time divided by the proved lower bound is 1.064 at ε = 0.1 and 1.006 at ε = 10−4. The check is floating point, so it shows the bound is nearly sharp and does not prove it. What is proved is the lower bound alone.

This issue
chapters added       1
verifier sections      9
Lean file, compiled    0 of 1
serial part        12 of 18
Lean runs are the author’s
An invitation
A math study group meets online, in the library. Everyone is welcome. Page 5 says how to join.

Chapter 10: book24/ch10-duality.html, with the verifier ch10-verify.py and the Lean file Duality.lean beside it.

Continued on Page 2 · Duality
Imaginary Origin · Vol. Ω No. 17Page 2 · Duality
Counting What Duality Predicts
Book XXIV Chapter 10 · Dual space, bilinear forms, tensor products

The chapter follows Lax, Linear Algebra and Its Applications, Chapter 2. The verifier opens the held copy of that text and checks that the pages it cites say what the chapter says they say. Each statement below was run over a finite family with exact integer or rational arithmetic, and each has a control built to fail, to show the check can tell the right statement from a wrong one.

StatementCases run, and the control
The dual basis is the rows of P−1All 496 invertible 2×2 integer matrices with entries −2 to 2. Control: the columns of P−1 are not a dual basis in general, and the check fails on them.
dim Y + dim Y⊥ = 3, and Y⊥⊥ = YAll 40 distinct subspaces of Q3 spanned by vectors with entries −1, 0, 1 (by dimension 1, 13, 25, 1). Control: the off-by-one claim, that the dimensions add to 4, is false for all 40.
Sylvester's law, 2×2The signature is unchanged by G → PTGP over 62,000 pairs, G symmetric and P invertible, entries −2 to 2. Control: the trace is not a congruence invariant; G = I and P = diag(2, 1) give trace 5, not 2.
Pure tensorsA 2×2 array factors as x ⊗ y exactly when its determinant is 0. Of the 625 arrays with entries −2 to 2, 129 factor and 496 do not.
QuadratureSimpson and the three-node rule above, exact in rational arithmetic, including the powers where each fails.
What the checks changed
WhereWhat changed before the final run
Annihilator controlThe first control, that dim Y⊥ = dim Y, was false for a trivial reason: the ambient dimension is 3, which is odd. It was replaced by the off-by-one control above, which is false for a reason that bears on the theorem.
Exercise 5(ii)A check that could not fail, because of an or True in it, and that carried the wrong label, was replaced by an exhaustive check over the grid.
Limits of the numbers

A finite grid does not prove a theorem for all matrices or all subspaces. The theorems are Lax’s. The counts show that the statements as the chapter writes them hold on every case tried and fail on the controls.

The Sylvester check is for 2×2 forms only. The universal property of the tensor product is described in the chapter and is not checked here.

Continued on Page 3 · The Fold
Imaginary Origin · Vol. Ω No. 17Page 3 · The Fold
A Lower Bound on the Time to Pass a Fold
Fold-flow files · what is proved, what is only measured

The fold-flow file FoldFlowPassage.lean states two results about the time T a trajectory spends passing the fold, for a small parameter ε > 0. The first is a lower bound, T ≥ arctan(√(3/ε)) / √(3ε). The second is a simpler consequence for 0 < ε ≤ 3, T ≥ (π/4) / √(3ε), which grows without bound as ε goes to 0. The simpler form gives up about a factor of 2 against the first as ε becomes small.

ItemState, and its limit
T1, T2 and the invariance resultFull lake build clean on the author’s machine, pushed.
finite_crossingsKernel-checked, pushed.
T3 · passage_time_lower_bound, passage_time_divergesFull lake build completed successfully on the author’s machine on 8 November 2026 (8,767 jobs, no errors), and both theorems depend only on propext, Classical.choice and Quot.sound. That build also reports one sorry, in another file (see Page 5).
T4, the case a < 2Not derived. The hand derivation comes first, then the Lean.
How close is the bound?

The measured passage time was divided by the arctan bound. The ratio is 1.064 at ε = 0.1 and 1.006 at ε = 10−4. The bound is therefore close to sharp at the small end of that range. The integration is floating point, so the ratios are measurements and not certified numbers, and only those two values are reported here.

A lower bound says the passage takes at least this long. It does not say how long, and it does not say the trajectory exists.
Limits of the result

The bound is conditional on a solution of the flow existing on the interval in question; the statement does not construct one. Neither form says the time equals the bound.

No claim is made that this flow models any physical or catalytic system in this issue.

Continued on Page 4 · Sources and How to Read
Imaginary Origin · Vol. Ω No. 17Page 4 · Sources and How to Read
What Was Read, and How to Test It
Sources for the polymathy account, and the instruction that goes with the series

The series' index now carries a short account of where broad learning has paid and where it has not, from Heraclitus's warning that much learning does not teach understanding, through the encyclopedists and the Victorian generalists, to the present. The argument that a shared description helps a specialist by exposing what two systems have in common is the series’ own. No cited source states it.

SourceWhat was read, and its limit
Araki (2025)Section 1.3 only. The rest of the paper was not read.
Cohen (2015), Robinson (2023), the 2024 De Morgan volumeRead for the passages the index cites. The rest of each was not read. Robinson’s observation, that very few Nobel laureates in science have been polymaths, is quoted for what it says and is not tested here.
The manifesto, Generative Contact Mechanics (Institutional Edition)Read, apart from Appendix A, the lexicon, and Appendix C. The term list for a shared language will start from Appendix A, which has not yet been read for that purpose.
Lax, Chapter 2The verifier checks each cited page in the held copy. Printed page = scan page − 17.
How to read the series

Do not take the series on trust; test it. Pick a system you already understand, an oscillator, a business cycle, a clock, a catalyst, and describe it in the series’ shared terms. Where the description holds, you have learned what your system has in common with others. Where it breaks, either the description is wrong or your model of the system was, and finding out which is the learning. The manifesto asks for exactly this: use the language, challenge it, and improve it (Nogueira Grossi, 2025, §5.4). A shared description does not replace what a specialist knows (§5.2); the gap between the two is the exercise. The same test applies to the series’ own claims, which is why Vol. VI publishes audits of them (WP-24, WP-28, WP-29, WP-30).

The manifesto calls itself a language and not a theory of everything (§5.1 to 5.2). This journal reads it that way: a shared form is not a shared invariant until someone derives it.

Continued on Page 5 · Corrections and the Open Desk
Imaginary Origin · Vol. Ω No. 17Page 5 · Corrections and the Open Desk
What Was Withdrawn, and What Is Still Unchecked
Corrections go inside the page, at the section they change, with a date; each open item is named so none can be mistaken for done
Withdrawn or superseded
WhereWhat changed
Ch 10 · verifier control for the annihilator theoremReplaced before the final run: the first control was false only because the dimension 3 is odd.
Ch 10 · Exercise 5(ii) checkReplaced before the final run: the first version could not fail and carried the wrong label.
The open desk
ItemState
book24/Duality.leanWritten this week; not yet compiled. Five of its ten theorems are one-line calls to Mathlib and record the shape of Mathlib’s statement, not a new proof. The others are exact rational arithmetic. The likeliest to need repair is congruence_not_trace. Nothing is claimed for the file until it has been run and its output read. open
Sylvester's law and the tensor universal propertyNot stated in Lean. The Sylvester check covers 2×2 forms on a finite grid. open
A sorry in the full buildThe 8 November build succeeded and reports one declaration that uses sorry, at Orthogenesis/Architecture/MagneticLattice.lean, line 242. It is not among the results reported in this issue, and it was not examined for this issue. The project as a whole is therefore not sorry-free. open
book24/Duality.lean and the buildThe default lake build does not compile the book24 files, so the clean build says nothing about Duality.lean. open
Sharpness of the T3 boundMeasured in floating point for ε between 10−4 and 0.1. Not proved. open
T4, the case a < 2Not derived. open
Appendix A of the manifestoNot yet read for the term list. open
From No. 16: open-set condition for the tent curve, the Hausdorff dimension of the π set, whether mπ can be a whole number, and book5/ExistenceBanach.leanUnchanged by this issue. No new result is reported on any of them; the file was last reported as not compiled. open
An invitation · Math study group

You are invited to join a math study group that meets online, in the library. Everyone is welcome.

To join, or to ask when it meets, write to g6llc@proton.me.

An open item stays on this page until the check it names has been run and the result written beside it.

The Reading Room follows on Page 6.

Continued on Page 6 · The Reading Room
Imaginary Origin · The Reading RoomPage 6
The Reading Room
A Serial in 18 Parts · Part 12
Week of November 14, 2026
The fort, and then the town — the first four days
No. 12 What the Name Was Still Doing There
Pierre et Mademoiselle, by Pablo Nogueira Grossi  ·  See the note on fact & fiction, below

They gave Marie a room with a window, which Fermat understood, correctly, to be the most valuable thing anyone in that fort had to give.

She slept for a day and a half. He sat in the corridor outside it for most of that, upright on a bench built for waiting, refusing three separate invitations to lie down himself, on the grounds — which he offered to no one and would not have been able to defend — that he had watched her slide off a buffalo's back once already and did not intend to be elsewhere the next time something took her without warning.

A garrison surgeon looked at her twice and said, both times, the same word, which Fermat did not know but could translate from the man's face: exhaustion. Not fever. Not the thing everyone in a colonial fort watches for. She had simply run out, five months and a reef and a jungle after she should have, and her body had finally been permitted to say so.

"She will wake hungry," the surgeon said, in slow Portuguese for the foreigner, "and she will be angry about something. That is how you will know."

She woke on the second evening, ate everything within reach, and was extremely angry about the state of her hair.

Fermat, sitting on the floor beside the bed because the chair had been given to someone with a better claim, put his head back against the wall and laughed until his ribs hurt.

It was in that first day and a half, with nothing to do but sit on a bench and be spoken past, that he heard the name and did not, at first, believe it.

He heard it perhaps a dozen times before it registered — from the surgeon, from a corporal, from two women carrying water, from a boy who had been sent to tell him something he could not follow — and each time it went by him as one more unfamiliar sound in a day made entirely of them. São Luís. It was only when a sergeant said it slowly, twice, pointing at the floor to mean here, this place, that Fermat heard what was inside it.

Saint Louis.

He asked. It took most of an afternoon and three people to assemble the answer, in his bad Portuguese and their worse French, and when he had it he sat with it for a long time.

Frenchmen had built this. Not conquered it, not renamed it — built it, from nothing, in the year twelve, and had named the fort for the boy who was then king at home. They had held it three years. In the year fifteen the Portuguese had thrown them out, and had kept the harbour, and the fort, and — for fifty-one years, without apparently finding anything odd in it — the name.

Then the Dutch had come, in the year forty-one, with nineteen ships, and had been thrown out in their turn after three years. And the name had survived that too.

Two occupations, Fermat thought. Two flags taken down. And the thing that stayed was a word.

He was a man who had spent his working life on the question of what survives an operation — what is left invariant when you transform, substitute, reduce. He turned it over on a bench in a corridor eight thousand miles from Toulouse and arrived at something he found genuinely beautiful and did not have anyone to tell.

You can expel the men. The men are the removable part.

The packet had come through the sea because it had been sewn into a coat.

That was the whole of it. Three ships of livestock, thirty years of quiet transactions, the trunk he had nearly drowned trying to lift — all of it at the bottom, and the one object that survived was a folded oilcloth against his chest that he had never once thought of as an asset, because it had been the cover, not the cargo.

He opened it on the third night, alone, and spread it on the floor by the window where Marie was sleeping properly for the first time in half a year.

It was undamaged. The seal was whole. An inspection of French trading interests and remaining colonial claims in the Grão-Pará region, a modest retinue, a modest budget, the minister's own hand at the bottom — a genuine instrument of the French crown, correctly executed, entirely in order.

Made out to a man who had died in Castres in January, and been carried down to the coast in a shuttered carriage with a physician's mark chalked on the door, and put into the sea two hundred yards from where the ship had taken him aboard three days later.

He could present it in the morning. That was the thing he made himself look at squarely, the way he had made himself look at every step of this. He could walk into the governor's rooms and be received — housed, fed, funded, listened to. A letter of credit drawn on the French crown was the only asset he had left in the world, and it existed entirely because a minister at Versailles believed he was alive.

He would be received once.

And then a clerk would enter the name in a book, because that is what a clerk is for. And the book would be copied to Belém, and to Lisbon, and eventually — not quickly, nothing crossed that water quickly, but eventually, in the unhurried and entirely reliable way that paper crosses an ocean — to Paris. Where it would sit in some office, in the same hand, six months after a death notice from Toulouse.

Two entries. One name. Two sides of an ocean.

Duval had understood it better than he had, and had said it plainly at the time without either of them noticing it was the whole doctrine: the safest place to hide two things is in plain sight of each other, where no one thinks to compare them. That worked because a death and a departure three days apart in one port were a single event that nobody had a reason to take apart. Two of the same name, six months and four thousand leagues apart, were not that. They were the other thing.

They were a pattern. And patterns were the one thing his entire life's work had trained him to notice in other men's mistakes.

He folded the commission back into the oilcloth and did not present it in the morning, or ever, and spent a not inconsiderable part of the next twenty years knowing exactly where it was.

So he needed a name, and discovered — sitting on the floor at four in the morning with the only useful document he owned rendered permanently useless by his own reasoning — that he had never made one.

This astonished him. He had solved for the physician, the carter, the barge, the port, the three-day interval, the manifest, the retinue, the cargo, the climate, the season, the plague. He had solved for Agnès in a good cloak on the Nantes road. He had solved for a hold full of animals against the advice of every man he consulted.

He had not solved for what he would be called.

Because — he made himself finish the thought, since he had never in his life permitted himself to abandon a line of reasoning simply because he disliked where it was heading — because some part of him had gone on assuming that the arrangement was temporary. That there would be a version of the future in which the name came back. He had built an irreversible operation and had privately, unexaminedly, declined to believe in it, and it had taken a shipwreck, a jaguar, and a Portuguese sergeant pointing at the floor to make him notice.

In the morning a corporal asked him, with a wax tablet and the particular patience of a man who has asked several times.

He heard himself say: "Pedro."

It was not one of the eleven answers he had ranked off the Canaries. It was simply his own name with the corners taken off — the smallest possible transformation, the least he could bring himself to do, and the corporal wrote it down without any sign of having witnessed a man give up fifty years of correspondence, four countries' worth of reputation, and the only word that had ever meant him.

Later, he would find this funny. Later, he would tell Marie that he had spent forty years proving that certain forms cannot be reduced, and had folded at the first clerk with a tablet.

Marie, from the bed, said: "And me?"

He turned around.

He had solved for a woman leaving Versailles in four days instead of six weeks. He had solved for a clerk who could not bathe with the crew and whose hands were wrong. He had stood outside a cabin door for five months inventing commissioner's business, and had never once, in three years of arithmetic, written down what she would be called on the far side of it.

He did not know, even now, whether that was because he had trusted her to choose it herself — or because some part of him had refused to draft a version of her that was his to draft.

"I don't know," he said. "I never did it. I am sorry."

She thought about it for a moment, in the borrowed room, with her hair in a state she had already described at length.

"Maria," she said. "It's the same. I'd rather not learn to answer to something new."

"That is precisely the reasoning I used, and I called it cowardice."

"You would." She lay back. "It isn't cowardice, Pierre. It's the only thing either of us brought."

He went out into the town on the fourth day, because Marie was asleep again and he could not sit on the bench any longer, and because there was a question he had been carrying since the corridor and could not put down.

A city named for a French king, in Portuguese hands, for fifty-one years.

He wanted to know what else had stayed.

The answer met him at the end of the second street, in the form of a boy of about ten sitting on a low wall with his heels knocking against it, who watched the strange old man come up the road with the frank, unbothered attention of a child who has decided that whatever this is, it is happening in his street and therefore concerns him.

He was Indian. There was nothing in the least European about him — not the face, not the hair, not the way he sat, not one thing about him that would have made a man in Toulouse look twice at anything except the ordinary strangeness of a boy from the other side of the world.

His eyes were blue.

Fermat stopped walking.

The boy said something. It was short, and it went past him entirely, and Fermat — standing in the middle of a road in a Portuguese colony four thousand leagues from anywhere he had ever been a person, with a name he had invented four days ago and had not yet got used to answering to — heard himself say, quietly, to nobody, in the language he had not used aloud in eleven days:

"Qu'est-ce que vous avez dit?"

He did not decide to say it. That was the part he would turn over for the rest of his life. He had been Pedro for four days, and had been careful for fifty years, and the sentence came out of him without passing through anything that could have stopped it, in the accent of the Parlement of Toulouse, on a street where such a sound had no business existing.

The boy stopped knocking his heels against the wall.

Then he leaned forward slightly, the way a child does when an adult has finally said something worth attending to, and repeated himself — patiently, a little louder, in the manner of someone helping out a foreigner who has plainly not been getting much help —

in French.

"C'est à vous, ça?"

Fermat stood there for a long moment. Sixty-four years old, four thousand leagues from home, officially dead, holding nothing, having just broken five months of discipline in a single reflex and received it back from a barefoot boy who had never in his life met a Frenchman.

The vowels were wrong. That was what undid him. They had been somewhere warm for two generations and they had gone soft and long in a way no one in France would have recognised as anything but a mistake — and it was, unmistakably and completely, French, and it was fifty-one years old, and it had been sitting on this street the entire time waiting for somebody to say the first word.

He looked past the boy, up the north road, where a very large grey animal was standing in the shade doing nothing whatsoever.

"Oui," he said. "I believe she is. Though I should tell you it is not at all clear that she agrees."

Note for the margin: São Luís was founded in 1612 by Daniel de La Touche, Sieur de La Ravardière, as the seat of la France Équinoxiale, and named for Louis XIII. The Portuguese expelled the French at the end of 1615, after the fighting at Guaxenduba the year before, and kept the name. The Dutch took the city on 25 November 1641 with nineteen ships and two thousand men, and were driven out in 1644. It is the only Brazilian capital founded by Frenchmen, and nobody has ever found it necessary to call it anything else.

Both occupations left children. Nobody stayed for them.

Part 12 of 18  ·  Fiction, drawn from the documented world; the ledger below says which is which. Set from its source file, as written.

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.

Fact & Fiction · the ledger for No. 12

Documented (series ledger, FACT_AND_FICTION.md): São Luís was founded in 1612 by Daniel de La Touche, Sieur de La Ravardière, as the seat of la France Équinoxiale, and named for Louis XIII. The French were expelled at the end of 1615, after the fighting at Guaxenduba in 1614, and the Portuguese kept the fort, the harbour and the name. The Dutch took the city on 25 November 1641 with nineteen ships and two thousand men and were driven out in 1644. It is the only Brazilian capital founded by Frenchmen. Fermat sat on the Parlement of Toulouse for thirty years and died at Castres on 12 January 1665. The ledger also records a mixed French, Dutch, Portuguese and Tupínambá population as a documented consequence of the occupations.

Invented: the days in the fort, the surgeon and Marie’s waking; the oilcloth packet surviving, and the reasoning that a clerk’s entry would pair his name with the death notice, which is the author’s account of how colonial records travelled and is not sourced; the decision never to present the commission (the ledger’s item 3); the names Pedro and Maria; the boy on the wall and the French he speaks, where the ledger documents a mixed population and not a surviving language. Marie, Duval and Agnès are the ledger’s item 2, and the fifty-one years the name was kept is the joke the ledger lists as ours (item 6). The staging of the death, recalled here, is its item 1, and the buffalo is the relocation recorded for No. 8.

Two distances in the text, “eight thousand miles” and “four thousand leagues”, are given as they stand in the source. Both are larger than the real distance from Toulouse to São Luís.

© 2026 Pablo Nogueira Grossi · G6 LLC · Newark, NJ 07104, USA · g6llc@proton.me · ORCID 0009-0000-6496-2186
Imaginary Origin · The Generative Science Journal · ISSN 3144-6787 (Online) · Vol. Ω No. 17 · Zenodo: Principia Orthogona · Licensed CC BY 4.0, except Pierre et Mademoiselle (The Reading Room), all rights reserved
← No. 16 · Dimensions Between the Integers · No. 17 → · Duals and the Clock at the Fold · Latest issue · the full run is listed on No. 2 · ← AXLE home
The Newsletter · Opt-in

Each issue, when it goes out. No list bought, harvested, or lifted from a conference roster. Unsubscribe by replying with the word stop.

Filed since No. 10 · 26 September 2026
Book 7 · Euler — F−E+V on nine solids and three surfaces; χ by two routes on six spaces; why χ separates none of three Conley indices; the index of this desk’s own field, +1 at every radius, and non-vanishing on both invariant circles. 26 checks.
Book 7 · Conley — no compact isolating neighbourhood contains any of Γ; a rescaling moves the multiplier sixty orders of magnitude and leaves the index fixed. Candidate closed. Block [8] compares the published normal form against the section-3b system: identical through first order, ż̇ = ω on Γ in both.
Book 7 · Smale — entropy exactly zero for the whole closure family, because dP/dr₀ is an exponential of an integral for every f.
Book 7 · Gelfand — dim C*(K,S) = n·p, (Mp)⊕n/p, over all 248 masks for n = 3…7, no violation.
Book 7 · Feigin — H²(Witt) = 1 computed; the −m forced by the Möbius sl₂; dual Coxeter numbers for fifteen types from Cartan matrices alone.
Book 7 · Newton — a definition names a quantity and fixes its measure; e−4π is an accelerative measure and an index is an absolute one.
Book 7 · Whitehead and Russell — sixteen of sixteen binary truth functions from the stroke; Nicod’s single primitive proposition a tautology on all 32 rows.
Book 6 · Nine Pages, No Proofs — Hardy, Ramanujan and the citation whose address will not resolve; the wide-scope rule for writing a retraction.
Book 13 · The Range of a Variable — a type is a range, and a vicious circle is a range containing the quantifier; 57 scripts audited.
docs/rh-criteria-check.py — pre-registered tests of the Lagarias and Robin inequalities, zeros on the line to height 300, and Re(ξ′/ξ) near the zeros; four controls, all fired. Standard library, numpy and mpmath.
tools/corpus_count.py · tools/self_reference.py — entity-aware counting, and the vicious-circle test. Both standard library only.
Book 3 · The Mini-Beast — released 26 September 2026: version 1 PDF, 10.5281/zenodo.22947908; version 2 reviewed pre-release on the web, release spring 2027.
Book 3 · The g-series — one canonical page: teaching labels g⁰, g², g⁶, g³³, g⁶⁴ and levels numbered apart; the fold proved (FoldHysteresis, FoldScaling); two older axioms refuted (GSeries).
Book 3 · Ψ · Latent Capacity — acquired savant syndrome, neurons in a dish, the fly connectome, computronium; a status on every claim.
Book 3 · gate files this week — GSeries, FoldHysteresis, CommitmentThreshold, TubulinChecks, SubcriticalApproach, OcioChecks, EntropyChecks, FoldScaling, ScaleChecks, PolylamininChecks, CollatzChecks, EpilogueChecks, OvertureChecks. Lean 4.32, no sorry, standard axioms only.
Book 24 · Chapter 10, Duality — dual space, annihilators, quadrature, congruence, tensor products; verifier all pass; Duality.lean written, not yet compiled. Added with No. 17.