rungValue_pos
rungValue_pos proves that the phi-rung value exp(k log phi) is strictly positive for every integer k. Researchers formalizing cost bounds in the 8-balanced J-subset sum cryptography module cite it to establish non-negativity of rung costs. The proof is a direct term-mode application that unfolds the exponential definition and invokes positivity of the real exponential function.
claimFor every integer $k$, the phi-rung value satisfies $0 < e^{k log phi}$.
background
The Balanced J-Subset Sum module defines an RS-native cryptography candidate in a deliberately boring form with no security claim. An instance consists of integer weights, residues in ZMod 8, phi-rungs, a target, and a J-cost bound; a witness is a finite subset satisfying the target equation, 8-neutrality, and the cost bound. The rungValue function is introduced upstream as the definition def rungValue (k : ℤ) : ℝ := Real.exp ((k : ℝ) * Real.log phi) to represent phi-rung values while avoiding integer-power API details.
proof idea
The proof is a one-line term wrapper: it unfolds the definition of rungValue to expose the real exponential, then applies the standard positivity fact for the exponential function on the reals.
why it matters in Recognition Science
This theorem feeds directly into rungCost_nonneg in the same module, which applies Jcost_nonneg to the result of rungValue_pos to obtain non-negativity of rung costs. It supplies the positivity foundation required for cost calculations inside the phi-ladder construction of the 8-balanced J-subset sum candidate, consistent with Recognition Science use of phi for self-similar fixed points and cost accounting.
scope and limits
- Does not address security properties of any subset-sum instance.
- Does not extend positivity to non-integer rung indices.
- Does not supply magnitude bounds or growth rates for rungValue.
Lean usage
exact Cost.Jcost_nonneg (rungValue_pos (inst.rung i))formal statement (Lean)
28theorem rungValue_pos (k : ℤ) : 0 < rungValue k := by
proof body
Term-mode proof.
29 unfold rungValue
30 exact Real.exp_pos _
31