def definition def or abbrev

`G_of`

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

formal statement (Lean)

  47noncomputable def G_of (F : ℝ → ℝ) (t : ℝ) : ℝ := F (Real.exp t)

Definition body.

  48
  49/-- The shifted log-lift (for d'Alembert). -/

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

analytic_bridge in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
analytic_bridge_full in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
differentiation_key_lemma in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
entangling_combiner_forces_hyperbolic in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
even_function_deriv_zero in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
F_forced_to_Jcost in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
full_inevitability in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
G_zero in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
H_of in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
log_consistency in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
P_forced_to_RCL in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
Q_boundary_u in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
Q_boundary_v in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use
separable_combiner_forces_flat in IndisputableMonolith.Foundation.DAlembert.AnalyticBridge decl_use

Lean names referenced from this declaration's body.

for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use