B_of_pos
The lemma establishes that the binary scale factor 2^k is strictly positive for every natural number k. Researchers constructing discrete scales or ladders in Recognition Science would cite this positivity to ensure exponential factors remain well-defined when applying composition laws or building phi-ladders. The proof is a short tactic sequence that first confirms 0 < 2 by norm_num then reduces via simplification to the general positivity of powers.
claimFor every natural number $k$, the real number $2^k$ satisfies $2^k > 0$.
background
The module introduces binary scales and φ-exponential wrappers. The binary scale factor is defined as the real number $2^k$. This lemma depends only on that definition and supplies the positivity needed for subsequent scale constructions in the same module.
proof idea
The tactic proof first uses norm_num to obtain 0 < 2, then applies simpa with the definition of the binary scale factor to reduce the goal to the standard lemma pow_pos.
why it matters in Recognition Science
This result supplies a basic positivity fact for the binary scale constructions in the module on binary scales and φ-exponential wrappers. It supports later arguments that rely on positive factors when forming ladders or invoking the Recognition Composition Law. No downstream theorems are recorded, so it functions as an elementary building block for the scale machinery.
scope and limits
- Does not address negative or fractional exponents.
- Does not connect the binary scale to the φ-exponential wrappers in the same module.
- Does not derive any relation to the eight-tick octave or spatial dimension results.
formal statement (Lean)
17lemma B_of_pos (k : Nat) : 0 < B_of k := by
proof body
Tactic-mode proof.
18 have : 0 < (2:ℝ) := by norm_num
19 simpa [B_of] using pow_pos this k
20