tick_addressing_is_power2
plain-language theorem explainer
The 8-tick addressing bit count equals $2^4$, i.e. sixteen addressable slots. Cosmology derivations that write the raw dark-energy saturation as $11/16$ cite this equality to make the denominator an explicit power of two rather than a bare numeral. The proof is a one-step computational decision of the definitional equality $16=2^4$.
Claim. The tick-addressing constant (the number of addressable slots in the 8-tick cycle) equals $2^4$.
background
In the $\Omega_\Lambda$ module the dark-energy fraction is built as an integer combinatorial ratio minus a small electromagnetic correction: $\Omega_\Lambda=11/16-\alpha/\pi$. The denominator 16 is the addressing budget of the fundamental 8-tick evolution period (the RS octave, forced at T7 of the unified forcing chain).
The definition tick_addressing simply records that budget as the natural number 16, with the accompanying gloss that it arises as four half-epoch bits ($2$ bits per half of the octave). The fundamental tick itself is the RS time quantum $\tau_0=1$ in native units; one octave is eight ticks.
This lemma only rewrites that numeral as an explicit power of two, so later steps can treat the saturated fraction as a pure dyadic rational forced by binary addressing rather than an arbitrary integer choice.
proof idea
One-line computational proof: by decide discharges $16=2^4$ by kernel evaluation of both sides as natural numbers. No lemmas are invoked; the goal is pure definitional arithmetic once tick_addressing unfolds to 16.
why it matters
The parent narrative is the one-measured-input theorem for $\Omega_\Lambda$: structural content is the pair of integers $(11,16)$ forced by the $[4,2,2]$ Gray-code asymmetry and 8-tick addressing, while $\alpha$ enters only as the CODATA boundary datum in the $-\alpha/\pi$ correction. Making $16=2^4$ a named theorem pins the denominator to the binary addressing of the eight-tick octave (T7) rather than a free combinatorial parameter.
Downstream siblings (omega_raw, omega_lambda, the open interval bounds around $0.68$–$0.69$) consume the ratio $11/16$; this equality is the justification that the denominator is the forced power-of-two address space. No further theorems currently depend on it by name, but it is the explicit bridge from the 8-tick DFT story to the saturated-fraction combinatorics used throughout the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.