lambda_efe_dimension
plain-language theorem explainer
The dark-energy-extended Einstein data package records spacetime dimension 4 for every real Hubble-scale input. Gravity and cosmology authors citing the Λ-augmented RS EFE chain use this to confirm the geometric slot matches the baseline package. The proof is pure definitional reflexivity: the structure sets dimension to 4.
Claim. For every real $H_0^2$, the spacetime dimension field of the Recognition Science full Einstein data carrying the forced cosmological constant $\Lambda_{\mathrm{RS}}(H_0^2)$ equals $4$.
background
This module closes the gravity-facing gap that the baseline RS Einstein package carried a vanishing cosmological constant. It installs the forced vacuum term $\Lambda_{\mathrm{RS}}(H_0^2) = 3 H_0^2 \cdot \Omega_\Lambda$ with the RS fraction $\Omega_\Lambda = 11/16 - \alpha/\pi$, keeping the derived coupling $\kappa = 8\varphi^5$ and dimension 4.
The structure rs_efe_data_with_lambda is the Λ-extended FullEFEData record: dimension hard-coded to 4, kappa copied from the baseline package, and cosmological constant set to $\Lambda_{\mathrm{RS}}(H_0^2)$. Upstream, that definition already supplies a reflexivity witness that dimension equals 4 inside the structure fields.
Dimension 4 here is the full spacetime count (three spatial plus time), consistent with the forcing-chain landmark that spatial dimension is three.
proof idea
One-line definitional reflexivity. The target field is literally assigned dimension := 4 in the structure definition of the Λ-extended EFE data, so equality to 4 holds by rfl with no further lemmas.
why it matters
The module's second established point is that the Λ-extended EFE data recovers the baseline: same $\kappa = 8\varphi^5$, same dimension 4; only the cosmological-constant slot changes. This theorem is the dimension half of that recovery claim.
It keeps the dark-energy package on the same geometric footing as the zero-Λ master chain, so downstream conservation and equation-of-state arguments (vacuum $w = -1$, covariant conservation of $c\cdot g$ via metric compatibility) do not have to re-negotiate dimension. No downstream dependents are wired yet in the graph; the declaration is a local structural sanity check inside the QG integration of the forced vacuum term.
It does not itself re-derive $D = 3$ spatial dimensions from the T0–T8 forcing chain; it only records the agreed spacetime count in the EFE data record.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.