PathAction

formal source

 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. -/