The Proof and the Program

Imprint manuscript · July 2026, revised August 2026 · Draft v4 after the archive’s six-referee panel (Paper No. 010, Thread II — Money). The pre-archive referee ran the verification harness and caught it destroying its own evidence; the archive panel then ran everything — fired one of the paper’s own disconfirmers against the rebuilt harness, showed the commissioned audit had been re-scored against the wrong artifact, and found the infeasibility frontier moves under the reconstruction’s own basis choice. All of it is now inside the paper, which is the only place a paper like this can honestly keep it. Panel memo, raw reports, and response letters are filed with the archive; the v3 reproduction harness ships inside replication package v4.3.

A note for the reader arriving cold: this archive is a single author’s public collection of numbered working papers; The Equality-Indexed Monetary-Trade System — EIMTS below — is an earlier entry, audited here; “the panel,” “rounds,” and “referees” name its internal review process; “cowork” is its filing workspace. None of that vocabulary is needed to follow the argument, which begins at the epigraph and stands alone.

· · ·

“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 required by no journal policy, no data-editor protocol, and no referee guideline this paper could locate — of which only three public guidelines could be examined at all: 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; the fourteen documents are enumerated in §1, and they are mostly deposit-and-verification policies, so the zero partly reflects their scope — which is the point made from the other side. This paper audits the proof–program join in the one case it can audit without asking the reader’s trust: its own. EIMTS, 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 at any tested level of the reconstruction its remediation chose — and movable, §5 now reports, by that reconstruction’s own unexamined basis choice, so the finding is stated as the envelope it always was — and a results pipeline that never calls the formal core at all. Every per-scenario, per-year results file in that paper regenerates from its shipped code to a stated tolerance — byte-exactly on its original platform, to fourteen decimal places off it, a distinction the archive panel taught this paper by firing its own reproduction disconfirmer — 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 in February 2026; its bottom-line verdict — not ready for publication — was correct, and this paper’s previous edition re-scored its itemized findings against what it believed was the audited code and concluded they mostly failed. The archive panel showed that belief was false: the preserved snapshot postdates the remediation, the audit’s headline number reproduces under the audit’s own stated criterion, and the audit’s text — briefed on mathematical correctness — had named two of the four join failures in February, from symptoms the author himself supplied. §6 now tells that story straight: the instrument was pointed, it fired, and it was mis-scored by its own commissioner twice — once in the disposition of the report, once in this paper’s account of it. 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 — which the archive panel then broke in turn, firing the paper’s reproduction disconfirmer against its byte-identity criterion and finding a transfer-basis mis-specification inside the remediation. The thesis has now been performed on the paper three times, each time by the next reviewer; the paper offers the count not as credential but as its instrument’s defect log. 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, the corresponding policies of Econometrica, the Journal of Political Economy, the Review of Economic Studies, the Quarterly Journal of Economics, the Economic Journal, and Computational Economics, and the three public referee guidelines the sweep could examine — those of the Journal of Monetary Economics, Theoretical Economics, and Quantitative Economics. 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 nine traditions 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 remediation’s 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, and its publication with a replication package. Two of them did not survive the commissioned code audit — which named the unexercised core and the unreachable theorem in February, under a brief that included mathematical correctness — and what failed thereafter was not detection but disposition: the author left the findings unacted, then re-scored them, in this paper’s previous edition, against a snapshot his own remediation had already overwritten. Auditing the join is cheap and mechanical; its application here found four things in the audited model, and its reviewers then found six more in the auditing instruments themselves. Three observations would disconfirm the paper’s contribution, restated with their current status in §9: an existing policy or practice that already requires the question — where the verb carries the claim, and §3's resizing procedure is the claim’s scope rather than an escape from it; a forensic finding that fails to reproduce from the shipped package — fired once, by the archive panel, against the harness’s byte-identity criterion, and repaired per the paper’s own Check 7 (§5); and a join failure that fits none of the four categories, with §7 now stating which of its named gaps would count.

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 essentially perfect — all five per-scenario results files regenerate from the shipped code, byte-exactly on the original platform and to fourteen decimal places across platforms. 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, approximated in one modeling tradition, automated for one property, and solved for a handful of theorems — with four more traditions verifying something real and adjacent; nine stand around the cell, and the paper’s claim survives all nine 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”; the slogan that divides the labor — “verification is the domain of mathematics and validation is the domain of physics” — circulates under Schwer’s name in the V&V overviews, its formulation tracing to Roache.

