hodgeCertifiedDisplayAudit
plain-language theorem explainer
Specializes the certified-display audit interface to the Hodge algebraic-witness problem: native certificates are the finite Hodge inventory, displays are certified continuum tags carrying those certificates. Cited by the four-problem finite-reduction headline. One-line application of the generic certified-display audit constructor to Hodge cert and payload types.
Claim. The Hodge algebraic-witness audit is the problem audit whose native certificate type is the finite Hodge inventory (cycle ledger, algebraic witness, transcendental obstruction), whose display objects are certified displays pairing those certificates with Hodge display payloads (cohomology class, algebraic cycle, transcendental class), and whose finite certificate type is again that inventory.
background
In the Primitive Recognition Calculus hard-problem audits, each classical open problem is given a finite certificate inventory and a continuum-facing display layer. A certified display pairs a native certificate with a payload tag; the certificate alone confers audit authority. The Hodge inventory has three constructors: finite cycle ledger, algebraic witness, and transcendental obstruction witness. Payloads tag cohomology-class, algebraic-cycle, or transcendental-class displays.
The generic constructor certifiedDisplayAudit builds a ProblemAudit from any certificate and inhabited payload type: completion maps certificates to default certified displays, legitimacy and pathology are the display-level predicates, and legitimacy is conservative over the native certificate layer. The module headline states that this is the correct Delta bridge shape for later analytic interfaces, not a solution of the four problems.
proof idea
One-line wrapper: instantiate the generic certified-display audit at the Hodge certificate inductive and the Hodge display-payload inductive. No extra obligations; both types are decidable and the payload is inhabited (default cohomology-class display), so the generic fields (completion, legitimacy, pathology, conservative legitimacy) specialize immediately.
why it matters
Feeds the conjunction in certified_display_audits_headline, which asserts finite reduction for the prime, Navier–Stokes, Yang–Mills, and Hodge certified-display audits. That headline is the module’s claim that every admissible hard-problem display now carries an explicit finite certificate and that the finite-reduction theorem applies uniformly. In the Recognition framework this is scaffolding for a Delta bridge from finite ledger witnesses to continuum statements (Hodge algebraic cycles vs transcendental classes), not a proof of the Hodge conjecture. It sits beside the sibling audits for the other three hard problems and keeps the identity-only interface from being the only display path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.