primeAnalyticAudit
plain-language theorem explainer
Packages the prime-critical-line hard-problem stub as a full problem audit: finite certificate inventory, analytic display record, vacuous legitimacy and pathology predicates, and conservativeness of both. Anyone citing the domain-specific analytic audits headline uses this object. The body is pure structure assembly from already-proved field witnesses.
Claim. The prime-critical-line analytic audit is the problem audit on the finite certificate set $\{\text{finite prime window},\ \text{Euler-product balance ledger},\ \text{zero-obstruction witness}\}$ with display type carrying a certificate, prime-window radius, balance depth, and payload, whose completion maps each certificate $c$ to the display $\langle c,0,0,\zeta\text{-display}\rangle$ certified by equality of certificates, whose legitimacy and pathology predicates are both $\top$, and whose conservativeness recovers the underlying certificate from any display.
background
In the Primitive Recognition Calculus hard-problem audit layer, each classical open problem is given a finite certificate inventory and a domain-specific analytic display, then wrapped as a ProblemAudit. For the prime-critical-line bridge the inventory is three constructors: a finite prime window, an Euler-product balance ledger, and a zero-obstruction witness. The display record stores the certificate together with a prime-window radius, a balance depth, and a payload kind (here the zeta display).
Upstream, primeAnalyticCompletion supplies the display map $c\mapsto\langle c,0,0,\zeta\text{-display}\rangle$ and the certification relation $c=d.\mathrm{cert}$. The predicates PrimeAnalyticLegitimate and PrimeAnalyticPathology are both constantly true. Conservativeness of both predicates relative to that completion is the conjunction proved by primeAnalytic_conservative: from any display one recovers its certificate with a reflexivity witness.
The local module only organises these named pieces; it does not claim a solution of the Riemann hypothesis or any zero-free region.
proof idea
Definitional structure fill-in, not a tactic proof. The five fields of the problem-audit record are assigned directly: completion to primeAnalyticCompletion, legitimate and pathology to the constantly-true predicates, and the two conservativeness obligations to the left and right projections of the already-proved conjunction primeAnalytic_conservative. No further rewriting or case analysis occurs.
why it matters
This audit is the first conjunct of domain_specific_analytic_audits_headline, which asserts that the four hard-problem stubs (prime-critical-line, Navier-Stokes energy, Yang-Mills gap, Hodge algebraic) each possess a named analytic display with certificate fields and domain-specific parameters and therefore admit a finite reduction. The downstream doc-comment is explicit: the reductions still do not solve the problems; they fix the exact display interface that future analytic proofs must refine.
Inside Recognition Science the construction sits in the foundation layer that turns classical hard problems into finite certificate audits compatible with the quantized proof method. It does not invoke the forcing chain (T5–T8), the Recognition Composition Law, or the mass ladder; it only supplies the audit shell those later analytic refinements would inhabit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.