`IndisputableMonolith.Astrophysics.FRBStructure`

IndisputableMonolith/Astrophysics/FRBStructure.lean · 21 lines · 3 declarations

Explainer status: pending

   1import Mathlib
   2import IndisputableMonolith.Astrophysics.UHECRStructure
   3
   4namespace IndisputableMonolith
   5namespace Astrophysics
   6namespace FRBStructure
   7
   8open UHECRStructure
   9
  10def frb_from_ledger : Prop := uhecr_from_ledger
  11
  12theorem frb_structure : frb_from_ledger := uhecr_structure
  13
  14/-- FRB structure implies UHECR-side structural input. -/
  15theorem frb_implies_uhecr (h : frb_from_ledger) : uhecr_from_ledger :=
  16  h
  17
  18end FRBStructure
  19end Astrophysics
  20end IndisputableMonolith
  21

source mirrored from github.com/jonwashburn/shape-of-logic