problemAudit_finiteReduction
plain-language theorem explainer
Every continuum problem packaged as a Delta audit automatically admits a finite-certificate reduction: legitimate objects and pathologies both descend to finite certificates under the audit's completion. Hard-problem audit schemas (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge) cite this as the uniform reduction step. The proof is a direct term application of the finite-certificate transfer headline to the audit's conservative fields.
Claim. Let $N$, $D$, and $\mathrm{Cert}$ be types. Given a problem audit $A$ consisting of a completion $C$ of continuum data $D$ by certificates $\mathrm{Cert}$, together with predicates $\mathrm{legitimate}$ and $\mathrm{pathology}$ on $D$ that are both conservative for $C$, both of the following hold: every legitimate $d\in D$ is certified by some $c\in\mathrm{Cert}$, and every pathological $d\in D$ is certified by some $c\in\mathrm{Cert}$.
background
In the Primitive Recognition Calculus, a continuum problem is audited by packaging a completion (a bridge from continuum objects $D$ to finite certificates $\mathrm{Cert}$) with two predicates: legitimate objects and pathologies. Conservativity means each predicate is stable under the completion's forgetful map, so continuum truth cannot appear or vanish without a certificate-level witness.
HasFiniteReduction is the Prop that both predicates descend: every legitimate continuum object and every pathology is hit by some certificate under the completion's certifies relation. The module sits downstream of FiniteCertificateTransfer, whose headline states that for any conservative completion, valid continuum witnesses and valid continuum obstructions both descend to finite certificates. That transfer is the formal hinge of the quantized-proof method.
Spatial dimension $D=3$ (forced by T8) and the eight-tick register appear elsewhere in the foundation stack; this declaration itself is type-parametric and does not fix those constants.
proof idea
One-line term wrapper. Unpack the five fields of the problem audit (completion, legitimate, pathology, and the two conservativity proofs) and feed them to finite_certificate_transfer. That upstream theorem returns the conjunction of the two descent statements, which is exactly HasFiniteReduction. No extra rewriting or case analysis.
why it matters
This is the uniform reduction lemma for every hard-problem audit in the stack. Downstream, primeCriticalLine_finiteReduction, navierStokesEnergy_finiteReduction, yangMillsGap_finiteReduction, and hodgeAlgebraic_finiteReduction are each one-line applications of it; the certified-display and domain-specific analytic audit headlines conjoin the four instances. The quantized-proof-method headline also depends on it.
The parent docs are explicit: these are audit schemas and Delta bridge shapes, not solutions of RH, Navier–Stokes regularity, the Yang–Mills mass gap, or Hodge. The declaration closes the generic half of the finite-certificate method so later analytic interfaces only need to supply a concrete conservative completion and the two predicates. It touches the scaffolding path for the four Millennium-style stubs without claiming any continuum theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.