B_of_zero
The lemma records that the binary scale factor equals unity at the zero exponent. Workers constructing inductive arguments over natural-number scales in Recognition Science cite this base case when building discrete ladders. The proof is a direct simplification that unfolds the power definition.
claim$B(0) = 1$, where the binary scale factor is defined by $B(k) = 2^k$ for $k$ a natural number.
background
The module supplies binary scales and φ-exponential wrappers. The binary scale factor is introduced as the real-valued function $B(k) = 2^k$. This definition supplies the discrete doubling structure that sits alongside the phi-ladder constructions elsewhere in the Recognition framework.
proof idea
The proof is a one-line wrapper that applies simp using the definition of B_of.
why it matters in Recognition Science
The result supplies the zero base case for binary scales inside the RecogSpec module. It anchors the doubling component that aligns with the eight-tick octave structure in the forcing chain. No downstream theorems are recorded, marking it as an early foundational element.
scope and limits
- Does not evaluate B for negative exponents.
- Does not relate B to the J-cost or Recognition Composition Law.
- Does not prove any inductive step or successor case.
formal statement (Lean)
12@[simp] lemma B_of_zero : B_of 0 = 1 := by simp [B_of]
proof body
13