The Proof and the Program.

---

The Proof and the Program

Imprint manuscript · July 2026 · Draft v3 after one adversarial round and the standing coverage round (Paper No. 010, Thread II — Money). The referee ran the verification harness, caught it destroying its own evidence, and found a live join failure inside the remediation package — all now inside the paper as its only permissible base-rate datum. Referee report, response letters, and the phase artifacts are filed with the archive; the reproduction harness ships inside the replication package.

· · ·

“Beware of bugs in the above code; I have only proved it correct, not tried it.” — Donald Knuth, memorandum to Peter van Emde Boas, 1977

· · ·

Abstract

A formal economics paper with a computational section contains two artifacts — a theorem, proved analytically, and a program, executed numerically — and makes a claim it never writes down: that they are the same model. The discipline runs two checks on such papers, and neither examines that claim. Proof review evaluates the derivation. Replication, whose reforms over the past two decades have been real and are conceded here in full, evaluates whether the code reproduces the reported exhibits. Each is sound within its scope, and the question that falls between them — does this program implement that theorem? — is asked by no journal policy, no data-editor protocol, and no referee guideline this paper could locate: across the governing policy corpus of the discipline’s major journals, the words theorem, proposition, lemma, corollary, analytical, and closed-form occur exactly zero times, and proof appears only in the sense of page proofs. This paper audits the proof–program join in the one case it can audit without asking the reader’s trust: its own. Paper No. 003 of this archive, a calibrated general-equilibrium model of an equality-indexed monetary and trade system, shipped a stability theorem whose stated property its implementation could never produce, a calibration that violates the condition the theorem requires — an inflation response of 0.5, beside the pre-Volcker estimates the determinacy literature identifies as the indeterminacy-prone regime — a headline equality target unreachable by the model’s own transfer mechanism at any admissible setting, and a results pipeline that never calls the formal core at all. Every per-scenario, per-year results file in that paper regenerates byte-identically from its shipped code — the dynamics reproduce exactly — while two figures in its summary table match no year of the underlying data and cannot be regenerated by any code in the repository; reproduction, where it was demonstrated, establishes stability and not correctness, and the paper claims no more. Its theorems, meanwhile, were doing work its program never did. A commissioned code audit examined the model; its bottom-line verdict — not ready for publication — was correct, as the four findings above confirm; of its three specific blocking findings, one reproduces at an inverted magnitude and two fail re-execution against the preserved pre-remediation code, and three of the four defects it was in a position to find went unnamed, because nothing in its brief pointed at the join. From the case, the paper derives a four-category taxonomy of join failures — unexercised, unreachable, uncalibrated, infeasible — each with a stated detection test, and a seven-item checklist an author can run against their own paper in an afternoon, the first three items without executing any code. What the paper does not do is generalize: one case cannot carry a base rate, the projections are confined to what the instrument would do rather than what the discipline contains, and the claim is correspondingly narrow and dull — there is an unchecked join between proofs and programs, checking it is cheap and mechanical, and its first application here found four things. One further datum belongs in the abstract because it is the paper’s thesis performed on the paper: referee review of this manuscript’s own verification harness found it mutating the package under audit and passing one check vacuously on an empty comparison — two defects of exactly the kind the paper documents, now fixed, disclosed in §5, and covered by the rebuilt harness. The archive binds itself to the instrument prospectively: every future paper here with a computational section ships a completed join audit, because a checklist its author does not run is not an instrument.

· · ·

§ IThe Join

Every paper in this archive tries to name a load-bearing assumption some framework will not state. This one names an assumption of form rather than of content, and the framework that holds it is the research paper itself.

A formal economics paper with a computational section contains two artifacts. The first is an analytical result — a theorem, a proposition, a lemma — with stated hypotheses, a stated property, and a proof. The second is a program: code that produces the paper’s tables, figures, and in-text numbers. The paper presents them together, in shared notation, in a deliberate order — the theorem first, the computation after, the second reading as an instance or an illustration of the first. And in that presentation it makes a claim that appears nowhere in the text: the program is an instance of a world in which the theorem holds. Call this the join claim. It is carried entirely by adjacency; and because it is never written down, no instruction this paper could locate directs anyone to referee it. What individual referees do with computational appendices in practice is unobserved, by this paper as by everyone — the claim here is about the discipline’s written apparatus, not its private diligence, and the distinction is kept throughout.

Here is what is refereed. The proof is reviewed: a referee checks the derivation, and a wrong proof is grounds for rejection. The computation, increasingly, is replicated: from Dewald, Thursby and Anderson’s demonstration that most requested datasets could not reproduce their papers’ results, through the episode that converted policy from voluntary to mandatory — McCullough and Vinod’s attempt to re-verify the nonlinear estimations of a single AER issue, the exchange it provoked, and Bernanke’s 2004 editorial statement making deposit compulsory — the major journals have built a serious verification apparatus: data editors, deposit requirements, pre-publication reproduction of the exhibits. Those reforms worked, this paper depends on their products, and nothing below is an argument against them. One feature of that founding episode belongs to this paper’s story and is developed in §3: what triggered the mandatory policy was a verification method — checks that a reported solution satisfies the mathematical conditions defining it — and what the policy institutionalized was the replication half alone. But the two checks have exactly the scopes their names suggest. Proof review never sees the code. Replication runs the code and compares its output against the published tables — in the words of the standard that governs the American Economic Association’s journals, the deposit must “reproduce all the computational exhibits,” and the exhibits are the tables, the figures, the in-text numbers. The join claim is about neither the derivation nor the exhibits. It is about the relation between them, and it falls between the two instruments by construction.

The demonstration that nothing spans the gap can be made mechanically, and the mechanical form is the right one, because any reader can repeat it in an afternoon. Take fourteen documents: the AEA Data and Code Availability Policy and its accompanying Data Editor protocol, the Data and Code Availability Standard, the Social Science Data Editors’ template, the data editors’ internal replication-report template, and the corresponding policies of Econometrica, the Journal of Political Economy, the Review of Economic Studies, the Quarterly Journal of Economics, and the Economic Journal. Search that corpus for the words theorem, proposition, lemma, corollary, analytical, closed-form. The count is zero. The word proof occurs once — as the plural token proofs, in the replication template, meaning page proofs (“when returning proofs…”); the singular never appears. Two honesties about what this shows, stated before it is used. First, these are mostly deposit-and-verification policies, and the zero-count partly reflects their scope — which is this paper’s point made from the other side: the documents that do verify code are scoped so that the join is outside them, and no other document picks it up. Second, the count is evidence about the discipline’s written apparatus, not about referee practice, of which only three public guidelines could be examined at all. Every verification standard in the corpus defines success as outputs match reported outputs; none defines it as code instantiates stated results; and the claim is stated at exactly that grade — we found no policy, protocol, template, or referee instruction that asks the question, with the scope enumerated and with the corpus texts to be snapshotted alongside the paper at imprint, since policies revise and the count decays. §3 resizes the claim against the three literatures that come closest.

The claim of this paper, stated so it can be wrong. The proof–program join is a distinct failure surface, invisible to both of the discipline’s existing checks because each is correctly scoped to something else. In the one case examined here in full — the author’s own — the join had failed in four ways at once: a theorem whose stated property the implementation could never produce; a calibration violating the condition the theorem requires; a policy target unreachable at any tested level of the most favorable reconstruction of the model’s own mechanism; and a verification core that the results-producing code never calls. All four survived the paper’s writing, its review, its publication with a replication package, and a commissioned code audit — whose bottom-line verdict was correct, whose itemized findings mostly failed re-execution against the preserved snapshot, and whose brief did not point at the join. Auditing the join is cheap, mechanical, and its application here found four things — then found two more in the audit instrument itself. Three observations would disconfirm the paper’s contribution, collected in §9: an existing policy or practice that already asks the question; a forensic finding that fails to reproduce from the shipped package; a join failure that fits none of the four categories.

