fromSubsetSum_isSolution
Ordinary subset-sum solutions embed directly as solutions to the balanced J-subset-sum instance obtained by setting all residues and rungs to zero. Recognition Science users working on the cryptography module would cite this to record the classical reduction. The proof is a direct verification that splits the isSolution conjunction and invokes the zero total J-cost lemma for the embedded instance.
claimLet $w : [n] → ℤ$ and $t ∈ ℤ$. If a finite subset $S ⊆ [n]$ satisfies $∑_{i∈S} w_i = t$, then the witness corresponding to $S$ satisfies the weight-target equation, the residue-neutrality condition (sum of residues ≡ 0 mod 8), and the J-cost bound for the BJSS instance built from $w$ and $t$ by assigning zero residues and zero rungs to every index.
background
The module defines the 8-Balanced J-Subset Sum problem as the first RS-native cryptography candidate, deliberately without security claims. An instance carries integer weights, residues in ℤ/8ℤ, phi-rungs, a target integer, and a J-cost bound; a witness is a finite subset of indices whose selected weights sum to the target, whose residues sum to zero modulo 8, and whose total J-cost stays within the bound.
proof idea
The proof applies constructor to split the three conjuncts of isSolution. The weightTarget conjunct follows by simpa from the hypothesis together with the definitions of weightSum and fromSubsetSum. The residueNeutral conjunct is discharged by simp, since fromSubsetSum sets every residue to zero. The jCostBound conjunct is obtained by rewriting with the lemma fromSubsetSum_totalJCost_zero and applying le_of_eq.
why it matters in Recognition Science
This theorem records the embedding of ordinary subset-sum into the RS-native BJSS setting, supplying the degenerate base case for the cryptography module. It sits inside the larger Recognition Science program that derives structures from the J-functional equation and the eight-tick octave, yet no downstream results currently depend on it. The open question is whether this reduction will later be used to import hardness statements or to construct explicit phi-ladder instances.
scope and limits
- Does not assert any cryptographic security properties.
- Does not apply to instances with nonzero residues or nonzero rungs.
- Does not guarantee existence of solutions for arbitrary targets.
- Does not address computational complexity or algorithms.
formal statement (Lean)
111theorem fromSubsetSum_isSolution {n : ℕ} (weight : Fin n → ℤ) (target : ℤ)
112 (S : Finset (Fin n)) (h : (∑ i ∈ S, weight i) = target) :
113 isSolution (fromSubsetSum weight target) ⟨S⟩ := by
proof body
Term-mode proof.
114 constructor
115 · simpa [weightTarget, weightSum, fromSubsetSum] using h
116 constructor
117 · simp [residueNeutral, residueSum, fromSubsetSum]
118 · have hcost := fromSubsetSum_totalJCost_zero weight target S
119 change totalJCost (fromSubsetSum weight target) ⟨S⟩ ≤ 0
120 exact le_of_eq hcost
121
122end
123
124end BalancedJSubsetSum
125end Cryptography
126end IndisputableMonolith