Physics Gamma Ray Bursts

Gamma-ray bursts in the ledger

Gamma-ray bursts are the most energetic electromagnetic events known, and Recognition Science treats them as a testbed for its ledger, the record of recognition events that the framework derives from its cost function. The module GammaRayBursts.lean does not derive bursts from first principles. It fixes a working model of their energy scale, their two observed classes, their Lorentz factor, and their Amati relation, then proves the consistency of that model.

The central scale is the isotropic energy release. The module defines a typical burst energy as 10 percent of the energy of one tenth of a solar mass, converted at 10 percent efficiency. The established theorem typical_grb_in_range places this value strictly between 10^51 and 10^54 erg, the accepted observational window for long gamma-ray bursts. A companion theorem, grb_energy_positive, shows that any positive fraction of a solar mass yields positive burst energy, so the model never produces a negative or zero release.

The two-class distinction is stated as a sharp boundary at a duration of 2 seconds. The theorem classes_disjoint proves that a duration which is both at least 2 and at most 2 must equal 2, and long_not_short proves that no duration can be strictly greater than 2 and strictly less than 2 at once. These are tautological consequences of the real number order, not physical discoveries, and the module presents them as such.

The Lorentz factor is defined as jet energy divided by baryon mass, with a proof that it is positive when both inputs are positive. The Amati relation, which links peak spectral energy to isotropic energy, is defined with a square-root exponent. The theorem amati_increases proves that the peak energy strictly increases with isotropic energy for positive inputs, and amati_exponent records that the exponent 1/2 arises from combining two 1/4 powers. These are the module's substantive claims: the model is internally consistent and monotone in the way the observed relation demands.

What the module establishes, in plain language, is a coherent set of definitions and inequalities that match the known numbers for gamma-ray bursts. It proves that a typical burst energy sits inside the observed range, that the two classes do not overlap, that Lorentz factors are positive, and that the Amati relation is increasing. It does not claim to explain why bursts occur, nor to derive their properties from the recognition cost function. The module is a bridge: it shows that the framework can host the standard phenomenology without contradiction.

MODEL typical_grb_energy · IndisputableMonolith/Physics/GammaRayBursts.lean

THEOREM typical_grb_in_range · IndisputableMonolith/Physics/GammaRayBursts.lean

THEOREM classes_disjoint · IndisputableMonolith/Physics/GammaRayBursts.lean

THEOREM amati_increases · IndisputableMonolith/Physics/GammaRayBursts.lean

What this page does not claim

No claim that gamma-ray bursts are derived from the recognition cost function. No claim that the 2-second class boundary is physically explained. No claim that the Amati relation exponent is derived rather than defined.

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/Physics/GammaRayBursts.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: