Encyclopedia Gravity Gravity Black Hole Echoes Si Bounce Radius Si Two Step

ARTICLE 3 claims 3 theorems

Gravity Black Hole Echoes Si Bounce Radius Si Two Step

A machine-checked library of formal theorems derives a simple scaling rule for a model of black hole bounce radii, and carefully stops short of claiming real echoes exist.

The two-step radius rule

In the Recognition Science framework, a ledger (a discrete record of events) can model a black hole bounce: a hypothetical reflection of infalling matter or light at some radius inside the hole. The framework's machine-checked library of formal theorems defines a sequence of possible bounce radii, one for each integer step N. The definition is simple: bounceRadius_SI N equals the Planck length (about 1.6 × 10⁻³⁵ meters, the scale where quantum gravity effects become strong) multiplied by the golden ratio φ (about 1.618) raised to the power N.

The key theorem, named bounceRadius_SI_two_step, proves a two-step scaling rule: the radius at step N+2 is exactly the radius at step N multiplied by φ². In plain terms, skipping two rungs on the ladder multiplies the radius by about 2.618. The same rule holds for the echo delay: the time between echoes at step N+2 is φ² times the delay at step N. The library also proves the radius is always positive and strictly increases as N grows. These are structural facts about the defined sequence, not measurements of real black holes.

The framework is explicit about what this theorem does not do. It does not claim that real black holes produce observable echoes. The physical mechanism that would connect this rung algebra to an actual horizon-consistent echo is marked as open or rejected in the library's own status notes. The SI conversion here is a structural lift: it takes a dimensionless model and expresses it in meters and seconds using the 2019 SI exact values for c and ℏ, plus one CODATA measurement of G. No free parameters are fitted, but the formulas are not a LIGO/Virgo falsifier until the missing exterior echo mechanism exists.

What the theorem changes is the status of the model's internal consistency. A reader can now see that the framework's bounce ladder is not an arbitrary list of numbers: it obeys a rigid two-step geometric law, and that law survives the conversion to physical units. Whether that law describes nature is a separate, open question.

THEOREM bounceRadius_SI_two_step · IndisputableMonolith/Gravity/BlackHoleEchoesSI.lean
theorem bounceRadius_SI_two_step (N : ℕ) :
    bounceRadius_SI (N + 2) = bounceRadius_SI N * phi ^ 2 := by
  unfold bounceRadius_SI
  rw [pow_add]
  ring
THEOREM bounceRadius_SI_pos · bounceRadius_SI_strict_mono · IndisputableMonolith/Gravity/BlackHoleEchoesSI.lean
theorem bounceRadius_SI_pos (N : ℕ) : 0 < bounceRadius_SI N := by
  unfold bounceRadius_SI
  exact mul_pos planckLength_SI_pos (pow_pos phi_pos N)
bounceRadius_SI_strict_mono · IndisputableMonolith/Gravity/BlackHoleEchoesSI.lean:142
theorem bounceRadius_SI_strict_mono (N : ℕ) :
    bounceRadius_SI N < bounceRadius_SI (N + 1) := by
  unfold bounceRadius_SI
  rw [pow_succ]
  have hN : 0 < phi ^ N := pow_pos phi_pos N
  have hℓ : 0 < planckLength_SI := planckLength_SI_pos
  have hphi : 1 < phi := one_lt_phi
  nlinarith [mul_pos hℓ hN]
THEOREM echoDelay_SI_two_step · IndisputableMonolith/Gravity/BlackHoleEchoesSI.lean
theorem echoDelay_SI_two_step (N : ℕ) :
    echoDelay_SI (N + 2) = echoDelay_SI N * phi ^ 2 := by
  rw [echoDelay_SI_eq_planckTime_form, echoDelay_SI_eq_planckTime_form,
      pow_add]
  ring

What this page does not claim

Real black holes produce observable echoes. The two-step radius rule is a measurement or a confirmed prediction. The SI conversion closes the physical echo mechanism.

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/BlackHoleEchoesSI.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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND