`IndisputableMonolith.TruthCore.ILGDisplay`

IndisputableMonolith/TruthCore/ILGDisplay.lean · 18 lines · 1 declarations

Explainer status: ready · generated 2026-05-13 06:49:53.284455+00:00

   1import Mathlib
   2import IndisputableMonolith.Gravity.ILG
   3
   4namespace IndisputableMonolith
   5namespace TruthCore
   6
   7noncomputable section
   8
   9@[simp] noncomputable def ILG_w_t_display
  10  (P : IndisputableMonolith.Gravity.ILG.Params)
  11  (B : IndisputableMonolith.Gravity.ILG.BridgeData) (Tdyn : ℝ) : ℝ :=
  12  IndisputableMonolith.Gravity.ILG.w_t_display P B Tdyn
  13
  14end
  15
  16end TruthCore
  17end IndisputableMonolith
  18

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