module module moderate

`IndisputableMonolith.Cryptography.BalancedJSubsetSum`

This module defines the Balanced J Subset Sum problem and supporting objects for the Recognition Science cryptography domain. It introduces rungValue as exp(k log phi) for phi-rung representation, BJSSInstance, BJSSWitness, weightSum, residueSum, rungCost, totalJCost, and jCostBound. Researchers developing RS-based cryptographic protocols would cite these objects. The module consists solely of definitions with no proofs.

claimrungValue(k) := exp(k log phi); BJSSInstance is a record specifying weights and residues; BJSSWitness is a subset selector; weightSum and residueSum compute the respective totals; rungCost and totalJCost measure J-costs; jCostBound asserts an upper limit on total J-cost.

background

The module imports Constants, whose doc states the fundamental RS time quantum (RS-native) τ₀ = 1 tick, and the Cost module. It introduces phi-rung values represented by exp(k log phi) to avoid integer-power API details. The local theoretical setting is the cryptography domain, supplying subset-sum structures balanced under J-cost from the Cost module.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the core definitions for Balanced J Subset Sum that feed into subsequent cryptography results in the Recognition Science framework. It prepares the ground for theorems that apply J-cost bounds and phi-ladder structures to cryptographic constructions.

scope and limits

Does not prove computational hardness of BJSS instances.
Does not supply algorithms or solvers for the subset sum problem.
Does not connect definitions to concrete cryptographic primitives.
Does not address security reductions or attack models.

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