PrimeCriticalLineCert
plain-language theorem explainer
Finite inventory of certificate kinds for the prime-critical-line (Riemann) audit in the hard-problem certificate layer. Three tags: finite prime window, Euler-product balance ledger, and zero-obstruction witness. Downstream audits, displays, and completions index on this type. Pure inductive definition with decidable equality; no proof content.
Claim. An inductive type enumerating the finite set of certificate kinds for the prime-critical-line audit: a finite-prime-window certificate, an Euler-product balance-ledger certificate, and a zero-obstruction witness certificate. Equality of constructors is decidable.
background
The module HardProblemCertificateAudits packages Recognition Science's audit layer for classical hard problems (prime critical line, Navier-Stokes energy, Yang-Mills gap, Hodge). Each problem gets a small inductive certificate inventory, a display record, and a ProblemAudit that separates legitimate certificates from pathologies.
Here the inventory is for the prime-critical-line bridge: certificates that a finite prime window, an Euler-product balance ledger, or a zero-obstruction witness has been produced. Sibling inventories (NavierStokesEnergyCert, YangMillsGapCert, HodgeAlgebraicCert) follow the same pattern. The module imports the quantized proof-method scaffolding used to attach analytic displays to these tags.
Upstream edges touch finite-dimensional Hamiltonian emergence, universal forcing self-reference meta-certificates, and Regge TT hinge geometry; those supply ambient RS structure, not the constructors themselves.
proof idea
Definitional inductive type, not a proved theorem. Three nullary constructors name the allowed certificate kinds; DecidableEq and Repr are derived automatically. No tactics, no lemmas, no sorry.
why it matters
Gives the prime-critical-line audit a closed, finite tag set so every audit path is exhaustive and machine-checkable. Downstream: primeCriticalLineAudit is the identity audit on this type; primeCertifiedDisplayAudit and primeAnalyticAudit / primeAnalyticCompletion wrap it with certified and analytic displays (PrimeAnalyticDisplay carries the cert plus window radius, balance depth, and zeta-style payload). Parallel certificates for NS, YM, and Hodge sit beside it, so the hard-problem layer stays uniform.
In the RS forcing picture this is bookkeeping for a bridge claim (critical-line / zero obstruction), not a step of T0-T8. It does not settle the Riemann hypothesis; it only names what a finite certificate would have to look like inside the audit API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.