IndisputableMonolith.Cosmology.VacuumHorizonForcing
Module that sets up causal contact on the RS substrate lattice and forces which cosmological horizon type vacuum-energy selection can use. It defines causal neighborhoods, three horizon models (particle, Hubble radius, de Sitter), a vacuum-energy exponent, and comparison lemmas that pick the particle horizon. Cosmologists matching RS vacuum energy to the φ-ladder would cite it. Structure is definitional models plus contact-set selection facts.
claimOn a substrate lattice, a causal contact relation holds between cells when a signal has linked them at some $t\le t_{\mathrm{now}}$ since $t=0$. The module defines the causal neighborhood of a cell, three horizon models (particle horizon, Hubble radius, de Sitter), and a vacuum-energy exponent, then records that causal accumulation selects the particle horizon, that the Hubble radius excludes past contacts, and that de Sitter requires a future boundary.
background
Recognition Science cosmology is built on discrete ticks and the φ-ladder. The module imports the RS time quantum $\tau_0=1$ tick from Constants and the baryon-rung arithmetic (factorizations through the 8-tick period) from PhiRungLadder.
The local objects are a causal contact relation on the substrate lattice: two cells are related precisely when a signal has traveled between them by the present time from the initial slice. From that relation one forms the causal neighborhood of a cell (which always contains the cell itself) and packages standard cosmological horizons as models: particle horizon (integrated past contacts from $t=0$), Hubble radius, and de Sitter.
A vacuum-energy exponent is the RS scalar whose admissible value is constrained by which horizon type can accumulate contacts consistently with the ladder and tick structure.
proof idea
Definition-led module, not a single theorem. It introduces the causal contact relation and causal neighborhood (with a reflexivity fact), an enumeration of horizon kinds, and concrete HorizonModel instances for particle, Hubble-radius, and de Sitter cases, plus the vacuum-energy exponent.
The argumentative content is three comparison lemmas: causal accumulation selects the particle horizon; the Hubble-radius model excludes past contacts; de Sitter requires a future boundary. Together those facts force the particle horizon as the only model compatible with causal accumulation for vacuum selection.
why it matters in Recognition Science
Gives the vacuum-horizon step of RS cosmology a discrete causal substrate instead of a continuum ansatz. The forced choice of particle horizon is the intended input to any later match of the vacuum-energy exponent against φ-ladder rungs and the eight-tick octave (T7), using the imported PhiRungLadder arithmetic.
No downstream used_by edges are recorded yet, so the module is presently a leaf: it packages the horizon-selection claim for a future global vacuum-energy theorem rather than discharging one. It does not itself close forcing-chain steps T0–T8; those remain upstream foundation.
scope and limits
- Does not derive a numerical vacuum energy density from first principles alone.
- Does not prove uniqueness of the underlying substrate lattice geometry.
- Does not treat metric dynamics or quantum backreaction beyond horizon kinematics.
- Does not fit observational H0 or dark-energy equation-of-state data.
- Does not discharge global forcing-chain landmarks T0–T8.
depends on (2)
declarations in this module (20)
-
structure
CausalContactRelation -
def
causalNeighborhood -
theorem
mem_causalNeighborhood_self -
inductive
HorizonType -
structure
HorizonModel -
def
particleHorizonModel -
def
hubbleRadiusModel -
def
deSitterModel -
def
vacuumEnergyExponent -
theorem
causal_accumulation_selects_particle_horizon -
theorem
hubbleRadius_excludes_past_contacts -
theorem
deSitter_requires_future -
def
particleHorizonRungCount -
theorem
vacuumExponent_particleHorizon -
theorem
hubble_vs_particle_rung_gap -
theorem
phi_power_ten_large -
structure
VacuumHorizonForcingCert -
def
vacuumHorizonForcingCert -
theorem
vacuumHorizonForcingCert_inhabited -
theorem
vacuum_horizon_forcing_one_statement