IndisputableMonolith.Foundation.VariationalDynamics
This module defines the variational dynamics setup for ledger states in Recognition Science. It introduces LedgerState as N positive real ratios indexed by tick, along with feasibility and defect notions. Researchers on topological conservation cite these to connect J-cost minimization to charge conservation. The module is purely definitional, importing convexity and determinism results without new proofs.
claimA ledger state consists of $N$ entries with positive real ratios $r_i > 0$, indexed by tick. Related objects include $ ext{Feasible}$ configurations, $ ext{log_charge}$, and $ ext{total_defect}$ measures built from the J-cost function.
background
The module sits inside the Foundation layer and imports Cost.Convexity (Jlog(t) = cosh t - 1 and Jcost(x) = ½(x + x⁻¹) - 1 are strictly convex), Determinism (unique minimizer for any constrained ledger update), TimeEmergence (time is the tick counter; minimal period is the 8-tick cycle for D = 3), LawOfExistence (x exists iff defect(x) = 0), and InitialCondition (low-entropy start). These supply the J-cost and defectDist primitives used to define ledger states and feasibility.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
Supplies the LedgerState, Feasible, and defect definitions required by TopologicalConservation (F-012: conservation laws arise from topology and linking in D = 3, not Noether symmetries) and WindingCharges (F-013: conservation realized via winding numbers of lattice paths). It bridges the variational J-cost layer to the topological charge layer.
scope and limits
- Does not derive or reprove convexity of J.
- Does not contain theorems on time emergence or determinism.
- Does not address initial conditions or the low-entropy puzzle.
- Does not prove any conservation laws or winding results.
used by (2)
depends on (6)
declarations in this module (34)
-
structure
LedgerState -
def
log_charge -
def
Feasible -
theorem
self_feasible -
theorem
feasible_nonempty -
def
IsVariationalSuccessor -
theorem
total_defect_nonneg' -
def
constant_config -
theorem
constant_config_log_charge -
theorem
constant_config_total_defect -
theorem
weighted_log_average -
theorem
weighted_Jlog_average -
theorem
total_defect_lower_bound -
theorem
eq_constant_config_of_defect_eq -
theorem
unity_log_charge_zero -
theorem
unity_is_optimal -
theorem
variational_step_exists -
theorem
variational_step_unique -
theorem
variational_step_reduces_defect -
def
Trajectory -
def
IsVariationalTrajectory -
theorem
variational_dynamics_deterministic -
theorem
trajectory_defect_monotone -
structure
LocalUpdate -
theorem
update_is_global -
theorem
variational_implies_recognition_step -
def
IsEquilibrium -
theorem
equilibrium_iff_minimizer -
theorem
unity_is_equilibrium -
theorem
equilibrium_attractive -
def
uniform_config -
theorem
uniform_config_charge -
theorem
uniform_is_variational_successor -
theorem
variational_dynamics_certificate