CoarseGrainingStableClass
plain-language theorem explainer
CoarseGrainingStableClass defines a cohomology class on a DefectBoundedSubLedger whose z_charge satisfies the data-processing inequality bound z_charge ≤ defect. Researchers formalizing the Recognition Science version of the Hodge conjecture cite it when distinguishing classes anchored to actual J-cost structure from statistical artifacts. The declaration is introduced as a structure extending CohomologyClass by a single stability predicate.
Claim. Let $L$ be a defect-bounded sub-ledger. A coarse-graining stable class on $L$ is a cohomology class with nonnegative symmetric charge $z$ satisfying $z ≤$ defect of $L$.
background
A DefectBoundedSubLedger is a finite list of recognition events whose total J-cost (defect) is bounded above by $φ^{44}$ and nonnegative. A CohomologyClass on such an $L$ is a real number z_charge together with the symmetry condition z_charge ≥ 0. The module translates the classical Hodge conjecture by identifying varieties with these sub-ledgers, Hodge classes with coarse-graining stable classes, and algebraic cycles with JCostMinimalCycles (recognition-closed subgraphs whose boundary nodes are balanced so that net defect vanishes).
proof idea
The declaration is a structure definition extending CohomologyClass L by the single field dpi_stable that directly asserts z_charge ≤ L.defect. No lemmas or tactics are invoked; the object is introduced by fiat as the RS counterpart of a Hodge class that survives zooming out.
why it matters
This definition supplies the target object for the proved direction of the RS Hodge conjecture: every JCostMinimalCycle is a CoarseGrainingStableClass. It is invoked in defect_budget_theorem (stable classes under all flows have z_charge = 0) and in HodgeCert. It leaves open the converse direction that every stable class is generated by minimal cycles, the precise content of the Recognition Science Hodge conjecture.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.