IsJCostMinimal
plain-language theorem explainer
A sub-ledger L on n voxels is J-cost minimal when its total defect is at most the total defect of every sub-ledger on strictly fewer voxels. Researchers translating the Hodge conjecture into Recognition Science cite this predicate to designate the algebraic cycles whose generated cohomology classes remain invariant under coarse-graining. The definition is expressed directly as a universal quantification over smaller cardinalities m, arbitrary sub-ledgers L' of size m, and all injective maps Fin m to Fin n.
Claim. A sub-ledger $L$ on $n$ voxels is J-cost minimal if for every $m < n$, every sub-ledger $L'$ on $m$ voxels, and every injective map $f : [m] → [n]$, the total defect satisfies totalDefect$(L) ≤$ totalDefect$(L')$.
background
The module develops the Recognition Science translation of the Hodge conjecture on defect-bounded sub-ledgers: every coarse-graining-stable cohomology class is generated by a J-cost minimal sub-ledger. SubLedger n is the structure consisting of a cost map Fin n → ℝ together with the proof that every value is non-negative; totalDefect is the sum of these costs. J-cost is the defect functional defect(x) = J(x), where J satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and arises from the multiplicative recognizer and observer-forcing constructions.
proof idea
The definition is a direct encoding of the minimality predicate; it simply asserts the universal inequality totalDefect L ≤ totalDefect L' for all smaller sub-ledgers L' under any injective relabeling, with no lemmas or tactics applied beyond the structural fields of SubLedger.
why it matters
IsJCostMinimal supplies the precise notion of algebraic cycle required by the RS Hodge conjecture. It is invoked by algebraic_generates_hodge to prove that minima generate coarse-graining-stable classes via the data-processing inequality, and by hodge_from_algebraic to prove the converse direction that stable classes arise only from minima. The two directions together close the biconditional inside HodgeAlgebraicCyclesCert and rs_hodge_conjecture, connecting J-cost minima (rooted in T5 J-uniqueness and the phi-ladder) to Hodge classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.