And economics has a native verification tradition of its own — two, in fact — a count this section itself initially got wrong, restored at review. 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 described their own status as of 2013 — quoted here with its date, because the present tense has begun to decay: verification methods for economic simulation “are not used in standard economic research” (Kamiński and Szufel, 2013).

The question is, for one property, automated — and governed by nobody, and it is the strongest objection this section must meet. 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: the mis-implemented model of EIMTS, whose backward-looking structure declares no forward-looking variables, satisfies the Blanchard–Kahn counting condition at its shipped calibration — zero jumpers against zero unstable roots; not trivially, since the same code acquires positive roots at equality coefficients above roughly 1.7 and would fail there, in 96 of the sweep’s 648 cells — while the theorem it was meant to instantiate claims saddle-path stability of a different system. And the code’s own γ̄ = 1.6985 is, in substance, that boundary: the model was computing a Blanchard–Kahn-equivalent object all along, under the wrong name, for the wrong theorem. A determinacy-enforcing solver, fed this system as declared, would have simulated it at the published settings without complaint. 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 EIMTS 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 §10'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 — nor in the document classes still arriving: structured replication protocols with explicit code-inspection stages (Ankel-Peters et al., 2025), the Institute for Replication’s AI replication engine and mass replication games (Brodeur et al., 2024, 2026), the ZBW’s ReproCheck service, and a verification-first protocol for machine-assisted theory whose worked example checks analytical claims against simulation (Koren, 2026) — each output-scoped or theorem-silent as of this revision’s sweep, and each a place the count could next decay. 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 measurably more likely to be caught when they produce an unexpected result — about a fifth again as likely, on a low detection base (Ferman and Finamor, 2025) — 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 unrequired — not empty. The Macroeconomic Model Data Base has spent over a decade re-implementing published macro models from their stated equations and comparing the results against the papers’ own exhibits (Wieland, Cwik, Müller, Schmidt and Wolters, 2012) — a differential test of exactly this join, staffed and running, whose public replication forum records paper-versus-implementation divergences traced to original authors’ code. den Haan’s comparison project measured how far independent implementations of one identical model drift (den Haan, 2010) — economics’ own N-version experiment, never read as a join question. And the organizational-modeling literature named the practice thirty years ago as “docking,” aligning implementations to establish model equivalence (Axtell, Axelrod, Epstein and Cohen, 1996). The check exists and is even staffed; nobody requires it of a paper’s own theorems, reports it in a paper’s own pages, or files its findings as theorem–code mismatches rather than replication issues — and with those traditions counted, this section’s map has nine standing around the cell. 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; model-comparison infrastructure runs the differential version of it as a standing service; 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. Nine traditions stand around the unrequired cell, which is precisely how a seam persists: everyone adjacent to it can reasonably believe it is someone else’s. The universal negative has now survived two coverage referees — the pre-archive round’s, and the archive panel’s live re-run of the policy corpus in August 2026 — 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.

