Gravity Bhecho Amplitudes Catalog Amplitude Pos

The echo amplitude certificate

Black-hole echoes are hypothetical repeating bursts of gravitational waves, expected if a black hole's event horizon is replaced by a reflective surface. The framework's recognition ledger, a discrete record of events, predicts that each successive echo is quieter than the last by a fixed factor. The declaration catalogAmplitude_pos is a theorem in the machine-checked library of formal theorems. It states that for any cataloged event and any echo number, the echo amplitude is strictly greater than zero.

The amplitude at reflection number n is defined as phi^(-n), where phi is the golden ratio, approximately 1.618. This gives a first echo amplitude of about 0.618 relative to the primary signal, a second of about 0.382, and so on. The positivity theorem is the foundation for the stronger claim that the signal-to-noise ratio between successive echoes is exactly 1/phi. It also guarantees the amplitudes form a strictly decreasing sequence, so the echoes never grow or oscillate in the model.

In Recognition Science, this is not a free parameter choice. The golden ratio arises from the forced cost function, and the echo attenuation is presented as a derived consequence. The certificate bhEchoAmplitudeCert bundles six such properties: positivity, primary unity, the one-step ratio, the SNR ratio, strict decrease, and catalog positivity. The kernel checks the proof with zero axioms beyond its standard three.

What the theorem does not claim is that black-hole echoes exist. It is a conditional statement: if an echo is observed, the framework predicts its amplitude ratio. The existence of echoes, their detection in LIGO/Virgo data, and the physical mechanism of the reflective surface are all outside this formal result. The falsifier named in the module is a high-SNR merger event showing no echo or a systematically different amplitude ratio.

theorem catalogAmplitude_pos (e : HeadlineEvent) (n : ℕ) :
    0 < catalogAmplitude e n := echoAmplitude_pos n

theorem catalogAmplitude_pos (e : HeadlineEvent) (n : ℕ) :
    0 < catalogAmplitude e n := echoAmplitude_pos n

/-- Echo amplitude at reflection number `n` (relative to primary). -/
def echoAmplitude (n : ℕ) : ℝ := phi ^ (-(n : ℤ))

/-- Amplitudes are strictly decreasing. -/
theorem echoAmplitude_strictly_decreasing (n : ℕ) :
    echoAmplitude (n + 1) < echoAmplitude n := by
  rw [echoAmplitude_succ_ratio]
  have hn : 0 < echoAmplitude n := echoAmplitude_pos n
  have : phi⁻¹ < 1 :=
    inv_lt_one_of_one_lt₀ (by have := Constants.phi_gt_onePointFive; linarith)
  linarith [mul_lt_iff_lt_one_right hn |>.mpr this]

What this page does not claim

Black-hole echoes have been observed in gravitational-wave data. The theorem proves that any specific LIGO/Virgo event contains an echo. The reflective surface mechanism is physically established.

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