twoPowZ
plain-language theorem explainer
The definition supplies the real value of 2 raised to any integer exponent k. It is cited by the three immediate lemmas that fix its value at zero, positive naturals, and negative successors. The body performs a sign test on k and delegates to real exponentiation after mapping the absolute value through toNat.
Claim. For any integer $k$, define $2^k$ by cases: if $k$ is nonnegative then $2$ raised to the natural number obtained from $k$ via toNat; otherwise the reciprocal of $2$ raised to the natural number obtained from $-k$ via toNat.
background
The module RecogSpec.Scales introduces binary scales together with their φ-exponential wrappers. The present definition supplies the integer-power case for base 2, providing the binary counterpart to the φ-ladder used elsewhere in the framework. Upstream, toNat from ArithmeticFromLogic maps a LogicNat to an ordinary Nat by counting iteration steps (identity maps to 0, each step adds a successor). The definition applies the corresponding Int.toNat to obtain a nonnegative exponent for real exponentiation.
proof idea
The definition is written directly as an if-then-else on the predicate 0 ≤ k. The true branch returns (2 : ℝ) ^ (Int.toNat k); the false branch returns the reciprocal of (2 : ℝ) ^ (Int.toNat (-k)). No auxiliary lemmas are invoked inside the definition.
why it matters
This definition anchors the binary-scale constructions that complement the φ-powers appearing in the Recognition framework. It is invoked by the three simp lemmas twoPowZ_zero, twoPowZ_ofNat and twoPowZ_negSucc that establish its concrete values at the obvious points. Those lemmas in turn feed the φ-exponential wrappers documented in the module header.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.