lemma
proved
term proof
w_t_rescale
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)
99lemma w_t_rescale (P : Params) (c Tdyn τ0 : ℝ) (hc : 0 < c) :
100 w_t P (c * Tdyn) (c * τ0) = w_t P Tdyn τ0 :=
proof body
Term-mode proof.
101 w_t_rescale_with defaultConfig P c Tdyn τ0 hc
102
103/-- Nonnegativity of time-kernel under ParamProps. -/
depends on (18)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
kernel
in IndisputableMonolith.Cosmology.BITKernelFamilies
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
defaultConfig
in IndisputableMonolith.Gravity.ILG
decl_use
-
ParamProps
in IndisputableMonolith.Gravity.ILG
decl_use
-
Params
in IndisputableMonolith.Gravity.ILG
decl_use
-
w_t
in IndisputableMonolith.Gravity.ILG
decl_use
-
w_t_rescale_with
in IndisputableMonolith.Gravity.ILG
decl_use
-
Tdyn
in IndisputableMonolith.Gravity.ParameterizationBridge
decl_use
-
kernel
in IndisputableMonolith.ILG.Kernel
decl_use
-
ParamProps
in IndisputableMonolith.ILG.Params
decl_use
-
Params
in IndisputableMonolith.ILG.Params
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
ParamProps
in IndisputableMonolith.Relativity.ILG.Params
decl_use
-
Params
in IndisputableMonolith.Relativity.ILG.Params
decl_use
-
Params
in IndisputableMonolith.Spiral.SpiralField
decl_use