The Equality-Indexed Monetary-Trade System (EIMTS), this archive’s one formal paper, 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 γ̄. A second result — printed in early editions under the label “Theorem 5.3,” which the current edition of EIMTS has withdrawn as a phantom citation, the object being its Theorem 5.4′ — characterizes the constrained optimum: prices, quantities, and transfers satisfying market clearing and a global inequality ceiling, the constraint binding at the optimum. (A flag carried throughout this paper: the current edition of EIMTS — v9, revised at its own archive panel in July 2026, five days before this paper first appeared — has retracted the γ̄ apparatus entirely, its classification governed by a sign condition independent of γ, and renamed the constrained-optimum result. §4's disposition and §5's findings concern the artifact as originally published and audited, with the v9 corrections noted where they bear.)

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 to a stated tolerance: all five per-scenario, per-year results files regenerate from the shipped code at 160 rows by 17 columns each — byte-exactly on the platform that produced them and, as the archive panel’s clean-room run established by firing this paper’s own reproduction disconfirmer, to within fourteen decimal places on one cell in 13,600 elsewhere [F6]; §5 reports the firing. 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. The counterfactual recursion of EIMTS 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 EIMTS is a judgment this paper owes an argument for, not a recital — and it owes the edition a name. Between this paper’s audit base and its publication, EIMTS was revised: the archive’s own panel reviewed it in July 2026, and its v9 edition landed five days before this paper first appeared — re-fronted around the reachable frontier, the phantom theorem label removed, the γ̄ apparatus retracted, panel memo and response letter filed. It stands, in that edition, for three reasons. Its July 2026 coda — and now the v9 revision built on it — disclose everything §5 reports: the disconnection, the restated theorem, the infeasible target, the summary-layer failure. Its proofs are not impeached, and its dynamics regenerate to tolerance, 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 — and the revision that occurred was the opposite of silent). A reader who weighs §5 and concludes the disclosures are 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, with the history the panel added: 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 on the platform that built it — then fourteen of fifteen at the archive panel, on a different platform, where one cell in 13,600 differed at the fifteenth decimal place against a byte-identity criterion. That is disconfirmer (b) firing, against the harness itself, on exactly the standard Check 7 warns against; the v3 harness replaces byte-identity with a stated tolerance, reports byte-exactness informationally, and returns sixteen of sixteen forensic. The firing stays in the record, repaired rather than erased. A flag key: [F1]–[F7], the envelope’s [F4b], and [R1]–[R4] name check groups, not a running count — twenty-one checks in twelve groups under v3, sixteen forensic and five regression — so there is no F8 to look for. 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 further defect sat beside them — in the remediation package rather than the harness: 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. (Non-mutation then had to be restored once more, at this edition’s pre-commit verification: the draft v3 envelope check wrote its exhibit CSV into the package — the in-place defect, back in the rebuilt instrument — and was set to write outside it before this edition shipped. The log counts instruments that shipped; that draft did not.) None of this is offered as color. It is the instrument’s defect log, kept in place of the base rate a one-case paper is forbidden to supply — one instrument, its author primed by the very thesis under test, its failures caught by the next reviewer every time. The failure mode recurred, immediately, in code written by an author actively writing a paper about it; the log does not pretend to be a sample.

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 result (Theorem 5.4′ in the current edition of EIMTS); 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 the constrained-optimum result — 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 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, and the Blanchard–Kahn counting condition then demands only that no root explode — a condition this code meets at its shipped calibration and, the panel’s sweep established, fails at equality coefficients above roughly 1.7, in 96 of 648 cells: the pass is calibration-specific, not structural. A determinacy-enforcing solver, fed this system as declared, would have simulated it at the published settings without complaint while the paper’s theorem asserted saddle-path stability of a different system — and the transcription into any such solver, from a continuous-time Jacobian, is a step this paper has not run and marks as unrun. 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 the inflation response begins to govern determinacy again — but not at the textbook bound. The coded three-variable system’s saddle boundary is nation-specific: α_π* between 1.12 and 1.40 at the shipped calibrations, derived by bisection on the shipped system itself [R4]. The previous edition wrote “saddle-path stability requires α_π > 1, the standard determinacy condition” — a transported condition, the two-equation textbook bound quoted where the shipped system’s own bound belonged, and Check 2's lesson landing on its own worked example: derive the inequality from the system you shipped. The paper calibrates α_π = 0.5 — a constant in the shipped model file, checkable by inspection, roughly half the smallest coded threshold — and the harness’s demonstration that 0.5 fails and 1.5 attains saddle-path runs on the remediated Jacobian, 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 (standard error 0.07) — and 0.5 sits below even that accommodative, indeterminacy-prone regime, a distance measured against the system’s own bound, since a calibration has no standard errors — 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 shipped code in fact carries two Taylor rules: a standard form whose total nominal response at these settings is Taylor’s own 1.5, and the EIMTS variant the pipeline uses, which omits the one-for-one inflation term — so the sharper diagnosis is a dropped +π in the paper’s equation 5.1, wearing a 1970s calibration’s clothes.) 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 the system’s bound or the theorem is restated as an asymptotic-stability result under adaptive expectations — every determinacy statement here local to the linearization, with the global-indeterminacy literature the standing caveat on promising more (Benhabib, Schmitt-Grohé and Uribe, 2001). (The coda of EIMTS takes the second option and flags the calibration as open; a post-publication package addendum — v4.2, August 2026, carried forward in v4.3 — takes the first, showing the original theorem recoverable at estimated post-Volcker calibrations with a magnitude cost near nine percent. Both options are now on the record.) A counterfactual note, for symmetry with Finding 2, and marked as derivation rather than run: this defect is the one a determinacy-enforcing toolchain would have caught — at α_π = 0.5 the remediated forward-looking system has no unstable root against one jump variable, the eigenvalue signature of indeterminacy, and a Blanchard–Kahn-enforcing solver refuses such a model at the first simulation. The paper has not run that tool on this system; the claim is the arithmetic, not the tool’s observed behavior. EIMTS 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 on the reconstruction swept, and the panel showed the scope is load-bearing. 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 rule ranked on per-capita utility with an equality-index tilt — and “the model’s own instrument” means that reconstruction. The previous edition called it the most favorable reading available to the original paper; the archive panel showed it is not, and showed the scope is load-bearing. The reconstruction ranks transfers on per-capita utility while the objective it faces is an unweighted Gini over aggregate national levels — a basis–objective mismatch of exactly the class the remediation was written to repair — and the frontier moves with the basis. The harness’s envelope check [F4b] therefore sweeps the same machinery under three ranking bases: on the shipped per-capita basis the floor is 0.463; on the v3-style within-nation-Gini basis, 0.397; and on an aggregate-level basis — the one nearest the original code’s own GDP-level scaling — the 0.30 target is reachable, at gross transfers near 47 percent of world GDP, a fiscal scale no polity would survive. Finding 4 is accordingly stated as the envelope it always was: unreachable on the reconstruction the remediation chose, reachable only under a basis and at a scale that convert the target from impossible to absurd — and the mis-specified basis is itself a live join failure inside the remediation package, the fifth in the case’s record, found by the panel doing what §10 prescribes. On the shipped basis, sweeping the transfer-scale cap to its maximum — where realized gross transfers reach roughly two and a half times world GDP, the L1 factor of about 2.6 that an earlier edition’s parenthesis named and its headline then ignored — the global between-nation Gini never falls below 0.4628; at gross transfers of exactly one hundred percent of world GDP the path reads 0.478 — a point, not a floor: the sweep dips to 0.4703 near ninety-one percent gross before rising [F4b]; a figure of 0.5241 printed earlier was the minimum under one particular cap, not the floor; and the nearest feasible targets begin around 0.55, at gross transfers of roughly thirteen to fifteen percent of world GDP (an earlier “six percent” confused the solver’s share parameter with the gross-transfer ratio). [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 reconstruction its remediation chose — 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 — none a join failure under §7's definition, all defects at the seam 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 to tolerance, and audited by a commissioned external review of the code. What each caught is now a matter of record rather than of this paper’s earlier belief: the audit — briefed on mathematical correctness — named the unexercised core and the unreachable theorem in February, from symptoms the author himself supplied; the calibration and the infeasibility survived everything until this paper; and where the join went unexamined was not the audit but the author’s disposition of it — which is §6's subject.

