B_of_succ
plain-language theorem explainer
The recurrence for the binary scale factor shows that its value at the successor index equals twice the value at the prior index. Researchers building inductive arguments over natural-number scales in the binary scales module cite this result to simplify successive doublings. The proof is a one-line simp wrapper that unfolds the scale definition and applies the successor power rule together with multiplication commutativity.
Claim. For the binary scale factor $B(k) = 2^k$ with $k$ a natural number, $B(k+1) = 2 B(k)$.
background
The module introduces binary scales and φ-exponential wrappers as part of the Recognition Science scales layer. The binary scale factor is defined by $B(k) = 2^k$ taking values in the reals. This supplies the basic recurrence needed for inductive arguments that appear in downstream lemmas on lower bounds for the scale.
proof idea
The proof is a one-line wrapper that applies simp with the definition of the binary scale factor, the successor rule for powers, and commutativity of multiplication.
why it matters
This lemma supplies the inductive step for the lower-bound result one_le_B_of. It fills the basic recurrence for binary scales, which supports construction of the phi-ladder and related constants in the Recognition framework. No open questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.