omega_raw_eq
plain-language theorem explainer
The raw dark-energy saturation fraction equals exactly 11/16 before any electromagnetic correction. Cosmologists citing the RS Ω_Λ derivation use this as the combinatorial baseline. The proof unfolds the two integer mode counts and reduces by norm_num.
Claim. The raw saturated fraction equals $11/16$: if $N_{\mathrm{sat}}=11$ is the $Q_3$-saturated mode count and $N_{\mathrm{addr}}=16=2^4$ is the 8-tick addressing budget, then $N_{\mathrm{sat}}/N_{\mathrm{addr}}=11/16$.
background
This module derives the cosmological constant fraction $\Omega_\Lambda$ from phase-mode saturation on the eight-tick cycle. The core claim is $\Omega_\Lambda=11/16-\alpha/\pi\in(0.680,0.700)$, matching Planck 2018 within error.
Upstream definitions fix the integers: $N_{\mathrm{modes,sat}}=11$ ("$Q_3$-saturated modes: 11, from $[4,2,2]$ Gray-code + gauge structure") and tick addressing $2^4=16$ ("8-tick addressing bits"). The raw fraction is their real quotient, before the one-loop EM correction $\alpha/\pi$.
The 11 count is the $Q_3$-symmetric sector under the forced 44-mode 8-tick DFT structure (3 spatial + gauge degrees of freedom); 16 is the 4-bit address space of the octave (two bits per epoch half). This sits on the T7 eight-tick landmark.
proof idea
Term-mode proof by unfolding. Expand the raw fraction definition to the ratio of the two naturals, substitute $N_{\mathrm{modes,sat}}=11$ and tick addressing $=16$, then norm_num discharges the rational equality $11/16=11/16$ in $\mathbb{R}$. No external lemmas beyond the three local defs.
why it matters
This is the exact combinatorial identity behind Step 2 of the $\Omega_\Lambda$ derivation: the saturated fraction is $11/16$ from 8-tick addressing combinatorics. Downstream, omega_raw_val rewrites it as the decimal $0.6875$, and omegaLambdaCert packages it as the raw_fraction field of the certificate (together with EM-correction bounds and the final interval).
In the framework it is the pre-correction baseline for dark energy: $\Omega_\Lambda=11/16-\alpha/\pi\approx0.6852$, compared with Planck $0.6889\pm0.0056$. It ties the cosmology side to T7 (eight-tick octave) and the forced mode budget, without yet touching $\alpha$ or the measured-input status of the EM term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.