hodgeAnalytic_conservative
plain-language theorem explainer
The analytic Hodge completion is conservative for both the legitimate and pathology predicates: every display satisfying either is certificate-covered. Certificate auditors for the Hodge hard-problem bundle cite this to discharge the two conservativity fields. The proof is a one-line constructor that witnesses coverage by the display's embedded certificate.
Claim. The analytic Hodge completion is conservative for the constantly-true legitimate predicate and for the constantly-true pathology predicate on analytic Hodge displays: every such display is certificate-covered.
background
In the Primitive Recognition Calculus, a completion packages native certificates into display data together with a certifies relation. Conservativity of a completion for a predicate $P$ means $P$ is certificate-covered: whenever a display satisfies $P$, some certificate certifies that display.
The analytic Hodge completion maps an algebraic Hodge certificate to a cohomology-class display (zero auxiliary parameters) and certifies by equality with the display's embedded certificate field. Both the legitimate and pathology predicates on analytic Hodge displays are defined as the constantly true proposition, so every display is in scope for coverage.
This lives in the hard-problem certificate-audits module, which builds parallel audit bundles for several Millennium-type problems (prime critical line, Navier-Stokes energy, Yang-Mills gap, algebraic and analytic Hodge).
proof idea
The goal is a conjunction of two Conservativity statements. Constructor splits the conjunction. On each side the proof introduces an arbitrary display $d$ (the predicate hypothesis is vacuous, since both predicates are True) and supplies the witness pair consisting of $d$'s embedded certificate together with reflexivity of equality, which is exactly the completion's certifies relation. No external lemmas are required beyond the definitions of Conservativity and the analytic Hodge completion.
why it matters
This theorem discharges the two conservativity obligations of the analytic Hodge problem audit. Downstream, that audit record packages the completion, the two predicates, and the two projections of this result into a single ProblemAudit. Within Recognition foundation work, such audits ensure that non-native display layers for hard problems introduce no uncertified artifacts: every legitimate or pathological display is backed by a native certificate. The analytic Hodge side is deliberately baseline (predicates True, certification by field projection); it is a certificate-coverage check, not a resolution of the Hodge conjecture, and it does not touch the RS forcing chain (T0-T8) or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.