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