`IndisputableMonolith.Astrophysics.StellarIMFStructure`

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

Explainer status: pending

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

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