def definition def or abbrev

`G`

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

formal statement (Lean)

  23@[simp] noncomputable def G (F : ℝ → ℝ) (t : ℝ) : ℝ := F (Real.exp t)

proof body

Definition body.

  24
  25/-- Convenience reparametrization: `H_F t = G_F t + 1`. -/

used by (40)

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

cost_algebra_unique in IndisputableMonolith.Algebra.CostAlgebra decl_use
cost_algebra_unique_aczel in IndisputableMonolith.Algebra.CostAlgebra decl_use
J_defect_form in IndisputableMonolith.Algebra.CostAlgebra decl_use
H_RSZeroParameterStatus in IndisputableMonolith.Astrophysics.MassToLight decl_use
E_coh in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
ml_zero_parameter_certificate in IndisputableMonolith.Astrophysics.ObservabilityLimits decl_use
BridgeData in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_dimensionless_id in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_dimensionless_id_physical in IndisputableMonolith.Bridge.DataCore decl_use
lambda_rec_pos in IndisputableMonolith.Bridge.DataCore decl_use
Physical in IndisputableMonolith.Bridge.DataCore decl_use
duhamelRemainderOfGalerkin_integratingFactor in IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D decl_use
AllReachable in IndisputableMonolith.Complexity.SAT.Completeness decl_use
IsolationInvariant in IndisputableMonolith.Complexity.SAT.Completeness decl_use
Reachable in IndisputableMonolith.Complexity.SAT.Completeness decl_use
G in IndisputableMonolith.Constants decl_use
G_pos in IndisputableMonolith.Constants decl_use
kappa_einstein in IndisputableMonolith.Constants decl_use
kappa_einstein_eq in IndisputableMonolith.Constants decl_use
lambda_rec_pos in IndisputableMonolith.Constants decl_use
alpha_seed_structural in IndisputableMonolith.Constants.AlphaDerivation decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G_ne_zero in IndisputableMonolith.Constants.Codata decl_use
G_pos in IndisputableMonolith.Constants.Codata decl_use
inner_nonneg in IndisputableMonolith.Constants.Derivation decl_use
tau0_planck_relation in IndisputableMonolith.Constants.Derivation decl_use
dimensions_status in IndisputableMonolith.Constants.Dimensions decl_use
dim_G in IndisputableMonolith.Constants.Dimensions decl_use
NA_SI in IndisputableMonolith.Constants.ExternalAnchors decl_use

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.

G in IndisputableMonolith.Constants decl_use
G in IndisputableMonolith.Constants.Codata decl_use
G in IndisputableMonolith.Gravity.JCostInflaton decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
F in IndisputableMonolith.Pipelines decl_use