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)
117theorem f_growth_gr_limit (P : KernelParams) (hC : P.C = 0) (k a : ℝ) (ha : 0 < a) :
118 f_growth_eds_ilg P k a = 1 := by
proof body
Term-mode proof.
119 simp [f_growth_eds_ilg, growth_prefactor, hC]
120
121/-- Proof of the X-reciprocity identity for the growth factor D(a, k) (Target C). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (13)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
reciprocity
in IndisputableMonolith.Foundation.LedgerForcing
decl_use
-
identity
in IndisputableMonolith.Foundation.ObserverForcing
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
f_growth_gr_limit
in IndisputableMonolith.Gravity.ILGGrowthFactor
decl_use
-
f_growth_eds_ilg
in IndisputableMonolith.ILG.GrowthODE
decl_use
-
growth_prefactor
in IndisputableMonolith.ILG.GrowthODE
decl_use
-
KernelParams
in IndisputableMonolith.ILG.Kernel
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
identity
in IndisputableMonolith.RRF.Foundation.VantageCategory
decl_use