hubbleRadius_excludes_past_contacts
plain-language theorem explainer
Any horizon model typed as the Hubble radius and carrying the non-accumulated flag has causal-accumulation unequal to true. Cosmologists selecting the vacuum-energy rung cite this to bar the instantaneous Hubble sphere from the ledger sum. The argument is a one-line Boolean simplification from the false flag; the type hypothesis is unused.
Claim. For every cosmological horizon model $H$, if $H$ has Hubble-radius type and its causal-accumulation flag equals $\mathrm{false}$, then that flag is not equal to $\mathrm{true}$.
background
The module forces which cosmological horizon bounds the vacuum ledger cost $\rho_\Lambda = \rho_{\mathrm{Pl}}\cdot\varphi^{-2s}$. Three candidates (particle horizon, Hubble radius, de Sitter event horizon) give rung counts $s\in{294,289,290}$ and very different $\rho_\Lambda$ ratios; only the particle horizon matches observation.
A HorizonModel packages horizon type, positive comoving radius, rung count from the substrate scale, and a Boolean isCausallyAccumulated recording whether the boundary is the past light-cone accumulation set. The causal-accumulation principle says the ledger $\mathcal{L}(i,j)$ is defined only for substrate cells that have already exchanged a comparison, so the vacuum cost is the ground-state sum over the maximal past-connected region.
The Hubble radius is the instantaneous surface where recession velocity equals $c$, not that accumulated set. Cells now outside $r_H$ may still sit in the past light cone from an earlier epoch; the ledger already recorded those comparisons.
proof idea
Term/tactic hybrid: introduce the model $H$, discard the unused Hubble-type hypothesis, and keep the hypothesis that the accumulation flag equals false. A single simp rewrite on that equality yields false $\neq$ true. No cost algebra, rung arithmetic, or horizon-radius lemmas are invoked.
why it matters
Closes one exclusion arm of vacuum-horizon forcing: the Hubble sphere cannot serve as the ledger boundary because it drops past contacts. Together with the sibling that de Sitter depends on future expansion, this leaves the particle horizon as the unique causally accumulated boundary, matching the module table entry $\rho_\Lambda/\rho_{\mathrm{obs}}\sim 1$ at rung $s=294$. Downstream selection theorems (e.g. causal accumulation selects the particle horizon) rely on this Boolean gate even though no used_by edge is recorded yet. Framework link: the vacuum cost sits on the $\varphi$-ladder; wrong horizon choice shifts the rung by $\sim 5$ and spoils the match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.