IndisputableMonolith.Foundation.VariationalDynamics

declarations in this module (34)

• structure LedgerState L77
• def log_charge L83
• def Feasible L90
• theorem self_feasible L94
• theorem feasible_nonempty L98
• def IsVariationalSuccessor L107
• theorem total_defect_nonneg' L112
• def constant_config L118
• theorem constant_config_log_charge L123
• theorem constant_config_total_defect L130
• theorem weighted_log_average L137
• theorem weighted_Jlog_average L145
• theorem total_defect_lower_bound L160
• theorem eq_constant_config_of_defect_eq L190
• theorem unity_log_charge_zero L238
• theorem unity_is_optimal L246
• theorem variational_step_exists L262
• theorem variational_step_unique L290
• theorem variational_step_reduces_defect L343
• def Trajectory L353
• def IsVariationalTrajectory L357
• theorem variational_dynamics_deterministic L366
• theorem trajectory_defect_monotone L403
• structure LocalUpdate L413
• theorem update_is_global L426
• theorem variational_implies_recognition_step L481
• def IsEquilibrium L507
• theorem equilibrium_iff_minimizer L517
• theorem unity_is_equilibrium L527
• theorem equilibrium_attractive L541
• def uniform_config L551
• theorem uniform_config_charge L556
• theorem uniform_is_variational_successor L574
• theorem variational_dynamics_certificate L615