hodge_hard_direction_case_B
plain-language theorem explainer
For any DefectBoundedSubLedger whose total defect is at most 1, every CoarseGrainingStableClass decomposes into a single JCostMinimalCycle whose z-charge equals the class charge. Researchers proving the Recognition Science version of the Hodge conjecture cite this result to settle the unit-defect case. The argument is a direct one-line wrapper that invokes the harmonic form theorem for minimal ledgers, builds the singleton list, and simplifies the charge sum.
Claim. Let $L$ be a defect-bounded sub-ledger with defect at most 1. For every coarse-graining stable class $cls$ over $L$ there exists a list of $J$-cost minimal cycles such that the $z$-charge of $cls$ equals the sum of the $z$-charges of the cycles in the list.
background
A DefectBoundedSubLedger is a finite list of recognition events equipped with a bounded total J-cost (the defect); it functions as the Recognition Science counterpart of a smooth projective variety. A CoarseGrainingStableClass extends a cohomology class by the stability condition that its z-charge is fixed under the data-processing inequality and satisfies z_charge ≤ defect(L). A JCostMinimalCycle is a recognition-closed subgraph whose net J-cost is zero and that generates a cohomology class; these play the role of algebraic cycles in the RS setting.
proof idea
The proof introduces the stable class, applies harmonic_form_theorem_minimal_ledger L h cls to obtain a single cycle cyc together with the equality hcyc, constructs the list [cyc], and simplifies the summed z-charge expression.
why it matters
This theorem supplies the core step for rs_hodge_holds_for_unit_defect, which states that the RS Hodge Conjecture holds for all unit-defect sub-ledgers. It completes Case B in the module's proof chain for the hard direction, where the Hodge decomposition is restricted to defect ≤ 1. The full conjecture for positive z_charge requires extending generation to rational combinations of cycles, an extension left open for HodgeConjecture.lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.