Trajectory
plain-language theorem explainer
A ledger trajectory with N entries is any map from natural-number ticks to configurations of positive real ratios. Workers on topological conservation or deterministic ledger evolution cite this definition when quantifying over sequences of states obeying the update rule. The declaration is a direct type abbreviation introducing the domain for variational successor statements.
Claim. A ledger trajectory on $N$ entries is a function $t : ℕ → C$, where each $C$ is a configuration consisting of $N$ positive real ratios (entries : Fin $N$ → ℝ with all entries positive).
background
Module VariationalDynamics supplies the missing equation of motion for the Recognition Science ledger: each step is the global argmin of total J-cost over the feasible set defined by the conservation law (sum of log-ratios invariant). Configuration, imported from InitialCondition, is the structure whose entries are positive reals; TotalDefect is the sum of individual J-costs on those entries. Upstream results establish that J has a unique minimum at 1 (LawOfExistence), that defect is non-increasing (TimeEmergence), and that convexity forces unique minimizers (Determinism).
proof idea
One-line definition that aliases the function type ℕ → Configuration N. No lemmas or tactics are invoked; the declaration merely names the carrier type used by IsVariationalTrajectory and the conservation statements.
why it matters
The definition supplies the domain for all downstream conservation results, including topological_charge_trajectory_conserved (charge invariant along any variational trajectory) and total_charge_always_zero (universe starts neutral). It completes the F-008 gap by enabling statements of the constrained J-minimization update rule. The same type appears in equilibrium_attractive, which shows defect sequences are monotone and bounded below.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.