one_le_B_of
plain-language theorem explainer
The lemma establishes that the binary scale factor B(k) = 2^k satisfies 1 ≤ B(k) for every natural number k. Cosmologists normalizing amplitudes in primordial spectra or scale factors within Recognition Science would cite this bound to keep quantities positive. The proof proceeds by induction on k, using the successor relation B(k+1) = 2 B(k) and monotonicity of multiplication by a positive constant.
Claim. For every natural number $k$, $1 ≤ 2^k$ holds in the reals.
background
The module RecogSpec.Scales defines binary scale factors as wrappers for exponential growth steps. B_of(k) is the real number 2^k, supplying the scale at integer rung k. This lower bound is invoked when composing scales with power spectra, where amplitude is multiplied by a factor depending on wavenumber k.
proof idea
The proof applies induction on k. The zero case simplifies B_of 0 directly to 1. The successor step multiplies the induction hypothesis by 2 via mul_le_mul_of_nonneg_left, then applies le_trans to the fact 1 ≤ 2 to reach 1 ≤ 2 B_of k, which equals B_of(k+1) by the successor lemma.
why it matters
This bound anchors the binary scales module, guaranteeing positivity when scales feed into spectrum calculations or φ-exponential wrappers. It supports the eight-tick octave structure by ensuring scale factors remain at least unity at every integer step. No downstream uses are recorded yet, but the result closes a basic consistency property required for the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.