JCostGradient
plain-language theorem explainer
The JCostGradient structure packages the real-valued rate of defect change under event perturbations together with the event count for any defect-bounded sub-ledger. Researchers translating classical Hodge theory into Recognition Science cite it when they need the explicit gradient object that vanishes at critical points. The declaration is a direct structure definition with no lemmas or reductions.
Claim. For a defect-bounded sub-ledger $L$, the J-cost gradient is the structure consisting of a real number $v$ (the defect change per unit perturbation of recognition events) and the integer equal to the number of events recorded in $L$.
background
Recognition Science defines the defect of a positive real as defect$(x) = J(x)$, where $J$ satisfies the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. Sub-ledgers collect recognition events whose total defect is bounded; the cost of each event is taken from the derivedCost of its comparator or from the J-cost of its state. The module translates classical Hodge theory by identifying a harmonic form with a sub-ledger whose J-cost gradient vanishes everywhere on the boundary, i.e., a configuration annihilated by the linearized recognition operator.
proof idea
This is a structure definition that directly assembles the gradient value as a real number and the length of the events list of the supplied sub-ledger. No upstream lemmas are invoked; the construction is purely packaging.
why it matters
JCostGradient supplies the basic object required by IsJCostCritical and the subsequent harmonic-form theorems in the same module. It thereby supports the RS analog of the Hodge decomposition, in which every cohomology class (Z-charge) possesses a unique minimum-cost representative. The definition sits inside the chain that begins with the defect functional (LawOfExistence) and the cost maps (ObserverForcing, MultiplicativeRecognizerL4) and feeds the hard direction of the Hodge conjecture analog via defect-budget arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.