B_of_succ
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not address negative or fractional indices.
- Does not relate the binary scale to the phi-exponential scale.
- Does not supply bounds or growth rates beyond the recurrence.
- Does not generalize the base or extend to other number systems.
formal statement (Lean)
14@[simp] lemma B_of_succ (k : Nat) : B_of (k+1) = 2 * B_of k := by
proof body
One-line wrapper that applies simp.
15 simp [B_of, pow_succ, mul_comm]
16