totalDefect_nonneg
totalDefect_nonneg shows that the sum of costs over any finite sub-ledger is nonnegative. Researchers formalizing the Recognition Science translation of the Hodge conjecture cite it when bounding J-cost sums prior to minimality arguments. The proof is a one-line term that applies Finset.sum_nonneg directly to the cost_nonneg field of the sub-ledger.
claimLet $n$ be a natural number and let $L$ be a sub-ledger on $n$ voxels equipped with a cost function $c : Fin n → ℝ$ such that $c(i) ≥ 0$ for every $i$. Then the total defect of $L$, defined as the sum of the costs, satisfies $0 ≤ ∑ c(i)$.
background
The module HodgeAlgebraicCycles develops the Recognition Science rendering of the Hodge conjecture: J-cost minimal sub-ledgers generate coarse-graining-stable cohomology classes. A SubLedger n is the structure carrying a cost map Fin n → ℝ together with the field cost_nonneg asserting that every entry is nonnegative; totalDefect is the finite sum of these costs, which coincides with the sum of the defect functional J applied to each voxel state.
proof idea
The proof is a direct term-mode wrapper: Finset.sum_nonneg (fun i _ => L.cost_nonneg i). It invokes the upstream theorem cost_nonneg (every recognition-event cost is nonnegative) and the standard fact that finite sums preserve nonnegativity.
why it matters in Recognition Science
The lemma is invoked by minimal_defect_concentrated to conclude that every J-cost minimal sub-ledger concentrates its defect on irreducible components. It supplies the elementary nonnegativity step required for the algebraic-to-Hodge direction of the RS Hodge conjecture (biggest-questions.md §XIII Q2) and rests on the J-cost minimum at unity together with the nonnegativity of the defect functional.
scope and limits
- Does not claim that total defect is strictly positive.
- Does not assume the sub-ledger is J-cost minimal or coarse-graining stable.
- Does not address the value of total defect under coarse-graining operations.
- Does not compute an explicit numerical lower bound beyond zero.
Lean usage
example {n : ℕ} (L : SubLedger n) : 0 ≤ totalDefect L := totalDefect_nonneg Lformal statement (Lean)
54theorem totalDefect_nonneg {n : ℕ} (L : SubLedger n) : 0 ≤ totalDefect L :=
proof body
Term-mode proof.
55 Finset.sum_nonneg (fun i _ => L.cost_nonneg i)
56
57/-- A sub-ledger is defect-bounded if its total defect is below a threshold. -/