rungValue
rungValue supplies the real value of the k-th phi-rung via exp(k log phi). Cryptography constructions in Recognition Science cite it to populate rung values inside balanced J-subset-sum instances. The definition is a direct abbreviation chosen to avoid integer-power API details.
claimFor integer rung index $k$, the phi-rung value is defined by $v(k) = e^{k log phi}$.
background
The 8-Balanced J-Subset Sum module presents the first RS-native cryptography candidate in a simple form with no security claims. An instance comprises integer weights, residues modulo 8, phi-rung values, a target sum, and a J-cost bound. A witness consists of a finite subset that satisfies the target equation, maintains 8-neutrality, and respects the cost bound.
proof idea
The declaration is a one-line definition that applies Real.exp to the scaled logarithm of phi.
why it matters in Recognition Science
This definition provides the phi-rung values required by rungCost to compute J-cost contributions of selected items. It supports the sibling theorems establishing positivity and the zero case for rungValue. Within the Recognition framework it realizes the rung values on the phi-ladder that appear in mass formulas and the self-similar fixed point phi.
scope and limits
- Does not claim any security properties for the subset sum problem.
- Does not link rung indices to specific physical particles or constants.
- Does not include the full definitions of BJSSInstance or BJSSWitness.
- Does not establish any J-cost bounds or neutrality properties.
formal statement (Lean)
26def rungValue (k : ℤ) : ℝ := Real.exp ((k : ℝ) * Real.log phi)
proof body
Definition body.
27