pith. machine review for the scientific record. sign in
def definition def or abbrev high

weightSum

show as:
view Lean formalization →

The definition sums the integer weights selected by a witness support inside an 8-balanced J-subset sum instance. RS modelers and subset-sum analysts cite it when verifying whether a candidate subset meets the declared integer target. It is implemented as a direct finite summation over the support indices using the instance weight map.

claimLet $I$ be an 8-balanced J-subset sum instance equipped with weight map $w : [n] → ℤ$ and let $W$ be a witness whose support is the finite set $S ⊆ [n]$. The weight sum equals $∑_{i ∈ S} w(i)$.

background

The module presents 8-Balanced J-Subset Sum as a deliberately elementary RS-native candidate problem. An instance packages a finite collection of items, each carrying an integer weight, a residue in ℤ/8ℤ, a phi-rung index, an integer target, and a real J-cost bound. A witness records only the chosen support as a finite subset of indices.

proof idea

The definition is a one-line wrapper that applies summation over the support set of the witness, indexing directly into the instance weight function.

why it matters in Recognition Science

This definition supplies the integer sum required by the weight-target predicate, which is invoked both by the from-subset-sum-is-solution theorem and by the uniform-weight results in the N-dimensional cost calibration module. It therefore links the cryptography constructions to the broader cost and rung machinery. Within the Recognition framework the sum serves as a concrete primitive for subset selection under the J-cost and phi-ladder conventions, remaining auxiliary to the T0-T8 forcing chain and carrying no security assertions.

scope and limits

formal statement (Lean)

  50def weightSum (inst : BJSSInstance) (w : BJSSWitness inst) : ℤ :=

proof body

Definition body.

  51  ∑ i ∈ w.support, inst.weight i
  52
  53/-- Mod-8 residue sum. -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.