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)
76def amplitudeScalarOnly (a_scalar v s : ℝ) : ℝ :=
proof body
Definition body.
77 a_scalar * s ^ 2 / v ^ 4
78
79/-- The total amplitude is the sum of gauge and scalar contributions. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (14)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
total
in IndisputableMonolith.NavierStokes.DiscreteVorticity
decl_use
-
and
in IndisputableMonolith.NumberTheory.CirclePhaseLift
decl_use
-
total
in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget
decl_use
-
amplitude
in IndisputableMonolith.QFT.SMatrixUnitarity
decl_use
-
amplitude
in IndisputableMonolith.Quantum.DoubleSlit
decl_use