`IndisputableMonolith.Experimental.FlybyAnomalyStructure`

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

Explainer status: ready · generated 2026-06-09 03:05:29.149035+00:00

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

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