hodgeAnalyticAudit
plain-language theorem explainer
Packages the Hodge algebraic-witness stub into a full ProblemAudit: completion map, legitimacy and pathology predicates, plus their conservativeness proofs. Anyone citing the four hard-problem analytic audits will pull this record. The body is a pure field assembly wiring the prebuilt completion and the two projections of the conservativeness theorem.
Claim. The Hodge analytic audit is the problem-audit triple whose certificate type is the finite Hodge algebraic inventory (finite cycle ledger, algebraic witness, or transcendental obstruction witness), whose display type carries a certificate together with complex dimension, cohomological degree and a Hodge display payload, and whose completion, legitimacy, pathology and conservativeness fields are the corresponding Hodge-analytic constructions.
background
The module HardProblemCertificateAudits equips four classical open problems (prime critical line, Navier–Stokes energy, Yang–Mills mass gap, Hodge) with a uniform audit schema: a finite certificate inventory, a domain-specific analytic display record, and a ProblemAudit that ties completion, legitimacy and pathology together under a conservativeness obligation.
For Hodge, the certificate inventory is the inductive type with three constructors: finite cycle ledger, algebraic witness, and transcendental obstruction witness. The display record adds complex dimension, cohomological degree and a display-payload tag (e.g. cohomology-class display). Completion sends each certificate to a default display that re-embeds the same certificate; legitimacy and pathology are native predicates on displays, later refinable by genuine analytic arguments.
Upstream, the conservativeness theorem states that both predicates are conservative for that completion: every legitimate or pathological display is certified by its own certificate field. The present definition simply installs those pieces into the ProblemAudit structure.
proof idea
Not a proof: a structure-value definition. The completion field is set to the already-defined Hodge analytic completion (display of a cert is the default cohomology-class display with that cert; certifies is equality of certs). Legitimacy and pathology are the named Hodge analytic predicates. The two conservativeness fields are the left and right projections of the conjunction proved by hodgeAnalytic_conservative (each direction is an intro that recovers d.cert with rfl).
why it matters
This is the Hodge leg of the four hard-problem analytic audits. Downstream, domain_specific_analytic_audits_headline asserts that the prime, Navier–Stokes, Yang–Mills and Hodge analytic audits all admit finite reductions; the Hodge conjunct is obtained by applying the generic problemAudit_finiteReduction lemma to this record.
The headline doc-comment is explicit: the reductions still do not solve the problems; they fix the exact display interface that future analytic proofs must refine. In the Recognition framework this sits in the foundation layer as scaffolding for a bridge from algebraic-cycle data to the recognition calculus, not as a claim that the Hodge conjecture is settled. It parallels the other three domain audits and keeps the certificate inventory finite so that later forcing-chain or ledger arguments can treat Hodge witnesses uniformly with the rest of the hard-problem suite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.