harmonic_form_theorem_zero_charge
plain-language theorem explainer
For any defect-bounded sub-ledger L and coarse-graining stable class cls with z-charge exactly zero, a J-cost minimal cycle exists realizing the same class. Researchers assembling the Recognition Science version of the Hodge conjecture cite this zero-charge case as the base step before the defect-budget argument. The proof is a direct term construction that builds the cycle record from L.events, sets the class charge to zero via le_refl, and discharges the hypothesis by symmetry.
Claim. Let $L$ be a defect-bounded sub-ledger and let $cls$ be a coarse-graining stable class on $L$ with $z$-charge$(cls)=0$. Then there exists a J-cost minimal cycle $cyc$ on $L$ such that $z$-charge of the cycle class of $cyc$ equals zero.
background
In the Recognition Science translation of Hodge theory, a harmonic form is a J-cost critical sub-ledger (gradient of J-cost vanishes on the boundary) that minimizes cost inside its cohomology class labeled by z-charge. The defect functional is defined as defect(x) := J(x) for positive x, and le_refl supplies the reflexive order on LogicNat used to witness symmetry of the zero class. CoarseGrainingStableClass collects classes invariant under all coarse-graining flows, while JCostMinimalCycle denotes those cycles that achieve the global minimum J-cost.
proof idea
The proof is a term-mode construction. It supplies a JCostMinimalCycle record whose cycle_events are copied from L.events, whose cycle_class has z-charge set to zero with the symmetric property witnessed by le_refl, and whose zero_defect is the left injection of reflexivity. The final exact step applies symmetry to the input hypothesis h_zero.
why it matters
This supplies the zero-charge case required by hard_direction_via_defect_budget, which combines it with the defect budget theorem to conclude every stable class is generated by a minimal cycle. The parent result hodge_hard_direction_case_A invokes the same construction for asymptotically trivial sub-ledgers. It closes the base case of the harmonic form theorem in the RS Hodge setting before the general defect-budget argument is applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.