j_cost_minimal_is_cgstable'
plain-language theorem explainer
Every J-cost minimal cycle on a defect-bounded sub-ledger with total defect at least one produces a cohomology class whose z-charge survives coarse-graining. Recognition Science researchers formalizing the Hodge conjecture cite it for the algebraic-to-Hodge direction. The proof builds the stable class directly from the cycle data and checks the stability bound by case split on the zero-defect disjunction together with ordering transitivity.
Claim. Let $L$ be a defect-bounded sub-ledger with $1$ ≤ defect($L$). Let $C$ be a J-cost minimal cycle on $L$. Then there exists a coarse-graining stable class cls on $L$ such that the z-charge of cls equals the z-charge of the cycle class of $C$.
background
A DefectBoundedSubLedger is a finite set of recognition events whose total J-cost (defect) is finite and nonnegative, serving as the RS stand-in for a smooth projective variety. A JCostMinimalCycle is a recognition-closed subgraph whose net defect (z-charge) is zero or at most one, the RS analog of an algebraic cycle. A CoarseGrainingStableClass extends a cohomology class by the condition that its z-charge is bounded by the ledger defect, ensuring invariance under the data-processing inequality.
proof idea
The tactic proof constructs the witness class by copying z-charge and symmetric from the input cycle, then proves the dpi_stable predicate by rcases on the zero_defect disjunction. The zero case applies defect non-negativity; the bounded case chains the inequality via le_trans with the ledger defect hypothesis. The final equality is discharged by rfl.
why it matters
This theorem supplies the algebraic-implies-Hodge direction inside hodgeCert, which packages the vocabulary definition, the implication, and the open status of the converse. It realizes the proved half of the RS Hodge conjecture stated in the module documentation, where the defect-budget argument shows that cost-minimal cycles are automatically stable under coarse-graining. The result anchors the Recognition Science translation by confirming that J-cost minimal structures survive the data-processing inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.