twoPowZ_zero
plain-language theorem explainer
The lemma records that the integer power function twoPowZ evaluates to 1 at the zero exponent. Researchers handling binary scaling identities in Recognition Science cite it to discharge the base case in simplification chains. The proof is a direct one-line simplification that unfolds the piecewise definition of twoPowZ.
Claim. Let $f(k) = 2^k$ for $k : ℤ$ be given by $f(k) = 2^k$ when $k ≥ 0$ and $f(k) = 1/2^{-k}$ otherwise. Then $f(0) = 1$.
background
The module RecogSpec.Scales supplies binary scales and φ-exponential wrappers. Its upstream definition twoPowZ realizes the map $k ↦ 2^k$ on the integers by the piecewise rule: for nonnegative $k$ it returns the real power $2^k$, and for negative $k$ it returns the reciprocal of $2^{-k}$. The present lemma isolates the zero case as a simp rule.
proof idea
The proof is a one-line wrapper that applies the simp tactic directly to the definition of twoPowZ.
why it matters
This identity anchors the binary scale layer that supports later constructions such as PhiPow and the B_of family inside the Recognition Science framework. It supplies the multiplicative unit required by the eight-tick octave structure (T7) and the self-similar fixed-point machinery (T6). No downstream theorems are recorded yet, leaving its use open for future scale identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.