twoPowZ_negSucc
plain-language theorem explainer
The lemma gives the explicit value of the integer two-power function at negative successors: twoPowZ(-(k+1)) equals the reciprocal of 2 to the (k+1). Workers on binary scaling inside spectral or cosmological calculations cite it to avoid case-by-case unfolding. The proof is a one-line simplification that matches the negative branch of the twoPowZ definition.
Claim. For every natural number $k$, the two-power function on integers satisfies $2^{-(k+1)} = 1 / 2^{k+1}$.
background
The module RecogSpec.Scales supplies binary scales together with phi-exponential wrappers. Its central definition twoPowZ(k) returns (2 : R)^(toNat k) when k is nonnegative and the reciprocal 1 / (2 : R)^(toNat (-k)) otherwise. The lemma isolates the negative-successor case, where Int.negSucc k stands for the integer -(k+1). Upstream, the power definition in PrimordialSpectrum multiplies amplitude by a scaled wavenumber, and the succ definitions in ArithmeticFromLogic and Vantage supply the successor operation used in the exponent.
proof idea
The proof is a one-line wrapper that applies simp with the twoPowZ definition. Unfolding the if-then-else immediately selects the else branch for a negative argument and replaces Int.toNat (-(negSucc k)) by k.succ, producing the stated reciprocal.
why it matters
The lemma finishes the integer coverage of twoPowZ, the binary-scale primitive that sits beside PhiPow in the same module. It supplies the negative-exponent arithmetic required by the power spectrum in Cosmology.PrimordialSpectrum and by any later use of binary factors in the eight-tick octave or dimensional counting. No downstream theorem yet depends on it, so it remains a local completion of the scale interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.