§ VIThe Case, III: The Audit That Found It, and the Author Who Filed It

On February 28, 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. The previous edition of this paper re-scored those findings against what it called the preserved pre-remediation snapshot, concluded that most failed re-execution, and read the audit as an instrument that missed the join because its brief never pointed there. The archive panel dismantled that account, and this section now reports what the record actually contains — under constraints that survive the inversion: no claim about the auditors’ competence is made or implied anywhere in it, the audit’s bottom line was correct, and the auditors have had no opportunity to reply, here or earlier.

First, the artifact. The snapshot the previous edition re-executed — eimts_cge_model.v3-preaudit.bak.py, its label notwithstanding — contains the audit’s own recommended first fix, near-verbatim to the docstring: it is post-remediation code. The audit’s contemporaneous fingerprints — file lengths of 575, 664, and 823 lines; a summary schema whose columns end in 2043 — match nothing in any package the archive holds, because nothing pre-remediation survives: the project’s own status report of March 19, written hours before remediation began, records the February findings as live and unfixed, and the remediation then edited the audited files in place, on March 19 and 20, before the first package was ever cut. The audited artifact was destroyed by its own remediation — a join-hygiene failure in its own right, worth one plain sentence: an audit’s object is evidence, and remediating in place eats it. Every “does not reproduce” in the previous edition is accordingly withdrawn; they were cross-version comparisons presented as auditor error. What replaces re-execution is documentation, and the documentation is unusually good: the project’s March 1 file summary independently records the audited model at 575 lines, and the March 19 status report restates the audit’s findings — γ̄ = 0.00, the unenforced constraint, the blank welfare columns, the money supply computed but unused — as current, nineteen days after the audit and hours before the overwrite.