A word on method, because in this paper the method carries an unusual burden. Every non-trivial sentence belongs to one of three registers: what is claimed — conceptual, cited; what was found — forensic, each claim carrying the file, the function, and the command that produces it, reproducible by a reader with a terminal; what can be expected — projections, few, and confined to the instrument rather than the population. Three rules govern the whole, and they exist because of what kind of paper this is. The no-generalization rule: this paper has one case and may not claim a frequency, a prevalence, or a discipline-wide diagnosis — sentences of the form “economics routinely…” are forbidden however strongly the author suspects them. The no-exculpation rule: the case is the author’s own model, and every finding is stated at the strength it would carry if the model were someone else’s. And the no-heroism rule, its mirror: self-audit is not a virtue display, the confessional register is banned throughout, and the paper does not offer its own candor as a reason to believe it. The three rules are not ornaments. The first is what lets a one-case paper say anything; the second and third are what let a self-audit say anything about itself.

§ IITwo Caricatures to Clear

Two pictures dominate any conversation about code and formal results, and each must be cleared before the argument can run — in the house manner, by concession first.

The first is the replication optimist: the code is public, the pipeline runs, the tables reproduce — the problem this paper gestures at was solved by the reforms of the last two decades, and what remains is mopping up. The concession is real and larger than politeness requires. The reforms worked: deposit rates went from scandalous to near-universal at the major journals, data editors reproduce exhibits before publication, and the case at the center of this paper is itself a beneficiary — every forensic claim below is checkable precisely because a replication package ships with the model. If this paper’s claim were that economics has a reproducibility problem, the optimist would win, and the paper concedes something sharper: in the case examined here, reproduction is perfect. All five per-scenario results files regenerate byte-identically from the shipped code. And that is the turn: reproducing a number establishes that the program is stable, not that it is the theorem’s program. The case reproduces exactly and fails the join four ways. Whatever the join check is, replication is not it — not because replication is weak, but because it is aimed elsewhere.

The second is the formalist: the theorem is proved, the proof is the contribution, and the code is a convenience — if the two disagree, so much the worse for the code. The concession, again, is real: a proof does not become false because an implementation is defective, and nothing in this paper impeaches any derivation. But the formalist position has a consequence its holders do not accept in practice. If the code is only a convenience, then the paper may not present the code’s output as evidence bearing on the theorem — no scenario table as illustration of the stability result, no counterfactual as demonstration that the constrained optimum is attainable. And papers invariably do exactly this; the join claim is the formalist’s own claim, made silently, every time the computation appears in the same paper as the theorem. One cannot both disown the program and cite its output. The formalist who accepts that discipline — theorems here, simulations there, no implied relation — has no quarrel with this paper and also, §5 will show, no description of the paper this paper examines.

What the two caricatures share is a division of labor so clean that the join belongs to nobody: the optimist assigns correctness to the replication apparatus, the formalist assigns it to the proof, and the relation between program and proof is each one’s picture of the other’s job. Clearing them is the first statement of the thesis.

§ IIIWhat the Discipline Already Checks

A paper claiming that a question goes unasked owes the reader a map of everyone who almost asks it. This section is that map, and it resizes the novelty claim before any referee has to — the question is owned in one literature, asked in one subfield, and approximated in one modeling tradition, and the paper’s claim survives all three at a precise and narrower size.

The question is owned, under the name code verification, by the verification-and-validation literature of computational science. The ASME’s V&V standards define a chain from conceptual model to mathematical model to computational model, and define code verification as establishing that the implementation and its solution algorithms are correct — canonically, by comparing code output against analytical solutions. Sargent’s formulation in the simulation literature is the cleanest: computerized model verification is “assuring that the computer programming and implementation of the conceptual model are correct”; Schwer’s slogan divides the labor — “verification is the domain of mathematics and validation is the domain of physics.”

And economics has a native verification tradition of its own — two, in fact — which the first draft of this section under-counted and its coverage referee restored. The first is the numerical-reliability lineage: McCullough and Vinod benchmarked econometric software against certified reference values in the Journal of Economic Literature, then, in the American Economic Review, proposed a four-step method for verifying that any reported nonlinear solution satisfies the mathematical conditions defining it — gradient at zero, convergence path, Hessian conditioning, likelihood profile — and applied it to a published issue. The exchange that followed even contains this paper’s harness motif in miniature: the audited authors showed the verification method itself mis-fired on unscaled problems, and the method was revised. That episode triggered Bernanke’s mandatory data-and-code policy — which is the origin of the very corpus §1 keyword-counts, and the sharpest single fact in this paper’s background: the discipline held the verification half in its hands in 2003 and institutionalized only the replication half. The lineage continues in empirical industrial organization, where loose solver tolerances and false convergence have been shown to move published estimates by large factors. The second native tradition is the accuracy-verification literature of computational macroeconomics — den Haan and Marcet’s simulation accuracy tests, Santos’s Euler-residual bounds that provably control policy-function error, Kubler and Schmedders on how far an “approximate equilibrium” can sit from any exact one — a theorem-grade literature, in the discipline’s best journals, on the relation between computed output and the model’s true solution. Both traditions verify something real, and neither verifies the join: the reliability lineage checks that a solution satisfies its estimator’s defining conditions, the accuracy literature checks distance to the model’s exact solution — each presupposes that the coded model is the paper’s model, which is the question. The clearest import of the V&V apparatus by name sits in the Journal of Political Economy — Cai and Lontzek’s social-cost-of-carbon model, with a section titled “A Verification Test” — required by no one, benchmarked against a numerical special case rather than a theorem proved in the paper; and in agent-based economics the proposals exist and describe their own status: verification methods for economic simulation “are not used in standard economic research.”

The question is, for one property, automated — and governed by nobody, and this is the objection the first draft left itself exposed to. The dominant DSGE toolchain machine-checks a determinacy condition at every execution: Dynare’s solver enforces the Blanchard–Kahn conditions as a precondition and refuses to simulate a model that fails them, its check command reports the eigenvalue count, and its sensitivity toolbox automates a parameter-space sweep for the stability-and-determinacy region — very nearly this paper’s Checks 2 and 5, run by default, for that one property, in thousands of papers. Stated at full strength, the objection is that the join is already checked wherever DSGE papers are written. Three facts answer it, and this paper’s own case supplies the decisive one. The toolchain verifies a property of the program alone — that the coded system has a unique stable solution — and cannot see the paper’s theorem: No. 003's mis-implemented model, whose backward-looking structure declares no forward-looking variables, passes the Blanchard–Kahn test trivially while the theorem it was meant to instantiate claims saddle-path stability of a different system. The toolchain would have blessed the unreachable join. Second, the check is one generic property, not the paper’s stated hypotheses. Third, it is infrastructure, not governance: no journal requires the tool, none requires reporting its verdict — the coverage sweep confirmed no determinacy-reporting requirement in any macro journal’s guidelines — and a paper that hand-rolls its solver, as No. 003 did, exits the guardrail entirely. Which is the precise shape of the gap: the papers outside the toolchain are exactly the papers the checklist is for.

