B_of_one
Binary scale evaluation at natural exponent 1 returns exactly 2 under the real power definition. Recognition Science workers on phi-exponential wrappers reference this base case when normalizing the B ladder before composing with J-cost or defect distances. The equality follows in one simplification step from the defining equation of the scale function.
claim$B(1) = 2$ where $B(k) := 2^k$ for natural number $k$.
background
The module RecogSpec.Scales supplies binary scales as real-valued powers of 2 to wrap phi-exponentials. The definition states that B_of maps each natural number k to the real 2 raised to k. This supplies the integer rung scaling that later lemmas combine with the phi-ladder and the eight-tick octave.
proof idea
One-line wrapper that applies the definition of B_of via the simp tactic.
why it matters in Recognition Science
The lemma supplies the unit base case for the binary scales that feed the phi-exponential wrappers and the Recognition Composition Law constructions. It anchors the B ladder before any addition or successor steps are taken in the same module.
scope and limits
- Does not treat negative or non-integer exponents.
- Does not invoke the J-uniqueness formula or the recognition composition law.
- Does not connect to spatial dimension forcing or the alpha band.
formal statement (Lean)
21@[simp] lemma B_of_one : B_of 1 = 2 := by simp [B_of]
proof body
22