def
definition
has_definite_pointer
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Modal.Actualization on GitHub at line 229.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
226def collapse_threshold : ℝ := 1
227
228/-- A configuration has definite pointer when C ≥ 1. -/
229def has_definite_pointer (c : Config) : Prop :=
230 J c.value ≥ collapse_threshold
231
232/-- **COLLAPSE IS AUTOMATIC**: No measurement postulate needed.
233
234 When recognition cost exceeds threshold, the universe automatically
235 selects a definite branch via J-minimization. -/
236theorem collapse_automatic (c : Config) (_ : J c.value ≥ collapse_threshold) :
237 has_definite_pointer (Actualize c) ∨ J (Actualize c).value < collapse_threshold := by
238 right
239 simp only [Actualize, identity_config, J_at_one, collapse_threshold]
240 norm_num
241
242/-! ## The Actualization Operator -/
243
244/-- **THE ACTUALIZATION OPERATOR A**: Maps current to actualized configuration.
245
246 A : Config → Config
247 A(c) = argmin_{y ∈ P(c)} J(y)
248
249 This is dual to the Possibility operator P:
250 - P gives what COULD happen
251 - A gives what DOES happen
252
253 Together, P and A completely characterize RS modal dynamics. -/
254def A : Config → Config := Actualize
255
256/-- A is well-defined (always produces valid config). -/
257lemma A_well_defined (c : Config) : (A c).value > 0 := actualize_valid c
258
259/-- A drives toward identity. -/