hodgeAlgebraicAudit
plain-language theorem explainer
Packages the Hodge algebraic-witness hard-problem stub as a Delta audit whose native, derived, and certificate types are the same finite inventory (cycle ledger, algebraic witness, transcendental obstruction). Anyone citing the hard-problem audit headline or the Hodge finite-reduction theorem uses this object. It is a one-line specialization of the identity certificate audit.
Claim. Define the Hodge algebraic-witness audit as the identity $\Delta$-audit on the finite certificate type whose values are a finite cycle ledger, an algebraic witness, and a transcendental-obstruction witness. Native data, derived data, and certificates coincide, with legitimacy and pathology the schema-level predicates on that inventory.
background
In the Primitive Recognition Calculus, a continuum hard problem is not attacked directly. It is packaged as a ProblemAudit: a completion map from native data through derived data to a finite certificate type, plus legitimacy and pathology predicates that are conservative for that completion. The identity audit is the special case where native, derived, and certificate types are identical and the completion is the identity map.
HodgeAlgebraicCert is the finite inventory for the Hodge algebraic-witness stub: a finite cycle ledger, an algebraic witness, and a transcendental-obstruction witness. The module treats these as schema-layer certificates only; later analytic interfaces may refine the legitimacy predicate. The surrounding file builds the same pattern for the prime critical line, Navier–Stokes energy, and Yang–Mills gap stubs.
proof idea
One-line wrapper: instantiate the identity certificate audit at the Hodge algebraic certificate type. That fills completion by the identity completion, legitimacy by the schema-level legitimate predicate, pathology by the schema-level pathology predicate, and both conservativity obligations by the identity-conservative lemma for those predicates.
why it matters
This is the Hodge slot in the hard-problem certificate audit suite. Downstream, hodgeAlgebraic_finiteReduction applies the generic finite-reduction lemma to this audit, and the headline theorem conjoins finite-reduction for all four stubs (prime critical line, Navier–Stokes energy, Yang–Mills gap, Hodge algebraic). The headline doc-comment is explicit: these are audit schemas, not solutions of the underlying continuum problems. In the Recognition stack the point is bookkeeping: each named hard problem gets a finite certificate inventory and a proved finite-reduction obligation before any continuum analysis is attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.