A structural claim is worth what it survives. Over the past year this desk has put one result — that the order in which operations act changes the outcome, and that the non-commutativity sits in a locatable place — into four unrelated fields. Each is deposited, each carries a kernel-verified core, and each states in advance what would prove it wrong.
| Domain | Result | Verified | DOI |
|---|---|---|---|
| Catalysis caju to sky · ethanol and cashew feedstock to jet-range fuel | Firing order of four operations sets zeolite selectivity; the gate commutes, the fold’s coupling does not. ~35× ratio in simulation. The Brazilian feedstock case ran in No. 2 | 19 | 21429016 |
| Atmosphere wildfire smoke over New York | A lid commutes with pointwise loss but not with vertical transport. Order-dependence rides the transport operator | 5 | 21431505 |
| Biology RNA switching, NGS, microtubules | Coherence Bridge: two systems sharing $(\mu_{\max},\omega,\kappa^*)$ are categorically equivalent under explicit contact morphisms | core | 20560849 |
| Finance forced selling, AI labour shock | Forced sales are observationally equivalent to panic when liquidity is latent; amplification A = 1/(1−ρ) | 6 | 21561819 |
Thirty theorems across three of those four report #print axioms → [propext, Classical.choice, Quot.sound] and no sorryAx. That is the strongest standard available without trusting anyone: a machine checked them and named exactly what it assumed.
That is the proved part. This issue is about the unproved part — because readers keep asking what it would be worth, and the desk would rather answer with its own arithmetic than let someone else invent a number.
That was not the expected result. It is reported here because it changes what the desk intends to do next, and because a framework that will not publish its own disappointing table has not earned the rest of the page. The accounting is on ; the bench work it points to is on .
Two domain axioms in the paper remain openly unproved. They are named on its own front matter, not in a footnote.
▸
What each domain costs the United States every year, as documented — and the conditional that has to hold before any of it moves.
▸
Why the two nucleic-acid domains are the ones to test, and the three predictions that would kill the framework.
▸
Ten applied AI centres in Brazil, their PIs and grant numbers, reported as journalism.
▸
The inversion. What this desk can do, what it has verified, and how to reach it.
The paper states falsifiable predictions with explicit protocols. It does not demonstrate a saving. The distance between those two sentences is the subject of this issue.
| Domain in the paper | Maps to | US burden / yr | Source |
|---|---|---|---|
| 1 · Riboswitch RNA conformational switching, aminoglycoside resistance |
Antimicrobial resistance | $4.6 bn 2.8 M infections |
CDC with Univ. of Utah School of Medicine; six most urgent resistant threats |
| 2 · Bridge amplification DNA cluster formation, Illumina flow cells |
Next-generation sequencing | $2.9–3.7 bn 2025, US market |
Precedence Research / Towards Healthcare. Revenue, not waste |
| 3 · Microtubule curvature volatile anaesthesia, neuroprotection |
Postoperative delirium | $32.9 bn range $26–42 bn |
National extrapolation from Medicare data, major elective surgery; $44,291 per affected patient / yr |
Roughly nine-tenths of the addressable burden sits in Domain 3 — anaesthesia — and almost none in Domain 2, which is the domain carrying the sharpest prediction.
The sequencing figure is a market, not a loss. It is revenue for work that gets done, and a yield improvement claims a fraction of a fraction of it. Sequencing is where the framework is cheapest to falsify. Anaesthesia is where it would matter. Those are not the same domain, and the desk had assumed they were.
The delirium literature is wider still — up to $150 bn for delirium generally, against $26–42 bn for the postoperative case. This page uses the tightest figure with a stated method, not the largest one available. That choice costs the argument about $117 bn and is made deliberately.
The honest form of the claim is conditional, and the conditional is steep.
Nobody has shown that. This desk has not shown it. What it has shown is that the curvature threshold $\kappa^*$ is the same object in all three systems — so that if $\kappa^*$ governs microtubule behaviour under volatile agents the way it governs cluster formation on a flow cell, the mechanism is addressable.
Which is a different and much smaller word than addressed.
Why publish the ceiling and the floor together: because the alternative is to quote the $32.9 billion, omit the conditional, and let the reader supply the optimism. A framework that will not state its own falsification criteria is not worth the arithmetic.
Domain 1 is an RNA conformational switch. Domain 2 is DNA on a glass surface. Neither requires an operating theatre, an anaesthesia protocol, or a cohort followed for ninety days. Both can be run in a molecular biology laboratory that already exists, on equipment already installed, by people already doing this work for other reasons.
That is the whole reason the Coherence Bridge Theorem is worth having. It is what lets a flow-cell result carry into a domain nobody would fund an outsider to enter directly. Prove $\kappa^*$ in the cheap system; the morphism does the rest — or it fails, and that has been learned too.
P1. $\kappa^*$ for NGS is derivable from DNA persistence length and primer spacing with no free parameters. If the derived value misses the measured critical primer density, P1 is dead. No fitting is permitted.
P2. The curve of cluster quality against primer density has Whitney $A_1$ bifurcation structure, with an asymmetry ratio $\geq 2$. A symmetric curve falsifies it.
P3. That curve is identical — via an explicit contact morphism — to the OFF-blocking dose–response curve of the Domain 1 aminoglycoside riboswitch. This is the bridge itself, stated as an experiment.
P3 is the one worth running. Two curves from two laboratories that have never spoken, predicted to coincide after a stated transformation, is either a result or an obituary.
Two domain axioms remain openopen and are named as such in the deposit. They are not presented as lemmas awaiting tidying. Until they close, the operator chain holds mathematically and the biological mapping is a hypothesis with a protocol attached.
The Lean 4 sources are public. A reader who doubts the core chain can compile it rather than take the desk’s word, which is the only form of trust this journal asks for.
A framework earns the right to speak about the expensive domain by being cheap to kill in the inexpensive one.
FAPESP, the Ministry of Science and Technology and CGI.br fund ten Applied Research Centres in Artificial Intelligence. Each receives BRL 1 million a year for up to ten years, matched by private partners — BRL 20 million per unit per year in total. Between them: 95 principal investigators and 739 researchers.
| Centre | Principal investigator | Institution | Grant |
|---|---|---|---|
| Reference Centre on AI (CEREIA) | José Soares de Andrade Júnior | UFC, Ceará | 20/09706-7 |
| Excellence in Applied AI for Industry | Antônio José da Silva Neto · Davidson Martins Moreira | SENAI CIMATEC, Bahia | 20/09770-7 |
| AI for Evolution of Industries to Standard 4.0 | Jefferson de Oliveira Gomes | IPT, São Paulo | 20/09850-0 |
| AI in the Remaking of Urban Environments (IARA) | André C. P. L. F. de Carvalho | ICMC-USP, São Carlos | 20/09835-1 |
| AI Innovation Centre for Health (CIIA-Health) | Virgilio A. F. Almeida | ICE-UFMG | 20/09866-4 |
| BIOS — Brazilian Institute of Data Science | João Marcos Travassos Romano | FEEC-UNICAMP | 20/09838-0 |
| Excellence in AI for Cybersecurity | Teresa Bernarda Ludermir | CI-UFPE | 22/00741-0 |
| Really Applied AI: Education (PRAIA) | Geber Lisboa Ramalho | CI-UFPE | 22/00688-1 |
| Data Science for Smart Industry (CDII) | José Alberto Cuminato | ICMC-USP, São Carlos | 23/14427-8 |
| Excellence in AI for Renewable Energy | Alvaro L. G. A. Coutinho | COPPE-UFRJ | 22/00720-2 |
Alongside them, C4AI — the Center for Artificial Intelligence, USP with IBM and FAPESP, under Fabio Gagliardi Cozman, at InovaUSP in São Paulo with sites in São Carlos, Ribeirão Preto and Piracicaba. FAPESP and IBM each contribute BRL 2 million a year for five years; USP adds BRL 4 million. Its work spans health, environment, food chains, the future of work, and natural-language processing in Brazilian Portuguese.
Nota. Este panorama é publicado como reportagem, não como candidatura. As bolsas de Treinamento Técnico da FAPESP só podem ser solicitadas como item de orçamento de um Auxílio já concedido — ou seja, através do pesquisador responsável, nunca diretamente. Quem procura bálcão encontra formulário; quem procura laboratório encontra pessoa.
Reported because it is worth reporting. That the names appear here before a letter arrives from this desk is not a coincidence, and is not concealed.
In No. 2 this desk published an independent Lean 4 recompilation of a field-defining disproof — 3,003 of 3,003 jobs passing, zero open sorry, compiled against the kernel from scratch. No part of that result is claimed here. The verification is the point: it can be run by anyone who doubts it, in an afternoon, on their own machine.
In No. 3 the same desk audited its own corpus and found two claims of machine verification that were false, and said so in public, on the front page, with the files named.
Those two facts are the whole application. A curriculum vitae asserts; a compiled kernel does not need to.
Formal verification of results a group already has — the tedious, unglamorous conversion of a proved-on-paper theorem into a machine-checked one. Contact-geometric modelling of threshold and switching behaviour. And the mathematics behind P1–P3 on , for any laboratory with nucleic acids and a reason to look.
github.com/TOTOGT/AXLE — Lean 4 / Mathlib4 sources, open
Zenodo · Principia Orthogona — the full deposit record
Disponível: mãos. Esta banca oferece verificação formal em Lean 4 e modelagem geométrica de limiares a qualquer grupo que precise. Trabalho publicado, código aberto, DOI para cada depósito.
Procura-se um laboratório de ácidos nucleicos disposto a testar P1–P3. Correspondência em português ou inglês, indiferentemente.
The Department of Energy, through ConnectWerx under the Office of Technology Commercialization, is running its first Phase I opportunity under OTC management: approximately 40 awards totalling $10 M, capped at $250,000 per concern ($256,500 with TABA). Applications are pitch-gated — four open-text questions, strict word counts, and only invited pitches proceed to a full application. Up to three pitches per company.
Of the four topics, Topic 1 — Scaling the Biotechnology Revolution names biomolecular design, genotype–phenotype relationships and genome engineering, which is the territory of Domains 1 and 2 on . Topic 4 — AI-Driven Autonomous Laboratories asks for repeatability in experimental workflows, which is what a machine-checked threshold is for.
Portal open date listed only as “mid-August”unspecified as of this issue. R&D must be performed entirely within the United States; ownership and control tests apply at award.
The desk does not ask to be believed. It asks to be compiled.
Each issue, when it goes out. No list bought, harvested, or lifted from a conference roster. Unsubscribe by replying with the word stop.