IndisputableMonolith.Gravity.EchoHorizonObstruction

   1import Mathlib
   2import IndisputableMonolith.Gravity.BlackHoleEchoesFromBounce
   3
   4namespace IndisputableMonolith
   5namespace Gravity
   6namespace EchoHorizonObstruction
   7
   8open BlackHoleEchoesFromBounce
   9
  10/-!
  11# Echo Horizon Obstruction: Causal Impossibility of Exterior Return from Interior Bounce
  12
  13## Abstract
  14
  15This module formalizes the causal obstruction that rejects the bounce-echo mechanism
  16described in `BlackHoleEchoesFromBounce`. An event horizon is a one-way boundary:
  17once a signal crosses to the interior, it cannot return to the exterior. The rejected
  18echo mechanism required all three of:
  19
  201. A signal crosses from the exterior to the interior of an event horizon.
  212. The signal reflects at a microscopic interior bounce radius strictly inside the horizon.
  223. The signal returns to the **same** exterior region.
  23
  24We encode this as an abstract causal model and prove that any such `ExteriorReturnClaim`
  25violates horizon causality: the one-way boundary axiom (interior is closed under the
  26future-directed step) makes the bounce-to-return path causally forbidden.
  27
  28This is an abstract causal model, not a formalization of full Lorentzian geometry.
  29The obstruction is purely combinatorial: a set closed under a function cannot reach
  30its complement via iterated application of that function.
  31
  32## Connection to `BlackHoleEchoesFromBounce`
  33
  34The module `BlackHoleEchoesFromBounce` records `bounce_escape_mechanism_rejected := true`
  35in `blackHoleEchoMechanismStatus`. This module provides the formal causal obstruction
  36that justifies that rejection: any exterior-return claim with an interior bounce
  37is causally impossible under the one-way boundary axiom.
  38-/
  39
  40/-- Reflexive-transitive closure of a deterministic step function.
  41    `StepStar step p q` means `q` is reachable from `p` in zero or more
  42    applications of `step`, defined by its universal property: any predicate
  43    closed under `step` that holds at `p` also holds at `q`. -/
  44def StepStar {Point : Type} (step : Point → Point) (p q : Point) : Prop :=
  45  ∀ P : Point → Prop, (∀ x, P x → P (step x)) → P p → P q
  46
  47namespace StepStar
  48
  49/-- Base case: every point reaches itself. -/
  50lemma base {Point : Type} {step : Point → Point} (p : Point) : StepStar step p p := by
  51  intros P h hp
  52  exact hp
  53
  54/-- Successor case: if `q` is reachable from `p`, then `step q` is also
  55    reachable from `p`. -/
  56lemma succ {Point : Type} {step : Point → Point} {p q : Point}
  57    (hs : StepStar step p q) : StepStar step p (step q) := by
  58  intros P hstep hp
  59  exact hstep q (hs P hstep hp)
  60
  61/-- If a predicate is closed under `step`, it is preserved by `StepStar`:
  62    any point reachable from a point satisfying `P` also satisfies `P`.
  63    This is the combinatorial heart of the one-way boundary: a set closed
  64    under a function cannot reach its complement via iteration. -/
  65lemma preserves_predicate {Point : Type} {step : Point → Point}
  66    {P : Point → Prop} (h : ∀ p, P p → P (step p)) :
  67    ∀ {p q : Point}, StepStar step p q → P p → P q := by
  68  intros p q hs
  69  exact hs P h
  70
  71/-- Transitivity: reachability chains compose. -/
  72lemma trans {Point : Type} {step : Point → Point} {p q r : Point}
  73    (hpq : StepStar step p q) (hqr : StepStar step q r) :
  74    StepStar step p r := by
  75  intros P h hp
  76  exact hqr P h (hpq P h hp)
  77
  78end StepStar
  79
  80/-- An abstract causal model with a one-way event horizon.
  81
  82The key axiom is `interior_closed_under_step`: the interior predicate is
  83closed under the future-directed step. This encodes the event horizon
  84as a one-way boundary—once inside, always inside. No interior point
  85can causally reach an exterior point.
  86
  87This is an abstract model, not a formalization of Lorentzian geometry.
  88The causal obstruction is purely combinatorial. -/
  89structure CausalModel where
  90  /-- Abstract spacetime point type -/
  91  Point : Type
  92  /-- Future-directed causal step (deterministic propagation) -/
  93  step : Point → Point
  94  /-- Interior of the event horizon -/
  95  isInterior : Point → Prop
  96  /-- Exterior of the event horizon -/
  97  isExterior : Point → Prop
  98  /-- Strictly interior: microscopic, deep inside the horizon -/
  99  strictlyInterior : Point → Prop
 100  /-- Same exterior region (same asymptotic universe) -/
 101  sameExteriorRegion : Point → Point → Prop
 102  /-- Strictly interior implies interior -/
 103  strictlyInterior_implies_interior :
 104    ∀ p, strictlyInterior p → isInterior p
 105  /-- **One-way boundary axiom**: interior is closed under the
 106      future-directed step. Once inside the horizon, always inside. -/
 107  interior_closed_under_step :
 108    ∀ p, isInterior p → isInterior (step p)
 109  /-- Exterior and interior are disjoint (no point is both) -/
 110  exterior_interior_disjoint :
 111    ∀ p, isExterior p → ¬ isInterior p
 112
 113/-- A claim that a signal crosses to the interior, bounces at a microscopic
 114radius strictly inside the horizon, and returns to the same exterior region.
 115
 116This captures the three facts the rejected echo mechanism would need
 117simultaneously:
 118
 1191. **Crossing**: The signal starts in the exterior and crosses to the interior.
 1202. **Interior bounce**: The signal reflects at a microscopic radius strictly
 121   inside the horizon (not at the horizon itself).
 1223. **Exterior return**: The signal returns to the same exterior region.
 123
 124Each pair of consecutive points is connected by a causal chain (`StepStar`),
 125representing future-directed propagation. -/
 126structure ExteriorReturnClaim (M : CausalModel) where
 127  /-- Starting point (exterior) -/
 128  start : M.Point
 129  /-- Crossing point (where signal enters interior) -/
 130  crossing : M.Point
 131  /-- Bounce point (microscopic, strictly inside horizon) -/
 132  bounce : M.Point
 133  /-- Return point (back in exterior) -/
 134  returnPoint : M.Point
 135  /-- Fact 1a: signal starts in the exterior -/
 136  start_exterior : M.isExterior start
 137  /-- Fact 1b: signal crosses to the interior -/
 138  crossing_interior : M.isInterior crossing
 139  /-- Fact 2: bounce at microscopic radius strictly inside the horizon -/
 140  bounce_strictly_inside_horizon : M.strictlyInterior bounce
 141  /-- Fact 3a: signal returns to the exterior -/
 142  returnPoint_exterior : M.isExterior returnPoint
 143  /-- Fact 3b: returns to the **same** exterior region -/
 144  returnPoint_same_exterior_region : M.sameExteriorRegion start returnPoint
 145  /-- Causal chain: start → crossing -/
 146  start_to_crossing : StepStar M.step start crossing
 147  /-- Causal chain: crossing → bounce -/
 148  crossing_to_bounce : StepStar M.step crossing bounce
 149  /-- Causal chain: bounce → return -/
 150  bounce_to_return : StepStar M.step bounce returnPoint
 151
 152/-- Predicate: a claim violates horizon causality (its return point is
 153    both interior and exterior, which is causally impossible under the
 154    one-way boundary axiom). -/
 155def ViolatesHorizonCausality {M : CausalModel} (claim : ExteriorReturnClaim M) : Prop :=
 156  M.isInterior claim.returnPoint ∧ M.isExterior claim.returnPoint
 157
 158/-- **Main theorem.** Any exterior-return claim with an interior bounce
 159    (strictly inside the horizon) violates horizon causality: the return
 160    point must be interior (by the one-way boundary axiom) but is also
 161    claimed to be exterior (by the return fact), which is impossible.
 162
 163    The proof uses the one-way boundary axiom: since the bounce point is
 164    strictly interior (hence interior), and the interior is closed under
 165    the future-directed step, the return point—reachable from the bounce
 166    via `StepStar`—must also be interior. But the claim asserts the return
 167    point is exterior, contradicting the disjointness of interior and
 168    exterior. -/
 169theorem bounce_echo_mechanism_violates_horizon_causality
 170    (M : CausalModel) (claim : ExteriorReturnClaim M) :
 171    ViolatesHorizonCausality claim := by
 172  unfold ViolatesHorizonCausality
 173  refine ⟨?_, claim.returnPoint_exterior⟩
 174  -- The bounce point is strictly interior, hence interior
 175  have hbounce_interior : M.isInterior claim.bounce :=
 176    M.strictlyInterior_implies_interior claim.bounce
 177      claim.bounce_strictly_inside_horizon
 178  -- By the one-way boundary, the return point is interior
 179  -- (StepStar preserves the interior predicate since it is closed under step)
 180  exact claim.bounce_to_return M.isInterior
 181    (fun p hp => M.interior_closed_under_step p hp) hbounce_interior
 182
 183/-- Corollary: an exterior-return claim with interior bounce is causally
 184    impossible (leads to contradiction). -/
 185theorem exterior_return_claim_impossible
 186    (M : CausalModel) (claim : ExteriorReturnClaim M) : False := by
 187  have h := bounce_echo_mechanism_violates_horizon_causality M claim
 188  exact M.exterior_interior_disjoint claim.returnPoint h.2 h.1
 189
 190/-- The obstruction is consistent with the status recorded in
 191    `BlackHoleEchoesFromBounce`: the bounce escape mechanism is rejected. -/
 192theorem blackHoleEchoMechanismStatus_records_rejection :
 193    blackHoleEchoMechanismStatus.bounce_escape_mechanism_rejected = true := by
 194  rfl
 195
 196end EchoHorizonObstruction
 197end Gravity
 198end IndisputableMonolith