solutionDecidable
The definition supplies classical decidability for whether a finite witness solves an 8-balanced J-subset-sum instance. Researchers embedding ordinary subset-sum into the Recognition Science J-cost framework would cite it when they need a decidable solution predicate. The implementation is a one-line classical wrapper that invokes inferInstance on the finite conjunction.
claimFor a finite instance with $n$ elements, integer weights $w_i$, residues $r_i$ in $Z/8Z$, rungs, target integer $t$, and real J-cost bound $b$, together with a witness subset $S$, the predicate that the sum of $w_i$ over $S$ equals $t$, the sum of $r_i$ over $S$ is neutral in $Z/8Z$, and the total J-cost is at most $b$, is decidable.
background
The module defines the 8-Balanced J-Subset Sum problem as the first RS-native cryptography candidate in deliberately simple form, with no security claims. BJSSInstance is the structure holding $n$, weight and residue maps from Fin $n$ to integers and ZMod 8, rung map to integers, target integer, and real bound. BJSSWitness is simply the support Finset of selected indices.
proof idea
The definition opens classical logic and then applies inferInstance directly to the finite predicate isSolution. No search procedure or algorithm is constructed; the classical axiom supplies decidability for the conjunction of weightTarget, residueNeutral, and jCostBound.
why it matters in Recognition Science
This definition makes the core solution predicate decidable inside the first RS-native cryptography module, enabling formal statements about J-cost bounded subset-sum embeddings. It sits downstream of the J-cost definitions in ObserverForcing and MultiplicativeRecognizerL4 and upstream of any later cryptographic constructions that would invoke isSolution. The eight-residue neutrality aligns with the eight-tick octave structure in the foundation while remaining a finite-search statement only.
scope and limits
- Does not supply a polynomial-time algorithm.
- Does not assert cryptographic security for the construction.
- Does not extend decidability to infinite instances or continuous bounds.
formal statement (Lean)
90noncomputable def solutionDecidable (inst : BJSSInstance) (w : BJSSWitness inst) :
91 Decidable (isSolution inst w) := by
proof body
Definition body.
92 classical
93 exact inferInstance
94
95/-- Ordinary subset-sum embeds by using zero residues, zero rungs, and zero
96cost bound. -/