twoPowZ_ofNat
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.