tick_addressing
plain-language theorem explainer
The 8-tick cycle carries a 4-bit addressing budget, fixed at the natural number 16 = 2^4. Anyone deriving the raw dark-energy fraction Ω_Λ from Recognition Science phase-mode combinatorics cites this constant as the denominator of the saturated mode count. It is a bare definition, not a proved identity.
Claim. The tick-addressing budget of the 8-tick cycle is the natural number $16 = 2^{4}$ (four addressing bits, two bits per epoch half).
background
The module derives the cosmological constant fraction $\Omega_\Lambda$ from phase-mode saturation on the forced 8-tick octave (forcing-chain landmark T7). The raw saturated fraction is an integer ratio: eleven $Q_3$-symmetric modes over a sixteen-slot addressing budget, before a one-loop electromagnetic correction of size $\alpha/\pi$.
The number sixteen is not free. It is the cardinality of 4-bit addresses on the 8-tick cycle (two bits per epoch half), equivalently $2^4$. The companion numerator is the saturated mode count $N_{\mathrm{modes,sat}} = 11$, coming from the $[4,2,2]$ Gray-code asymmetry under $S_3$ breaking (three spatial axes plus the gap sector).
Downstream, the raw fraction is exactly this ratio cast to $\mathbb{R}$, and the full $\Omega_\Lambda$ subtracts the measured CODATA $\alpha/\pi$ correction.
proof idea
Bare definition: the constant is introduced by assigning the natural number 16. No tactics, no lemmas. A sibling theorem later records the power-of-two identity $16 = 2^4$ by decide.
why it matters
This constant is the structural denominator in the Recognition Science formula $\Omega_\Lambda = 11/16 - \alpha/\pi$. It is unfolded in omega_raw (the raw saturated fraction), in the equality proof that the raw fraction equals $11/16$, and in the one-measured-input and canonical-form theorems that isolate combinatorics from the single CODATA $\alpha$ input.
The power-of-two companion theorem records $16 = 2^4$ as the 4-bit addressing of the 8-tick cycle, tying the constant to T7 (eight-tick octave) rather than to an empirical fit. Without a fixed addressing budget the saturated fraction would not be a pure rational, and the claim that only $\alpha$ is measured would fail.
The module's target band $(0.680, 0.700)$ and the Planck 2018 anchor both sit on top of this integer skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.