totalJCost_nonneg
Non-negativity of the aggregate J-cost holds for every witness of an 8-balanced J-subset sum instance. Researchers constructing RS-native cryptographic primitives would cite the result to guarantee that solution costs remain non-negative. The argument proceeds by unfolding the total-cost definition and invoking non-negativity of each rung cost inside a finite sum.
claimLet $I$ be an 8-balanced J-subset sum instance with integer weights, residues modulo 8, and phi-rungs, and let $W$ be any witness support for $I$. Then $0$ is a lower bound on the total J-cost of $W$, defined as the sum of rung costs over the selected indices.
background
The module introduces 8-balanced J-subset sum as a deliberately elementary RS-native candidate with no security claim. An instance consists of a finite set of size $n$, integer weights, residues in the ring of integers modulo 8, rung indices drawn from the phi-ladder, an integer target sum, and a real-valued J-cost bound. A witness is simply a finite subset of the indices whose weights sum to the target and whose residues sum to zero modulo 8 while respecting the cost bound. The total J-cost of a witness is the sum, over the chosen support, of the individual rung costs; each rung cost is obtained from the non-negative J-cost function applied to the positive rung value.
proof idea
The proof is a one-line wrapper. It unfolds the definition of totalJCost as the Finset sum of rungCost over the witness support, then applies the standard lemma that a finite sum of non-negative real numbers is non-negative, citing rungCost_nonneg at each term.
why it matters in Recognition Science
The declaration supplies the elementary cost lower bound required for any later statement that a witness respects the instance bound. It rests on the non-negativity of the J-cost function (imported via Cost.Jcost_nonneg and rungValue_pos) and on the finite-sum infrastructure of Mathlib. Within the Recognition framework it anchors the cost accounting for the first RS-native cryptography construction, ensuring that the phi-ladder rung costs remain non-negative before any existence or search claims are attempted.
scope and limits
- Does not assert existence of any witness satisfying the target and bound.
- Does not address computational complexity or search algorithms.
- Does not extend to infinite instances or continuous weights.
- Does not link J-cost values to cryptographic security notions.
formal statement (Lean)
83theorem totalJCost_nonneg (inst : BJSSInstance) (w : BJSSWitness inst) :
84 0 ≤ totalJCost inst w := by
proof body
Term-mode proof.
85 unfold totalJCost
86 exact Finset.sum_nonneg (fun i _hi => rungCost_nonneg inst i)
87
88/-- Classical decidability of the finite solution predicate. This is only a
89finite search statement, not an efficiency claim. -/