omega_lambda_from_phi_carried_prop
plain-language theorem explainer
Packages the four carried claims of the cosmological-constant clause (M4): the closed formula Ω_Λ = 11/16 − α/π with CODATA α, the numerical band (0.683, 0.686), Planck-2018 2σ consistency, and the gap-from-dimension rung −44 at D = 3. Cosmologists and RS auditors cite it as the pure content half of Track 4.A. It is a bare Prop conjunction, not a proved theorem.
Claim. The conjunction of: (i) $\Omega_\Lambda = 11/16 - \alpha_{\mathrm{CODATA}}/\pi$; (ii) $0.683 < \Omega_\Lambda < 0.686$; (iii) $|\Omega_\Lambda - \Omega_\Lambda^{\mathrm{Planck\,2018}}| < 2\,\sigma_{\mathrm{Planck}}$; (iv) the baryon-asymmetry rung from the gap-from-dimension formula at spatial dimension $D=3$ equals $-44$.
background
Module Gravity.MasterTheorem authors the twelve-clause master statement of RS quantum gravity (Track 7.A). Closed clauses are inhabited from existing theorems; open ones remain hypothesis inputs. Clause M4 is the cosmological-constant prediction from φ (Track 4.A).
Upstream, OmegaLambdaDerivation.omega_lambda is defined as $\Omega_\Lambda = 11/16 - \alpha/\pi$. The raw piece $11/16 = 0.6875$ is the vacuum-mode fraction of the eight-tick ledger cycle; the $-\alpha/\pi$ term is the electromagnetic correction from matter-coupled modes. Here $\alpha$ is pinned to the external CODATA 2022 anchor. The same module supplies the Planck-2018 central value and $1\sigma$ error used in the $2\sigma$ consistency check.
Separately, eta_B_rung_from_dimension d := A - dimensionGap(d) evaluates at the T8/T9-forced $D=3$ to the integer rung $-44$, linking the dark-energy clause to the baryon-asymmetry ladder.
proof idea
Definitional packaging only: a four-way ∧ of equalities and inequalities already named in Cosmology.OmegaLambdaDerivation and Cosmology.EtaBExactRungDerivation. No tactics, no lemmas applied, no proof obligations discharged. The inhabitation of this Prop is deferred to the surrounding Track 4.A certificate and to the master-theorem proof that consumes omega_lambda_from_phi.
why it matters
This is the pure mathematical content half of master-clause M4. Downstream, omega_lambda_from_phi conjoins it with Nonempty Track4ACert, so the master theorem can cite a single named Prop for "cosmological constant from φ."
Framework landmarks: the $11/16$ vacuum fraction sits on the T7 eight-tick octave; $D=3$ is the T8 spatial-dimension forcing; the rung $-44$ is the gap-from-dimension evaluation that also feeds $\eta_B$. The formula uses the external CODATA $\alpha$ rather than the RS-native $\alpha$ band, keeping the clause observationally anchored.
It does not itself close Track 4.A; the certificate half remains separate. Inside the conditional master theorem it is among the CLOSED clauses discharged from existing Lean material once the five open hypothesis inputs are assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.