twoPowZ_ofNat
The lemma shows that the binary scale function at a non-negative integer recovers ordinary real exponentiation by two. Workers on discrete scales and phi-ladder constructions in Recognition Science cite it when reducing natural-number cases. The proof is a one-line simplification that invokes the piecewise definition of the scale function.
claimFor every natural number $k$, the binary scale function evaluated at the non-negative integer $k$ equals $2^k$.
background
The module RecogSpec.Scales supplies binary scales and φ-exponential wrappers. The upstream definition twoPowZ gives two raised to an integer power: if the exponent is non-negative then the ordinary real power, otherwise the reciprocal of the positive power. This supplies the general integer case that the present lemma specializes to natural numbers.
proof idea
One-line wrapper that applies the definition of twoPowZ via the simp tactic.
why it matters in Recognition Science
The lemma supplies a simp rule for the non-negative case inside binary scales, which feed the phi-ladder and mass formulas. It supports the T7 eight-tick octave and discrete exponent handling required for D=3 spatial dimensions. No downstream uses are recorded, leaving it as a basic reduction step.
scope and limits
- Does not treat negative integer exponents.
- Does not extend the equality to real-valued exponents.
- Does not derive further algebraic properties of the scale function.
formal statement (Lean)
42@[simp] lemma twoPowZ_ofNat (k : Nat) : twoPowZ (Int.ofNat k) = (2 : ℝ) ^ k := by simp [twoPowZ]