What is 'certified hyper-optimization' in one sentence?	Untrusted search plus a kernel-checked correctness certificate: let any aggressive optimizer (a superoptimizer, an LLVM backend, a frontier LLM) propose fast code, then prove in a minimal trusted kernel that the proposal is observationally equivalent to the original. If the proof checks, the fast code ships with the certificate; if not, it's discarded.
Why is this a category and not a feature?	Because of an asymmetry in where value accumulates. Capability is *rented* (you can swap in the world's best optimizer at any time) and *improving* (LLMs get better, free for you). Trust is *owned* and *fixed* (the kernel and metatheory don't grow). Competitors' optimizer improvements become your improvements the moment you wrap them. A feature gets out-shipped; a category that turns everyone else's progress into your moat compounds.
Why is EVM bytecode the beachhead — what are the three conditions?	Where it pays, three conditions converge: (1) hot/amortized — the code runs enough times that an expensive prove-once compile pays for itself; (2) correctness is expensive to get wrong — a miscompile costs real money; (3) optimization is hard and high-stakes. EVM is the extreme case of all three: immutable bytecode (prove once at deploy), billions of executions, every op gas-metered (so every saved opcode is denominated money).
What is the central commercial tension the analysis names instead of hides?	The EVM fee pool we'd price against is partly deflationary by protocol design — per-unit gas fell ~95% from 2024 peaks. The thesis survives on the legs that *don't* deflate: execution-client COGS (sequencer/RPC CPU is real money regardless of gas price) and zkVM proving cost (linear in executed instructions, so every optimized instruction is directly monetizable). Deploy-time end-user-gas pricing is the weakest, first-to-be-killed leg.