IsDefectBounded
plain-language theorem explainer
A sub-ledger on n voxels is defect-bounded by a real threshold when the sum of its per-voxel costs stays at most that threshold. Workers on the Recognition Science translation of the Hodge conjecture invoke this predicate to restrict attention to controlled-cost domains that can support stable cohomology classes. The definition is a direct comparison of the total cost sum against the supplied bound.
Claim. Let $L$ be a sub-ledger on $n$ voxels equipped with a nonnegative cost function $c: Fin n → ℝ$. Then $L$ is defect-bounded by $b ∈ ℝ$ when $∑_{i ∈ Fin n} c(i) ≤ b$.
background
The module recasts the Hodge conjecture inside Recognition Science: every coarse-graining-stable cohomology class on a defect-bounded sub-ledger arises from a J-cost minimal sub-ledger. A SubLedger n is a finite collection of n voxels together with a cost map Fin n → ℝ that is nonnegative at every index. The total defect of such a ledger is the ordinary sum of these costs over the finite index set.
proof idea
The definition is a one-line wrapper that applies the totalDefect summation to the supplied sub-ledger and compares the result against the given bound.
why it matters
This predicate supplies the domain restriction required by the RS translation of the Hodge conjecture (biggest-questions.md §XIII Q2). It ensures that only sub-ledgers whose collective cost remains finite and controlled can participate in the generation of coarse-graining-stable classes. The module establishes the converse direction: every such stable class arises from a J-cost minimal sub-ledger inside a defect-bounded ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.