HodgeDisplayPayload
plain-language theorem explainer
Three-tag enumeration of what a Hodge audit display may show: a cohomology class, an algebraic cycle, or a transcendental class. Downstream Hodge analytic displays and certified-display audits index their payload field by this type. The declaration is a plain inductive with decidable equality and a default inhabitant.
Claim. There is a finite set of Hodge display kinds consisting of three labels: cohomology-class display, algebraic-cycle display, and transcendental-class display. Equality of labels is decidable, and the default inhabitant is the cohomology-class label.
background
The module HardProblemCertificateAudits packages certificate audits for several classical hard problems (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge). Each problem gets an algebraic certificate type and a domain-specific analytic display record that can be fed to a generic certified-display audit.
For Hodge, the algebraic side is HodgeAlgebraicCert. The analytic display record carries that certificate together with a complex dimension, a cohomological degree, and a display-kind tag. The present inductive supplies exactly those tags: whether the display is presenting a cohomology class, an algebraic cycle, or a transcendental class.
The surrounding infrastructure (imported QuantizedProofMethod) treats displays as structured witnesses that a certificate has been rendered in a problem-specific analytic form, not as proofs of the underlying conjecture.
proof idea
No proof content. The declaration is an inductive type with three nullary constructors, deriving decidable equality and a printable representation, plus a one-line Inhabited instance that picks the cohomology-class constructor as default.
why it matters
This tag type is the payload field of HodgeAnalyticDisplay and is hard-wired into hodgeAnalyticCompletion, which always emits the cohomology-class tag when completing an algebraic Hodge certificate to an analytic display. It is also the payload parameter of hodgeCertifiedDisplayAudit, the certified-display audit instance for the Hodge bridge.
In the Recognition Science foundation layer these audits are scaffolding around hard-problem certificates, not claims that the Hodge conjecture is settled. The tags keep the analytic display honest about which geometric object is being exhibited when a certificate is rendered for audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.