Gravity Echo Horizon Obstruction Succ

The one-way step

An event horizon is a one-way boundary in spacetime. Once a signal crosses it from the exterior to the interior, it cannot return to the same exterior region. The Recognition Science framework encodes this as a purely combinatorial fact about a step function, a deterministic rule that moves from one point to the next. The declaration succ is the single step of that rule: if a point q is reachable from p in zero or more applications of the step, then applying the step once more keeps you in the reachable set. Formally, it states that StepStar step p q implies StepStar step p (step q).

This is the building block of the framework's causal model. The model treats the interior of a horizon as a set closed under the step function: applying the step to any interior point keeps you inside. The succ lemma is what makes that closure transitive. Together with the reflexive base case, it proves that anything reachable from an interior point remains interior. The framework's library then uses this to reject a specific physical mechanism, the bounce-echo, in which a signal crosses the horizon, reflects at a microscopic interior radius, and returns to the same exterior region. The theorem bounce_echo_mechanism_violates_horizon_causality derives a contradiction from such a claim, and exterior_return_claim_impossible concludes False.

The proof is abstract and does not depend on the details of general relativity. It works for any deterministic step function and any partition of points into interior and exterior sets that are disjoint and closed under the step. The framework's library, a machine-checked collection of formal theorems, verifies the argument. The result is not a statement about the geometry of spacetime, but about the logical structure of a one-way boundary. If a set is closed under a function, no iterated application of that function can reach its complement.

What succ establishes, in plain terms, is that the reachable set of a deterministic process is closed under one more step. This is the foundation for the horizon obstruction. It does not claim that the step function models any particular physical process, nor that the interior of a real black hole behaves exactly this way. It proves a conditional statement: if a causal model satisfies the one-way boundary axiom, then an exterior return claim is impossible. The framework's library records this rejection in blackHoleEchoMechanismStatus, but the formal result itself is a theorem about abstract sets, not a measurement of astrophysical phenomena.

/-- Successor case: if `q` is reachable from `p`, then `step q` is also
    reachable from `p`. -/
lemma succ {Point : Type} {step : Point → Point} {p q : Point}
    (hs : StepStar step p q) : StepStar step p (step q) := by
  intros P hstep hp
  exact hstep q (hs P hstep hp)

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

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

/-- If a predicate is closed under `step`, it is preserved by `StepStar`:
    any point reachable from a point satisfying `P` also satisfies `P`.
    This is the combinatorial heart of the one-way boundary: a set closed
    under a function cannot reach its complement via iteration. -/
lemma preserves_predicate {Point : Type} {step : Point → Point}
    {P : Point → Prop} (h : ∀ p, P p → P (step p)) :
    ∀ {p q : Point}, StepStar step p q → P p → P q := by
  intros p q hs
  exact hs P h

What this page does not claim

The step function models any specific physical process. The interior of a real black hole behaves exactly as the abstract set in the model. The result is a measurement of astrophysical phenomena.

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: