H_ScaleInvariance
plain-language theorem explainer
Hypothesis that phase-saturation vacuum energy is scale-invariant: for every positive real scale, the dark-energy fraction equals the fixed RS formula 11/16 − α/π. Cosmologists working the RS Ω_Λ derivation cite it as the scale-independence assumption. Encoded as a Prop; the matching consistency theorem is a one-line reflexivity proof.
Claim. For every real number $s > 0$, the RS dark-energy fraction satisfies $\Omega_\Lambda = \frac{11}{16} - \frac{\alpha}{\pi}$, with $\alpha$ the measured fine-structure constant.
background
This module identifies the cosmological dark-energy fraction with the equilibrium vacuum share of a discrete ledger under phase saturation. The RS prediction is $\Omega_\Lambda = 11/16 - \alpha/\pi$: a cube-geometry seed $11/16$ from passive-mode counting on $Q_3$, corrected by the electromagnetic term $\alpha/\pi$.
Here $\alpha$ is the single measured input (CODATA fine-structure constant). $\Omega_\Lambda$ is defined exactly as that closed form. The NonExistenceCost functional is stated on abstract LightMemoryState patterns in an abstract Region, with no built-in length scale.
The local chain runs: finite phase capacity ($\varphi^{45}$) $\to$ cosmic matter/vacuum equilibrium $\to$ vacuum fraction equals the passive-mode fraction $\to$ numerical value $\approx 0.6852$. Scale invariance is the claim that this equilibrium formula does not pick a preferred scale.
proof idea
Not a proved theorem: a Prop definition. The body is the universal statement that for every positive real scale, $\Omega_\Lambda$ equals the constant expression $11/16 - \alpha/\pi$.
No lemmas are applied at the definition site. Downstream, scale_invariance_consistent discharges the Prop by introducing the scale hypothesis and closing with rfl, because the right-hand side is definitionally $\Omega_\Lambda$ and carries no scale dependence.
why it matters
Anchors the scale-free reading of phase-saturation vacuum energy inside the RS cosmology stack. Downstream, scale_invariance_consistent proves the Prop holds definitionally, and the same module’s cosmic-phase-equilibrium consistency theorem uses the identical $\Omega_\Lambda$ unfolding.
Doc-comment status is HYPOTHESIS: the NonExistenceCost and its equilibrium theorem never mention a particular scale, so the mechanism is asserted to apply from abstract ledger regions up to the observable universe. That underwrites treating $\Omega_\Lambda \approx 0.685$ as a global fraction rather than a scale-dependent density, which is the entry point to the module’s resolution of the $10^{120}$ vacuum-energy mismatch (RS vacuum energy is not a Planck-scale density).
Ties to the broader forcing picture only indirectly: $\alpha$ is the measured EM input already constrained in the RS constant ladder; the geometric $11/16$ seed is combinatorial mode counting, not a T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.