`collapse_threshold`

definition

show as: view math explainer →

module: IndisputableMonolith.Modal.Actualization
domain: Modal
line: 226 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Modal.Actualization on GitHub at line 226.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 223    - Superposition collapses to definite state
 224    - No measurement postulate needed
 225    - Built into dynamics, not added as axiom -/
 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). -/

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.