primeCriticalLine_finiteReduction
plain-language theorem explainer
The prime-critical-line audit admits a finite-certificate reduction: every legitimate object and every pathology is witnessed by some finite certificate. Anyone citing the hard-problem audit headline (the four Millennium-style stubs) depends on this fact. The proof is a one-line wrapper of the generic problem-audit finite-reduction lemma.
Claim. The identity audit attached to the prime-critical-line certificate satisfies the finite-reduction property: for every legitimate datum $d$ there exists a finite certificate $c$ that certifies $d$, and likewise for every pathology.
background
In the quantized-proof layer, a continuum problem is packaged as a ProblemAudit with three type parameters (nominal objects, data, certificates) together with predicates for legitimate objects and pathologies, and a completion map that issues certificates. Finite reduction means both classes descend to finite certificates: legitimate data and pathologies are each witnessed by some certificate under the completion.
The prime-critical-line audit is the identity audit on the prime-critical-line certificate type: legitimate and pathology predicates, and the completion, are all the identity certificate structure for that stub. The generic lemma problemAudit_finiteReduction already shows that every such audit has the finite-reduction property, via a conservative transfer of certificates from the completion.
Local module setting: hard-problem certificate audits for four named stubs (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic). These are audit schemas, not continuum solutions.
proof idea
One-line wrapper. Apply the generic theorem that every ProblemAudit has finite reduction (itself a call to finite-certificate transfer on the audit's completion, legitimate predicate, pathology predicate, and the two conservativity hypotheses built into the audit). Specialize to the prime-critical-line identity audit. No extra case analysis.
why it matters
Feeds the hard-problem audit headline, which conjoins finite reduction for all four application stubs (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic). The headline's own doc-comment stresses the point: these are audit schemas with concrete finite certificate inventories, not solutions of the underlying continuum problems.
Inside Recognition Science this sits in the Primitive Recognition Calculus foundation layer: it records that the prime-critical-line stub is certificate-auditable in the finite sense required by the quantized proof method. It does not touch the forcing chain (T0–T8), the Recognition Composition Law, or the mass ladder; it is infrastructure for treating hard analytic problems as certificate problems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.