`IndisputableMonolith.Experimental.ANITAUpgoingStructure`

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

Explainer status: ready · generated 2026-05-16 07:19:22.188621+00:00

   1import Mathlib
   2import IndisputableMonolith.Experimental.GalliumAnomalyStructure
   3
   4namespace IndisputableMonolith
   5namespace Experimental
   6namespace ANITAUpgoingStructure
   7
   8open GalliumAnomalyStructure
   9
  10def anita_upgoing_from_ledger : Prop := gallium_anomaly_from_ledger
  11
  12theorem anita_upgoing_structure : anita_upgoing_from_ledger := gallium_anomaly_structure
  13
  14/-- ANITA-upgoing structure implies gallium-anomaly structural input. -/
  15theorem anita_implies_gallium (h : anita_upgoing_from_ledger) :
  16    gallium_anomaly_from_ledger :=
  17  h
  18
  19end ANITAUpgoingStructure
  20end Experimental
  21end IndisputableMonolith
  22

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