rungValue
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.