abbrev definition def or abbrev

`Energy`

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

formal statement (Lean)

  56abbrev Energy := ℝ

used by (40)

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

applied in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
hamilton_equations_from_EL in IndisputableMonolith.Action.Hamiltonian decl_use
totalEnergy in IndisputableMonolith.Action.Hamiltonian decl_use
timeTranslationFlow in IndisputableMonolith.Action.Noether decl_use
eV_to_J_pos in IndisputableMonolith.Applied.PhotobiomodulationDevice decl_use
of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
hcp_ratio_near_phi in IndisputableMonolith.Chemistry.CrystalStructure decl_use
Hypothesis in IndisputableMonolith.ClassicalBridge.Fluids.CPM2D decl_use
EnergySkewHypothesis in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
galerkinNSRHS in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D decl_use
tau0_pos in IndisputableMonolith.Constants decl_use
energy_raw in IndisputableMonolith.Constants.RSNativeUnits decl_use
hbarQuantum_eq_Ecoh in IndisputableMonolith.Constants.RSNativeUnits decl_use
momentumQuantum_eq_cohQuantum in IndisputableMonolith.Constants.RSNativeUnits decl_use
planckEnergy_rs in IndisputableMonolith.Constants.RSNativeUnits decl_use
to_joules in IndisputableMonolith.Constants.RSNativeUnits decl_use
phiLadderSum in IndisputableMonolith.Cosmology.CosmologicalConstant decl_use
lambda_positive in IndisputableMonolith.Cosmology.DarkEnergy decl_use
phase_locked_energy_constant in IndisputableMonolith.Cosmology.DarkEnergyEOS decl_use
initial_state_is_zero_defect in IndisputableMonolith.Cosmology.EarlyUniverse decl_use
alpha_over_pi_bounds in IndisputableMonolith.Cosmology.HubbleTension decl_use
H_late_pred in IndisputableMonolith.Cosmology.HubbleTension decl_use
hubble_ratio_from_ledger in IndisputableMonolith.Cosmology.HubbleTension decl_use
hubble_ratio_topo in IndisputableMonolith.Cosmology.HubbleTension decl_use
ode_neg_zero_uniqueness in IndisputableMonolith.Cost.AczelProof decl_use
CPMConstantsRecord in IndisputableMonolith.CPM.LawOfExistence decl_use
Model in IndisputableMonolith.CPM.LawOfExistence decl_use
gridStabilityControlsCert in IndisputableMonolith.Energy.GridStabilityControlsFromConfigDim decl_use
RunawaySignature in IndisputableMonolith.Energy.VacuumPump decl_use
E_coh_storage_pos in IndisputableMonolith.Engineering.EnergyStorageDensityStructure decl_use

… and 10 more