isSolution
plain-language theorem explainer
The declaration defines the predicate for a complete solution to a finite 8-Balanced J-Subset Sum instance. Researchers working on Recognition Science cryptography candidates would cite it when verifying that a selected support meets the weight target, residue neutrality modulo 8, and J-cost bound at once. The definition is a direct conjunction of the three component predicates weightTarget, residueNeutral, and jCostBound.
Claim. Let $I$ be an instance with integer weights, residues in $Z/8Z$, rungs, target integer $t$, and real bound $b$. A witness $w$ (a finite support subset) solves $I$ when the sum of selected weights equals $t$, the sum of selected residues equals 0 in $Z/8Z$, and the total J-cost is at most $b$.
background
The module defines the 8-Balanced J-Subset Sum as the first RS-native cryptography candidate in deliberately minimal form. An instance packages a finite collection of items, each carrying an integer weight, a residue in ZMod 8, a phi-rung, together with a target integer and a real-valued J-cost bound. A witness records only the chosen support as a Finset of indices.
proof idea
The definition is a one-line conjunction of the three predicates weightTarget, residueNeutral, and jCostBound.
why it matters
This predicate supplies the acceptance criterion for the BJSS problem and supplies the pattern used downstream when constructing IdentificationHypothesis objects in ContinuumLimit2D (for example in coeffBound and continuum_limit_exists). It mirrors the isSolution predicate from ECDLPWatch and occupies the solution-concept slot in the cryptography section of the Recognition framework. The ZMod 8 residues tie directly to the eight-tick octave (T7) while the rungs reference the phi-ladder from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.