Second, the findings. Re-run under the audit’s own stated criterion — the saddle-path test, which its text says find_gamma_bar should be reporting — even the preserved post-remediation snapshot yields γ̄ = 0.00 for every nation: the audit’s headline number reproduces, and the 1.6985 the previous edition wielded against it arises only under the disjunctive criterion is_stable = saddle_stable or asymptotic_stable — the precise concealment mechanism Finding 2 catalogues. The previous edition refuted its auditors with the bug it was teaching. The transfer-magnitude item — one percent, against the fifty-nine the preserved code produces — is the record’s one genuine divergence, and with the audited artifact gone it can no longer be adjudicated in either direction; it is recorded, not scored. And the blank-welfare finding, which the previous edition scored as false of its object and prophetic of its author, is now corroborated for its object too — the March 19 status report repeats it of the audited artifact — while remaining prophetic all the same: the remediation package rebuilt the identical defect five months later.

Third, the brief — and this is the finding that inverts the section. The audit’s scope line includes mathematical correctness, and its text performs it: the first item of its executive summary reads “Stability analysis returns all negative eigenvalues (no saddle-path stability detected) - contradicts claimed theoretical properties” — Finding 2, named in February, at the top of the report; a section titled “Mathematical Correctness vs. Movement Chapters” tabulates each chapter equation against its implementing lines; its mechanism table flags equation 5.8 “Formula OK, NOT USED” and equation 5.17 “never called in solve_equilibrium(),” which is Finding 1, named three ways; and its recommendations include verifying the code against the paper’s chapter specifications — a join check, requested in writing, by the instrument the previous edition said was never pointed at the join. The symptoms, moreover, came from the author: the audit’s own problem statement records him reporting that stability showed all eigenvalues negative and that the equilibrium solver might not be implementing the system’s adjustments. So the case’s honest shape is this. The instrument was pointed. It fired. It named two of the four failures. And the failures survived anyway — because the author who commissioned the audit filed its report without acting on it, remediated in place a month later without preserving the evidence, and then, writing a paper about unexamined joins, re-scored the audit against the artifact his own remediation had substituted. The join was never invisible here. It was seen, said, and set aside.

