harmonic_form_theorem_minimal_ledger
plain-language theorem explainer
For defect-bounded sub-ledgers with total defect at most 1, every coarse-graining stable cohomology class is realized by a J-cost minimal cycle carrying exactly the same z-charge. Researchers working on the Recognition Science translation of the Hodge conjecture cite this result to guarantee harmonic representatives in the low-defect regime. The argument is a direct term-mode construction that assembles the cycle from the ledger events and invokes the stability bound to witness zero defect.
Claim. Let $L$ be a defect-bounded sub-ledger with defect at most 1 and let $cls$ be a coarse-graining stable class on $L$. Then there exists a J-cost minimal cycle $cyc$ on $L$ such that the z-charge of the cycle class of $cyc$ equals the z-charge of $cls$.
background
A DefectBoundedSubLedger consists of a finite list of recognition events together with a real-valued defect equal to the total J-cost; this structure plays the role of a smooth projective variety in the RS setting. A CoarseGrainingStableClass on such an $L$ extends a cohomology class by the condition that its z-charge satisfies the data-processing inequality, specifically z_charge ≤ defect($L$), so the class survives coarse-graining and remains anchored to the underlying J-cost geometry. The module identifies harmonic forms with J-cost critical points (where the gradient of J-cost vanishes) and minimal cycles with zero net defect as the RS analogs of algebraic cycles that minimize cost within their class.
proof idea
The proof is a direct term-mode construction. It supplies a JCostMinimalCycle whose events are taken verbatim from $L$, whose cycle_class copies the z_charge and symmetry data from $cls$, and whose zero_defect witness is the right disjunct of the dpi_stable hypothesis. No auxiliary lemmas are invoked; the existential quantifier is discharged by exhibiting the record.
why it matters
The result supplies the existence step needed for the hard direction of the RS Hodge conjecture when defect ≤ 1. It is invoked by hodge_hard_direction_case_B to produce lists of minimal cycles and by hodge_decomposition_exists to obtain a decomposition whose correction term is identically zero. In the framework this realizes the claim that every stable class decomposes as a zero-defect cycle plus boundary correction, confirming that J-cost critical points serve as the unique minimal representatives inside their cohomology class.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.