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)
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:
- What physical mechanism could connect the rung algebra to a horizon-consistent exterior echo?
- How would the two-step scaling law appear in gravitational-wave data if real echoes existed?
- Does the golden-ratio ladder survive when the model is extended beyond the current rung algebra?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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] ringThe radius at step N+2 is exactly the radius at step N multiplied by φ². bounceRadius_SI_two_step · IndisputableMonolith/Gravity/BlackHoleEchoesSI.leanTHEOREM 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)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]The library also proves the radius is always positive and strictly increases as N grows. bounceRadius_SI_pos · bounceRadius_SI_strict_mono · IndisputableMonolith/Gravity/BlackHoleEchoesSI.leanTHEOREM 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] ringThe same rule holds for the echo delay: the time between echoes at step N+2 is φ² times the delay at step N. echoDelay_SI_two_step · IndisputableMonolith/Gravity/BlackHoleEchoesSI.lean