What survives of the previous edition’s structural reading is one sentence, relocated and inverted: an audit finds what its brief points at — and this brief pointed at the join, which is why the audit’s report is the strongest document in the case. The scope-effect conjecture is retired with its projection; §8 records what replaces both. In their place stands the observation the record actually supports, the paper’s thesis at one remove: between a finding and its uptake there is a second join — call it the disposition layer — and no instrument audits that one either. §7 records it as the taxonomy’s first confirmed extension.

§ 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 coded saddle boundary of 1.12 to 1.40 by nation against a calibration of 0.5 — a regime-scale violation rather than a boundary case, and a warning inside the warning: the previous edition quoted the textbook’s “α_π > 1” where the shipped system’s own bound belonged, so even the check’s demonstration needed the check. 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 basis-conditional floor — 0.46 on the reconstruction swept, reachable only under an aggregate-level basis at gross transfers near half of world GDP — 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 — with the policy stated in advance: a hit inside one of the four named gaps confirms a stated limit and does not fire it; a hit outside both the categories and the named gaps does. One such hit is already on the books: the disposition layer §6 reports — a correct detection, filed and unacted — sits outside all four categories and all four named gaps, and the taxonomy is accordingly marked extended rather than intact.

§ 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. Observed, once: applied once in earnest, six of §10's seven checks returned determinate answers — an integer, a satisfied/violated verdict, a frontier and a monotonicity property — none requiring judgment about anyone’s intent; the seventh, Check 6, is a remedy with no verdict space of its own, a miscount the panel corrected. 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. Observed, once: 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, in at least three of any five independently reported applications — which would mean the checklist’s adoptable part is its least informative part.

Projection 3 — detection is not uptake; the disposition layer is the unaudited join. The previous edition projected here that audits find only what their briefs point at, with the falsifier “a code-quality audit in the wild that surfaces a join failure unprompted” — named as the projection the paper would most like to lose. It had lost it before publishing: the falsifying document was the audit in the paper’s own files, and §6 now reports it. The replacement is the projection the record supports. Observed, once: a correct audit finding, delivered to its commissioner, survived unacted for weeks and was then re-scored against a substituted artifact. Assumption: the disposition join — between a finding and its uptake — is unaudited wherever authors commission their own reviews, for the same structural reason the proof–program join is unaudited: it falls between instruments each correctly scoped to something else. Expectation: join failures that get named will still ship, because naming is not uptake. Falsifier: an audit-response artifact — a documented finding-by-finding disposition, of the kind journals require for referee reports and commissioned audits do not — attached to a self-commissioned code audit, in the wild. The check is artifact-gated and third-party decidable: the document exists or it does not. This is now the projection the paper would most like to lose, for the same reason as its predecessor — losing it would mean the discipline needs no new instrument, only its existing paperwork, 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 (the scientific-software defect-rate literature — Hatton and Roberts, 1994; Hatton, 1997 — is the nearest external base rate, cited for the reader’s use and not annexed); 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, plus a fifth in the remediation package (the envelope’s basis mis-specification) and a disposition failure across the whole case; forensic checks separated from regression checks, sixteen of sixteen forensic under the v3 harness after the panel’s clean-room run fired disconfirmer (b) against the v2 harness’s byte-identity criterion; the tolerance-bounded regeneration of the five per-year results files (byte-exact on the original platform), 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, inverted from the previous edition: a brief that included mathematical correctness, two of four findings named in February, a headline number that reproduces under the audit’s own criterion, provenance settled by document — the audited artifact overwritten in place before any package was cut — one magnitude divergence recorded as unadjudicable, and no claim about competence, the failed instrument in the case being its commissioner’s disposition, twice; and the instruments’ own defect log, six entries across two rounds, each found by someone else and reported flatly.

