\section{Toward a Computational Thermodynamics} \label{sec:comp-thermo} As established above, total/strongly normalizing calculi gain verification power at the price of general recursion, while reflection and metaprogramming gain flexibility at the cost of global guarantees. The natural question is whether other \emph{computational formalisms} exhibit analogous tradeoffs once they are pushed toward physical or mathematical fidelity. \medskip We emphasize that any such analogy is \emph{discipline-dependent}: what counts as ``expressiveness,'' ``verifiability,'' and ``tractability'' depends on the computational regime under study. The EVT thesis here is not a literal transfer of PL theorems to physics, but a claim that similar boundary phenomena recur when one demands (a) a rich model class, (b) controlled guarantees, and (c) feasible computation. \subsection{Lattice Gauge Theory} \label{sec:lattice-gauge-theory} Lattice gauge theory provides a particularly clear case study. It is a computational formalism for nonperturbative quantum field theory: one discretizes spacetime, integrates over large configuration spaces, and attempts to recover continuum observables with controlled systematic errors. \paragraph{A computational reading.} In an EVT-like translation: \begin{itemize} \item \textbf{Expressiveness} corresponds to the richness of the modeled dynamics: gauge fields with (in the continuum) infinitely many degrees of freedom, strong coupling phenomena, and path-integral expectation values over large configuration spaces. \item \textbf{Verifiability} corresponds to the ability to make \emph{controlled} claims: continuum extrapolations, finite-volume systematics, renormalization, and reproducible uncertainty quantification. \item \textbf{Tractability} corresponds to whether the resulting computation is feasible: sampling/mixing time, variance, and asymptotic cost as one approaches physically relevant regimes. \end{itemize} The point is not that lattice gauge theory is ``a programming language,'' but that it is a structured computational pipeline whose costs and guarantees interact in systematic ways. \paragraph{Where the wall appears.} As one pushes toward physically faithful regimes (large volumes, small lattice spacing, light quark masses, and/or finite density), costs can deteriorate sharply. A well-known obstruction is \emph{critical slowing down} toward the continuum limit: autocorrelation times grow rapidly, and the slowest modes are often topological, leading to severe sampling difficulties and ``topological freezing'' in practice \cite{SchaeferSommerVirotta2011CriticalSlowingDown}. A second obstruction is the \emph{sign problem} for many fermionic systems (notably at finite chemical potential), for which a generic cure would imply polynomial-time solutions to NP-hard problems; Troyer and Wiese formalize this as an NP-hardness barrier \cite{TroyerWiese2005SignProblem}. These are not mere implementation bugs: they behave like thermodynamic walls in the computational sense, where increasing model fidelity and maintaining controlled errors drive the required resources out of practical reach. \paragraph{EVT-style moral.} The pattern is reminiscent of the earlier ``burden-shifting'' failure narratives: one can maintain correctness (faithful modeling and controlled systematics) and verifiability (quantified uncertainties) while retaining a rich expressive model class, but the irreducible difficulty reappears as exploding computational cost and method burden. The working physicist pays the price in algorithmic sophistication and computational budgets, even when the underlying formalism remains conceptually clean. \paragraph{Relief valves: structure and geometry.} There are, however, important exceptions where new structure changes the computational landscape. The amplituhedron program is a striking example: by exploiting special symmetry and restricting to a highly structured corner (planar $\mathcal{N}=4$ super Yang--Mills), it recasts certain scattering amplitude computations in terms of positive geometry, dramatically reorganizing and often simplifying what looks combinatorially explosive in standard representations \cite{ArkaniHamedTrnka2014Amplituhedron}. From the EVT perspective, the lesson is not that ``geometry magically defeats complexity,'' but that \emph{tractability is recovered by moving to a structured subregime}: one trades generality of the theory class for a representation in which verification and computation become more coherent. \medskip \noindent This is the sense in which lattice gauge theory supports a broader ``computational thermodynamics'' viewpoint: when a formalism is simultaneously expressive and verification-driven, some notion of computational feasibility typically becomes the limiting resource, and genuine breakthroughs often come from finding hidden structure that effectively reduces the state space one must traverse. \subsection{Numerics and PDEs} \label{sec:numerics-pdes} Numerical analysis for PDEs offers a near-perfect ``computational thermodynamics'' analogy: one often trades admissible dynamics, invariants, and guarantees against feasible update rules and stable step sizes. \paragraph{A computational reading.} In an EVT-like translation: \begin{itemize} \item \textbf{Expressiveness} corresponds to the class of phenomena one attempts to simulate (shocks, turbulence, stiff source terms, multiscale structure, long-time dynamics). \item \textbf{Verifiability} corresponds to enforced properties of the discrete evolution (stability, convergence, conservation laws, monotonicity/entropy conditions, time reversibility, long-time energy behavior). \item \textbf{Tractability} corresponds to feasible step sizes and computational cost (time-step restrictions, stiffness barriers, solver complexity). \end{itemize} \paragraph{Stability walls (CFL-type constraints).} For explicit schemes applied to hyperbolic problems, stability typically demands that the numerical domain of dependence include the physical domain of dependence; this yields Courant--Friedrichs--Lewy (CFL) type constraints that upper-bound the timestep as a function of grid spacing and characteristic wave speed \cite{CourantFriedrichsLewy1928}. In practice, increasing resolution or wave speed can force $\Delta t$ to shrink dramatically, so that seeking higher fidelity and stronger stability guarantees drives cost upward. \paragraph{Structure-preserving schemes: invariants at a price.} In Hamiltonian and reversible dynamics, \emph{geometric numerical integration} aims to preserve qualitative structure (symplectic form, reversibility, modified energies) over long times \cite{HairerLubichWanner2006GNI}. These methods often improve long-time reliability, but they also restrict admissible updates (e.g.\ to symplectic maps or splitting/composition forms) and may complicate implementation or require implicit solves. Conversely, aggressive damping or stabilization can make computations robust and easy to run, but it typically destroys time-reversal symmetry and fine invariants that one might have wished to verify. The ``thermodynamic'' moral is the same: enforcing stronger global guarantees generally constrains the update dynamics or shifts cost elsewhere. \subsection{Many-body Systems and Field Theory} \label{sec:many-body} Many-body physics provides a final instructive analogy. Certain ``integrable'' corners admit exact charges and factorization, but these corners are structurally special; generic regimes are expressive yet analytically resistant. In the extreme, some semantic properties of dynamics are not decidable uniformly. \paragraph{Integrable corners: high verifiability in measure-zero regimes.} Exactly solved models (e.g.\ those accessible via Bethe ansatz/quantum inverse scattering techniques) exhibit extraordinary structure: large families of conserved quantities, factorized scattering, and exact formulas for spectra and correlation functions \cite{Baxter1982ExactlySolved, KorepinBogoliubovIzergin1993QISM}. In an EVT-like reading, this is a regime where verifiability is unusually high because the dynamics sit inside a rigid algebraic scaffold. But these regimes occupy a thin subset of parameter space: the techniques do not extend uniformly once one perturbs away from integrability. \paragraph{Generic regimes: expressiveness without uniform semantic control.} Away from integrable structure, the space of possible many-body behaviors becomes vastly richer (phases, excitations, long-range entanglement structure), but general analytic classification becomes correspondingly difficult. This is not merely a matter of ``we have not found the right trick yet'': formal barriers are showing that certain global questions about dynamics cannot be decided by a uniform algorithm over all models. \paragraph{Undecidability as a semantic barrier.} A sharp illustration is the \emph{spectral gap problem}: given a local, translation-invariant Hamiltonian on an infinite lattice, determine whether it is gapped or gapless in the thermodynamic limit. Cubitt, P{\'e}rez-Garc{\'\i}a, and Wolf prove that this problem is undecidable in general \cite{CubittPerezGarciaWolf2015SpectralGap}. This is a direct analogue of the ``semantic undecidability'' pressure that motivates EVT on the PL side: beyond a certain expressive regime, there is no uniform procedure that can always decide nontrivial global properties of the system. \medskip Examples abound. Though a full examination of artificial intelligence systems is beyond the scope of this work, it bears mentioning that recent work by Floridi \cite{floridi2025conjecture} suggests an analogous tradeoff may even infect the logic of AI systems. \medskip The three case studies above are not meant to ``prove'' the EVT in physics, but to motivate a broader stance: whenever a formalism is asked to be simultaneously rich (expressive), controlled (verifiable), and usable (feasible in computation and practice), it tends to develop boundary phenomena and recognizable failure modes. In the remainder of this paper, we return to programming languages and make this intuition operational via \emph{resource theory}: a framework for treating expressiveness, verifiability, and their certificates as resources with conversion laws, monotones, and obstructions. \subsection{Resource Theory and the Future of the EVT Hypothesis} \label{sec:future-resource-theory} Resource theories (in the broad sense developed in categorical quantum mechanics and related work) provide a natural formal language for turning ``tradeoffs'' into mathematically tractable structure: one specifies a class of \emph{free operations}, a notion of \emph{convertibility} between resources, and \emph{monotones} that witness impossibility of certain conversions \cite{CoeckeFritzSpekkens2016ResourceTheory,AbramskyCoecke2004CategoricalQM}.\footnote{We treat this as future work; the present paper is intended to stand independently without committing to a specific categorical formalization.} \paragraph{Future direction.} A resource-theoretic EVT program would proceed in stages. \begin{enumerate}[leftmargin=2.2em] \item \textbf{Choose the resource objects.} Model a ``language design'' (or a fragment) as an object carrying: (a) an expressiveness signature (available constructs/abstractions), (b) a verification discipline (types/certificates and their checking relation), and (c) a compilation/evaluation interface. Alternatively, treat \emph{programs and certificates} as the primary resources and languages as resource-generating environments. \item \textbf{Specify free operations.} Identify transformations that should not count as ``consuming'' the resources we wish to measure, e.g.: \begin{itemize} \item conservative syntactic refactorings/definitional expansions, \item macro-eliminations that preserve observational semantics, \item certificate translation that preserves soundness with bounded overhead, \item admissible compiler elaborations and erasures. \end{itemize} The goal is to formalize ``same computational content'' versus ``genuine increase in expressive or verification power.'' \item \textbf{Define convertibility preorders.} Expressibility and verifiability subsumption then become instances of resource convertibility: \[ \mathbf{L}_0 \to \mathbf{L}_1 \quad\text{meaning}\quad \mathbf{L}_1\ \text{can simulate/host}\ \mathbf{L}_0 \ \text{under the free operations.} \] The $E$- and $V$-preorders of this paper should arise as induced orders from this conversion structure. \item \textbf{Identify monotones (``thermodynamic potentials'').} Develop quantities that are monotone under the free operations and therefore certify impossibility results: candidates include bounded derivation/certificate complexity measures, width/structure measures for dependency graphs, and other invariants of the compilation--checking--evaluation pipeline. These monotones would play the role of ``resource potentials'' that cannot increase for free. \item \textbf{Recover the frontier and failure modes as no-go theorems.} Recast the EVT boundary as a statement about non-convertibility: certain simultaneous upgrades in expressiveness and verifiability are impossible without consuming additional resources (proof burden, compilation cost, or comprehensibility). The three failure modes (correctness, compilability, comprehensibility collapse) would correspond to distinct ways of relaxing the free-operation constraints or admitting additional ``unpaid'' resources (oracles, trusted automation, human proof labor). \item \textbf{Connect to categorical semantics.} Once a stable resource formulation exists, one can integrate it with categorical models of computation and process theories: viewing programs as morphisms, compilation as functors, and certificates as structured morphisms/2-morphisms, with EVT monotones arising from functorial invariants. \end{enumerate} \paragraph{Status.} We view this resource-theoretic program as the most promising route to turning EVT from a collection of boundary phenomena into a compositional calculus of tradeoffs. However, executing it cleanly requires careful choices of free operations and categorical setting, and is best undertaken with specialist input. Accordingly, we leave it as future work and focus here on establishing the order-theoretic and fixed-point/undecidability foundations that any such resource theory must respect. \medskip \paragraph{Closing Remarks on the EVT Hypothesis.} Proving the expressiveness/verifiability tradeoff for finite state, non-Von Neumann, or geometric models is an exercise suitable for graduate coursework. Extending the result to full Von Neumann architectures and modeling the curve between programming languages is the realm of doctoral dissertations or collaborations between professional research mathematicians and computer scientists with backgrounds in human-computer interaction. But to prove the general EVT Hypothesis at the categorical level, capturing all forms of computation, digital or analog? \medskip That would require mathematical insight worthy of a Fields Medal. \newpage \appendix \section{Disclosures} \subsection*{Funding Sources} None. \subsection*{Conflicts of Interest} None. \subsection*{Data Availability} There is no associated data with this manuscript. \subsection*{AI Contributions and Acknowledgments} OpenAI ChatGPT was used as a writing assistant during the development of this work.