JCostGradient
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute an explicit numerical value for the gradient.
- Does not assert that the gradient is zero for any ledger.
- Does not relate the gradient to the phi-ladder or to specific constants such as alpha.
- Does not prove existence or uniqueness of critical points.
formal statement (Lean)
44structure JCostGradient (L : DefectBoundedSubLedger) where
45 /-- The gradient value (defect change per unit perturbation) -/
46 value : ℝ
47 /-- Computable from the recognition events: δJ/δeᵢ for each event eᵢ -/
48 event_count : L.events.length
49
50/-- A sub-ledger is J-cost critical if its gradient is zero:
51 no perturbation decreases the defect further. This is the RS analog of
52 a harmonic form (annihilated by the Laplacian). -/