`IndisputableMonolith.Experimental.XenonExcessStructure`

IndisputableMonolith/Experimental/XenonExcessStructure.lean · 22 lines · 3 declarations

Explainer status: ready · generated 2026-05-13 05:56:14.367226+00:00

   1import Mathlib
   2import IndisputableMonolith.Experimental.DAMAModulationStructure
   3
   4namespace IndisputableMonolith
   5namespace Experimental
   6namespace XenonExcessStructure
   7
   8open DAMAModulationStructure
   9
  10def xenon_excess_from_ledger : Prop := dama_modulation_from_ledger
  11
  12theorem xenon_excess_structure : xenon_excess_from_ledger := dama_modulation_structure
  13
  14/-- Xenon-excess structure implies DAMA-modulation structural input. -/
  15theorem xenon_excess_implies_dama (h : xenon_excess_from_ledger) :
  16    dama_modulation_from_ledger :=
  17  h
  18
  19end XenonExcessStructure
  20end Experimental
  21end IndisputableMonolith
  22

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