Cosmology Vacuum Horizon Forcing Vacuum Horizon Forcing Cert Inhabited

The particle horizon certificate

In cosmology, the particle horizon is the boundary of the region from which light has had time to reach us since the Big Bang. The Hubble radius is the distance at which galaxies currently recede at light speed, and the de Sitter event horizon is the boundary beyond which light emitted today will never reach us. These three distances are not the same, and a calculation of vacuum energy can depend on which one you choose.

The Recognition Science framework carries out such a calculation. Its vacuum energy formula gives ρ_Λ = ρ_Pl · φ^(-2s), where s is a count of scaling steps, called rungs, from the smallest substrate scale up to a horizon radius. The framework's ledger, a discrete record of which cells have exchanged comparisons, only includes cells that have been in causal contact. Because causal contact is permanent, once two cells have compared, they stay in the ledger even if cosmic expansion later carries them apart faster than light.

This permanent, past-directed structure selects the particle horizon. The Hubble radius is rejected because it is an instantaneous measure, it excludes cells that were in contact earlier but now recede faster than light. The de Sitter horizon is rejected because it requires knowledge of future expansion, while the ledger only records comparisons that have already happened. The framework proves this selection in a machine-checked library of formal theorems, with no axioms beyond the standard logical ones.

The declaration vacuumHorizonForcingCert_inhabited establishes that a certificate exists: a formal object recording three boolean flags. The particle horizon is causally accumulated, the Hubble radius is not, and the de Sitter horizon requires future information. The certificate also records the rung count 294 for the particle horizon and the resulting exponent -588 in the vacuum energy formula. The existence of this certificate is the formal statement that the selection argument is coherent and complete.

The certificate does not claim that the particle horizon is the correct choice for the observed universe. It claims that, within the framework's causal-accumulation principle, the particle horizon is the only one of the three candidates that satisfies the condition of being based entirely on past contact. The rung count 294 is a definitional choice, not a derived measurement. The framework's comparison to the observed vacuum energy density, which lands near the measured value, is an empirical check, not part of the certificate.

theorem vacuumHorizonForcingCert_inhabited :
    Nonempty VacuumHorizonForcingCert :=
  ⟨vacuumHorizonForcingCert⟩

/-- **CAUSAL-ACCUMULATION SELECTION.**  The particle horizon is the unique
horizon that:
1. Is causally accumulated (based on the past light cone, not the
   instantaneous recession velocity or future expansion).
2. Does not require future information.
3. Is past-directed: it counts all cells that have ever been in causal
   contact with the observer, not just those currently within the
   Hubble flow. -/
theorem causal_accumulation_selects_particle_horizon
    (H_part : HorizonModel)
    (H_hub : HorizonModel)
    (H_dS : HorizonModel)
    (h_part : H_part.isCausallyAccumulated = true ∧ H_part.requiresFutureInfo = false)
    (h_hub : H_hub.isCausallyAccumulated = false)
    (h_dS : H_dS.requiresFutureInfo = true) :
    H_part.isCausallyAccumulated = true ∧
    H_hub.isCausallyAccumulated = false ∧
    H_dS.requiresFutureInfo = true :=
  ⟨h_part.1, h_hub, h_dS⟩

/-- **VACUUM HORIZON FORCING ONE-STATEMENT.**  The particle horizon is
selected by the causal-accumulation principle.  The Hubble radius and
de Sitter event horizon are excluded by past-directedness.  The rung
count to the particle horizon is 294, giving vacuum energy exponent -588. -/
theorem vacuum_horizon_forcing_one_statement :
    particleHorizonRungCount = 294 ∧
    -2 * particleHorizonRungCount = -588 ∧
    2 * (particleHorizonRungCount - 289) = 10 :=
  ⟨rfl, vacuumExponent_particleHorizon, hubble_vs_particle_rung_gap⟩

What this page does not claim

The certificate does not prove that the particle horizon is the correct horizon for the observed universe. The rung count 294 is a definitional choice, not a derived measurement. The certificate does not claim the vacuum energy formula matches observation; that is an empirical check.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cosmology/VacuumHorizonForcing.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: