pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Gravity.BHEchoesLIGOCatalog

show as:
view Lean formalization →

This module defines the generic bounce-radius and echo-delay scaling functions for black hole echoes at recognition rung N in RS-native units. LIGO/Virgo echo modelers cite it to obtain the structural relations before specializing to individual events. It consists solely of definitions and basic properties with no theorems or proofs.

claimThe module introduces bounceRadius(N) for the bounce radius and echoDelay(N) for the echo delay at recognition rung N, both expressed in RS-native units with time quantum τ₀ = 1 tick.

background

Recognition Science treats gravity phenomena via the J-cost functional and the phi-ladder of recognition rungs. This module sits in the gravity domain and imports the fundamental RS time quantum τ₀ = 1 tick from Constants. It supplies the core objects bounceRadius and echoDelay that encode the generic scaling for black hole echo predictions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

This module supplies the generic BH-echo cert that feeds the per-event prediction tables in BHEchoPerEventCatalog. It provides the structural bounce-radius and echo-delay scaling required for the Recognition Science treatment of LIGO/Virgo black hole echoes.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (8)