What can be expected (Register P, §8): three projections, each about the instrument rather than the population, each with a falsifier — the third rebuilt in this edition after its predecessor’s falsifier fired from the paper’s own files.

The three disconfirmers of §1, collected here with their status. An existing policy or practice that already requires the question: unfired — two coverage referees have now re-run the corpus at its exact letter, and §3's resizing procedure is stated as the claim’s scope, so a candidate either narrows the claim in the open or fires it, never both silently. A forensic finding that fails to reproduce from the shipped package: fired, by the archive panel, against the v2 harness’s byte-identity criterion — one cell in 13,600, at the fifteenth decimal place — and repaired per Check 7, with the firing kept on the record. A join failure fitting none of the four categories: hit once, at the disposition layer §6 reports, outside the categories and the named gaps alike; the taxonomy is marked extended.

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 the published results of EIMTS 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, its detections are credited in full, the failed instrument on the record is its commissioner’s disposition, 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 instruments failed, the failures are in §5 and §6, found by someone else each time.

§ 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. The case’s own record carries the check’s sharpest lesson: enumerate the shipped system’s conditions — the previous edition wrote “α_π > 1, the standard determinacy condition” where the coded system’s own boundary runs 1.12 to 1.40 by nation [R4]; a transported textbook inequality at the join is the same defect as a transported calibration.

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. (As specified this check is a remedy rather than a test — it has no failure verdict of its own, and Projection 1 counts it accordingly.)

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. The cross-platform caveat is no longer hypothetical: this paper’s own package fired on exactly that standard at its archive panel, and the data editors’ shop documents the same phenomenon in the wild (AEA Data Editor blog, July 2026).

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. To the model-comparison infrastructures, whose replication archives already run the differential version of this check at scale: your forum threads are the nearest thing the discipline has to a join-failure registry, and filing them as theorem–code findings rather than replication issues would populate §7's taxonomy from outside this archive. 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, restored to the record here: 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: the architecture of EIMTS 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 on the reconstruction swept, and which of its numbers reproduce to tolerance, 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, and one thing he had been told and set aside — written down, all of it, precisely enough to be wrong about; some of it already was, and the record now says so.

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 instruments' record. The verification harness has failed four times across two rounds, each failure caught by the next reviewer: v1's NumPy-boolean identity test, vacuous byte-identity pass, and in-place pipeline re-run (pre-archive referee); and v2's byte-identity criterion, fired as disconfirmer (b) by the archive panel's clean-room run, per the paper's own Check 7. Two further defects sat in the remediation package the harness verifies: the summary-rebuild script's blank welfare columns, and the transfer-basis mis-specification the panel's envelope exposed. None is a join failure under §7's definition; all are defects of the checking apparatus; the v3 harness covers each with a check, and the log is kept in place of the base rate the paper may not claim. [§5]

On the audit. The commissioned audit of February 28, 2026 was scoped to code quality, mathematical correctness, and publishability; its verdict was correct, its text named two of this paper's four findings, and its provenance is settled by document rather than by re-execution — the audited artifact was overwritten in place by the March remediation before any package was cut, so the previous edition's re-executions are withdrawn and the one magnitude divergence is recorded as unadjudicable. The failed instrument in the record is the author's disposition of the report. The auditors have had no reply; 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; the audited artifact itself is established unrecoverable and documentarily identified — the project's file summary of March 1 records the model at 575 lines, and its status report of March 19 restates the audit's findings as live, hours before the in-place remediation — so provenance is closed as a question and kept open as a lesson. [§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, the policies of Econometrica, JPE, REStud, QJE, the Economic Journal, and Computational Economics, and the public referee guidelines of the JME, Theoretical Economics, and Quantitative Economics]

American Economic Association Data Editor (2026). The same code, a different answer: Stata convergence across platforms. Data Editor blog, July 24, 2026.

