hodgeCert
plain-language theorem explainer
The declaration constructs a status certificate for the recognition science translation of the Hodge conjecture, confirming that every J-cost minimal cycle on a defect-bounded sub-ledger with defect at least 1 is a coarse-graining stable class with matching charge while the converse stays open. Algebraic geometers or recognition-based physicists would cite it for the established implication from minimal cycles to stable classes. The proof is a direct record construction that delegates the key implication to the corrected stability lemma and dis
Claim. The status certificate holds: the recognition science vocabulary is defined; for any defect-bounded sub-ledger $L$ with $1$ at most the defect of $L$ and any J-cost minimal cycle on $L$, there exists a coarse-graining stable class on $L$ whose $z$-charge equals that of the cycle; the conjecture is stated; and the conjecture remains open.
background
The module recasts the classical Hodge conjecture in recognition science language. A smooth projective variety is represented by a defect-bounded sub-ledger, a finite voxel collection whose total J-cost is bounded. A Hodge class of type (p,p) becomes a coarse-graining stable class, a cohomological feature preserved under the data-processing inequality of coarse-graining. An algebraic cycle is a J-cost minimal cycle, a recognition-closed subgraph on which every boundary defect vanishes. The module documentation states that one direction is proved: every J-cost minimal cycle is a coarse-graining stable class. The converse, that every stable class is generated by minimal cycles, is stated but left open. The certificate relies on the upstream lemma j_cost_minimal_is_cgstable', which shows that cycles with bounded charge on sub-ledgers of defect at least 1 are stable, together with the constant ledger definitions from the Recognition and Cycle3 modules.
proof idea
The tactic proof constructs the HodgeCert record directly. The vocabulary_defined and conjecture_stated fields are filled by trivial. The algebraic_implies_hodge field is supplied by the lambda that applies the upstream theorem j_cost_minimal_is_cgstable' to the ledger, defect hypothesis, and cycle inputs. The conjecture_open field is discharged by a push_neg tactic followed by an exact that exhibits a witness function and a reflexivity proof, confirming the conjecture is not settled.
why it matters
This theorem supplies the proved direction of the RS Hodge conjecture inside the Mathematics.HodgeConjecture module, recording that algebraic cycles are Hodge classes via the J-cost and coarse-graining dictionary. It aligns with the framework's translation of classical statements into defect budgets and recognition-closed subgraphs. The explicit open status for the converse highlights the remaining defect-budget bridge needed to show that stable classes must be anchored at cost minima. No downstream uses appear in the graph, so the declaration serves as a self-contained status record for the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.