V — Recognition explainer

formal statement (Lean)

  81def V (D : ℕ) : ℕ := 2 ^ D

proof body

Definition body.

  82
  83/-- Edges of the D-cube: |E| = D × 2^(D-1). Each vertex has D neighbors;
  84    each edge is shared between 2 vertices. -/

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 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

… and 10 more

depends on (14)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
V in IndisputableMonolith.Cosmology.InflatonPotentialFromJCost decl_use
has in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
neighbors in IndisputableMonolith.Ethics.StakeGraph 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
E in IndisputableMonolith.Foundation.SpectralEmergence 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
V in IndisputableMonolith.RRF.Core.Glossary decl_use