HasFiniteReduction
plain-language theorem explainer
A continuum problem audit admits a finite-certificate reduction when every legitimate object and every pathology is witnessed by some finite certificate under the audit's completion map. Anyone wiring hard-problem stubs (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge) into the Delta audit layer cites this predicate. It is a pure Prop definition: the conjunction of two universal–existential certificate conditions.
Claim. Let $A$ be a Delta audit of a continuum problem, with domain type $D$, certificate type $\mathrm{Cert}$, and completion map. Then $A$ has a finite-certificate reduction if (i) every legitimate $d\in D$ is certified by some $c\in\mathrm{Cert}$, and (ii) every pathological $d\in D$ is likewise certified by some $c\in\mathrm{Cert}$.
background
In the Primitive Recognition Calculus, continuum problems are not attacked directly. They are packaged as a ProblemAudit: a completion (bridge from a finite name type $N$ into domain objects $D$ with certificates $\mathrm{Cert}$), plus two predicates on $D$ (legitimate objects and pathologies), each required to be conservative for that completion.
Conservativity means the predicates respect the completion's certificate discipline: membership cannot jump without a certificate witness. The finite-reduction property strengthens that discipline to a full covering statement: every legitimate case and every pathology must actually possess a certificate.
The surrounding module builds a quantized proof method for hard continuum questions. Upstream constants such as spatial dimension $D=3$ (T8) and active-edge count appear only as ambient RS landmarks; they are not parameters of this predicate.
proof idea
Definitional, not a proved theorem. The body is the conjunction of two quantified statements over the audit's domain: legitimate objects descend to certificates, and pathologies descend to certificates, both via the audit's completion certifies relation. No tactics or lemmas are invoked; downstream theorems discharge the predicate by applying the generic lemma that every well-formed problem audit satisfies it.
why it matters
This predicate is the common target of the hard-problem certificate audit layer. Downstream headlines assert it for four Millennium-style stubs (prime critical line, Navier–Stokes energy, Yang–Mills mass gap, Hodge algebraic cycles), and again for certified-display and domain-specific analytic audit variants.
Those headlines are explicit that the reductions are audit schemas, not solutions: they fix the Delta bridge shape so later analytic interfaces can refine certificates without changing the reduction contract. In the Recognition framework this sits under the Primitive Recognition Calculus, separating finite certificate bookkeeping from continuum analysis, consistent with the forcing-chain discipline that keeps continuum claims pinned to discrete witnesses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.