The question is asked — with checklists, task-force endorsement, and journal uptake — in health economics. The TECH-VER checklist opens from the observation that model-credibility guidance in that field “always declare[s] verification of the programmed model as a fundamental step, such as 'is the model implemented correctly and does the implementation accurately represent the conceptual model?'” — and its stress tests include comparing pen-and-paper analytic results against the model in simplified cases. This is the nearest thing in economics to the instrument §10 proposes, and the paper cites it before any referee raises it. It does not reach this paper’s question for a structural reason: the models it verifies are decision trees and Markov structures, and the “conceptual model” they are checked against is a specified narrative, not a proved result with hypotheses a calibration could satisfy or violate. Health economics verifies implementations of models that contain no theorems. That the machinery exists there is the best available evidence that it is buildable wherever a field decides implementation errors matter; that it stops short of theorems is why the join remains open.

The question is approximated, generically, in CGE practice. Dixon and Rimmer’s validation chapter describes homogeneity testing — shock every nominal exogenous variable by ten percent and verify that nominal endogenous variables move ten percent and real ones not at all — which is a theory-implied property checked against code, and thus a true join check in miniature. But the property is generic Walrasian homogeneity, used as a debugging heuristic; it is nobody’s Proposition 2. Benchmark replication, the other CGE staple, is weaker than it looks: solving with zero iterations to confirm the calibrated SAM is an equilibrium of the coded system is a data-consistency check, and a model coded with the wrong production function will pass it if calibrated to the same SAM.

The question is, at its maximal cost, solved — inside economics’ own journal system, for a handful of theorems. The mechanized-reasoning program has machine-verified Vickrey’s theorem in the Journal of Mathematical Economics and, in its strongest form, generated executable auction code from a machine-checked proof — proof and program one artifact, the join discharged by construction. That endpoint exists, no applied paper pays its cost, and §11's checklist is priced as the cheap point on the cost curve whose expensive end this literature already built. The general-purpose tooling between the two endpoints also exists, in software engineering: property-based testing generates inputs against stated invariants, and metamorphic testing checks theory-implied relations between runs precisely where no oracle knows the true output — the instrument class this paper’s Checks 4 and 5 hand-roll. And the discipline’s remaining verification infrastructure is uniformly output-scoped, confirmed at the source: the cascad certification agency attests that running the code reproduces the reported results and states that its certificate “covers the code and data, not the scientific conclusions”; the TIER protocol specifies reproduction documentation; the Journal of Applied Econometrics replication section and its successors publish replications of empirical results, with no theorem–code-mismatch category located in any of them. The adjacent-error record runs the same way: the two canonical cases of code not implementing a stated specification — Foote and Goetz’s reconstruction of the abortion-crime regressions, and Herndon, Ash and Pollin’s re-execution of the Reinhart–Rogoff spreadsheet, where the method as stated was not the method as computed and the corrected number changed sign — were both found by outside replication, neither involved a theorem, and one recent experiment adds the detail that matters most for the join: coding errors are substantially more likely to be caught when they produce an unexpected result, which is exactly why a join failure that flatters the theorem survives review.

One completion of the map, briefly, because it closes Schwer’s split in economics’ own terms. The discipline built the validation half — Fair’s tradition of testing macroeconometric models against data, the model-evaluation literature, the calibration debate — and it built the output-reproduction half, twice over. The verification half, program against the paper’s own analytical results, is the cell that remained empty; this section’s map now has seven traditions standing around it. And the discipline’s referee guidance, where it exists at all, is eloquent by omission: the most detailed public guide, for a journal whose core output is computational macroeconomics, runs to some twelve thousand characters, partitions papers into theoretical and empirical with a checklist for each, and contains not one occurrence of code, program, computation, simulation, numerical, calibration, or replication. Theory review reaches “erroneous mathematical derivations.” Empirical review reaches “a loose link between the economic model and the empirics.” A paper that is both has no cell — which is not a criticism of the guide but a description of the taxonomy the discipline reviews with.

The resized claim, then, stated once and defended in §9: not that nobody asks whether code implements theory — computational science owns the general question; economics’ own reliability and accuracy lineages verify solutions against their defining conditions; health economics operationalized the check for theorem-free models; CGE practice gestures at it with generic properties; the DSGE toolchain automates it for one property at nobody’s requirement; and mechanized economics has solved it outright for a handful of theorems at a cost no applied paper pays — but that no economics journal requires, no data editor checks, and no referee guideline mentions whether a paper’s code exercises the paper’s own analytical results. Seven traditions stand around the empty cell, which is precisely how a seam persists: everyone adjacent to it can reasonably believe it is someone else’s. The universal negative survived this paper’s own coverage referee at its exact letter, and it is stronger for the company — the discipline that held the verification half in its hands in 2003, and mandated the replication half in 2004, did not decline the join check; it never noticed the join was a place.

§ IVThe Case, I: What Was Built

The case must first be stated as its author intended it, without foreshadowing, because the argument requires the reader to see a competent artifact before seeing what is wrong with it. Nothing in this section is concessive. It is a description of a paper this archive published and, per the disposition recorded below, leaves standing.

Paper No. 003 of this archive, The Equality-Indexed Monetary-Trade System, proposes a monetary and trade architecture in which the instruments of international economic coordination are indexed to equality rather than to market-clearing alone. Its formal core is a small dynamic system: an equality-augmented Taylor rule, in which the policy rate responds to inflation, the output gap, and a national equality gap; an equality-indexed money supply; an equality-adjusted gravity model of bilateral trade; a fair-exchange-rate corridor; and a general-equilibrium formulation with a binding equality constraint. Two analytical results anchor it. Theorem 5.1 asserts dynamic stability — saddle-path stability of the linearized three-variable system in inflation, output, and inequality — for equality-response coefficients below a bound γ̄. Theorem 5.3 characterizes the constrained optimum: prices, quantities, and transfers satisfying market clearing and a global inequality ceiling, the constraint binding at the optimum.

The computational side is a calibrated eight-nation model — the United States, China, Germany, India, Brazil, Nigeria, Sweden, South Africa — with parameters drawn from standard sources (national accounts, SWIID inequality series, WID distributional data, Penn World Table capital shares), and a dynamic counterfactual pipeline that simulates the world from 2023 to 2042 under five scenarios: a baseline, monetary reform only, trade reform only, the full system, and an aggressive variant. The published results are the scenario tables: the full system reduces average inequality substantially where the baseline lets it drift upward, with the aggressive variant reaching the model’s floor. A replication package ships with the paper.

Two facts about the artifact’s quality belong in this section rather than later, because the no-exculpation rule cuts in both directions and the reader must not discount them after §5. First, the paper’s citation apparatus survived an external check of roughly forty factual claims with zero errors. Second — established in the forensics below and stated with its exact scope — the dynamics reproduce byte-identically: all five per-scenario, per-year results files regenerate exactly from the shipped code, at 160 rows by 17 columns each, maximum absolute difference zero [F6]. The scope restriction matters and is not buried: the paper’s summary table is a different artifact, two of whose figures match no year of the underlying data and cannot be regenerated by any code in the repository [F7] — §5 reports this in full. And a distinction this paper’s own §2 draws must be applied to this paper’s own case: reproduction establishes that the program is stable under re-execution, not that its numbers are right. No. 003's counterfactual recursion is not derived from its constrained-equilibrium formulation and runs at the calibration §5 questions; its outputs regenerating exactly says nothing about their validity, and this paper asserts nothing about their validity, in either direction. What the forensics license is precisely: stable, and disconnected from the theorems — not wrong, and not right.

The disposition of No. 003 is a judgment this paper owes an argument for, not a recital. It stands as published, for three reasons. Its July 2026 coda discloses everything §5 reports — the disconnection, the restated theorem, the infeasible target, the summary-layer failure — so no reader of the original can now take the join claim at face value; the correction a stranger’s paper would warrant is, in substance, that coda, and it exists. Its proofs are not impeached, and its dynamics regenerate exactly, so neither withdrawal trigger — false results or unreproducible results — is met. And the archive’s convention of showing work in progress openly is built for exactly this case: the alternative dispositions would either overstate the severity (withdrawal, when nothing published is shown wrong) or hide the record (silent revision). A reader who weighs §5 and concludes the coda is insufficient is making a defensible judgment, and the paper does not pretend the question is closed — it states where its author came down, and why.

