module module moderate

`IndisputableMonolith.Cryptography.BalancedJSubsetSum`

This module defines the Balanced J-Subset Sum problem and its supporting structures using phi-rung values and J-costs drawn from the Recognition framework. Cryptographers building RS-native primitives would cite these definitions when encoding subset-sum instances with residue neutrality and bounded total J-cost. The module is purely definitional, introducing types for instances, witnesses, weight sums, and cost bounds without any theorems.

claimLet $r_k = e^{k log phi}$ denote the phi-rung value at integer rung $k$. A BJSSInstance comprises a target weight $w$ together with a multiset of rung values. A BJSSWitness is a subset selection such that weightSum equals $w$ and residueSum is neutral. The functions rungCost, totalJCost and jCostBound attach J-costs to rungs and enforce an upper bound on the aggregate cost of any valid witness.

background

Recognition Science equips every scale with a J-cost via the Recognition Composition Law, where J measures departure from the fixed point phi. The phi-ladder supplies discrete mass and energy quanta through rungValue(k) = exp(k log phi), avoiding direct integer-power handling. This module imports the base time quantum tau_0 = 1 tick from Constants and the cost primitives from Cost to embed those scales inside a cryptographic subset-sum setting.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the concrete objects needed to formulate cryptographic hardness questions inside the Recognition framework, directly supporting later theorems that would link J-cost bounds to security parameters. It sits between the core phi-ladder constructions and any downstream cryptographic protocol that must respect residue neutrality and totalJCost limits.

scope and limits

Does not establish computational hardness of BJSS.
Does not provide solvers or reduction proofs.
Does not define any encryption or signature scheme.
Does not quantify security levels or attack costs.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (19)

def rungValue L26
theorem rungValue_pos L28
theorem rungValue_zero L32
structure BJSSInstance L37
structure BJSSWitness L46
def weightSum L50
def residueSum L54
def rungCost L58
def totalJCost L62
def weightTarget L65
def residueNeutral L68
def jCostBound L71
def isSolution L75
theorem rungCost_nonneg L78
theorem totalJCost_nonneg L83
def solutionDecidable L90
def fromSubsetSum L97
theorem fromSubsetSum_totalJCost_zero L105
theorem fromSubsetSum_isSolution L111