def definition def or abbrev

`V`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  44def V (phi_inf : ℝ) : ℝ := Cost.Jcost (1 + phi_inf)

proof body

Definition body.

  45
  46/-- The vacuum value `V(0) = 0`. -/

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

applied in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
energyConservationCert in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
EnergyConservationCert in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
conjugateMomentum in IndisputableMonolith.Action.Hamiltonian decl_use
energy_conservation in IndisputableMonolith.Action.Hamiltonian decl_use
hamilton_equations_from_EL in IndisputableMonolith.Action.Hamiltonian decl_use
hamiltonPDotEquation in IndisputableMonolith.Action.Hamiltonian decl_use
hamiltonQDotEquation in IndisputableMonolith.Action.Hamiltonian decl_use
standardHamiltonian in IndisputableMonolith.Action.Hamiltonian decl_use
totalEnergy in IndisputableMonolith.Action.Hamiltonian decl_use
NewtonSecondLawCert in IndisputableMonolith.Action.NewtonSecondLawDomainCert decl_use
energy_conservation_of_J_action in IndisputableMonolith.Action.Noether decl_use
space_translation_invariance_implies_momentum_conservation in IndisputableMonolith.Action.Noether decl_use
kineticAction in IndisputableMonolith.Action.QuadraticLimit decl_use
newton_second_law in IndisputableMonolith.Action.QuadraticLimit decl_use
standardEL in IndisputableMonolith.Action.QuadraticLimit decl_use
standardLagrangian in IndisputableMonolith.Action.QuadraticLimit decl_use
Cycle in IndisputableMonolith.Algebra.LedgerAlgebra decl_use
caTimeBound in IndisputableMonolith.Complexity.SAT.Runtime decl_use
Q3_faces in IndisputableMonolith.Constants.PlanckScaleMatching decl_use
potential_positive in IndisputableMonolith.Cosmology.Inflation decl_use
powerSpectrum in IndisputableMonolith.Cosmology.Inflation decl_use
slow_roll_at_large_phi in IndisputableMonolith.Cosmology.Inflation decl_use
slowRollEpsilon in IndisputableMonolith.Cosmology.Inflation decl_use
slowRollEta in IndisputableMonolith.Cosmology.Inflation decl_use
InflatonPotentialCert in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
V_eq_quadratic in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
V_nonneg in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
V_pos_off_vacuum in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
V_quadratic_at_origin in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.

V in IndisputableMonolith.Foundation.SpectralEmergence decl_use
Cost in IndisputableMonolith.Measurement.RSNative.Core decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
V in IndisputableMonolith.RRF.Core.Glossary decl_use
vacuum in IndisputableMonolith.Unification.YangMillsMassGap decl_use