HodgeAlgebraicCert
plain-language theorem explainer
Finite inventory of algebraic certificate kinds used to audit the Hodge problem in the Recognition certificate schema: finite cycle ledger, algebraic witness, and transcendental obstruction witness. Downstream audits treat every such certificate as schema-legitimate by identity, then refine via analytic displays. The declaration is a pure inductive enumeration with decidable equality; no proof content.
Claim. There is a finite set of algebraic certificate labels for the Hodge audit, consisting of three mutually exclusive kinds: a finite cycle ledger, an algebraic witness, and a transcendental obstruction witness. Equality of labels is decidable.
background
The module HardProblemCertificateAudits packages finite certificate inventories and audit predicates for several hard analytic problems (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge). Each problem gets a small inductive type of certificate tags, then a ProblemAudit that records which tags count as legitimate versus pathological at the schema layer.
HodgeAlgebraicCert is the algebraic-side tag set for Hodge. Its three constructors name the only finite certificate shapes the algebraic-witness audit is allowed to emit: a finite cycle ledger entry, a positive algebraic witness, or an explicit transcendental obstruction witness. Later analytic interfaces (complex dimension, cohomological degree, display payload) sit on top of these tags rather than replacing them.
The surrounding audit language is intentionally conservative: the native predicate asserts that every finite certificate is legitimate at the schema layer, with room for analytic refinements to tighten or split cases.
proof idea
No proof. This is an inductive definition with three nullary constructors and automatic DecidableEq and Repr instances. Mathematical content is the enumeration itself, not a derivation.
why it matters
This tag type is the algebraic carrier for the Hodge bridge inside the hard-problem certificate suite. hodgeAlgebraicAudit is the identity audit on these tags (every finite certificate is schema-legitimate). hodgeAnalyticCompletion and HodgeAnalyticDisplay wrap a tag with complex dimension, cohomological degree, and a display payload (e.g. cohomology class), while hodgeAnalyticAudit and hodgeCertifiedDisplayAudit supply the refined analytic and certified-display audits.
In the Recognition stack this is bookkeeping infrastructure, not a resolution of the Hodge conjecture. It fixes a finite algebraic certificate vocabulary so later modules can state conservative legitimacy, pathology, and completion maps without smuggling open analytic content into the schema layer. It sits beside sibling inventories for the other named hard problems and feeds the module’s certified-display headline that the hard-problem stubs now share a uniform audit shape.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.