ApplicationStub
plain-language theorem explainer
Four named application targets (Riemann critical line, Navier–Stokes energy transfer, Yang–Mills mass gap, Hodge finite algebraic witness) tag continuum hard problems as stubs for the finite-certificate method. They are labels, not solutions. Anyone citing the quantized proof method or stub obligations uses this enum. The declaration is a plain inductive enumeration with decidable equality.
Claim. There is a finite set of application stub names $\{\mathrm{prime\ critical\ line},\ \mathrm{Navier\text{-}Stokes\ energy\ transfer},\ \mathrm{Yang\text{-}Mills\ mass\ gap},\ \mathrm{Hodge\ finite\ algebraic\ witness}\}$, used only as typed targets for the finite-certificate audit method; equality of names is decidable.
background
In the Primitive Recognition Calculus quantized-proof module, continuum hard problems are not attacked by direct analytic assault. The method first requires a problem audit: a certificate-preserving completion interface that is conservative for legitimate displays and for the relevant pathology or obstruction. Once that audit exists, both good objects and counterexample pathologies reduce to finite certificates (via HasFiniteReduction).
ApplicationStub is the name layer for the first four Millennium-facing entries. The doc-comment is explicit: these are not solutions; they are typed targets. Downstream, every stub is assigned the same obligation shape (StubObligation): supply such an audit. The headline theorem packages the universal finite-reduction fact with a trivial identity over all stubs, marking the stubs as placeholders until concrete audits land.
Local setting is foundation-level method design, not a claim about any of the four analytic problems themselves.
proof idea
No proof body: this is an inductive enumeration of four constructors, deriving DecidableEq and Repr. There is nothing to reduce or discharge. Downstream code pattern-matches on the constructors or quantifies over all stubs (as in the headline theorem’s second conjunct).
why it matters
The enum is the typed hook that lets the quantized proof method talk about Millennium-facing problems without pretending they are solved. StubObligation is defined on this type (currently the trivial proposition, same for every stub). The headline theorem quantized_proof_method_headline states that every problem audit has a finite reduction and that stub obligations are well-formed over all ApplicationStub values; its doc-comment says the Millennium-facing entries remain application stubs until concrete audits are supplied.
It also appears in the dependency fan-in of stronger closure packaging (StrongClosureCertificate in the Delta-native strong closure module), where certificate registries and closure entries are assembled. In Recognition Science terms this sits upstream of any claim that continuum pathologies (mass gap, critical zeros, blowup, Hodge cycles) have been reduced to finite certificates on the recognition register; the stubs mark open audit work, not completed forcing-chain steps (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.