Gravity Echo Horizon Obstruction Exterior Return Claim Impossible

The one-way boundary

An event horizon is a boundary in spacetime that lets things in but not out. Once a signal crosses from the exterior into the interior of a black hole, it cannot return to the exterior region it came from. This is the classical one-way property of horizons, and it is the foundation of the theorem in question.

The theorem exterior_return_claim_impossible formalizes this obstruction in an abstract causal model. The model is not full Lorentzian geometry; it is a combinatorial structure where a deterministic step function moves a point from one state to the next. The interior is defined as a set closed under this step function: applying the step to an interior point always yields another interior point. The theorem proves that any claim requiring a signal to cross into the interior, bounce at a microscopic radius, and then return to the exterior is false, because the interior being closed under the step function makes it impossible to reach the exterior by iterated application of that function.

In plain terms, the proof is a simple containment argument. If a set is closed under a function, then starting inside that set and applying the function any number of times keeps you inside. The exterior is the complement of the interior. So a path from an interior point to an exterior point cannot exist. The declaration exterior_return_claim_impossible (a machine-checked theorem in the framework's library) states this directly: given any such exterior-return claim, it derives a contradiction, because the return point would have to be both interior and exterior at once.

This theorem does not prove that black holes exist, nor does it model the full physics of gravitational collapse or quantum gravity. It works within an abstract causal model where the one-way boundary axiom is assumed. The result is a formal rejection of a specific bounce-echo mechanism that had been proposed in a companion module. The theorem shows that mechanism is causally impossible under the stated axioms, not that it is physically impossible in every conceivable theory of gravity.

What the theorem changes is the status of bounce-echo proposals. Before this result, one could entertain the idea that a signal might cross a horizon, reflect at a small interior radius, and emerge again. The theorem closes that door within the framework's causal model. Any future proposal for horizon-crossing echoes must either abandon the one-way boundary axiom or find a different mechanism that does not require a return to the same exterior region.

/-- Corollary: an exterior-return claim with interior bounce is causally
    impossible (leads to contradiction). -/
theorem exterior_return_claim_impossible
    (M : CausalModel) (claim : ExteriorReturnClaim M) : False := by
  have h := bounce_echo_mechanism_violates_horizon_causality M claim
  exact M.exterior_interior_disjoint claim.returnPoint h.2 h.1

/-- An abstract causal model with a one-way event horizon.

The key axiom is `interior_closed_under_step`: the interior predicate is
closed under the future-directed step. This encodes the event horizon
as a one-way boundary—once inside, always inside. No interior point
can causally reach an exterior point.

This is an abstract model, not a formalization of Lorentzian geometry.
The causal obstruction is purely combinatorial. -/
structure CausalModel where
  /-- Abstract spacetime point type -/
  Point : Type
  /-- Future-directed causal step (deterministic propagation) -/
  step : Point → Point
  /-- Interior of the event horizon -/
  isInterior : Point → Prop
  /-- Exterior of the event horizon -/
  isExterior : Point → Prop
  /-- Strictly interior: microscopic, deep inside the horizon -/
  strictlyInterior : Point → Prop
  /-- Same exterior region (same asymptotic universe) -/
  sameExteriorRegion : Point → Point → Prop
  /-- Strictly interior implies interior -/
  strictlyInterior_implies_interior :
    ∀ p, strictlyInterior p → isInterior p
  /-- **One-way boundary axiom**: interior is closed under the
      future-directed step. Once inside the horizon, always inside. -/
  interior_closed_under_step :
    ∀ p, isInterior p → isInterior (step p)
  /-- Exterior and interior are disjoint (no point is both) -/
  exterior_interior_disjoint :
    ∀ p, isExterior p → ¬ isInterior p

/-- **Main theorem.** Any exterior-return claim with an interior bounce
    (strictly inside the horizon) violates horizon causality: the return
    point must be interior (by the one-way boundary axiom) but is also
    claimed to be exterior (by the return fact), which is impossible.

    The proof uses the one-way boundary axiom: since the bounce point is
    strictly interior (hence interior), and the interior is closed under
    the future-directed step, the return point—reachable from the bounce
    via `StepStar`—must also be interior. But the claim asserts the return
    point is exterior, contradicting the disjointness of interior and
    exterior. -/
theorem bounce_echo_mechanism_violates_horizon_causality
    (M : CausalModel) (claim : ExteriorReturnClaim M) :
    ViolatesHorizonCausality claim := by
  unfold ViolatesHorizonCausality
  refine ⟨?_, claim.returnPoint_exterior⟩
  -- The bounce point is strictly interior, hence interior
  have hbounce_interior : M.isInterior claim.bounce :=
    M.strictlyInterior_implies_interior claim.bounce
      claim.bounce_strictly_inside_horizon
  -- By the one-way boundary, the return point is interior
  -- (StepStar preserves the interior predicate since it is closed under step)
  exact claim.bounce_to_return M.isInterior
    (fun p hp => M.interior_closed_under_step p hp) hbounce_interior

What this page does not claim

This theorem does not prove that black holes exist in nature. This theorem does not model the full physics of gravitational collapse or quantum gravity. This theorem does not rule out all possible echo mechanisms, only those requiring a return to the same exterior region.

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/Gravity/EchoHorizonObstruction.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: