mem_causalNeighborhood_self
plain-language theorem explainer
Every substrate cell lies in its own causal neighborhood under any causal contact relation. Cosmologists deriving vacuum-horizon selection from causal accumulation cite this as the reflexivity baseline for the ledger sum. The proof is a one-line appeal to the relation's built-in reflexivity field.
Claim. Let $C$ be a causal contact relation on a substrate lattice $\Lambda$. For every cell $i \in \Lambda$, one has $i \in N_C(i)$, where $N_C(i) = \{ j \in \Lambda : C(i,j) \}$ is the causal neighborhood of $i$.
background
This module forces the vacuum energy horizon from the causal-accumulation principle. The vacuum ledger cost is the ground-state value of $\sum_{i,j} \mathcal{L}(i,j)$ over the maximal causally connected region; that region's boundary is the particle horizon by definition, excluding the Hubble radius (instantaneous, not accumulated contact) and the de Sitter event horizon (future-dependent).
A causal contact relation $C$ on lattice $\Lambda$ is a predicate $C(i,j)$ meaning a signal has traveled between cells $i$ and $j$ at some $t \le t_{\mathrm{now}}$ since $t=0$. It carries reflexivity (every cell contacts itself), symmetry, and permanence (contact once established is never lost). The causal neighborhood $N_C(i)$ is the set ${j : C(i,j)}$.
proof idea
One-line term proof: membership $i \in N_C(i)$ unfolds to $C(i,i)$, which is exactly the reflexivity field of the causal contact structure applied at $i$.
why it matters
Reflexivity is the minimal sanity check before any ledger sum over a causal neighborhood: without self-membership the diagonal terms of $\sum_{i,j} \mathcal{L}(i,j)$ would be ill-defined. The module uses this neighborhood apparatus to select the particle horizon (rung $s \approx 294$, $\rho_\Lambda/\rho_{\mathrm{obs}} \approx 1$) over the Hubble radius and de Sitter event horizon via causal accumulation. Downstream horizon-selection lemmas (particle-horizon selection, Hubble exclusion of past contacts, de Sitter future-dependence) rest on neighborhoods being well-formed reflexive sets. No external used-by edges are recorded yet; the result is local scaffolding for §2 horizon-type comparisons.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.