This book presents a reproducible method for checking the chain from assumptions to claims, proofs, computations, and public artifacts. Six self-contained case studies show how the method works across selection, simulation, dynamics, demand, set-valued choice, and inverse problems.
A research audit begins by fixing the object under review. Titles, filenames, and repository labels can survive substantive revisions, so each source needs a version record. A claim ledger then connects quoted propositions to assumptions, proof locations, code paths, data inputs, and the auditor's residual conclusion.
A proof is a sequence of typed implications. Every arrow has a domain, quantifiers, fixed and varying objects, and a conclusion. Auditing the arrows often reveals that a result combines a valid component with an unsupported extension, allowing the conclusion to be narrowed without discarding the surrounding argument.
A useful counterexample preserves the disputed assumptions and changes only enough structure to reverse the claimed conclusion. Small state spaces, discrete shocks, or low-dimensional operators expose the mechanism. An economic implementation then shows that the mathematical witness belongs to the model class rather than to an unrelated abstraction.
Computation can reveal a mechanism, refute a universal statement through an exact witness, or support a bounded certificate. These roles require different evidence. Floating-point roots, ranks, and optimizer statuses are diagnostics unless error bounds, exact arithmetic, intervals, or primal-dual arguments turn them into guarantees.
A printed equation becomes a computational result through a chain of data transformations, functions, branches, and parameters. The audit follows that lineage from economic primitives to final output and checks whether normalizations, support restrictions, derivative formulas, and approximation choices remain invariant along the path.
A computational chapter should tell readers what it proves, what it illustrates, which inputs it uses, and how to rerun it. Environment locks, source manifests, deterministic seeds, tests, and clean execution turn a collection of files into a reproducible artifact. Web display and executable computation remain distinct delivery modes.
A symmetric vector of shocks can have zero mean coordinate by coordinate while a statistic selected using those shocks has a nonzero expectation. The distinction between a fixed order statistic and a shock-dependent selected statistic is the central audit object in boundary moment inequalities and other post-selection arguments.
Simulation-based dynamic estimators involve the sample size, the number of simulated alternatives or paths, and the number of draws per object. Root-n inference depends on their joint rates. A simulated first stage can add variance or bias to the score even when the population target remains unchanged.
Signed interactions, exact root counts, and observable modes address different questions in dynamic networks. Replacing a signed system by absolute coefficients can yield a useful sufficient contraction condition, yet it may discard cancellations. Repeated roots further require a generalized-mode calculation, with transfer-function cancellation checked separately.
The case compares an exact residual-income utility with a linear price implementation. The two specifications can agree near a base point while producing different affordability, derivatives, purchaser moments, markups, and welfare away from it. The audit follows that difference through the full computational chain.
Channel bundles can be valued by solving a viewing-time problem for each set. Replacing those set values with increments calculated at a reference bundle is exact only under modularity or a corresponding structural restriction. Bargaining and welfare then require the same set-value function and consumer shock law used for demand.
Nonclassical measurement models use conditional operators to connect latent variables and repeated measurements. Candidate-specific invertibility does not automatically permit similarity transforms across candidates, shared spectral projections, or inverse action on reconstructed probabilities. A wrapped-Gaussian witness makes the range and stability problems visible in Fourier coordinates.