Trajectory
A trajectory is a function from natural numbers to configurations of N positive real ledger entries. Researchers formalizing charge conservation or defect monotonicity cite it to index sequences along which the variational update applies at every step. The declaration is a direct type abbreviation with no further structure or constraints imposed.
claimA trajectory for parameter $N$ is a map $tmapsto c_t$ where each $c_t$ belongs to Configuration$(N)$, the structure whose entries field assigns a positive real to each of the $N$ positions.
background
The VariationalDynamics module supplies the missing update rule after LawOfExistence (J-cost minimum at unity), InitialCondition (zero-defect start), TimeEmergence (non-increasing defect), and Determinism (unique minimizers from convexity). Configuration is the structure with entries : Fin N → ℝ and entries_pos positivity proof. The module states the ledger evolves by constrained global J-cost minimization: state(t+1) equals argmin of TotalDefect over the feasible set, preserving the invariant sum of log-ratios.
proof idea
The declaration is a one-line type abbreviation equating Trajectory N with the function type ℕ → Configuration N.
why it matters in Recognition Science
This definition is the sequence type required by the topological conservation theorems (charge_at_any_tick, topological_charge_trajectory_conserved, total_charge_always_zero) that establish exact invariance of integer-valued charges along any path. It completes the F-008 equation-of-motion formalization and feeds equilibrium_attractive and variational_dynamics_deterministic. The construction connects to the RCL identity and the D=3 requirement for three independent charges.
scope and limits
- Does not impose the IsVariationalSuccessor condition on consecutive terms.
- Does not encode the argmin update rule or feasibility constraint.
- Does not restrict trajectories to finite length or prescribe an initial state.
- Does not assume any particular value of the conserved log-ratio sum.
formal statement (Lean)
353def Trajectory (N : ℕ) := ℕ → Configuration N
proof body
Definition body.
354
355/-- **Definition**: A trajectory follows the variational dynamics if
356 each successive pair satisfies the variational update rule. -/