jCostBound
plain-language theorem explainer
The J-cost bound predicate requires that the summed rung costs of a witness subset in an 8-balanced J-subset-sum instance stay at or below the instance bound. Cryptographers examining RS-native search problems would cite this predicate inside solution checks. It is realized as a direct comparison of the total J-cost summation against the supplied real bound.
Claim. Let $I$ be a finite 8-balanced J-subset-sum instance with integer weights, residues in the cyclic group of order 8, phi-rung indices, an integer target, and real bound $B$. For a witness subset $W$, the bound condition holds precisely when the total J-cost of $W$ satisfies total J-cost$(I,W) ≤ B$.
background
The module presents an elementary 8-balanced J-subset-sum problem as the first RS-native cryptography candidate, explicitly making no security claim. An instance consists of a finite collection of elements each equipped with an integer weight, a residue modulo 8, a phi-rung index, a target integer sum, and a real J-cost bound; a witness is simply a finite subset of those elements. The total J-cost of a witness is the sum of individual rung costs over the chosen support, where rung cost is obtained from the J-function evaluated at the rung value.
proof idea
The definition is a one-line wrapper that invokes the total J-cost summation over the witness support and compares the resulting real number against the instance bound.
why it matters
This predicate is one of the three conjuncts that together define a full solution for the finite problem. It supplies the explicit cost constraint required by the 8-balanced formulation, which draws its periodicity from the eight-tick octave in the forcing chain. The construction leaves open any reduction showing that the bounded-cost search problem is hard relative to the underlying J-cost or phi-ladder properties.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.