Ankel-Peters, J., et al. (2025). A protocol for structured robustness reproductions and replicability assessments. Q Open, 5(3).

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).

Axtell, R., Axelrod, R., Epstein, J. M., & Cohen, M. D. (1996). Aligning simulation models: A case study and results. Computational and Mathematical Organization Theory, 1(2).

Benhabib, J., Schmitt-Grohé, S., & Uribe, M. (2001). The perils of Taylor rules. Journal of Economic Theory, 96(1–2).

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. (2024). Mass reproducibility and replicability: A new hope. IZA DP 16912. Brodeur, A., et al. (2026). AI-assisted teams outperform AI-led teams but not human-only teams in assessing research reproducibility in quantitative social science. PNAS.

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. (2010). Comparison of solutions to the incomplete markets model with aggregate uncertainty. Journal of Economic Dynamics and Control, 34(1), 4–27.

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.

Ferman, B., & Finamor, L. (2025). There must be an error here! Experimental evidence on coding errors' biases. Institute for Replication DP 266; arXiv:2508.20069.

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.

Hatton, L. (1997). The T experiments: Errors in scientific software. IEEE Computational Science & Engineering, 4(2).

Hatton, L., & Roberts, A. (1994). How accurate is scientific software? IEEE Transactions on Software Engineering, 20(10).

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.

Kamiński, B., & Szufel, P. (2013). LNBIP 158. [the §3 quotation on verification in economic simulation]

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]

Koren, M. (2026). Theorist toolbox: Tools for agent-based LLM-assisted economic theory research. arXiv:2606.22337.

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.

Roache, P. J. (1998). Verification and Validation in Computational Science and Engineering. Hermosa.

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.

Schwer, L. E. An overview of the ASME V&V 10 verification and validation guide. [the §3 slogan; formulation tracing to Roache]

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.

Wieland, V., Cwik, T., Müller, G. J., Schmidt, S., & Wolters, M. (2012). A new comparative approach to macroeconomic modeling and policy analysis. Journal of Economic Behavior & Organization, 83(3), 523–541. [the Macroeconomic Model Data Base and its Rep-MMB replication archive]

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

· · ·

Companion papers in the archive: The Equality-Indexed Monetary-Trade System (EIMTS) — the paper under audit, standing in its v9 edition (revised July 2026 at its own archive panel) with the coda and revision that disclose everything reported here. The forensic base is EIMTS_Replication_v4.3.zip — it unpacks to EIMTS_Replication_v4/, with VERSION.txt identifying the edition: both model versions, the tolerance-reproducing per-year results, both summaries, the transfer-basis envelope, and the v3 reproduction harness — sixteen forensic checks, five 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 and panel shelves, claim outline, taxonomy and checklist, projection set, referee report, and response letters are filed under cowork; the decision memo and six raw reports of the archive panel are filed in the archive itself. 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.

The Proof and the Program.

Abstract

§ IThe Join

§ IITwo Caricatures to Clear

§ IIIWhat the Discipline Already Checks

§ IVThe Case, I: What Was Built

§ VThe Case, II: What Was Found

§ VIThe Case, III: The Audit That Found It, and the Author Who Filed It

§ VIIThe Anatomy of a Join Failure

§ VIIIWhat Can Be Expected

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

§ XThe Checklist

§ XIA Research Program

Notes

References

Slides · accompanying lecture

References

Abstract

§ IThe Join

§ IITwo Caricatures to Clear

§ IIIWhat the Discipline Already Checks

§ IVThe Case, I: What Was Built

§ VThe Case, II: What Was Found

§ VIThe Case, III: The Audit That Found It, and the Author Who Filed It

§ VIIThe Anatomy of a Join Failure

§ VIIIWhat Can Be Expected

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

§ XThe Checklist

§ XIA Research Program

Notes

References

Slides · accompanying lecture

References

Related work