§ VThe Case, II: What Was Found

Everything in this section is forensic. Each finding carries the check that reproduces it — named [F*], from the harness reproduce_findings.py that ships inside the replication package and exits non-zero on any failure. The harness separates its checks into two groups, and the distinction carries evidential weight: forensic checks run against the preserved pre-remediation code and the shipped results, and are evidence about the published artifact; regression checks test that the remediation behaves as its author intended, and are evidence about nothing except the patch. Only the first group appears in this section. The clean-room protocol and its result are stated once: the package was unzipped in a directory that had never held the working files, on the shipped code alone, and the forensic group returned fifteen of fifteen. A reader with a terminal can repeat this in minutes; the paper’s evidentiary base is that command, not the author’s word.

The harness itself has a history this section is obliged to report, because it is the paper’s thesis enacted on the paper. The first version, reviewed with this manuscript, contained two defects of exactly the kind catalogued below: its byte-identity check could pass vacuously on an empty comparison — a permissive success criterion, the §5 lesson, inside the instrument that teaches it — and its pipeline re-run mutated the package under audit, overwriting the one artifact this paper describes as unrecoverable; the referee’s execution of the harness destroyed the working copy of that exhibit, restored afterward from the archived package. A third defect sat beside them: the remediation’s own summary-rebuild script referenced columns that do not exist in the per-year files and silently wrote blank welfare values — a silent implementation failure in the very package built to document silent implementation failures, and one §6 must now account for. All three are fixed; the rebuilt harness is non-mutating, asserts its comparison counts, and covers every forensic sentence in this section with a check of at least the sentence’s strength. None of this is offered as color. It is the base-rate datum the paper is otherwise forbidden to supply: the join failure mode recurred, immediately, in code written by an author actively writing a paper about it.

Finding 1 — unexercised. The results pipeline never calls the verification core, and the scope of that sentence matters. The script that generates every scenario file, and therefore every published number, is run_counterfactuals.py. Searched for the three functions that implement the paper’s formal machinery — solve_equilibrium, the constrained optimum of Theorem 5.3; check_stability and find_gamma_bar, the apparatus of Theorem 5.1 — it contains zero references to any of them. [F5] The scope, stated precisely because the finding is easy to overstate: the pipeline does call the model’s behavioral equations — the equality-augmented Taylor rule and the equality-adjusted gravity model — while the money-supply adjustment it re-implements independently rather than calling [F5]; what it never touches is the verification and solution core, the code that would establish the theorems’ properties. Nor is “never called by the results script” itself damning — a results pipeline has no business invoking diagnostics, and a paper with a standalone validation suite whose output was reported would be in perfectly good order. The finding is that no such suite ran anywhere that reached the paper: the stability check’s only execution path was a demonstration block at the bottom of the model file, printing to a console no published exhibit ever saw, and the constrained solver’s results appear in no table. The counterfactuals run on an independent recursion — a year-by-year inequality dynamic driven by r-minus-g gaps and policy terms, competent in itself and nowhere derived from the constrained-equilibrium formulation. A reader who took the scenario tables as an instance of Theorem 5.3 — which is what their placement invites — was misled by the paper’s structure while every number in the tables regenerates exactly. This is the join claim failing in its purest form, and it is the finding the rest of the case sits inside: the defects below live in code that no published result ever ran.

Finding 2 — unreachable. Theorem 5.1's stated property was unobtainable. The theorem claims saddle-path stability — a rational-expectations property requiring the linearized system to have exactly one unstable root, so that inflation, the jump variable, can leap to the saddle path. The implementation’s Jacobian encoded a backward-looking Phillips curve: its first row was [0, κ, 0] — inflation responding to the output gap with no forward-looking term, hence no positive root to jump on. Under that structure the saddle-path criterion is not hard to satisfy but impossible: across the full sweep of the equality coefficient — eighty-one values of γ from zero to two, in all eight calibrated nations, six hundred forty-eight cells — the saddle-path check returned false in every one. [F2] What concealed this for the model’s whole life is a single line in the stability checker: is_stable = saddle_stable or asymptotic_stable. The theorem claims the first; the code accepted the second; the function reported success. The generalizable lesson is worth a sentence of its own: any success criterion of the form A or B, where the theorem claims A, will report success under B forever, and disjunctive success criteria are where unreachability hides. One more fact about this finding, added at the coverage round because it disposes of the strongest objection to §3: the standard DSGE toolchain would not have caught it. A backward-looking implementation declares no forward-looking variables, requires no explosive roots, and passes the Blanchard–Kahn precondition trivially — Dynare would have simulated this model without complaint while the paper’s theorem asserted saddle-path stability of a different system. The automated check verifies the program’s solvability; nothing automated verifies the program’s identity with the theorem.

