causalNeighborhood
plain-language theorem explainer
The causal neighborhood of a lattice cell is the set of all cells that have exchanged a comparison signal with it since the initial condition. Cosmologists working the vacuum-horizon selection argument cite it as the domain of the recognition ledger sum. It is a one-line set comprehension from the contact predicate of a causal-contact relation.
Claim. Given a causal contact relation $C$ on a substrate lattice $\Lambda$ and a cell $i \in \Lambda$, the causal neighborhood of $i$ is the set $\{ j \in \Lambda \mid C.\mathrm{inContact}(i,j) \}$.
background
The module forces which cosmological horizon enters the vacuum-energy rung count. Vacuum density is written $\rho_\Lambda = \rho_{\mathrm{Pl}} \cdot \varphi^{-2s}$ with $s$ the rung count from substrate scale to horizon; particle, Hubble, and de Sitter horizons give different $s$ and only the particle horizon matches observation.
A causal contact relation on $\Lambda$ packages a predicate "in contact" together with reflexivity, symmetry, and permanence: two cells are in contact iff a signal has traveled between them at some $t \le t_{\mathrm{now}}$ since $t=0$. The recognition ledger $\mathcal{L}(i,j)$ is defined only for pairs that have compared, so the vacuum cost is the ground-state total ledger sum over the maximal causally connected region.
Upstream, the foundation lattice already uses a finite-resolution neighborhood (cells sharing an observed label). Here the neighborhood is causal rather than observational: it is exactly the contact class of a fixed cell.
proof idea
Pure definition: the set comprehension ${ j \mid C.\mathrm{inContact}, i, j }$. No lemmas are applied. Reflexivity of the contact relation immediately places $i$ in its own neighborhood (used by the next theorem).
why it matters
This set is the domain over which the causal-accumulation principle sums ledger cost. Downstream, mem_causalNeighborhood_self records that every cell lies in its own neighborhood via contact reflexivity, which is the base fact before horizon-type models (particle, Hubble, de Sitter) are compared.
The module's structural claim is that the boundary of the maximal causally connected region is the particle horizon by definition, excluding the Hubble radius (instantaneous, not accumulated contact) and the de Sitter event horizon (future-dependent). The neighborhood definition is the set-theoretic carrier for that selection. It sits in the cosmology layer that feeds the vacuum rung $s$ into the $\varphi$-ladder mass and density formulae; it does not itself invoke T5--T8 or the RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.