Gravity Echo Horizon Obstruction Base

The causal wall

An event horizon is the boundary around a black hole beyond which nothing, not even light, can escape to the outside. Once a signal crosses this boundary, it cannot return to the region it came from. This one-way property is the core of what makes a black hole a black hole, and it is the subject of a formal proof in the Recognition Science framework's machine-checked library of formal theorems.

The framework models the situation in deliberately simple terms. Its causal model, a discrete record of which points can reach which other points through a step function, treats the interior of the horizon as a set closed under the future-directed step: if you are inside, the next step keeps you inside. The proof then shows that any claim of an exterior return, meaning a signal that goes in, bounces at an interior point, and comes back to the same outside region, contradicts this closure. The bounce-to-return path would require the signal to be both inside and outside at the same time, which the model forbids.

The result is a theorem named bounce_echo_mechanism_violates_horizon_causality, and it is proved in the Lean kernel with no special axioms. It establishes that the rejected echo mechanism, one that would let a signal escape after an interior bounce, is causally impossible under the one-way boundary axiom. The proof is purely combinatorial: a set closed under a function cannot reach its complement by iterating that function. This is not a claim about the full geometry of spacetime; it is an abstract causal skeleton.

What the declaration base does not claim is just as important. It does not model the actual curvature of spacetime, the metric, or the equations of general relativity. It does not say that no echo-like signal can ever be observed; it only rules out the specific mechanism of an exterior return after an interior bounce. The framework's library records this rejection in a status flag, bounce_escape_mechanism_rejected := true, as a formal bookkeeping entry, not as a new physical discovery. The physical content is the horizon's one-way nature, which the proof makes precise.

For a reader, the consequence is a clean logical wall: the bounce-echo idea fails not because of a numerical accident or a tuning problem, but because the very structure of a one-way boundary makes the return path a contradiction. The proof gives a reason, not just a result.

/-- 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

/-- **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

/-- The obstruction is consistent with the status recorded in
    `BlackHoleEchoesFromBounce`: the bounce escape mechanism is rejected. -/
theorem blackHoleEchoMechanismStatus_records_rejection :
    blackHoleEchoMechanismStatus.bounce_escape_mechanism_rejected = true := by
  rfl

What this page does not claim

This page does not claim the framework models the metric or curvature of spacetime. This page does not claim the proof rules out all possible echo or signal-return mechanisms. This page does not claim the rejection flag is a physical measurement.

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: