HodgeAnalyticDisplay
plain-language theorem explainer
A record type packaging one Hodge algebraic certificate with complex dimension, cohomological degree, and a display-payload tag (cohomology class, algebraic cycle, or transcendental class). Citation target for anyone wiring the Hodge side of the hard-problem certificate audits. Pure structure definition: no proof obligations.
Claim. An analytic display for the Hodge bridge is a 4-tuple $(c, n, k, \tau)$ where $c$ is a finite Hodge algebraic certificate (finite cycle ledger, algebraic witness, or transcendental obstruction witness), $n \in \mathbb{N}$ is a complex dimension, $k \in \mathbb{N}$ is a cohomological degree, and $\tau$ is a display payload tag among cohomology-class, algebraic-cycle, and transcendental-class displays.
background
The module HardProblemCertificateAudits builds a uniform audit schema for several classical hard problems (primes on the critical line, Navier–Stokes energy, Yang–Mills gap, Hodge). Each problem gets a finite certificate inventory, a display record, and legitimacy/pathology predicates plugged into a shared ProblemAudit interface.
For Hodge, the algebraic certificate inventory is the three-constructor type with finite cycle ledger, algebraic witness, and transcendental obstruction witness. Display payload tags mark whether the analytic face is showing a cohomology class, an algebraic cycle, or a transcendental class. The present structure is the domain-specific analytic display that pairs one such certificate with two natural-number coordinates (complex dimension and cohomological degree) and one payload tag.
This sits downstream of the Primitive Recognition Calculus one-primitive layer and the quantized proof-method scaffolding imported by the module; it does not itself encode the Hodge conjecture, only the bookkeeping face used by later audit predicates.
proof idea
No proof. The declaration is a structure with four fields and a derived Repr instance. Field types are the in-module inductive certificate inventory, two natural numbers, and the in-module display-payload inductive. Downstream completion maps every certificate to a default display with dimension and degree zero and the cohomology-class payload tag.
why it matters
This record is the display type parameter of the Hodge analytic audit. It is consumed by hodgeAnalyticCompletion (which builds a default display from any algebraic certificate), by the trivial legitimacy and pathology predicates on displays, and finally by hodgeAnalyticAudit, the ProblemAudit instance that packages completion, legitimacy, pathology, and the two conservativity lemmas.
In the Recognition Science foundation stack this is scaffolding for a Hodge bridge inside the hard-problem certificate layer, not a forcing-chain step (T0–T8) and not a physical constant identity. It lets later analytic interfaces refine what a legitimate Hodge display means without changing the algebraic certificate inventory. Open refinement: legitimacy and pathology are currently the constant-true predicates, so the display is a typed carrier awaiting a nontrivial analytic criterion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.