B_of
plain-language theorem explainer
The definition supplies the binary scale factor B(k) = 2^k as a real number in the Recognition Science scales module. Researchers deriving discrete octave progressions or eight-tick structures cite it when separating binary doubling from phi-ladder scaling. It is introduced by a direct power assignment with an empty proof body.
Claim. Define the binary scale factor by $B(k) := 2^k$ for each natural number $k$.
background
The RecogSpec.Scales module introduces binary scales together with phi-exponential wrappers to encode the discrete structure required by Recognition Science. Binary scale B(k) supplies the exact doubling factor 2 raised to integer k, which supports the eight-tick octave of period 2^3. This stands apart from the phi-ladder used for mass formulas and continuous exponents elsewhere in the framework.
proof idea
The declaration is a direct definition that maps each natural number k to the real power 2^k. No lemmas or tactics are invoked inside the definition body.
why it matters
B_of feeds the sibling lemmas B_of_zero, B_of_succ, B_of_pos, B_of_one and one_le_B_of that establish the basic arithmetic properties of the binary scale. These properties are required to realize the eight-tick octave (T7) inside the UnifiedForcingChain. The definition therefore closes the discrete binary half of the scale infrastructure before phi-based continuous scaling is layered on top.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.