abbrev definition def or abbrev

`Action`

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

formal statement (Lean)

  57abbrev Action := ℝ

used by (26)

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
energy_conservation_one_statement in IndisputableMonolith.Action.EnergyConservationDomainCert decl_use
eulerLagrange_status in IndisputableMonolith.Action.EulerLagrange decl_use
functionalConvexity_status in IndisputableMonolith.Action.FunctionalConvexity decl_use
hamiltonian_status in IndisputableMonolith.Action.Hamiltonian decl_use
NewtonSecondLawCert in IndisputableMonolith.Action.NewtonSecondLawDomainCert decl_use
newton_second_law_one_statement in IndisputableMonolith.Action.NewtonSecondLawDomainCert decl_use
noether_status in IndisputableMonolith.Action.Noether decl_use
space_translation_invariance_implies_momentum_conservation in IndisputableMonolith.Action.Noether decl_use
pathSpace_status in IndisputableMonolith.Action.PathSpace decl_use
quadraticLimit_status in IndisputableMonolith.Action.QuadraticLimit decl_use
action_raw in IndisputableMonolith.Constants.RSNativeUnits decl_use
energy_raw in IndisputableMonolith.Constants.RSNativeUnits decl_use
status in IndisputableMonolith.Constants.RSNativeUnits decl_use
analysisAction_count in IndisputableMonolith.Foundation.OptionAEmpiricalActionPlan decl_use
stationarity_iff_laplacian_zero in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
response_enhancement in IndisputableMonolith.Gravity.CaldeiraLeggett decl_use
Jcost_nonneg in IndisputableMonolith.Gravity.CoherenceCollapse decl_use
deficit_neg_of_angle_excess in IndisputableMonolith.Gravity.ReggeCalculus decl_use
determined_necessary_for_minimal in IndisputableMonolith.Modal.Actualization decl_use
diagOp in IndisputableMonolith.NumberTheory.HilbertPolyaCandidate decl_use
shiftOp in IndisputableMonolith.NumberTheory.HilbertPolyaCandidate decl_use
hume_guillotine_dissolved in IndisputableMonolith.Philosophy.ObjectiveMoralityStructure decl_use
symmetry_maps_cells in IndisputableMonolith.RecogGeom.Symmetry decl_use
phi_sq in IndisputableMonolith.RRF.Hypotheses.PhiLadder decl_use