def definition def or abbrev

`Trajectory`

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

formal statement (Lean)

 353def Trajectory (N : ℕ) := ℕ → Configuration N

Definition body.

 354
 355/-- **Definition**: A trajectory follows the variational dynamics if
 356    each successive pair satisfies the variational update rule. -/

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

charge_at_any_tick in IndisputableMonolith.Foundation.TopologicalConservation decl_use
topological_charge_trajectory_conserved in IndisputableMonolith.Foundation.TopologicalConservation decl_use
topological_conservation_certificate in IndisputableMonolith.Foundation.TopologicalConservation decl_use
total_charge_always_zero in IndisputableMonolith.Foundation.TopologicalConservation decl_use
equilibrium_attractive in IndisputableMonolith.Foundation.VariationalDynamics decl_use
IsVariationalTrajectory in IndisputableMonolith.Foundation.VariationalDynamics decl_use
trajectory_defect_monotone in IndisputableMonolith.Foundation.VariationalDynamics decl_use
variational_dynamics_deterministic in IndisputableMonolith.Foundation.VariationalDynamics decl_use

Lean names referenced from this declaration's body.

Configuration in IndisputableMonolith.Foundation.InitialCondition decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
Configuration in IndisputableMonolith.Foundation.RecognitionForcing decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use
trajectory in IndisputableMonolith.Robotics.PIDStabilityFromJCost decl_use