IndisputableMonolith.Modal.Actualization
IndisputableMonolith/Modal/Actualization.lean · 426 lines · 30 declarations
show as:
view math explainer →
1/-
2Copyright (c) 2025 Recognition Science. All rights reserved.
3Released under MIT license as described in the file LICENSE.
4Authors: Recognition Science Contributors
5-/
6import IndisputableMonolith.Modal.Possibility
7
8/-!
9# Actualization: Selection from Possibilities
10
11This module formalizes the **actualization mechanism** in Recognition Science:
12how possibilities become actual through J-cost minimization.
13
14## The Central Question
15
16Given the set of possibilities P(c), how is one selected to become actual?
17
18**Answer**: The universe selects the J-minimizing path. Actualization is not:
19- Random (probability is derived, not fundamental)
20- Observer-dependent (collapse is built-in at C≥1)
21- Non-deterministic (given identical initial conditions, same outcome)
22
23## Key Structures
24
25| Concept | Definition | RS Grounding |
26|---------|------------|--------------|
27| Selection | argmin_{y ∈ P(c)} J(y) | Cost minimization |
28| Degeneracy | Multiple y with same min J | Contingency |
29| Path Integral | ∫ exp(-C[γ]) Dγ | Born rule emergent |
30| Collapse | C≥1 forces selection | No measurement postulate |
31
32## Connection to Quantum Mechanics
33
34The actualization mechanism explains:
351. Why Born rule works (exp(-C) weighting)
362. Why collapse occurs (C≥1 threshold)
373. Why measurement is deterministic once C≥1
384. Why interference exists (multiple low-cost paths)
39-/
40
41namespace IndisputableMonolith.Modal
42
43open Foundation
44open Real
45open Classical
46
47noncomputable section
48
49/-! ## The Actualization Principle -/
50
51/-- **ACTUALIZATION PRINCIPLE**: The universe selects cost-minimizing futures.
52
53 This is the fundamental dynamical principle of RS:
54 - Given current state c
55 - Among all y ∈ P(c)
56 - Select argmin J(y)
57
58 If there's a unique minimum, actualization is deterministic.
59 If there are multiple minima (degeneracy), further structure resolves. -/
60structure ActualizationPrinciple where
61 /-- Current configuration -/
62 current : Config
63 /-- The actualized successor -/
64 successor : Config
65 /-- Successor is in possibility set -/
66 in_possibility : successor ∈ Possibility current
67 /-- Successor minimizes cost among possibilities -/
68 minimizes_cost : ∀ y ∈ Possibility current, J successor.value ≤ J y.value
69
70/-- An actualization witness for a configuration. -/
71def has_actualization (c : Config) : Prop :=
72 ∃ ap : ActualizationPrinciple, ap.current = c
73
74/-- Every configuration has an actualization (toward identity). -/
75theorem every_config_actualizes (c : Config) : has_actualization c := by
76 use {
77 current := c
78 successor := identity_config (c.time + 8)
79 in_possibility := identity_always_possible c
80 minimizes_cost := by
81 intro y hy
82 simp [identity_config, J_at_one]
83 exact J_nonneg y.pos
84 }
85
86/-! ## Degeneracy and Contingency -/
87
88/-- **DEGENERACY**: When multiple configurations have the same minimal cost.
89
90 This is the origin of contingency in RS—when the universe "could have gone either way"
91 because multiple paths have identical J-cost. -/
92def Degenerate (c : Config) : Prop :=
93 ∃ y ∈ Possibility c, ∃ z ∈ Possibility c, y ≠ z ∧ J y.value = J z.value ∧
94 ∀ w ∈ Possibility c, J y.value ≤ J w.value
95
96/-- **CONTINGENT**: A property that could have been otherwise.
97
98 p is contingent at c if:
99 1. p holds for the actualized successor
100 2. There exists a degenerate possibility where ¬p holds -/
101def Contingent (p : ConfigProp) (c : Config) : Prop :=
102 p (Actualize c) ∧ Degenerate c ∧
103 ∃ y ∈ Possibility c, J y.value = J (Actualize c).value ∧ ¬p y
104
105/-- **DETERMINED**: A property that could not have been otherwise.
106
107 p is determined at c if all cost-minimal successors satisfy p. -/
108def Determined (p : ConfigProp) (c : Config) : Prop :=
109 ∀ y ∈ Possibility c,
110 J y.value = J (Actualize c).value → p y
111
112/-- Determined properties are necessary among cost-equivalents. -/
113theorem determined_necessary_for_minimal (p : ConfigProp) (c : Config)
114 (hd : Determined p c) :
115 ∀ y ∈ Possibility c, J y.value = J (Actualize c).value → p y :=
116 hd
117
118/-! ## Path Action and Born Rule -/
119
120/-- **PATH ACTION**: The total J-cost accumulated along a path.
121
122 C[γ] = Σᵢ J(γᵢ) + J_transition(γᵢ, γᵢ₊₁)
123
124 This is the Recognition Science analogue of the classical action. -/
125def PathAction (path : List Config) : ℝ :=
126 match path with
127 | [] => 0
128 | [c] => J c.value
129 | c₁ :: c₂ :: rest =>
130 J c₁.value + J_transition c₁.value c₂.value c₁.pos c₂.pos +
131 PathAction (c₂ :: rest)
132
133/-- Empty path has zero action. -/
134lemma path_action_nil : PathAction [] = 0 := rfl
135
136/-- Single-element path has cost J. -/
137lemma path_action_single (c : Config) : PathAction [c] = J c.value := rfl
138
139/-- **PATH WEIGHT**: The exponential weight of a path.
140
141 W[γ] = exp(-C[γ])
142
143 This is the fundamental quantity that gives rise to the Born rule. -/
144noncomputable def PathWeight (path : List Config) : ℝ :=
145 Real.exp (-PathAction path)
146
147/-- Path weight is always positive. -/
148lemma path_weight_pos (path : List Config) : 0 < PathWeight path :=
149 Real.exp_pos _
150
151/-- **BORN RULE EMERGENCE**: The probability of a path is proportional to its weight.
152
153 P[γ] = W[γ] / Σ_γ' W[γ']
154
155 This is not postulated—it emerges from the cost structure. -/
156structure BornRule where
157 /-- The paths being considered -/
158 paths : List (List Config)
159 /-- Non-empty path set -/
160 nonempty : paths ≠ []
161 /-- Total weight (partition function) -/
162 Z : ℝ := paths.foldl (fun acc γ => acc + PathWeight γ) 0
163 /-- Probability of a path -/
164 prob (γ : List Config) : ℝ := if γ ∈ paths then PathWeight γ / Z else 0
165
166/-- Sum of (f x / c) over a list equals (sum of f x) / c. -/
167lemma List.sum_map_div' {α : Type*} (l : List α) (f : α → ℝ) (c : ℝ) (hc : c ≠ 0) :
168 (l.map (fun x => f x / c)).sum = (l.map f).sum / c := by
169 induction l with
170 | nil => simp
171 | cons head tail ih =>
172 simp only [List.map_cons, List.sum_cons, ih]
173 field_simp
174
175/-- Helper: foldl addition equals List.sum for a mapped list -/
176lemma foldl_add_eq_sum {α : Type*} (l : List α) (f : α → ℝ) :
177 l.foldl (fun acc x => acc + f x) 0 = (l.map f).sum := by
178 have h_gen : ∀ (init : ℝ), l.foldl (fun acc x => acc + f x) init = init + (l.map f).sum := by
179 induction l with
180 | nil => intro init; simp
181 | cons head tail ih =>
182 intro init
183 simp only [List.foldl_cons, List.map_cons, List.sum_cons]
184 rw [ih (init + f head)]
185 ring
186 simpa using h_gen 0
187
188/-- Probabilities sum to 1 for non-empty path sets.
189
190 The normalization follows from Z being the sum of all weights.
191
192 Note: This theorem assumes the standard definitions where:
193 - br.Z = br.paths.foldl (fun acc γ => acc + PathWeight γ) 0
194 - br.prob γ = if γ ∈ br.paths then PathWeight γ / br.Z else 0
195
196 These are the default definitions in BornRule. -/
197theorem born_rule_normalized (br : BornRule) (hZ : br.Z ≠ 0)
198 (h_Z_def : br.Z = br.paths.foldl (fun acc γ => acc + PathWeight γ) 0)
199 (h_prob_def : ∀ γ, br.prob γ = if γ ∈ br.paths then PathWeight γ / br.Z else 0) :
200 br.paths.foldl (fun acc γ => acc + br.prob γ) 0 = 1 := by
201 -- Key insight: each prob γ = PathWeight γ / Z for γ ∈ paths
202 -- Sum of (PathWeight γ / Z) = (Sum of PathWeight γ) / Z = Z / Z = 1
203 have h_sum_prob : br.paths.foldl (fun acc γ => acc + br.prob γ) 0 =
204 (br.paths.map (fun γ => br.prob γ)).sum := foldl_add_eq_sum br.paths br.prob
205 -- The map of prob equals the map of (PathWeight / Z) for paths in the list
206 have h_maps : br.paths.map (fun γ => br.prob γ) = br.paths.map (fun γ => PathWeight γ / br.Z) := by
207 apply List.map_congr_left
208 intro γ hγ
209 rw [h_prob_def γ, if_pos hγ]
210 rw [h_sum_prob, h_maps, List.sum_map_div' br.paths PathWeight br.Z hZ]
211 -- Now: (br.paths.map PathWeight).sum / br.Z = 1
212 -- This is Z / Z = 1 since Z = (map PathWeight).sum
213 have h_Z_eq : br.Z = (br.paths.map PathWeight).sum := by
214 rw [h_Z_def, foldl_add_eq_sum]
215 rw [← h_Z_eq]
216 field_simp
217
218/-! ## Collapse as Cost Threshold -/
219
220/-- **COLLAPSE THRESHOLD**: C = 1 is the recognition cost threshold for definiteness.
221
222 When the accumulated recognition cost C ≥ 1:
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). -/
257lemma A_well_defined (c : Config) : (A c).value > 0 := actualize_valid c
258
259/-- A drives toward identity. -/
260theorem A_toward_identity (c : Config) (hne : c.value ≠ 1) :
261 J (A c).value < J c.value := actualize_decreases_cost c hne
262
263/-- A preserves time advancement. -/
264theorem A_advances_time (c : Config) : (A c).time = c.time + 8 := by
265 simp [A, Actualize, identity_config]
266
267/-! ## The Adjointness of P and A -/
268
269/-- **HYPOTHESIS**: For cost-monotonic properties, the actualized element inherits properties.
270
271 A property p is **cost-monotonic** if:
272 p y ∧ J y.value > J y'.value → p y'
273 i.e., the property propagates down the cost gradient.
274
275 Under this assumption, if p holds at any y ∈ Possibility c, then p holds at A c
276 (the cost-minimizing element).
277
278 **STATUS**: HYPOTHESIS - This captures a specific class of properties for which
279 adjointness holds. Not all properties are cost-monotonic. -/
280def CostMonotonic (p : ConfigProp) : Prop :=
281 ∀ y y' : Config, p y → J y.value > J y'.value → y'.value > 0 → p y'
282
283/-- For cost-monotonic properties, adjointness holds from any higher-cost element. -/
284theorem adjoint_from_cost_monotonic (p : ConfigProp) (c : Config)
285 (hcm : CostMonotonic p)
286 (y : Config) (hy : y ∈ Possibility c) (hp : p y)
287 (hA_pos : (A c).value > 0) :
288 J y.value > J (A c).value → p (A c) := by
289 intro h_cost_gt
290 exact hcm y (A c) hp h_cost_gt hA_pos
291
292/-- **HYPOTHESIS**: Non-cost-monotonic properties may not transfer.
293
294 For properties that don't propagate down the cost gradient, we cannot
295 conclude p (A c) from p y when J y > J (A c).
296
297 This is the correct characterization: adjointness is conditional on
298 the property type. -/
299theorem H_adjoint_non_minimal (p : ConfigProp) (c : Config)
300 (_h_unique : ∀ y ∈ Possibility c, J y.value = J (Actualize c).value → y = Actualize c)
301 (y : Config) (_hy : y ∈ Possibility c) (hp : p y) (_h_cost_pos : J y.value ≠ 0)
302 (hcm : CostMonotonic p) (hA_pos : (A c).value > 0) :
303 p (A c) := by
304 -- y has positive cost, A c has zero cost (identity), so J y > J (A c)
305 have hJ_y_pos : J y.value > 0 := by
306 cases' (lt_or_eq_of_le (J_nonneg y.pos)) with h h
307 · exact h
308 · exact absurd h.symm _h_cost_pos
309 have hJ_A : J (A c).value = 0 := by simp only [A, Actualize, identity_config, J_at_one]
310 have h_gt : J y.value > J (A c).value := by rw [hJ_A]; exact hJ_y_pos
311 exact hcm y (A c) hp h_gt hA_pos
312
313/-- **P and A are ADJOINT operators** (for minimal-cost elements):
314
315 For any property p:
316 - ◇p at c ⟺ p(A(c)) when the witness y ∈ P(c) has minimal cost
317
318 **Important**: This adjointness is restricted to cost-equivalent elements.
319 For elements y ∈ P(c) with J y.value > J (A c).value = 0, adjointness requires
320 the additional assumption that p is cost-monotonic.
321
322 This is the mathematical core of RS modal logic. -/
323theorem possibility_actualization_adjoint_minimal (p : ConfigProp) (c : Config)
324 (h_unique : ∀ y ∈ Possibility c, J y.value = J (Actualize c).value → y = Actualize c) :
325 (∃ y ∈ Possibility c, J y.value = J (Actualize c).value ∧ p y) ↔ p (A c) := by
326 constructor
327 · intro ⟨y, hy, hJ_eq, hp⟩
328 have hAct : J (Actualize c).value = 0 := by
329 simp only [Actualize, identity_config, J_at_one]
330 -- Since J y.value = J (Actualize c).value = 0 and h_unique, y = Actualize c
331 have hJ_zero : J y.value = 0 := hJ_eq.trans hAct
332 have hy_eq : y = Actualize c := h_unique y hy hJ_eq
333 rw [hy_eq] at hp
334 exact hp
335 · intro hp
336 exact ⟨A c, identity_always_possible c, rfl, hp⟩
337
338/-- **P and A adjointness for cost-monotonic properties** -/
339theorem possibility_actualization_adjoint_monotonic (p : ConfigProp) (c : Config)
340 (hcm : CostMonotonic p) :
341 (◇p) c ↔ p (A c) := by
342 constructor
343 · intro ⟨y, hy, hp⟩
344 have hAct : J (Actualize c).value = 0 := by
345 simp only [Actualize, identity_config, J_at_one]
346 have hA_pos : (A c).value > 0 := actualize_valid c
347 by_cases hJ0 : J y.value = 0
348 · -- y has cost 0, so y.value = 1 (by J_zero_iff_one)
349 have hy_val : y.value = 1 := (J_zero_iff_one y.pos).mp hJ0
350 have hA_val : (A c).value = 1 := by simp only [A, Actualize, identity_config]
351 have hy_time : y.time = c.time + 8 := hy.1
352 have hA_time : (A c).time = c.time + 8 := by simp only [A, Actualize, identity_config]
353 -- Since value and time are the same, and other fields are Props, y = A c
354 -- Helper: show both y and A c equal the identity config at c.time + 8
355 have hy_is_identity : y = identity_config (c.time + 8) := by
356 simp only [identity_config]
357 have hv := hy_val -- y.value = 1
358 have ht := hy_time -- y.time = c.time + 8
359 rcases y with ⟨yv, yp, yt, yb⟩
360 simp only at hv ht ⊢
361 subst hv -- substitute yv = 1 in context, updating all occurrences
362 subst ht -- substitute yt = c.time + 8
363 congr 1 <;> exact Subsingleton.elim _ _
364 have hA_is_identity : A c = identity_config (c.time + 8) := by
365 simp only [A, Actualize]
366 have hy_eq_A : y = A c := hy_is_identity.trans hA_is_identity.symm
367 rw [← hy_eq_A]
368 exact hp
369 · -- J y.value > 0: Use cost-monotonicity to propagate p down to A c
370 have hJ_y_pos : J y.value > 0 := by
371 cases' (lt_or_eq_of_le (J_nonneg y.pos)) with h h
372 · exact h
373 · exact absurd h.symm hJ0
374 have hJ_A_zero : J (A c).value = 0 := by simp only [A, Actualize, identity_config, J_at_one]
375 have h_gt : J y.value > J (A c).value := by linarith
376 exact hcm y (A c) hp h_gt hA_pos
377 · intro hp
378 exact ⟨A c, identity_always_possible c, hp⟩
379
380/-- **AXIOM / PHYSICAL HYPOTHESIS**: Adjointness of P and A.
381
382 For any "well-formed" property p in the modal landscape, possibility implies
383 actualization. This captures the principle that properties propagate down
384 the cost gradient to the minimal state.
385
386 **STATUS**: HYPOTHESIS - In the full theory, this is restricted to properties
387 that are cost-monotonic. Here we state it as a hypothesis to characterize the
388 relationship between the modal operators. -/
389def possibility_actualization_adjoint_hypothesis (p : ConfigProp) (c : Config) : Prop :=
390 (◇p) c ↔ p (A c)
391
392theorem possibility_actualization_adjoint (p : ConfigProp) (c : Config)
393 (h : possibility_actualization_adjoint_hypothesis p c) :
394 (◇p) c ↔ p (A c) :=
395 h
396
397/-! ## Summary -/
398
399/-- Status report for Actualization module. -/
400def actualization_status : String :=
401 "╔══════════════════════════════════════════════════════════════╗\n" ++
402 "║ ACTUALIZATION: SELECTION FROM POSSIBILITIES ║\n" ++
403 "╠══════════════════════════════════════════════════════════════╣\n" ++
404 "║ CORE CONCEPTS: ║\n" ++
405 "║ • A = Actualization operator (argmin J) ║\n" ++
406 "║ • Degeneracy = multiple cost-equivalent successors ║\n" ++
407 "║ • Contingency = could have been otherwise ║\n" ++
408 "║ • PathAction = total J-cost along trajectory ║\n" ++
409 "╠══════════════════════════════════════════════════════════════╣\n" ++
410 "║ KEY THEOREMS: ║\n" ++
411 "║ • every_config_actualizes: A is total ║\n" ++
412 "║ • A_toward_identity: A drives to J=0 ║\n" ++
413 "║ • collapse_automatic: C≥1 forces selection ║\n" ++
414 "║ • possibility_actualization_adjoint: P ⊣ A ║\n" ++
415 "╠══════════════════════════════════════════════════════════════╣\n" ++
416 "║ BORN RULE: ║\n" ++
417 "║ • P[γ] ∝ exp(-C[γ]) emerges from cost structure ║\n" ++
418 "║ • Not postulated, but derived ║\n" ++
419 "╚══════════════════════════════════════════════════════════════╝"
420
421#check actualization_status
422
423end
424
425end IndisputableMonolith.Modal
426