CausalContactRelation
plain-language theorem explainer
A causal contact relation on a substrate lattice packages the binary predicate of past light-cone contact, with reflexivity and symmetry. Cosmologists citing the vacuum-horizon selection argument use it as the interface for the causal-accumulation principle. The declaration is a pure structure definition: contact predicate, refl, symm, and a permanence field currently filled by the trivial proposition True.
Claim. A causal contact relation on a type $\Lambda$ of substrate cells is a binary predicate $C(i,j)$ meaning a signal has traveled between $i$ and $j$ at some time $t \le t_{\mathrm{now}}$ since the initial condition at $t=0$, together with proofs that $C$ is reflexive and symmetric. Permanence of contact (once in contact, always in contact) is recorded as a field currently witnessed by the trivial proposition $\mathrm{True}$.
background
The module VacuumHorizonForcing addresses which cosmological horizon should enter the vacuum-energy rung count. The vacuum density is written $\rho_\Lambda = \rho_{\mathrm{Pl}} \cdot \varphi^{-2s}$ with $s$ the rung count from substrate scale to horizon; particle horizon, Hubble radius, and de Sitter event horizon give three different $s$ and three different $\rho_\Lambda/\rho_{\mathrm{obs}}$ ratios. Only the particle horizon matches observation near unity.
The selection rests on the causal-accumulation principle: the recognition ledger $\mathcal{L}(i,j)$ is defined only for cells that have exchanged a comparison, and two cells can compare only if a signal has already traveled between them. The vacuum ledger cost is then the ground-state total over the maximal causally connected region, whose boundary is the particle horizon by definition.
This structure is the abstract interface for that contact relation on an arbitrary cell type $\Lambda$. It does not yet encode dynamics or a metric; it only records the logical shape of contact (reflexive, symmetric, and notionally permanent).
proof idea
No proof body: the declaration is a structure (data + axioms as fields). The four fields are the contact predicate, a reflexivity axiom, a symmetry axiom, and a permanence slot currently filled by True as a placeholder. Downstream definitions read the fields directly (e.g. neighborhood membership reduces to the reflexivity field).
why it matters
This structure is the entry point for the causal-accumulation argument that forces the particle horizon over the Hubble radius and the de Sitter event horizon. Downstream, causalNeighborhood builds the set of cells in contact with a fixed cell, and mem_causalNeighborhood_self is the immediate reflexivity corollary used when summing ledger cost over that set.
In the module narrative, permanence of contact is what excludes the Hubble radius: cells that contacted earlier remain in the ledger even if their present recession speed exceeds $c$. The de Sitter event horizon is excluded because it needs future null infinity. The structure therefore sits under the structural theorem that causal accumulation selects the particle horizon (rung count $s \approx 294$), tying vacuum energy to the $\varphi$-ladder cosmology without an extra free scale.
It is definitional scaffolding for that selection, not itself a dynamical theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.