pith. sign in
module module high

IndisputableMonolith.Foundation.VariationalDynamics

show as:
view Lean formalization →

VariationalDynamics introduces ledger states as finite sequences of positive real ratios indexed by discrete ticks and defines variational successors via J-cost minimization. Researchers deriving time emergence, determinism, and topological conservation from the Recognition framework would cite it. The module's structure rests on convexity of J from Cost.Convexity to guarantee unique minimizers for feasible updates.

claimA ledger state is a map $s: Ticks → (0,∞)^N$ where each entry is a positive real ratio. A configuration is feasible when total defect vanishes. The variational successor is the unique minimizer of the summed J-cost subject to the feasibility constraint.

background

This module operates in the Foundation layer of Recognition Science. It imports the strict convexity of Jlog(t) = cosh(t) - 1 and Jcost(x) = ½(x + x⁻¹) - 1 from Cost.Convexity, which underpins uniqueness of minimizers. LawOfExistence supplies the equivalence x exists ⇔ defect(x) = 0, while TimeEmergence identifies time with the tick counter and fixes the minimal 8-tick period for D = 3. Determinism and InitialCondition supply the low-entropy starting point and the guarantee that constrained J-minimization yields a unique successor.

proof idea

This is a definition module. LedgerState, Feasible, and IsVariationalSuccessor are introduced by direct construction. Theorems such as feasible_nonempty, self_feasible, and constant_config_total_defect are obtained by exhibiting explicit constant-ratio configurations and invoking non-negativity of total defect.

why it matters in Recognition Science

VariationalDynamics supplies the update rule that TopologicalConservation and WindingCharges rely on to obtain charge conservation from linking numbers rather than Noether symmetries. It fills the dynamical step between the initial low-entropy condition and the emergence of independent winding charges in three dimensions.

scope and limits

used by (2)

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

depends on (6)

Lean names referenced from this declaration's body.

declarations in this module (34)