totalDefect
plain-language theorem explainer
The total defect sums the per-voxel costs over any finite sub-ledger of size n. Researchers formalizing the Recognition Science translation of the Hodge conjecture cite this quantity when defining bounded-defect sets or checking J-cost minimality. The definition is a direct Finset sum applied to the cost vector carried by the SubLedger structure.
Claim. For a sub-ledger $L$ on $n$ voxels equipped with a cost function $c : {1,..,n} → ℝ$, the total defect equals $∑_{i=1}^n c(i)$.
background
A SubLedger consists of a finite collection of n voxels together with a cost function that assigns a real number to each voxel and is required to be non-negative on every index. The total defect is simply the sum of these assigned costs. This definition sits inside the module that translates the Hodge conjecture into Recognition Science language, where defect-bounded sub-ledgers correspond to coarse-graining-stable cohomology classes generated by J-cost minima. Upstream results supply the cost function itself from the J-cost of recognition events and from the derived cost of multiplicative recognizers.
proof idea
One-line definition that applies the Finset universal sum directly to the cost field of the supplied sub-ledger.
why it matters
This quantity supplies the basic collective J-cost measure used to define defect-bounded sub-ledgers and J-cost minimal sub-ledgers in the same module. It therefore supports both directions of the RS Hodge conjecture: algebraic cycles (J-cost minima) produce stable classes, and stable classes must arise from such minima. The definition connects to the eight-tick octave and the Recognition Composition Law through the underlying J-cost function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.