globally_minimal_gives_cycle
plain-language theorem explainer
A globally minimal sub-ledger admits a J-cost minimal cycle whose Z-charge is bounded by the ledger defect. Researchers translating Hodge theory into Recognition Science cite this when linking global criticality to harmonic representatives. The proof is a direct term-mode construction that equips the ledger events with a zero-charge cycle class and invokes defect non-negativity.
Claim. Let $L$ be a defect-bounded sub-ledger that is globally minimal, meaning its defect equals zero or is at most one. Then there exists a J-cost minimal cycle $cyc$ on $L$ such that the Z-charge of the cycle class of $cyc$ is at most the defect of $L$.
background
In the Hodge Harmonic Forms module the classical Hodge theorem is recast as the statement that every cohomology class on a DefectBoundedSubLedger possesses a J-cost critical representative. The module defines a harmonic form as a sub-ledger configuration where the gradient of J-cost vanishes on the boundary, and it equates this with a JCostMinimalCycle. IsGloballyMinimal is the non-trivial criticality condition requiring that the defect of $L$ is a global minimum among all sub-ledgers sharing the same Z-charge structure; its definition is the disjunction defect = 0 or defect ≤ 1.
proof idea
The term proof directly constructs the required cycle by setting its events to those of $L$, its cycle class to a zero Z-charge class with the reflexive symmetry relation, and its zero-defect witness to the left disjunct of reflexivity. It then closes the existence claim by applying the upstream theorem defect_nonneg, which establishes non-negativity of the defect functional for positive arguments.
why it matters
This theorem supplies the elementary direction of the RS Hodge-Harmonic Form Theorem by showing that global minimality immediately yields a zero-charge JCostMinimalCycle. It feeds the sibling results harmonic_form_theorem_zero_charge and HodgeDecomposition, and it closes the zero-charge case of the conjecture that every cohomology class possesses a harmonic representative. The construction relies on the upstream defect_nonneg lemma and the arithmetic reflexivity lemma le_refl, both drawn from the Law of Existence and ArithmeticFromLogic foundations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.