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)
64noncomputable def mapDeltaCharge (δ : ℤ) (hδ : δ ≠ 0) (qe : ℝ) : DeltaSub δ → ℝ :=
proof body
Definition body.
65 mapDelta δ hδ (chargeMap qe)
66
67/-- Existence of affine δ→time mapping via τ0. -/
depends on (14)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
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
-
chargeMap
in IndisputableMonolith.Masses.AnchorPolicy
decl_use
-
chargeMap
in IndisputableMonolith.RecogSpec.Scales
decl_use
-
DeltaSub
in IndisputableMonolith.RecogSpec.Scales
decl_use
-
mapDelta
in IndisputableMonolith.RecogSpec.Scales
decl_use
-
chargeMap
in IndisputableMonolith.UnitMapping
decl_use
-
DeltaSub
in IndisputableMonolith.UnitMapping
decl_use
-
mapDelta
in IndisputableMonolith.UnitMapping
decl_use