rs_hodge_holds_for_trivial_ledgers
plain-language theorem explainer
The result proves that for any defect-bounded sub-ledger whose coarse-graining flows all reach limit zero, every stable class decomposes into a list of J-cost minimal cycles whose z-charges sum exactly to the class charge. Workers assembling the hard direction of the Recognition Science Hodge conjecture cite this when treating the zero-limit case. The argument is a direct one-line application of the pre-established case-A lemma.
Claim. Let $L$ be a defect-bounded sub-ledger. If every coarse-graining flow on $L$ has flow limit zero, then every coarse-graining stable class $cls$ on $L$ admits a finite list of J-cost minimal cycles such that the z-charge of $cls$ equals the sum of the z-charges of the cycles.
background
A defect-bounded sub-ledger is a finite collection of recognition events whose total J-cost (the defect) is finite. A coarse-graining flow on such a ledger records the apparent defect after successive zoom-out steps; the flow limit is the infimum of this decreasing sequence. A coarse-graining stable class extends a cohomology class by the requirement that its z-charge is fixed under the data-processing inequality and therefore does not exceed the ledger defect. J-cost minimal cycles are the recognition-closed subgraphs with zero net defect, serving as the RS analogs of algebraic cycles.
proof idea
The proof is a one-line wrapper that applies the case-A lemma hodge_hard_direction_case_A to the supplied ledger, the flow-limit hypothesis, and the stable class.
why it matters
This theorem supplies the case-A component of hodgeHardCert and is invoked by hodge_hard_direction_summary. It fills the zero-limit slot in the module's proof chain for the RS Hodge conjecture, where vanishing flow limit forces every stable class to have z-charge zero and therefore to be generated by zero-defect cycles. The result aligns with the framework's J-cost minimization principle but leaves the positive z-charge case open for later extension to rational combinations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.