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)
68noncomputable def mapDeltaTime (δ : ℤ) (hδ : δ ≠ 0) (U : Constants.RSUnits) : DeltaSub δ → ℝ :=
proof body
Definition body.
69 mapDelta δ hδ (timeMap U)
70
71/-- Existence of affine δ→action mapping via an explicit ħ parameter. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (18)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
RSUnits
in IndisputableMonolith.Constants
decl_use
-
U
in IndisputableMonolith.Constants.RSNativeUnits
decl_use
-
Constants
in IndisputableMonolith.CPM.LawOfExistence
decl_use
-
via
in IndisputableMonolith.Derivations.MassToLight
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
DeltaSub
in IndisputableMonolith.LedgerUnits
decl_use
-
U
in IndisputableMonolith.Recognition
decl_use
-
DeltaSub
in IndisputableMonolith.RecogSpec.Scales
decl_use
-
mapDelta
in IndisputableMonolith.RecogSpec.Scales
decl_use
-
timeMap
in IndisputableMonolith.RecogSpec.Scales
decl_use
-
RSUnits
in IndisputableMonolith.TruthCore.Display
decl_use
-
DeltaSub
in IndisputableMonolith.UnitMapping
decl_use
-
mapDelta
in IndisputableMonolith.UnitMapping
decl_use
-
timeMap
in IndisputableMonolith.UnitMapping
decl_use