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