def
definition
def or abbrev
Possibility
show as:
view Lean formalization →
formal statement (Lean)
230def Possibility (c : Config) : Set Config :=
proof body
Definition body.
231 {y : Config |
232 -- Within one octave step
233 y.time = c.time + 8 ∧
234 -- Cost-respecting (change doesn't increase total cost)
235 J c.value + J_transition c.value y.value c.pos y.pos + J y.value ≤
236 J c.value + J_stasis c.value
237 }
238
239/-- The identity is always possible from any configuration.
240
241 The boundedness constraint is now part of the Config structure,
242 ensuring all physical configurations can reach identity in one step. -/
used by (31)
-
rs_modal_logic_status -
A_advances_time -
ActualizationPrinciple -
adjoint_from_cost_monotonic -
collapse_automatic -
Contingent -
Degenerate -
Determined -
determined_necessary_for_minimal -
H_adjoint_non_minimal -
possibility_actualization_adjoint_minimal -
modal_completeness -
modal_distance_symm -
modal_nyquist -
possibility_space_connected -
actualize_decreases_cost -
Counterfactual -
identity_always_possible -
identity_in_all_possibility_spaces -
identity_prefers_stasis -
identity_unique_attractor -
modal_K -
Necessary -
PossibilitySpace -
possibility_status -
Possible -
why_anything_happens -
actual_has_zero_modal_distance -
necessary_is_one -
ph013_modal_certificate