`IndisputableMonolith`

IndisputableMonolith.lean · 36 lines · 0 declarations

Explainer status: ready · generated 2026-05-13 09:28:42.942087+00:00

   1import IndisputableMonolith.Foundation.PrimitiveDistinction
   2import IndisputableMonolith.Foundation.MagnitudeOfMismatch
   3import IndisputableMonolith.Foundation.ObserverFromRecognition
   4import IndisputableMonolith.Foundation.RecognizerInducesLogic
   5import IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
   6import IndisputableMonolith.Foundation.BranchSelection
   7import IndisputableMonolith.Foundation.AlphaCoordinateFixation
   8import IndisputableMonolith.Foundation.NonTrivialityFromDistinguishability
   9import IndisputableMonolith.Foundation.PreTemporalForcingOrder
  10import IndisputableMonolith.Foundation.RecognitionLattice3
  11import IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer
  12import IndisputableMonolith.Foundation.RealityTerminalCategory
  13import IndisputableMonolith.Foundation.RealityFromDistinction
  14import IndisputableMonolith.Foundation.IntegrationGap
  15import IndisputableMonolith.Cosmology.EtaBExactRungDerivation
  16import IndisputableMonolith.Cosmology.EtaBPrefactorDerivation
  17
  18-- Standard Model: Higgs EFT low-energy limit (Anil reviewer chain)
  19import IndisputableMonolith.StandardModel.HiggsEFTBridge
  20import IndisputableMonolith.StandardModel.ElectroweakMassBridge
  21import IndisputableMonolith.StandardModel.HiggsYukawaBridge
  22import IndisputableMonolith.StandardModel.HiggsObservableSkeleton
  23import IndisputableMonolith.StandardModel.LongitudinalVectorScattering
  24import IndisputableMonolith.StandardModel.HiggsEFTLowEnergyLimit
  25
  26/-!
  27# Shape of Logic — root module
  28
  29Umbrella module exposing the master forcing-chain theorem plus the
  30supporting T-1 / absolute-floor and foundation-repair theorem surfaces,
  31plus the `IntegrationGap` infrastructure, the two η_B worked-example
  32modules cited in the companion paper, and the six-module Standard-Model
  33Higgs effective-field-theory low-energy-limit chain
  34(`StandardModel/Higgs*`, `StandardModel/Electroweak*`, `StandardModel/Longitudinal*`).
  35-/
  36

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