rungValue_zero
plain-language theorem explainer
The base case for the phi-rung value function establishes that its value at rung index zero is one. Cryptographers modeling 8-balanced J-subset sum problems would cite this when verifying trivial subsets or normalizing J-cost bounds. The proof is a direct unfolding of the exponential definition followed by numerical simplification.
Claim. The phi-rung value at rung index zero equals one, where the phi-rung value for rung index $k$ is defined as $e^{k log phi}$.
background
The module defines 8-Balanced J-Subset Sum as the initial RS-native cryptography candidate in a deliberately simple form, making no security claims. Instances include integer weights, residues in ZMod 8, phi-rungs, a target, and a J-cost bound, with witnesses being finite subsets satisfying the target equation, 8-neutrality, and the cost bound. The phi-rung value is introduced as $e^{k log phi}$ to avoid integer-power API details in the first definition module.
proof idea
The proof unfolds the definition of the phi-rung value and applies numerical normalization to confirm the exponential at zero equals one.
why it matters
This result supplies the zero rung base case for the phi-rung value in the 8-balanced J-subset sum module. It supports the phi-ladder central to Recognition Science cost calculations, linking to the forced phi fixed point and the eight-tick octave from the unified forcing chain. No parent theorems are listed among the downstream results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.