def definition def or abbrev

`w_t_display`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  73@[simp] def w_t_display (P : Params) (B : BridgeData) (Tdyn : ℝ) : ℝ :=

proof body

Definition body.

  74  w_t_with defaultConfig P Tdyn B.tau0
  75

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

ILG_w_t_display in IndisputableMonolith.TruthCore.ILGDisplay decl_use

depends on (12)

Lean names referenced from this declaration's body.

BridgeData in IndisputableMonolith.Bridge.DataCore decl_use
tau0 in IndisputableMonolith.Compat.Constants decl_use
tau0 in IndisputableMonolith.Constants decl_use
tau0 in IndisputableMonolith.Constants.Derivation decl_use
BridgeData in IndisputableMonolith.Gravity.ILG decl_use
defaultConfig in IndisputableMonolith.Gravity.ILG decl_use
Params in IndisputableMonolith.Gravity.ILG decl_use
w_t_with in IndisputableMonolith.Gravity.ILG decl_use
Tdyn in IndisputableMonolith.Gravity.ParameterizationBridge decl_use
Params in IndisputableMonolith.ILG.Params decl_use
Params in IndisputableMonolith.Relativity.ILG.Params decl_use
Params in IndisputableMonolith.Spiral.SpiralField decl_use