`IndisputableMonolith.Experimental.AtomkiX17Structure`

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

Explainer status: ready · generated 2026-06-09 12:58:42.804170+00:00

   1import Mathlib
   2import IndisputableMonolith.Experimental.XenonExcessStructure
   3
   4namespace IndisputableMonolith
   5namespace Experimental
   6namespace AtomkiX17Structure
   7
   8open XenonExcessStructure
   9
  10def atomki_x17_from_ledger : Prop := xenon_excess_from_ledger
  11
  12theorem atomki_x17_structure : atomki_x17_from_ledger := xenon_excess_structure
  13
  14/-- Atomki-X17 structure implies xenon-excess structural input. -/
  15theorem atomki_x17_implies_xenon (h : atomki_x17_from_ledger) :
  16    xenon_excess_from_ledger :=
  17  h
  18
  19end AtomkiX17Structure
  20end Experimental
  21end IndisputableMonolith
  22

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