`IndisputableMonolith.Experimental.GalliumAnomalyStructure`

IndisputableMonolith/Experimental/GalliumAnomalyStructure.lean · 21 lines · 3 declarations

Explainer status: ready · generated 2026-06-06 22:14:52.878651+00:00

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Experimental
   6namespace GalliumAnomalyStructure
   7
   8open Constants
   9
  10def gallium_anomaly_from_ledger : Prop := 0 < phi
  11
  12theorem gallium_anomaly_structure : gallium_anomaly_from_ledger := phi_pos
  13
  14/-- Gallium-anomaly structure implies positivity of `phi`. -/
  15theorem gallium_implies_phi_pos (h : gallium_anomaly_from_ledger) : 0 < phi :=
  16  h
  17
  18end GalliumAnomalyStructure
  19end Experimental
  20end IndisputableMonolith
  21

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