fromSubsetSum_totalJCost_zero
plain-language theorem explainer
The embedding of ordinary subset sum into the balanced J-subset-sum framework via zero residues and zero rungs produces witnesses with vanishing total J-cost. Researchers examining the cost structure of RS-native cryptographic primitives would reference this result when checking boundary cases of the J-cost bound. The proof proceeds by a single simplification step that invokes the unit lemma for Jcost together with the definitions of totalJCost and rungCost.
Claim. Let $n$ be a natural number, $w :$ Fin $n$ to integers the weights, $t$ an integer target, and $S$ a finite subset of Fin $n$. For the BJSS instance obtained from the ordinary subset-sum problem by setting all residues and rungs to zero, the total J-cost of the witness supported on $S$ equals zero.
background
The module introduces the 8-balanced J-subset-sum problem as a deliberately simple RS-native candidate for cryptography, with no security claims. An instance consists of integer weights, residues modulo 8, phi-rungs, a target sum, and a J-cost bound; a witness is a subset meeting the target equation, 8-neutrality, and the cost bound.
proof idea
The proof is a one-line term-mode simplification. It unfolds the definitions of totalJCost, rungCost, and fromSubsetSum, then applies the lemma Jcost_unit0 which establishes that the J-cost of the unit rung value is zero.
why it matters
This result supports the theorem fromSubsetSum_isSolution, which shows that any ordinary subset-sum solution yields a degenerate BJSS solution. It fills the role of verifying the cost bound in the embedding, consistent with the framework's emphasis on non-negative J-cost as in the totalJCost definition from PhysicsComplexityStructure. Within Recognition Science, it relates to the J-uniqueness property by confirming that the zero-rung case incurs no cost penalty.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.