Finding 3 — uncalibrated. The calibration and the theorem belong to different monetary regimes. Correcting the Phillips curve exposes a second, independent defect. The v3 IS-curve row also omitted the Fisher term — it used the inflation coefficient α_π where the real-rate logic requires α_π − 1 — which deleted the Taylor principle from the linearization entirely: determinacy no longer depended on the inflation response at all. Restore the term, and saddle-path stability requires α_π > 1, the standard determinacy condition. The paper calibrates α_π = 0.5 — a constant in the shipped model file, checkable by inspection, and the theorem’s condition is a result of the determinacy literature rather than of any code; the harness’s demonstration that 0.5 fails and 1.5 attains saddle-path runs on the remediated Jacobian and is therefore a regression check on the patch, cited as illustration and not as evidence about the published artifact [R1, labeled as such]. The right frame for the number is not “too low” but whose it is: Clarida, Galí and Gertler’s estimates put the pre-Volcker Federal Reserve at 0.83 with a standard error of 0.07 — so 0.5 sits more than four standard errors below even the accommodative, indeterminacy-prone regime — against 2.15 post-Volcker, while Taylor’s canonical 1.5 is a calibration, not an estimate, and the estimated post-Volcker range runs 2.0 to 2.2. At 0.5, the model’s central bank raises nominal rates by half the increase in inflation, cutting real rates into every inflation. The paper’s monetary regime and its stability theorem belong to different decades, and no line of code can reconcile them — either the calibration moves above unity or the theorem is restated as an asymptotic-stability result under adaptive expectations. (No. 003's coda takes the second option, and flags the calibration as open.) A counterfactual note, for symmetry with Finding 2: this defect is the one the DSGE toolchain would have caught — a forward-looking specification at α_π = 0.5 fails the Blanchard–Kahn precondition, and Dynare halts with an indeterminacy error at the first simulation. No. 003 hand-rolled its solver and never crossed that guardrail, which locates the checklist’s constituency exactly: the automated check exists only inside one toolchain, is required by no journal even there, and the papers outside it have nothing.

Finding 4 — infeasible. The headline target is unattainable, and this finding’s own first draft needed three corrections the referee supplied. The equality constraint sets a global Gini target of 0.30. Establishing what the mechanism can reach requires a caveat stated before any number: the original solver cannot answer the question at all — its transfer rule was keyed to within-nation inequality gaps, which cannot systematically move the between-nation dispersion the constraint is written on — so the frontier below is swept on the remediation’s reconstruction of the mechanism, a progressive per-capita rule with an equality-index tilt, and “the model’s own instrument” means that reconstruction, the most favorable reading available to the original paper. Under it, sweeping the transfer scale to gross transfers of one hundred percent of world GDP, the global between-nation Gini never falls below 0.4628 — the earlier draft’s figure of 0.5241 was the minimum under one particular cap, not the mechanism’s floor — and the target of 0.30 is unreachable at any tested level; the nearest feasible targets begin around 0.55, at gross transfers of roughly fifteen percent of world GDP (the draft’s “six percent” confused the solver’s share parameter with the gross-transfer ratio; they differ by a factor of about 2.6). [F4] The raw path is also non-monotone — dispersion falls, rises, and falls again as the transfer scale grows, with the first reversal at gross transfers around world-GDP scale [F4] — far beyond any policy-relevant range, so the non-monotonicity’s practical content is not “modest transfers overshoot” but methodological: an ascent method pointed at this objective cannot be trusted to converge even where an optimum exists, and its failures will read as numerics. That is how the original solver behaved: it ran to its budget of one thousand iterations with the recorded constraint violation frozen at its initial value — computed from a pre-transfer quantity that transfers cannot move [F3] — and gross transfers diverging to fifty-nine percent of world GDP [F3], against the commissioned audit’s report of one percent. The solver could not say the one thing that was true: this target is not reachable. Infeasibility is a substantive finding about the model — its headline target exceeds its mechanism’s reach severalfold on the most favorable reconstruction — and it presented, for the model’s whole life, as a convergence warning.

A footnote completing the harness’s record. Before the referee’s findings, the harness had already failed once on its own: two checks reported failure while printing the expected values, because the stability function returns a NumPy boolean, and a NumPy False is not the Python singleton False under an identity test. Three harness-side defects in one small verification instrument, all at the join between a claim and the code asserting it. The facts are reported because the register reports what was found; no moral is drawn beyond the one §8 is permitted.

What the four findings survived. The paper was written, worked through this archive’s internal review, published with a replication package that reproduces perfectly, and audited by a commissioned external review of the code. Three of the four findings were named by none of these. The fourth was named once, at the wrong magnitude, by the audit — which is §6's subject.

§ VIThe Case, III: The Audit That Missed It

In February 2026 the model received a commissioned audit, scoped — in its own words — to “code quality, mathematical correctness, publishability.” It returned a score of 4.9 out of 10, a verdict of “NOT READY FOR PUBLICATION,” and three blocking findings. Three constraints govern this section, stated at the outset. No claim about the auditors’ competence is made or implied anywhere in it. The audit’s bottom line was correct — the model was not ready for publication, as §5's four findings establish more thoroughly than the audit did, and any reading of this section as a discrediting of the verdict has it backwards: the verdict was right and the itemization beneath it was not. And a caveat about the evidence itself: the audit’s commissioning brief and the exact artifact it examined are not among the surviving records, so the re-executions below run against the preserved pre-remediation snapshot, whose identity with what the auditors saw is probable — it is the only version the repository ever held — but not certain, and the auditors have had no opportunity to reply. The asymmetry is real: the author’s claims get a harness he wrote; the auditors’ claims get re-executed against a reconstruction. The section’s conclusions are stated at the strength that asymmetry permits.

The three blocking findings, against re-execution of the preserved snapshot. First: “stability analysis fails — γ̄ = 0.00 for all nations.” This does not reproduce: the code returns γ̄ = 1.6985 — for every nation, identically, which is a real defect (the Jacobian read nothing nation-specific) but the opposite kind of number. [F1] Second: “equality constraint not enforced; transfers roughly one percent of GDP against five to ten needed.” The substance reproduces — the constraint never binds — but the magnitude is inverted by a factor of about sixty: transfers were diverging toward fifty-nine percent of world GDP, not stalling at one [F3], and a remediation keyed to the audit’s direction — make the transfers bigger — would have worsened the actual defect. Third: “welfare calculations incomplete; blank CSV columns” — and here this paper’s first draft owed the audit a concession it failed to make, supplied by the referee of this manuscript and recorded now. Against the pre-remediation artifact the finding does not reproduce: welfare computes and the shipped summary’s welfare columns are populated. But the remediation package — the July 2026 artifact this paper itself ships — contained, until this revision, a summary-rebuild script that referenced columns absent from the per-year files, swallowed the error silently, and wrote blank welfare values in every row. “Welfare calculations incomplete; blank CSV columns” was a false description of the artifact the audit examined and a literally accurate description of an artifact its author built five months later while writing a paper about silent implementation failures. The audit’s third finding is therefore scored: wrong about its object, prophetic about its author. The defect is fixed, the harness now covers it [R3], and the sentence stands here at full strength per the no-exculpation rule.

The structural reading, which is the only one this paper offers. An audit finds what its brief points at. A brief that says code quality directs attention to the code as code — style, structure, numerical hygiene, whether outputs populate — and nothing in it points at the relation between the code and the paper’s theorems, so that relation went unexamined. This is not a failure of diligence within the brief; it is the brief. And a conjecture the case suggests, offered as conjecture because the paper has one observation of it: in this case, the person who set the audit’s scope was the person whose work was audited — and if that arrangement is common, as it plausibly is wherever authors commission their own reviews, then scope is where self-interest would operate most invisibly: not by suppressing findings, but by never pointing the instrument at the place a finding would hurt. The paper asserts no such motive here and has specific reason not to: the author set this brief, and the author did not think of the join either. That is rather the point. The join was not protected by anyone. It was simply on no one’s list, including the list its owner wrote.

One more fact about the audit belongs in the record because it bears on audits as instruments generally: the finding it got substantively right, it got wrong in the direction that mattered for repair. A conduct instrument that detects the right defect with an inverted magnitude is not half right; for the purpose of guiding remediation it is wrong twice, once about size and once about which way to push. §8 will draw the only projection this supports.

§ VIIThe Anatomy of a Join Failure

This section is the framework, and it is labeled as such: a taxonomy derived from one case, offered for testing, and almost certainly incomplete — the specific gaps are listed at its end, and a failure fitting none of its categories is one of the paper’s named falsifiers.

Define the object first. A paper makes a join claim when it contains an analytical result R — stated hypotheses, stated property, proof — and a computational artifact P producing reported exhibits, and presents P’s output as bearing on R. The claim is almost never written; it is carried by adjacency, shared notation, and ordering; and it asserts that P is an instance of a world in which R holds. Four ways that can be false, distinguished by where the join breaks:

Unexercised. P never invokes R. Both are real; they are not connected. Detection: static call-graph search from the results-producing script to the functions implementing R — a text search, requiring no execution. In the case: zero calls from the pipeline to any of the three formal-core functions. What it does not mean: that the results are wrong. It means the theorems are not doing the evidentiary work their placement implies, and the paper owes the reader a sentence saying which work they are doing.

Unreachable. P is invoked but its structure forbids R’s property; the implementation encodes a different model than the one proved. Detection: ask whether the code has ever reported R’s property as satisfied on any admissible parameterization — and read the success criterion, because a disjunctive criterion accepting a weaker property will conceal unreachability indefinitely. In the case: saddle-path in zero of eight nations across the full sweep, behind an or. What it does not mean: that R is false. R may be exactly true of the model the code fails to implement.

Uncalibrated. P implements R faithfully and is run outside R’s domain: the shipped parameters violate the theorem’s stated hypotheses. Detection: enumerate the hypotheses as inequalities; evaluate at the calibration — the cheapest check in the set, requiring no execution at all. In the case: a determinacy condition requiring α_π > 1 against a calibration of 0.5, a regime-scale violation rather than a boundary case. What it does not mean: that the model is uninteresting. It means R may not be cited in support of results computed there.

Infeasible. The model states a target its own instrument cannot reach at any admissible setting, and the solver reports the impossibility as non-convergence. Detection: sweep the instrument; record the attainable frontier; check the target against it, and check monotonicity while there. In the case: a 0.30 target against a 0.52 minimum, behind an exhausted iteration budget. What it does not mean: that the target is wrong as an aspiration. It means the paper’s mechanism cannot deliver it, which is a result, and the paper should have been the one to report it.

What the four share is the paper’s structural claim in miniature. Each is invisible to proof review, because none is a defect in a proof. Each is invisible to replication, because in every one of them — and in the case, literally — the numbers reproduce. The join is not unchecked because anyone declined to check it. It is unchecked by construction, because both existing instruments are correctly aimed at something else.

What the taxonomy does not cover, named so the gap is visible rather than discovered: results stated informally rather than as theorems, where there are no hypotheses to enumerate; papers whose computation is estimation rather than simulation, where the join runs through the likelihood; multi-paper programs, where R is proved in one paper and silently relied on by the code of another; and implementations faithful to R applied to data outside R’s scope conditions. Each of these is a join; none of them is covered by the four categories; a failure in any of them that the categories cannot absorb is invited as the taxonomy’s falsifier.

§ VIIIWhat Can Be Expected

Everything here is projection, and this is deliberately the shortest substantive section in the paper. The reason is the constraint stated in §1: one case establishes that join failures occur, that they survive the existing checks, and that a cheap instrument finds them. It establishes nothing about how often, and the reader will supply the generalization unaided — from four-in-one-paper to probably everywhere is a slide requiring no assistance. The paper declines to make it, and its projections are therefore confined, structurally, to what the instrument would do rather than to what the discipline contains.

Projection 1 — the checks are decidable. Trend: applied once in earnest, all seven checks of §10 returned determinate answers — an integer, a satisfied/violated verdict, a frontier and a monotonicity property — and none required judgment about anyone’s intent. Assumption, doing real work: that the case is not unusually legible — that other papers state hypotheses explicitly enough to enumerate and ship code traceable enough to search. A paper whose conditions live in prose (“provided policy is sufficiently responsive”) makes the cheapest check non-evaluable — and in the one case examined, the conditions that went unevaluated longest were exactly the ones stated least formally, a pattern the paper suspects generalizes and cannot show. Falsifier: a good-faith application to a comparable paper in which most checks return “not evaluable” — which would demote the checklist from instrument to standard, and §10 from list to guidance. Reports of exactly this outcome are invited.

Projection 2 — the categories are unequally cheap, and the cheapest was the most consequential. Trend: in the case, the four findings differed by orders of magnitude in cost — a text search; one inequality at one number; a criterion read plus a sweep; a frontier construction the original code could not perform. Assumption: the ordering is a property of the categories — static checks are intrinsically cheaper than execution sweeps — not of this codebase. Expectation: adoption, if any, proceeds from the top of the list; and the asymmetry runs the right way, because the cheapest check found the deepest defect — not a wrong number but a formal core doing no work. The highest-yield check costs a text search. Falsifier: cases where the cheap checks pass and only the expensive ones fail, systematically — which would mean the checklist’s adoptable part is its least informative part.

Projection 3 — audits find what their briefs point at, and briefs are written by the audited. Trend: a commissioned audit scoped to code quality returned code-quality findings, missed three of four join defects, and failed re-execution on most of its own headlines. Assumption: scope effect, not competence effect — an auditor working to a join brief would have found join defects; the paper has no evidence about skill and asserts none. Expectation: commissioning an audit will continue to be mistaken for auditing the join, by authors who — like this one — write the brief themselves and do not think of it. Falsifier: a code-quality audit in the wild that surfaces a join failure unprompted, establishing that the check emerges from competent review without being named. This is the projection the paper would most like to lose, because losing it means the discipline needs no new instrument — only its existing auditors, better used.

What this register does not project, listed because omission should be legible: no prevalence — the paper does not estimate how many published papers fail the join, and does not know; no severity distribution — here the results reproduced and nothing published was numerically wrong, and whether that is typical or lucky is unknowable from one case; no diagnosis of formal economics — this is not an argument that the discipline over-formalizes or that CGE is unreliable; and no adoption forecast — §11's invitation is an invitation.

§ IXThe Ledger: What We Claim and What We Do Not

In the house manner, the register audit.

What is claimed (Register C, §§1–3, 7): the join claim as an object, carried by adjacency, with no located instruction directing anyone to referee it — a claim about the written apparatus, not about referees’ private practice; the two existing checks as correctly scoped elsewhere, with the replication reforms conceded in full; the mechanical demonstration — six terms, zero occurrences, across fourteen enumerated and snapshotted documents, stated at search grade with its scope limits named in §1; the resized novelty claim — owned by computational science as code verification, asked by health economics of theorem-free models, approximated in CGE by generic properties, and required by no economics journal for a paper’s own theorems; the four-category taxonomy, labeled framework, with detection tests and named gaps.

What was found (Register F, §§4–6): four join failures in one published model — unexercised, unreachable, uncalibrated, infeasible — each carrying a harness check of at least the sentence’s strength, forensic checks separated from regression checks on the remediation, fifteen of fifteen forensic in a clean room; the byte-exact regeneration of the five per-year results files, stated as firmly as the failures and at its exact scope, beside the summary table whose figures match no year of the data for two scenarios and whose generating code is unrecoverable — reproduction establishing stability, not correctness, in both directions; the audit record — bottom line correct, one itemized finding reproducing at an inverted magnitude, one refuted against the preserved snapshot, and one false of its object while accurate of a script its author wrote five months later — read structurally, with the provenance caveat carried and no claim about competence; and the harness’s own three defects, two found by this manuscript’s referee, reported flatly.

What can be expected (Register P, §8): three projections, each about the instrument rather than the population, each with a falsifier, one named as the projection the paper prefers to lose.

What the paper does not claim. No prevalence, no frequency, no “economics routinely” — one case, and the no-generalization rule holds to the last page. No claim that No. 003's published results are right — and none that they are wrong: the dynamics regenerate exactly, which establishes stability and nothing further, and the paper polices that distinction in its own favor as strictly as against it. No claim that its theorems are false — Theorem 5.1 is restated, not refuted, and the proofs are not impeached. No claim about the auditors — the audit’s verdict is conceded correct, the scope effect is §6's entire content, the author wrote the scope, and the auditors have not had a reply. No claim that economics should adopt formal verification wholesale — the checklist is seven items, not a proof assistant. No claim that this taxonomy is complete — four named categories, four named gaps, one invited counterexample. And no claim that the paper’s self-audit makes it trustworthy — the forensic register is checkable by command, which is the only basis on which the paper asks to be believed; where its instrument failed, the failures are in §5, found by someone else.

§ XThe Checklist

The house tradition ends with what to measure. This paper ends with what to run. Seven checks, for an author auditing their own paper before submission; no knowledge of the case above is required; the first three execute no code; the estimated total for a paper with one theorem and one simulation is an afternoon. Each check states what a failure means and what it does not, because the likeliest misuse of a list like this is over-reading a red flag.

1 · Name the join claim. Write one sentence: the paper’s computational results bear on Theorem R because ____. If the sentence cannot be completed, the remaining checks are unnecessary — and the paper owes the reader the sentence saying the theorem and the computation are independent contributions. A failure means the join claim was decorative. It does not mean either artifact is defective.

2 · Evaluate the hypotheses at the calibration. Enumerate R’s conditions as inequalities; evaluate each at the shipped parameters; record satisfied, violated, or not evaluable. Two limits of the check, stated in the check: conditions in prose (“shocks sufficiently small”) and conditions on function spaces rather than scalars (concavity, Inada, fixed-point requirements on primitives) are not evaluable this way — record them as such rather than skipping them, because not evaluable is itself a finding about how the paper states its theorem. Grade violations by distance — a boundary case is a robustness question, a regime-scale violation is a category error. A failure means R may not be cited in support of results computed there. It does not mean the results are wrong or the theorem false.

3 · Locate where R’s property was ever established. The naive version — count calls to R’s functions from the results script — misclassifies good practice, since a results pipeline has no business invoking diagnostics, and a package with a standalone validation suite would score zero while being in perfect order; a plain string count is also defeated by one wrapper, so trace imports, not just names. The real question has three parts: was R’s property ever established on the shipped configuration, by any code in the package; where is that code’s output; and did the output reach anything the reader sees? A demonstration block printing to a console no exhibit ever saw — the case above — is an answer of no wearing an answer of yes. A failure means the theorems are not doing the evidentiary work their placement implies. It does not mean the results are wrong.

4 · Ask whether the code can ever say yes. Find the function that checks R’s property; read its success criterion; if it is disjunctive and the theorem claims the stronger disjunct, establish whether that disjunct has ever been achieved on any admissible parameterization. This is the check most likely to find something and the one most likely to be skipped, because the code reports success. A failure means the property is structurally unreachable and the checker has been reporting a substitute. It does not mean R is false.

5 · Sweep the instrument; find the frontier. For any stated target or constraint, sweep the policy instrument across its admissible range; record the attainable frontier; check the target against it, and check monotonicity on the way. A target outside the frontier is a substantive finding, not a solver problem. Non-monotonicity is a second finding: it means ascent methods cannot be trusted to locate the optimum, and convergence failures will masquerade as numerics.

6 · Make the solver say which failure it had. If the solver’s only failure signal is an exhausted iteration budget, add an explicit feasibility determination. A solver that cannot distinguish infeasible from did not converge will misreport the model’s most interesting negative result as a warning message.

7 · Regenerate everything, including the summary layer — in a copy, not in place. Copy the package to a temporary directory; run the pipeline there; compare byte-for-byte against what ships — on the original platform; across platforms, floating-point and library differences make byte-identity the wrong standard, and a stated numerical tolerance replaces it. Then regenerate any aggregation or summary layer separately from the primary outputs. In the case above, the summary layer was the only unreproducible artifact in an otherwise byte-exact package — and, in the same case, the first version of the verification harness ran the pipeline in place and overwrote the very artifact whose unreproducibility it existed to document. Verify in a sandbox; the instrument must not be able to eat the evidence.

Report all seven results in a numerical appendix — the passes and the non-evaluables as well as the failures. A checklist reported only when it finds something is a marketing document.

And the commitment that makes the list an instrument rather than an exhortation, recorded here per the ratification in this paper’s execution brief: every future paper in this archive with a computational section ships a completed join audit. The rule binds the author before it recommends itself to anyone else, which is the only order in which such a rule can be offered.

§ XIA Research Program

This paper is one move in a longer argument, conducted in the open, and the move is the dullest in the archive on purpose: between two well-audited artifacts there is an unaudited seam, and the paper stitches a checklist across it. The forensic base is one model; the instrument is seven items; the projections are three, confined to the instrument; and the generalization the reader will want is exactly the thing the paper does not supply, because it cannot.

The invitations, named. To authors of formal papers with computational sections: run the seven checks on your own paper and report the results — including, and especially, seven passes, because the paper’s evidence base is one case and every reported application moves it, in either direction. To data editors: the first three checks execute no code and could ride inside existing verification workflows at near-zero marginal cost; whether they should is a policy question this paper does not presume to settle, but the cost side of it is now measured. To the health economists whose verification tradition is the nearest working precedent: the TECH-VER lineage stopped at models without theorems because its models have none; the extension is yours if you want it. To the V&V community, and to the property-based and metamorphic testers whose instrument class Checks 4 and 5 hand-roll: economics has been importing your vocabulary one author at a time; a worked bridge — code verification stated for a discipline whose conceptual models are theorems, with theory-implied relations as the metamorphic properties — would be worth more than this paper. To the mechanized-economics program, which has already closed the join outright for a handful of theorems by generating the program from the machine-checked proof: the checklist is the cheap point on your cost curve, and the curve needs its middle filled in. To the toolchain maintainers: Dynare’s determinacy precondition is the one automated join-adjacent check in the discipline’s daily practice, and a check_theorem block — the paper’s stated hypotheses evaluated at the calibration, reported in the log — is a feature request this paper is happy to have made in public. And to whoever finds the fifth category: the taxonomy is over-fitted by construction, §7 names four joins it does not cover, and its falsifier is an invitation with a section number on it. The checklist itself has an ancestor this revision restores to the record: McCullough and Vinod’s four-step verification of nonlinear solutions is §10's lineage, published in the AER in 2003, revised under fire in 2004, and adopted by no policy since — the afternoon this paper asks for was first asked for twenty-three years ago.

The thread placement, last, because it is the oddest in the archive. This is the Money thread’s second paper, and it audits the first. That is not a detour from the thread’s question — what a monetary order designed for fair exchange would look like — but a precondition of continuing to ask it: No. 003's architecture cannot be extended until its foundations are known, and they are now known precisely — which theorems hold as stated, which hold restated, which target its mechanism cannot reach, and which of its numbers reproduce, namely all of them. The thread resumes from that surveyed ground. Knuth’s memorandum warned the reader to beware of code he had proved correct but never run. The discipline this paper examines has spent two decades learning to run everything — and the join Knuth pointed at, between the proving and the running, is still nobody’s job. The paper’s whole claim is that it should be somebody’s, that it costs an afternoon, and that the author, having run it on himself, found four things he did not know were there — written down, all four, precisely enough to be wrong about.

---

Notes

On the registers. Register C is what is claimed — conceptual, cited. Register F is what was found — forensic observations of one artifact, each carrying the file, the function, and the harness check that reproduces it; the register is not called E because it may not borrow the authority of measurement of the world. Register P is what can be expected — three projections, confined to the instrument rather than the population. [§1]

On the three rules. No-generalization: one case, no prevalence claim, to the last page. No-exculpation: every finding about the author's own model stated at the strength it would carry against a stranger's — in both directions, so the byte-exact reproduction is stated as firmly as the failures. No-heroism: the confessional register is banned, and candor is nowhere offered as an argument. [§1, §9]

On the harness's own record. The verification instrument failed three times at the join it audits: a NumPy-boolean identity test that reported failure while printing correct values; a byte-identity check that passed vacuously on zero files; and an in-place pipeline re-run that overwrote the one artifact the paper describes as unrecoverable — destroyed during referee review, restored from the archived package. All three are reported in §5 as the paper's only permissible base-rate datum, and the v2 harness is non-mutating, guarded, and grouped into forensic and regression checks. [§5]

On the audit. The commissioned audit's bottom-line verdict was correct; its itemized findings mostly failed re-execution against the preserved snapshot, whose identity with the audited artifact is probable but not certain; the auditors have had no reply; and its third finding — false of the artifact it examined — became literally true of a script its author wrote five months later. No competence claim is made anywhere. [§6]

On open imprint items. The policy-corpus texts behind the zero-count are to be snapshotted into the submission package, since policies revise and the count decays; the audit's commissioning brief remains unrecovered and is flagged rather than resolved. [§1, §6]

---

References

American Economic Association. Data and Code Availability Policy; Data Editor verification protocol and replication-report template. [the keyword-test corpus, with the DCAS, the Social Science Data Editors template, and the policies of Econometrica, JPE, REStud, QJE, and the Economic Journal]

Aruoba, S. B., Fernández-Villaverde, J., & Rubio-Ramírez, J. F. (2006). Comparing solution methods for dynamic equilibrium economies. Journal of Economic Dynamics and Control, 30(12).

Bernanke, B. S. (2004). Editorial statement. American Economic Review, 94(1), 404.

Blanchard, O. J., & Kahn, C. M. (1980). The solution of linear difference models under rational expectations. Econometrica, 48(5), 1305–1311.

Brodeur, A., et al. Mass reproducibility and replicability. IZA DP 16912.

Bullard, J., & Mitra, K. (2002). Learning about monetary policy rules. Journal of Monetary Economics, 49(6), 1105–1129.

Buyukkaramikli, N. C., et al. (2019). TECH-VER: A verification checklist to reduce errors in models. PharmacoEconomics, 37(11), 1391–1408.

Cai, Y., & Lontzek, T. S. (2019). The social cost of carbon with economic and climate risks. Journal of Political Economy, 127(6). [§B, "A Verification Test"]

Caminati, M., Kerber, M., Lange, C., & Rowat, C. (2015). Sound auction specification and implementation. ACM EC'15.

Chang, A. C., & Li, P. (2022). Is economics research replicable? Critical Finance Review / Fed working paper lineage.

Chen, T. Y., et al. (2018). Metamorphic testing: A review of challenges and opportunities. ACM Computing Surveys, 51(1).

Christensen, G., & Miguel, E. (2018). Transparency, reproducibility, and the credibility of economics research. Journal of Economic Literature, 56(3).

Claessen, K., & Hughes, J. (2000). QuickCheck. ICFP.

Clarida, R., Galí, J., & Gertler, M. (2000). Monetary policy rules and macroeconomic stability. Quarterly Journal of Economics, 115(1), 147–180.

den Haan, W. J., & Marcet, A. (1994). Accuracy in simulations. Review of Economic Studies, 61(1), 3–17.

Dewald, W. G., Thursby, J. G., & Anderson, R. G. (1986). Replication in empirical economics. American Economic Review, 76(4).

Dixon, P. B., & Rimmer, M. T. Validation in CGE modeling. In Handbook of CGE Modeling, Vol. 1, ch. 19.

Dreber, A., & Johannesson, M. (2025). A framework for evaluating reproducibility and replicability in economics. Economic Inquiry.

Drukker, D. M., & Wiggins, V. (2004). Comment. American Economic Review, 94(1), 397–399.

Dubé, J.-P., Fox, J. T., & Su, C.-L. (2012). Improving the numerical performance of static and dynamic aggregate discrete choice random coefficients demand estimation. Econometrica, 80(5).

Fair, R. C. (1994). Testing Macroeconometric Models. Harvard University Press.

Fernández-Villaverde, J., Rubio-Ramírez, J. F., & Santos, M. S. (2006). Convergence properties of the likelihood of computed dynamic models. Econometrica, 74(1), 93–119.

Foote, C. L., & Goetz, C. F. (2008). The impact of legalized abortion on crime: Comment. Quarterly Journal of Economics, 123(1), 407–423.

Galí, J. Monetary Policy, Inflation, and the Business Cycle, ch. 4.

Gertler, P., Galiani, S., & Romero, M. (2018). How to make replication the norm. Nature, 554.

Herndon, T., Ash, M., & Pollin, R. (2014). Does high public debt consistently stifle economic growth? Cambridge Journal of Economics, 38(2), 257–279.

Hurlin, C., & Pérignon, C. (2024). Reproducibility certification in economics research. Harvard Data Science Review, 6(2). [cascad]

Judd, K. L. (1998). Numerical Methods in Economics. MIT Press.

Kanewala, U., & Bieman, J. M. (2014). Testing scientific software: A systematic literature review. Information and Software Technology, 56(10).

Kerber, M., Lange, C., & Rowat, C. (2016). An introduction to mechanized reasoning. Journal of Mathematical Economics, 66, 26–39.

Klein, P. (2000). Using the generalized Schur form to solve a multivariate linear rational expectations model. Journal of Economic Dynamics and Control, 24(10).

Knittel, C. R., & Metaxoglou, K. (2014). Estimation of random-coefficient demand models: Two empiricists' perspective. Review of Economics and Statistics, 96(1), 34–59.

Knuth, D. E. (1977). Memorandum to Peter van Emde Boas. [the epigraph]

Kubler, F., & Schmedders, K. (2005). Approximate versus exact equilibria in dynamic economies. Econometrica, 73(4), 1205–1235.

Lubik, T. A., & Schorfheide, F. (2004). Testing for indeterminacy. American Economic Review, 94(1), 190–217.

MacIver, D. R., & Hatfield-Dodds, Z. (2019). Hypothesis: A new approach to property-based testing. Journal of Open Source Software, 4(43).

McCullough, B. D., & Vinod, H. D. (1999). The numerical reliability of econometric software. Journal of Economic Literature, 37(2), 633–665.

McCullough, B. D., & Vinod, H. D. (2003). Verifying the solution from a nonlinear solver: A case study. American Economic Review, 93(3), 873–892. [and the 2004 Comments and Reply, AER 94(1)]

McCullough, B. D., McGeary, K. A., & Harrison, T. D. (2006). Lessons from the JMCB archive. Journal of Money, Credit and Banking, 38(4), 1093–1107.

Menkveld, A. J., et al. (2024). Nonstandard errors. Journal of Finance, 79(3).

Oberkampf, W. L., & Roy, C. J. (2010). Verification and Validation in Scientific Computing. Cambridge University Press.

Pérignon, C., et al. (2019). Certify reproducibility with confidential data. Science, 365(6449). [cascad]

Pesaran, M. H. (2003). Introducing a replication section. Journal of Applied Econometrics, 18(1), 111.

Pesaran, M. H., & Smith, R. (1985). Evaluation of macroeconometric models. Economic Modelling, 2(2).

Ratto, M. (2008). Analysing DSGE models with global sensitivity analysis. Computational Economics, 31(2), 115–139. [the Dynare GSA toolbox]

Reinhart, C. M., & Rogoff, K. S. (2010). Growth in a time of debt. American Economic Review: Papers & Proceedings, 100(2), 573–578.

Santos, M. S. (2000). Accuracy of numerical solutions using the Euler equation residuals. Econometrica, 68(6), 1377–1402.

Sargent, R. G. Verification and validation of simulation models. Winter Simulation Conference lineage.

Shachar, R., & Nalebuff, B. (2004). Comment. American Economic Review, 94(1), 382–390.

Sims, C. A. (2002). Solving linear rational expectations models. Computational Economics, 20(1–2). [gensys and its existence-uniqueness flags]

Smets, F., & Wouters, R. (2007). Shocks and frictions in US business cycles. American Economic Review, 97(3), 586–606.

Taylor, J. B. (1993). Discretion versus policy rules in practice. Carnegie-Rochester Conference Series on Public Policy, 39, 195–214.

Woodford, M. Interest and Prices, ch. 4 §2.2. Princeton University Press.

· · ·

Companion papers in the archive: No. 003, The Equality-Indexed Monetary-Trade System — the paper under audit, standing as published with the July 2026 coda that discloses everything reported here. The forensic base is EIMTS_Replication_v4.zip: both model versions, the byte-identical per-year results, both summaries, and the v2 reproduction harness — fifteen forensic checks, four regression checks, non-mutating, exiting non-zero on any failure.

The 17-slide companion deck — The Proof and the Program — sits beside this paper; the corpus index with its coverage-round shelf, claim outline, taxonomy and checklist, projection set, referee report, and response letters are filed under cowork. The checklist binds this archive prospectively: every future paper here with a computational section ships a completed join audit. Run the harness before believing the paper — that is the intended order. Comments welcome at contactme​@​marshallcahill.com.